The Coq mailing list

[Yannick <yannick.zakowski AT irisa.fr>]

Dear Coq Club,

I am a bit confused with Coq's behavior towards hypotheses whose name
collude with a definition in its context. Please consider the following
minimal example, also enclosed with the mail:

Ltac inv H := inversion H; try subst; clear H.

Definition bar := False.

Inductive Eq: nat -> nat -> Prop :=
  | Eq_def: forall n m, n = m -> Eq n m.

Lemma foo: forall (n:nat) (m:nat) (bar: Eq n m), False.
 intros n m bar.

A first observation here: 'intros' would rename bar as bar0, but 'intros
n m bar' will indeed name it bar. I guess it makes sense, we do not want
to shadow unless explicitly required.

What confuses me more is the behavior of subst:

 inversion bar. (* Context: bar: Eq n m and a bunch of equalities named
H, H0, H1 *)
 subst. (* Context: bar0: Eq m m *)

Here subst actually renamed "abusively" my hypothesis.

Finally, I am at total lost with the following:
  Restart.
  Fail (intros n m bar; inv bar).
(*
The command has indeed failed with message:
In nested Ltac calls to "inv" and "clear H", last call failed.
Error: Ltac variable H is bound to a value of type var which cannot be
coerced to a variable.
*)
  intros n m bar.
  inv bar. (** Succeed, by renaming on the way my hypothesis from bar to
bar0 **)
  Restart.
  intros n m bar.
  Fail (inversion bar; subst; clear bar).
(*
The command has indeed failed with message:
No such hypothesis: bar
*)

Given the previous observation on the behaviour of subst, the third case
failing is to be expected. However I do not quite grasp why wrapping it
in a Ltac call allows it to succeed, and even more so why it does not
when chained with a semi-colon.


Naturally, I would agree at any rate that using pre-existing names for
hypotheses is not quite a good policy. However I happened to do it
accidentally and had quite a hard time figuring what was going on. Any
explanation or pointers as to what is really going on in each case, and
confirmation that these behaviours are indeed desired, would be awesome.

Thanks a lot in advance,
Best,
Yannick
Ltac inv H := inversion H; try subst; clear H.

Definition bar := False.

Inductive Eq: nat -> nat -> Prop :=
  | Eq_def: forall n m, n = m -> Eq n m.

Lemma foo: forall (n:nat) (m:nat) (bar: Eq n m), False.
  intros n m bar.
  inversion bar.
  subst. (** Here subst rename my hypothesis from bar to bar0 **)
  Restart.
  Fail (intros n m bar; inv bar).
  intros n m bar.
  inv bar. (** Succeed, by renaming on the way my hypothesis **)
  Restart.
  intros n m bar.
  Fail (inversion bar; subst; clear bar).
Abort.