The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq users,

 

I sometimes get an error using “rewrite with” when local names and the names used for bound variables in the rewriting lemma clash. Below is an example. Rewrite says that I can’t use the names from the lemma, but have to use some extended names. I don’t see a way to know these different names in automation. Also in other situations the name clash doesn’t seem to be a problem. Is this a bug or do I miss something?

 

Best regards,

 

Michael

 

(* ===== Example for rewrite with issue ===== *)

 

Require Import List.

Import ListNotations.

 

Lemma app_cons: forall {T : Type} (x : T) (l : list T), x::l = [x]++l.

Proof. reflexivity. Qed.

 

Example ExNotOk: forall {T : Type} (x : T) (l : list T),  x::l = [x]++l.

Proof.

  intros T x l.

  (* The below rewrite with fails with

     Error: No such bound variable x (possible names are: x0 and l0) *)

  Fail rewrite app_cons with (x:=x) (l:=l).

 

  (* The rewrite with renamed variables works *)

  rewrite app_cons with (x0:=x) (l0:=l).

  reflexivity.

Qed.

 

Example ExOk: forall (l m n : list nat),

  l ++ m ++ n = (l ++ m) ++ n.

Proof.

  intros l m n.

  (* But this rewrite works, although I use the same names locally as in the definition of the rewrite lemma *)

  rewrite app_assoc with (l:=l) (m:=m) (n:=n).

  reflexivity.

Qed.