The Coq mailing list

[Duckki Oe <duckki AT mit.edu>]

Hi all,

I know [auto] tactic instantiates evars. What I just noticed was, auto's 
behavior in the presence of evar differs from eauto. I think the problem 
comes form the fact that assumption tactic does not instantiate evars, but 
apply does. I think their behavior should be consistent (in the presence of 
evars). Thus, the behavior of auto and eauto can be consistent as well. In 
summary, I want one of these behaviors:  1) assumption and apply are both 
allowed to instantiate evars, or 2) both should not instantiate evars.

Here's an example where auto and eauto instantiate evars differently.

Variable P : nat -> nat -> Prop.
Axiom P_refl : forall x, P x x.
Axiom P_trans : forall x y z, P x y -> P y z -> P x z.

Hint Immediate P_refl. (* triggers auto *)

Goal forall x y z, P x y -> P y z -> P x z.
intros.
eapply P_trans.
(* we have a goal with an evar *)
(* eauto will solve correctly based on the hypothesis *)
auto. (* auto incorrectly applied P_refl, ignoring the hypothesis *)

Abort.


-- Duckki