Existential creation and generalization in coq

Question

Can someone please give me a simple example of an existential instance and existential generalization in Coq? When I want to prove exists x, P , where P is some Prop that uses x , I often want to call x (like x0 or some like that) and manipulate P. Could this be in Coq?

Answer 1

If you are going to prove existentiality directly, and not through a lemma, you can use eapply ex_intro . This introduces an existential variable (recorded ?42 ). Then you can manipulate the term. To complete the proof, you need to ultimately provide a way to construct the value for this variable. You can do this explicitly using instantiate tactics or implicitly using tactics like eauto .

Beware that it is often cumbersome to work with existential variables. Many tactics suggest that all conditions are created and can hide existences in subgoals; you will find out when Qed reports "Error: attempt to save incomplete evidence." You should only use existential variables if you have a plan to create them in the near future.

Here is a silly example illustrating the use of eapply .

 Goal exists x, 1 + x = 3. Proof. (* ⊢ exists x, 1 + x = 3 *) eapply ex_intro. (* ⊢ 1 + ?42 = 3 *) simpl. (* ⊢ S ?42 = 3 *) apply f_equal. (* ⊢ ?42 = 2 *) reflexivity. (* proof completed *) Qed.