The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

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