The Coq mailing list

[Brian Aydemir <baydemir AT cis.upenn.edu>]

Hi everyone,

The following toy example illustrates the interaction of the rewrite  
and autorewrite tactics with existential variables.  The behavior I'm  
seeing (in Coq 8.1pl1) surprises me, so I am hoping that someone here  
can explain exactly what is happening.

(* *** *)

Require Import List.

(* Pick a theorem to use as a rewrite rule. *)

Check app_nil_end. (* forall (A : Type) (l : list A), l = l ++ nil *)
Hint Rewrite <- app_nil_end : db.

(* Use that theorem in a silly proof now.
   The statement itself is unimportant. *)

Lemma test : exists L : list nat, ~ In 0 L -> True.
Proof.
  (* Introduce an existential variable.
     This is a key point in this example. *)
  econstructor.
  intros H.

  (* The goal now looks like the following:
       H : ~ In 0 ?3
       ============================
        True
  *)

  (* The following loops forever it seems: autorewrite with db in H.
     Let's try something simpler. *)
  rewrite <- app_nil_end in H.

  (* The goal now looks like the following:
       H : ~ In 0 ?35484
       ============================
        True
  *)
Admitted.

(* *** *)

It seems that (auto)rewrite is succeeding even when the term being  
rewritten is an existential variable.  Is this the intended behavior  
of these tactics or is this a bug?  If the behavior is intended, how  
should I make sense of it?

Also, is there a way to prevent (auto)rewrite from rewriting a term  
that is an existential variable?  In the larger example where I first  
encountered this behavior, autorewrite is being invoked via a Hint  
Extern in order to simplify goals.  This in turn helps (e)auto solve  
many, uninteresting goals.  Thus, I do not want to remove the Hint  
Externs.  Is my only other choice to be more careful where eauto is  
used?


Thanks,
Brian