The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 27/03/2017 20:11, Igor Jirkov wrote:
> Hello!
> 
> I have a problem trying to prove a property of form:
> 
> /forall (n:nat) (m:T),  n > s m -> f (g n m) = f n./
> 
> Here /f: T -> //U , g: nat -> T -> T , s: T -> nat./
> 
> The problem is that /g/  is defined as a fixpoint with decreasing /n//,
> /I presume that it obliges me to use the proof by induction.
> 
> However, induction over /n/  is giving me premises I can not satisfy:
> 
> /(n > s m -> f (g n m) = f n) -> (S n > s m -> f (g n m) )/.
> 
> Having /(S n > s m)/ I can not deduce /(n > s m)./

Your premise (S n > s m) implies either (n > s m) or (n = s m). So one
of the first proof steps has to perform this case disjunction. In the
first case, you can then apply your induction hypothesis.

If you are unable to prove the property in the (n = s m) case. That
presumably means that your original property was not sufficiently
generalized.

Best regards,

Guillaume