The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

I assume that you use the <= of the standard library.
In this case, <= is itself an inductive, and I suggest you to try to prove:

Theorem n_le_m__pred_n_le_pred_m : forall n m,
  n <= m -> pred n <= pred m.

starting with "intros n m H. induction H." From there, what you want to prove should be trivial.
The point is that the full pattern matching form is the following one:

  match H as H0 in _ <= x return P x H0 with … end

So here, your "S m" would be unified with 'x', meaning that in the return type you would not see "S m" nor "m" but "x".
If you replace "m" with "pred (S m)" in your goal, then "S m" will be replaced with "x" and "pred (S m)" with "pred x".

On the same idea, you could also try to prove:

Theorem Sn_le_Sm__n_le_m : forall n m',
  S n <= m' -> forall m, m' = S m -> n <= m.
Proof.
  intros n m' H; induction H.

2014-03-02 21:33 GMT+01:00 Jack Kolb <kolb0128 AT umn.edu>:

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.

--
.../Sedrikov\...