The Coq mailing list

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

Yeah, naming non-dependent products is not a bad idea, but in many of
my developments, I like to keep my hypothesis names under tighter,
more local control.

 - Aaron

2011/2/18 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
>