The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-08-01 17:02 GMT+02:00 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.

In fact, when write "evar (i:nat).", that means that the evar "i" depends on the context in which it was introduced,
that is: "n:nat". When you do "revert n.", "n" is removed from the dependencies of "i" (as it would have been with a "clear n"),
meaning that evar "i" must be closed under the empty context.
When you do "intro n.", you introduce a variable which cannot instantiate "i", as "n" is not a term closed in the empty context.

I cannot try it, but what is the result of:

Goal forall (n:nat), True.
intros.
evar (i:nat).
generalize n; intro m.
Fail instantiate (1:=m) in (Value of i).
Abort.

Here, I do not know if the link between "m" and "n" is established, and as "n" is still in the dependencies of "i", it could work.

For your second case, I do not know how rename works internally. It could be implemented as something equivalent to a
"revert all terms dependent on 'n', then revert 'n', then intro 'm', then intro all terms now dependent on 'm'".
If this is the case, that could explain the error.

To test it, one can do something like:

Definition test : Type -> Type.
  intros x.
  rename x into y.
  exact y.
Defined.

Print test.

And see how y is introduced in the proof term.

Some remark:

Goal forall m n, m<n -> False.
Proof.
  intros m n Hmn.
  revert m. (* ← triggers an error for obvious reasons *)
Abort.

But with evars, no such thing is done (more or less thankfully, as it could be quite inconvenient not to be able to use tactics
like clear in presence of evars introduced when these hypotheses were alive).
Maybe a warning could be raised in these cases?

Or more ideally, maybe that a "dependent reverse" could be defined (well, that may already be the case), and when calling it, all dependencies (including evars) could be generalized.
This way, the link would not be lost.

n : nat.
i := ?(n) : nat (*evar*)
m : nat
H : P m i
========
Q

------------
"dependent revert n."
would produce:

m : nat
========
forall n:nat, set i := ?(n) in P m i -> Q


 

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

--
.../Sedrikov\...