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?
10
votes
i know there have been coq questions here in the past, but i suspect that as more sites are introduced the best place for coq questions is now cs.stackexchange.com (not so happy with the fragmentation myself, but it's a fact of life...)
– andrew cooke
@andrewcooke This hasn't been established conclusively. My feeling is that Coq questions are more on-topic on SO if the goal is to get a proof done, and on Computer Science if the goal is to understand why a proof technique is working or not working, but it's a very thin line. The expertise is spread over Stack Overflow, Computer Science and Theoretical Computer Science.
– Gilles 'SO- stop being evil'
1 Answers
7
votes
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.
