The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

Hi Aaron,

I would definitely call that a bug, or at least disturbing behaviour.
Over the years, I have come to almost systematically name the
non-dependent products in inductives on which I use inversion a lot,
in that case something like:

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

It doesn't solve the issue of hypothesis' naming as a whole, but it's
quite nice to know that hypotheses resulting from inversions will be
named in a systematic fashion, and being able to tell instantly where
an hypothesis comes from just by looking at its name.

Stéphane

On Fri, Feb 18, 2011 at 8:10 PM, Aaron Bohannon 
<bohannon AT cis.upenn.edu>
 wrote:
> 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
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06