The Coq mailing list

[Aaron Bohannon <bohannon AT cis.upenn.edu>]

Hi,

The "inversion" tactic can take a pattern for the names of the
hypotheses it generates.  However, its treatment of names does not
seem "hygienic" to me.  Consider the following code:

<coq>

Parameter A: Set.
Parameter F: A -> Prop.

Inductive G: option A -> Prop :=
  | G_Some: forall a, F a -> G (Some a)
  | G_None: G None.

Lemma example:
  forall a, G (Some a) -> F a.
Proof.
  intros a H.
  (* tactic A:
    inversion H as [a1 J1 Heq1 | ]. *)
  (* tactic B:
    inversion H as [a1 J1 | ]. *)
  (* tactic C:
  inversion H as [a1 H1 | ]. *)
Admitted.

</coq>

In Coq 8.3, I observe the following behavior:  After tactic A, the
hypothesis I'm interested in will be named "J1".  After tactic B, the
hypothesis I'm interested in will be named "J1".  After tactic C, the
hypothesis I'm interested in will be named "H0" (because inversion
uses "H1" for the equation).  Is this something that we can agree to
call a bug?  It would at least be better for tactic C fail than have
it silently ignore the names given in the pattern, right?

 - Aaron