The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Sat, Aug 2, 2014 at 9:19 AM, Jonathan 
<jonikelee AT gmail.com>
 wrote:
> A further note to whomever might consider fixing evars - please keep in mind
> that it's not just renaming that is the problem.  Renaming might be the
> least of the problem, as illustrated here:
>
>
> Goal forall (n:nat), True.
> intros.
> evar (i:nat).
> apply id in n.
> Fail instantiate (1:=n) in (Value of i).
>
> If Coq is to allow true backward chaining, then it has to give evars more
> freedom than this.

But of course, it can't allow too much freedom or something like this
would fail only at Qed time:

Goal exists n:nat, forall m:nat, m <= n.
Proof.
eexists.
intro m.
eapply le_n.
Qed.

(Sorry if I'm pointing out the obvious here.)
-- 
Daniel Schepler