Bug 2433 - Coq 8.3 drops ability to test if a term contains evars
: Coq 8.3 drops ability to test if a term contains evars
Status: RESOLVED FIXED
Product: Coq
Classification: Unclassified
Component: Tactics
: 8.3
: All All
: P5 major
: ---
Assigned To: Stephane Glondu
Depends on:
Blocks:
  Show dependency treegraph
 
Reported: 2010-11-09 14:50 CET by Adam Chlipala
Modified: 2010-11-29 12:11 CET (History)
3 users (show)

See Also:


Attachments

Note You need to log in before you can comment on or make changes to this bug.
Description Adam Chlipala 2010-11-09 14:50:04 CET
Though I haven't yet tried Coq 8.3, I'm adding this bug preemptively, based on what I see in the recent coq-club thread "Ltac Determine if a variable is an existential".  Most of my serious Coq projects depend on the ability to detect, in Ltac, if a term contains existentials.  In 8.2, this has required some fairly nasty code, but at least it's possible.

Could a simple Ltac way of checking if a term contains evars be added to 8.3?  Stéphane Glondu posted a suggested plug-in in the coq-club thread I mentioned; the "fix" could be as simple as adding it to the standard codebase.  I won't be able to switch to 8.3 until this is resolved, and I don't want to ask users of my libraries to install a plugin first.  (Example of a library that uses evar testing in a critical way: http://adam.chlipala.net/bedrock/)

Thanks!
Comment 1 Stephane Glondu 2010-11-09 15:01:16 CET
I guess Adam is talking about the following thread:

http://thread.gmane.org/gmane.science.mathematics.logic.coq.club/5469

IMHO, the tactic I posted to coq-club escapes the scope of patch level releases, so my initial answer would be to wait for next (>= 8.4) version.

However, since there is an apparent regression with 8.2, I'd agree to commit it in the v8.3 branch (under "popular pressure"). I don't know exactly how Adam was detecting evars before, but Gregory's proposition is obviously a hack and should never have been, in my opinion, relied on in the first place.

I'm waiting for opinions from other Coq developers (and users) before proceeding...
Comment 2 Adam Chlipala 2010-11-09 15:06:55 CET
You can see the precise tactic I'm using in this tarball:
  http://adam.chlipala.net/dist/bedrock-20101027.tgz

It's the last definition in src/PropXTac.v.  Here's the code:

====================================
Ltac ensureNotUnif E :=
  match E with
    | E => idtac
    | ?f _ => ensureNotUnif f
    | ?f _ _ => ensureNotUnif f
    | ?f _ _ _ => ensureNotUnif f
    | ?f _ _ _ _ => ensureNotUnif f
  end.
====================================

I use the tactic in src/Separation.v, to prevent overeager unification in a tactic for crossing out matching conjuncts on both sides of an implication.
Comment 3 Arthur Charguéraud 2010-11-09 15:07:36 CET
Like Adam, I would be blocked from migrating to v8.3 until this issue is resolved. I suggest providing a function 'is_evar' and a function 'contains_evar' to test where are the evars. By the way, a direct access to the function 'unify' from Ltac would be very useful to. 

Many Thanks, Arthur.
Comment 4 Adam Chlipala 2010-11-09 15:10:07 CET
Arthur, I'm not familiar with the function "unify", but would the following tactic accomplish what you want?  It essentially unifies two terms.

Ltac equate x y := let H := fresh "H" in assert (H : x = y) by reflexivity; clear H.
Comment 5 Arthur Charguéraud 2010-11-09 15:16:46 CET
Yes, I guess 'equate' would behave like 'unify', though it would be nicer if there was a standard mechanism, to avoid every developer coming up with a trick of his own for unifying terms.
Arthur
Comment 6 Stephane Glondu 2010-11-09 15:38:00 CET
(In reply to comment #2)
> Ltac ensureNotUnif E :=
>   match E with
>     | E => idtac
>     | ?f _ => ensureNotUnif f
>     | ?f _ _ => ensureNotUnif f
>     | ?f _ _ _ => ensureNotUnif f
>     | ?f _ _ _ _ => ensureNotUnif f
>   end.

I don't see what in Ltac documentation would guarantee the semantics of that.

(In reply to comment #4)
> Ltac equate x y := let H := fresh "H" in assert (H : x = y) by reflexivity;
> clear H.

On the other hand, this one looks fine to me (and I use similar stuff myself).

(In reply to comment #3)
> Like Adam, I would be blocked from migrating to v8.3 until this issue is
> resolved. I suggest providing a function 'is_evar' and a function
> 'contains_evar' to test where are the evars. By the way, a direct access to the
> function 'unify' from Ltac would be very useful to. 

Is 'is_evar' different from my 'match_evar'? Could you give use cases for 'is_evar' and 'contains_evar'? Maybe a new kind of pattern explicitly matching evars would be useful... but this looks too intrusive for a PL release.
Comment 7 Adam Chlipala 2010-11-09 15:41:14 CET
> I don't see what in Ltac documentation would guarantee the semantics of that.

Yes, I found this behavior by trial and error.  However, do you really want to be taking the position that all the important behavior of Ltac be documented precisely?  I don't see a formal semantics in the manual, so this seems like a dangerous path. ;)
Comment 8 Arthur Charguéraud 2010-11-09 18:05:50 CET
> Could you give use cases for 'is_evar' and 'contains_evar'?

I don't have a 'good' example in mind right now, but I remember cases where writing my tactic with 'is_evar' would have been simple but where I came up with complicated work-around to avoid using Adam's hack, precisely because I suspected that the hack of matching a term with itself would most probably end up being broken at some point. 

Let me now give one 'bad' motivation for 'contains_evar', which is the reason that would prevent me from migrating to v8.3. Currently (in v8.2 and v8.3), the semantics of "autorewrite" is such that it usually loops forever when invoked on terms that contain evars (I have sent a message on coqdev explaining why this happen and how to fix it). Currently, my tactics check that there is no evar in the goal before calling autorewrite, so that I don't end up restarting Coqide every two minutes... 

Arthur
Comment 9 Arthur Charguéraud 2010-11-09 18:14:39 CET
Sorry, I forgot a point:

> "Maybe a new kind of pattern explicitly matching evars would be useful... but this looks too intrusive for a PL release."

That would be great! You only need to find one token to refer to evars. Let's say it's the token "@@evar". 

Then one could write:

"match t with @@evar => .."

as well as

"match t with context[ @@evar ] => .."

That would be perfect, I guess.

Note that the prefix @@ should not break many scripts, since building a user notation on top of the @ symbol is a pretty bad idea. Since the feature would not break many scripts and would be only a few lines of Caml to implement, I would say it's a good candidate for a PL release :)

Arthur
Comment 10 Arthur Charguéraud 2010-11-09 18:14:39 CET
Sorry, I forgot a point:

> "Maybe a new kind of pattern explicitly matching evars would be useful... but this looks too intrusive for a PL release."

That would be great! You only need to find one token to refer to evars. Let's say it's the token "@@evar". 

Then one could write:

"match t with @@evar => .."

as well as

"match t with context[ @@evar ] => .."

That would be perfect, I guess.

Note that the prefix @@ should not break many scripts, since building a user notation on top of the @ symbol is a pretty bad idea. Since the feature would not break many scripts and would be only a few lines of Caml to implement, I would say it's a good candidate for a PL release :)

Arthur
Comment 11 Stephane Glondu 2010-11-16 14:19:30 CET
(In reply to comment #7)
> [...]  However, do you really want to
> be taking the position that all the important behavior of Ltac be documented
> precisely? [...]

No, but I avoid relying on behaviours that are obviously buggy...

Anyway, as nobody gave me a more elegant way to test evars, I've committed the new tactic "is_evar" v8.3 branch (r13636). It should be part of the next PL release.
Comment 12 Stephane Glondu 2010-11-16 14:29:12 CET
(In reply to comment #10)
> "match t with context[ @@evar ] => .."

This could be written "match t with context[ ?t ] => is_evar t; ..." with the is_evar tactic. However, be aware that context only matches closed terms.

> Note that the prefix @@ should not break many scripts, since building a user
> notation on top of the @ symbol is a pretty bad idea. Since the feature would
> not break many scripts and would be only a few lines of Caml to implement, I
> would say it's a good candidate for a PL release :)

I would like to see the few lines of Caml... :-) To me, it would mean changing the AST of patterns (but maybe I'm wrong), which is too intrusive for a PL release IMHO. It could be a new feature to be experimented in the trunk, though. Feel free to submit a new wishlist bug and/or a patch for this.
Comment 13 Adam Chlipala 2010-11-16 15:07:21 CET
Thanks, that looks perfect!
Comment 14 Stephane Glondu 2010-11-29 12:11:56 CET
I also added "has_evar" (which goes under binders) in the v8.3 branch (r13658).