Reputation: 5266
I wanted to see a few hands on examples of Coq proofs of the form:
\exists A(x1,...,xn)
essentially where the Goal had an existential quantifier. I was having issues manipulating the goal in meaningful ways to make progress in my proof and wanted to see a few examples of common tactics to manipulate.
What are some good existential quantifiers examples in Coq to prove?
My specific example I had:
Theorem Big_Small_ForwardImpl :
forall (P : Program) (S' : State),
(BigStepR (B_PgmConf P) (B_StateConf S')) -> (ConfigEquivR (S_PgmConf P) (S_BlkConf EmptyBlk S')).
Proof.
intros.
induction P.
unfold ConfigEquivR.
refine (ex_intro _ _ _) .
my context and goals was:
1 subgoal
l : list string
s : Statement
S' : State
H : BigStepR (B_PgmConf (Pgm l s)) (B_StateConf S')
______________________________________(1/1)
exists N : nat, NSmallSteps N (S_PgmConf (Pgm l s)) (S_BlkConf EmptyBlk S')
but then changed to:
1 subgoal
l : list string
s : Statement
S' : State
H : BigStepR (B_PgmConf (Pgm l s)) (B_StateConf S')
______________________________________(1/1)
NSmallSteps ?Goal (S_PgmConf (Pgm l s)) (S_BlkConf EmptyBlk S')
after using the refine (ex_intro _ _ _)
tactic. Since I am not sure what is going on I was hoping some simpler examples could show me how to manipulate existential quantifiers in my Coq goal.
helpful comment:
The ?Goal was introduced by Coq as a placeholder for some N that will have to be deduced later in the proof.
Upvotes: 0
Views: 710
Reputation: 786
The following example is based on the code provided in this answer.
Suppose we have a type T
and a binary relation R
on elements of type T
. For the purpose of this example, we can define those as follows.
Variable T : Type.
Variable R : T -> T -> Prop.
Let us prove the following simple theorem.
Theorem test : forall x y, R x y -> exists t, R x t.
Here is a possible solution.
Proof.
intros. exists y. apply H.
Qed.
Instead of explicitly specifying that y
is the element we are looking for, we can rely on Coq's powerful automatic proof mechanisms in order to automatically deduce which variable satisfies R x t
:
Proof.
intros.
eexists. (* Introduce a temporary placeholder of the form ?t *)
apply H. (* Coq can deduce from the hypothesis H that ?t must be y *)
Qed.
There exist numerous tactics that make ise of the same automated deduction mechanisms, such as eexists
, eapply
, eauto
, etc.
Note that their names often correspond to usual tactics prefixed with an e
.
Upvotes: 1