existential instantiation and generalization in coq

coq

Solution

If you're going to prove the existential directly and not through a lemma, you can use `eapply ex_intro`. This introduces an existential variable (written `?42`). You can then manipulate the term. To complete the proof, you need to eventually provide a way to construct a value for that variable. You can do this explicitly with the `instantiate` tactic, or implicitly through tactics such as `eauto`.

Beware that it is often cumbersome to work with existential variables. Many tactics assume that all terms are instantiated and may hide existentials in subgoals; you'll only find out when `Qed` tells you “Error: Attempt to save an incomplete proof”. You should only use existential variables when you have a plan to instantiate them soon.

Here's a silly example that illustrates 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.

Problem

Can someone please give me a simple example of existential instantiation 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 name `x` (as `x0` or some such), and manipulate P. Can this be one in Coq?

Original source