The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Yours is a standard problem that I would expect any Coq introduction to 
discuss.  In general, [induction] doesn't work well on predicates 
applied to arguments that aren't just variables.  Also, you should run 
[induction] in a context where any variables that change in the course 
of the induction remain quantified with [forall].

Here's one solution:

Lemma Sn_le_Sm__n_le_m' : forall n m,
  n <= m -> pred n <= pred m.
  induction 1; simpl; auto.
  destruct m; auto.
Qed.

Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
  intros; apply Sn_le_Sm__n_le_m' in H; auto.
Qed.

But I recommend reading a source like CPDT 
<http://adam.chlipala.net/cpdt/> to get an organized account of all the 
issues.


On 03/02/2014 03:33 PM, Jack Kolb wrote:
> Hi,
>
> I am still new to Coq, so bear with me if I'm missing something obvious.
>
> I have encountered a problem with the induction tactic when trying to 
> prove the following simple theorem:
>     Theorem Sn_le_Sm__n_le_m : forall n m,
>       S n <= S m -> n <= m.
>
> My instinct is to start the proof like so:
>     Proof.
>       intros. induction H.
>
> However, the induction tactic doesn't preserve any information about n 
> and m, and I am unable to make any forward progress. It is possible 
> that I'm overlooking something, but this seems to be a problem with 
> the induction tactic. I've done some research and found a similar 
> situation here: 
> http://stackoverflow.com/questions/4519692/keeping-information-when-using-induction. 
> However, the suggestions made in this post don't seem to solve my problem.
>
> Is there some way to use induction while preserving the information 
> about n and m?
>
> Thanks.