The Coq mailing list

[Nicolas Magaud <magaud AT unistra.fr>]

Dear Gaetan Gilbert,

I made a mistake and meant to write this code (which is the one written in 
the attached file) :

Lemma u : forall p q:nat, p=q -> TS p -> TS q.
Proof.
  intros p q Hpq Hts; inversion Hpq.
  Restart.
  intros p q Hpq; rewrite Hpq; auto.
Qed.

Cheers,

Nicolas Magaud


> On 08 Jun 2017, at 15:11, Gaetan Gilbert 
> <gaetan.gilbert AT ens-lyon.fr>
>  wrote:
> 
> In Lemma t you do inversion on the [Hnm : n=m] hypothesis
> In Lemma u you do inversion on the [Hts : TS p] hypothesis
> The difference has nothing to do with parameters vs variables.
> 
> Gaëtan Gilbert
> 
> On 08/06/2017 15:07, Nicolas Magaud wrote:
>> Dear all,
>> 
>> Using the tactic inversion, I face a strange behaviour :
>> 
>> 1/ If I have the 2 following parameters :
>> 
>> Parameter TS : nat -> Type.
>> Parameter n m:nat.
>> 
>> And try to prove this lemma :
>> 
>> Lemma t : n=m -> TS n -> TS m.
>> 
>> I can proceed by using inversion
>> 
>> intros Hnm Hts; inversion Hnm.
>> 
>> The goal is then TS n, which is proved easily using assumption.
>> 
>> 2/ If I try to prove
>> 
>> Lemma u : forall p q:nat, p=q -> TS p -> TS q.
>> 
>> intros p q Hpq Hts; inversion Hts.
>> 
>> does not help at all (q is not replaced by p).
>> Of course, I can do rewrite before introducing the 2nd hypothesis "TS p”. 
>> But I would expect inversion to do the job.
>> 
>> 3/ As you can see in the file attached below (Lemma v), I can print the 
>> proof term generated by inversion in the first lemma t and use it (with 
>> the tactic exact) to prove the expected lemma (Lemma v).
>> 
>> My question is: why inversion does not work the same when n and m are 
>> parameters (as in Lemma t) or introduced universally-quantified variables 
>> (as in Lemma u) ?
>> 
>> Thanks in advance.
>> 
>> Nicolas Magaud
>>