8.2 EApply
Example: Assume we have a relation on nat which is transitive:
Coq < Variable R:nat->nat->Prop.Coq < Hypothesis Rtrans : (x,y,z:nat)(R x y)->(R y z)->(R x z).Coq < Variables n,m,p:nat.Coq < Hypothesis Rnm:(R n m).Coq < Hypothesis Rmp:(R m p).Consider the goal (R n p) provable using the transitivity of R:
Coq < Goal (R n p).The direct application of Rtrans with Apply fails because no value for y in Rtrans is found by Apply:
Coq < Apply Rtrans.Error during interpretation of command:
Apply Rtrans.
Error: Cannot refine to conclusions with meta-variables
A solution is to rather apply (Rtrans n m p).
Coq < Apply (Rtrans n m p).2 subgoals
============================
(R n m)
subgoal 2 is:
(R m p)
More elegantly, Apply Rtrans with y:=m allows to only mention the unknown m:
Coq < Apply Rtrans with y:=m.2 subgoals
============================
(R n m)
subgoal 2 is:
(R m p)
Another solution is to mention the proof of (R x y) in Rtrans...
Coq < Apply Rtrans with 1:=Rnm.1 subgoal
============================
(R m p)
... or the proof of (R y z):
Coq < Apply Rtrans with 2:=Rmp.1 subgoal
============================
(R n m)
On the opposite, one can use EApply which postpone the problem of finding m. Then one can apply the hypotheses Rnm and Rmp. This instantiates the existential variable and completes the proof.
Coq < EApply Rtrans.2 subgoals
============================
(R n ?3139)
subgoal 2 is:
(R ?3139 p)
Coq < Apply Rnm.1 subgoal
============================
(R ?3139 p)
Coq < Apply Rmp.Subtree proved!