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?
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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With