The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 08/02/2014 12:45 PM, Daniel Schepler wrote:
> 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.)

Certainly, cycles have to be excluded!  That might point in the 
direction of a better solution: keep a dependency graph and use it to 
prevent evar instantiations that would introduce cycles. Probably 
over-simplifying - I'm sure there are other things that must be 
prevented as well.  Oh - here's one: you must prevent a non-Prop evar 
created in a non-Prop context from being instantiated in or following 
the transformation of the goal into a Prop context, else you could 
violate Coq's Prop/Type separation.

-- Jonathan