The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 08/01/2014 05:23 AM, Enrico Tassi wrote:
> On Thu, Jul 31, 2014 at 04:28:31PM -0400, Jonathan wrote:
> > - Is there access to a development version that works with the trunk version
> > of Coq?
> It is there:
>    
> https://gforge.inria.fr/scm/viewvc.php/trunk/Saclay/Ssreflect/?root=coq-contribs
>
> But don't use it in "production"
>
> > - As I recall, SSReflect relies considerably on revert/re-intro style
> > patterns.  Do the SSReflect versions of these destroy evar instantiability
> > as they do in vanilla Coq?  I have been learning how to write Ltac tactics
> > that don't alter the context to the point where evars become uninstantiable
> > (as well as others that try to prevent uninstatiability) - and it seems like
> > SSReflect's style could make this harder rather than easier.  Or, does
> > SSReflect have ways around this already?
> I'm not sure I understand what you mean by destroy evar instantiability.

An example of how fragile evar instantiability is in Coq:

Goal forall (n:nat), True.
intros.
evar (i:nat).
instantiate (1:=n) in (Value of i). (*this works*)
Abort.

Goal forall (n:nat), True.
intros.
evar (i:nat).
rename n into m. (*renaming blocks instantiation:*)
Fail instantiate (1:=m) in (Value of i).
Abort.

Goal forall (n:nat), True.
intros.
evar (i:nat).
revert n; intro n. (*even this blocks instantiation:*)
Fail instantiate (1:=n) in (Value of i).
Abort.


> Ssr POV is that evars are constants, no ssr tactic should let you
> instantiate them, but should not "destroy" them either.  We hardly use
> evars in our goals.

Perhaps the occurrence of evars is much more likely when using backward 
chaining.

-- Jonathan