Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

How to express "there exists a unique X" in Coq?

Tags:

coq

I was wondering if there is a succinct way of writing that there exists a unique something (i.e. write unique existential quantifier) in Coq?

For example, to say that there exists an x s.t. 2 + x = 4:

Goal exists x, 2 + x = 4.

How can I write that there exists a unique x with the same property?

I know I can replicate the predicate in the s.t. part like this:

Goal exists x, 2 + x = 4 /\ forall y, 2 + y = 4 -> y = x.

But this is a lot of repetition in general, and is there a way to somehow encode a new quantifier, and write:

Goal exists1, 2 + x = 4.

to express the same goal?

like image 986
thor Avatar asked Sep 07 '16 20:09

thor


1 Answers

Coq already provides an exists! notation. For example:

Goal exists! x, 2 + x = 4.
Proof.
exists 2. split.
+ reflexivity.
+ intros. injection H; intro.
  symmetry; assumption.
Qed.
like image 109
Daniel Schepler Avatar answered Oct 16 '22 10:10

Daniel Schepler