Induction on evidence for the "less than" relation in coq

Question

I am working on the proof of the following theorem Sn_le_Sm__n_le_m in IndProp.v of Software Foundations (Vol 1: Logical Foundations).

Theorem Sn_le_Sm__n_le_m : ∀n m,
  S n ≤ S m → n ≤ m.
Proof.
  intros n m HS.
  induction HS as [ | m' Hm' IHm'].
  - (* le_n *) (* Failed Here *)
  - (* le_S *) apply IHSm'.
Admitted.

where, the definition of le (i.e., ≤) is:

Inductive le : nat → nat → Prop :=
  | le_n n : le n n
  | le_S n m (H : le n m) : le n (S m).
Notation "m ≤ n" := (le m n).

Before induction HS, the context as well as the goal is as follows:

n, m : nat
HS : S n <= S m
______________________________________(1/1)
n <= m

At the point of the first bullet -, the context as well as the goal is:

n, m : nat
______________________________________(1/1)
n <= m

where we have to prove n <= m without any context, which is obviously impossible.

Why does it not generate S n = S m (and then n = m) for the le_n case in induction HS?

Thill

Possible duplicate of this and many others (just search for [coq] induction). Short answer: before you do induction on a relation, use remember (subexpr) as var to make it a primitive form e.g. x <= y where x and y are just variables. Then you can preserve necessary information after induction. – Candi

You may be interested in the dependent induction tactic. (I might turn this into a full answer later.) – Gould

@JasonGross Looking forward to it. – Thill

Answer 1

The main problem here -I think- is it is impossible to prove the Theorem using induction on HS as there is no way to say something about n with only hypothesis about S n because non of the constructors of le do not change the value of n. But anyway the reason that after first bullet - there is no assumption is because calling induction has the effect of replacing all occurrences of the property argument by the values that correspond to each constructor and it doesn't help in this case since the term that gets replaced S n is not mentioned anywhere. There are some tricks to avoid this. for example you can replace n with pred(S n) as follows.

Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
Proof.
  intros n m HS.
  assert(Hn: n=pred (S n)). reflexivity. rewrite Hn.
  assert(Hm: m=pred (S m)). reflexivity. rewrite Hm.
  induction HS.
  - (* le_n *) apply le_n.
  - (* le_S *) (* Stucks! *) Abort.

But as I mentioned above it is impossible to go further. Another way is to use inversion which is smarter but in some cases it may not help since induction hypothesis would be necessary. But it worth to know about it.

Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
Proof.
  intros n m HS.
  inversion HS.
  - (* le_n *) apply le_n.
  - (* le_S *) (* Stucks! *) Abort.

Best way to solve the problem is use of remember tactic as follows.

Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
Proof.
  intros n m HS.
  remember (S n) as Sn.
  remember (S m) as Sm.
  induction HS as [ n' | n' m' H IH].
  - (* le_n *)
    rewrite HeqSn in HeqSm. injection HeqSm as Heq.
    rewrite <- Heq. apply le_n.
  - (* le_S *) (* Stucks! *) Abort.

According to Software Foundations (Vol 1: Logical Foundations)

The tactic remember e as x causes Coq to (1) replace all occurrences of the expression e by the variable x, and (2) add an equation x = e to the context.

Anyway, although it is impossible to prove the fact using induction on HS -imo-, performing an induction on m will solve the case. (Note the use of inversion.)

Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
Proof.
  intros n.
  induction m as [|m' IHm'].
  - intros H. inversion H as [Hn | n' contra Hn'].
    + apply le_n.
    + inversion contra.
  - intros H. inversion H as [HnSm' | n' HSnSm' Heq].
    + apply le_n.
    + apply le_S. apply IHm'. apply HSnSm'.
Qed.

Opacity

Answer 2

Just more examples of Kamyar's answer. Well, let's take a look of le induction scheme :

Compute le_ind.

forall (n : nat) (P : nat -> Prop),
       P n ->
       (forall m : nat, n <= m -> P m -> P (S m)) ->
       forall n0 : nat, n <= n0 -> P n0

P is some proposition that holds one natural number, which means in the case of le_n, our preposition n <= m will be reduced to forall n, n <= m. Indeed, it's the same lemma that we want to prove, however unprovable because there is no premise.

An easy to solve this is doing induction where le_ind doesn't do.

For example :

Theorem Sn_le_Sm__n_le_m' : forall m n,
  S n <= S m -> n <= m.
 elim.
 by intros; apply : Gt.gt_S_le .
 intros; inversion H0.
 by subst.
 by subst; apply : le_Sn_le.
Qed.

Notice that we doing induction by m, and using inversion to generates the two possible construction of le ({x = y} + {x < y}). Optionally, you can use le decidability.

Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
  intros.
  generalize dependent n.
  elim.
  auto with arith.
  intros.
    have : n <= m.
    by apply : H; apply : le_Sn_le.
  move => H'.
  destruct m.
  auto with arith.
  destruct (le_lt_eq_dec _ _ H').
  assumption.
  subst.
  (* just prove that there is no S m <= m *) 
Qed.

For the sake of your time, coq has the tactic dependent induction that easily solves your goal :

Theorem Sn_le_Sm__n_le_m'' : forall n m,
  S n <= S m -> n <= m.
 intros.
 dependent induction H.
 auto.
 by apply : (le_Sn_le _ _ H).
Qed.

Inconsequential

Answer 3

I just want to correct Kamyar's answer about "it is impossible to prove the Theorem using induction on HS". Since it's possible to prove this theorem using induction on HS.

I'll post my proof here (It's not hard to prove pred_Sn, so I omit its proof):

Check pred_Sn: forall n : nat, n = Nat.pred (S n).

Theorem Sn_le_Sm__n_le_m': forall n m,
    S n <= S m -> n <= m.
Proof.
  intros n m H.
  rewrite (pred_Sn m).
  rewrite (pred_Sn n).
  induction H as [|m' Hm' IH].
  - apply le_n.
  - destruct m'.
    + inversion Hm'.
    + apply (le_S _ _ IH).
Qed.

Gal