The Coq mailing list

[Jacques Garrigue <garrigue AT math.nagoya-u.ac.jp>]

I have the same kind of problem as described in

  http://logical.saclay.inria.fr/coq-puma/messages/1e1098e5dd22df43

and

  http://logical.saclay.inria.fr/coq-puma/messages/16f7d4c858cc1da4

Namely, when hypotheses contain existential variables, repeatedly
applying rewrite can cause an infinite loop (the variables get
incrementally instantiated...)

I really wish there were a version of rewrite that would not
match on existentials.

Alternatively, is there any way to detect whether the current goal
contains existentials? I've written a tactic to do that, but it seems
rather ad-hoc (it just tries to instantiate, and fails when succeeding).

Ltac instantiate_fail :=
  instantiate;
  try ((instantiate (1 := nil) || instantiate (1:={})) ; fail 1);
  try (match goal with H: _ |- _ =>
   (instantiate (1:=nil) in H || instantiate (1:={}) in H) end;
   fail 1).

Jacques
---------------------------------------------------------------------------
Jacques Garrigue      Nagoya University     garrigue at math.nagoya-u.ac.jp
                   <A HREF=http://www.math.nagoya-u.ac.jp/~garrigue/>JG</A>