The Coq mailing list

[Venanzio Capretta <venanzio AT cs.kun.nl>]

Why don't the existential variables created by EApply get instantiated
during the proof?
Consider the example from the reference manual for version 6.2.4 pg.135:

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).


Coq < Goal (R n p).
1 subgoal
  
  ============================
   (R n p)

Unnamed_thm < EApply Rtrans.
2 subgoals
  
  ============================
   (R n ?136)

subgoal 2 is:
 (R ?136 p)

Unnamed_thm < Apply Rnm.
1 subgoal
  
  ============================
   (R ?136 p)

At this point the existential variable ?136 should already have been
instantiated with m. Why doesn't this happen?

----------------------
Venanzio Capretta
University of Nijmegen
Faculty of Mathematics
       and Informatics
the Nederlands
tel.: +31-24-3652232
----------------------