Coq: How to prove that forall n m, n <= m \/ m <= n

user_17379532 0
Viewed 123

How to prove

Theorem le_total : forall n m, n <= m \ / m <= n.

Here are theorems that I have that could possibly help:

Inductive le : nat -> nat -> Prop :=
 | le_n (n : nat)                : le n n
 | le_S (n m : nat) (H : le n m) : le n (S m).

Notation "n <= m" := (le n m).

Theorem le_le_S : forall n m,
 n <= m -> S n <= S m.
Proof.
 intros n m H. induction H.
 - (* le_n *)
   apply le_n.
 - (* le_S *)
   apply le_S. apply IHle.  Qed.

(** **** Exercise: 1 star, standard (le_trans) *)

Lemma le_trans : forall m n o, m <= n -> n <= o -> m <= o.
Proof.
 intros m n o Lmn Lno.
 generalize dependent Lmn.
 generalize dependent m.
 induction Lno.
 -intros. apply Lmn.
 -intros. apply le_S. apply IHLno. apply Lmn.
Qed.
(** [] *)

(** **** Exercise: 1 star, standard (O_le_n) *)
Theorem O_le_n : forall n,
 0 <= n.
Proof.
 intros. induction n.
 apply le_n.
 apply le_S. apply IHn.
Qed.

I was able to get to a point that using induction on n would get me to a good spot but I'm not sure where to go after that.

coq
2 Answers

My guess is that your induction hypothesis is not general enough. Some results about two variables (n and m in this case) need an induction on n that generalizes on m. So at the very beginning, instead of

Proof.
  intros n m.
  induction n.

do:

Proof.
  intros n.
  induction n.
user_23054580

As @ana-borges suggested, the proof is straightforward if you induct with a generalized m. I'd encourage you to try the proof again with this in mind.

[Edit: solution removed]

In general, when you think a goal should be provable by induction, but can't get it, it is often useful to consider whether the inductive hypothesis may be generalized. Occasionally, depending on the order of hypotheses, you may need to generalize assumptions explicitly with revert or generalize dependent.

user_111266320
Related