Induction over relations

Question

I'm trying to prove the following toy theorem about the ordering of the naturals:

Inductive Le : nat -> nat -> Prop :=
| le_n : forall n, Le n n
| le_S : forall n m, Le n m -> Le n (S m).

Theorem le_Sn_m : forall n m, Le (S n) m -> Le n m.forall n m : nat, Le (S n) m -> Le n m

On paper, this is a simple induction on Le (S n) m. In particular, the base case of le_n is trivial.

In Coq though, beginning my proof with induction gives me the following:

Proof.forall n m : nat, Le (S n) m -> Le n m
  intros n m H.n, m: nat
H: Le (S n) m
Le n m induction H.n, n0: nat
Le n n0
n, n0, m: nat
H: Le n0 m
IHLe: Le n m
Le n (S m) 2 subgoals

  n, n0 : nat
  ============================
  Le n n0

subgoal 2 is:
 Le n (S m)

How should I proceed instead?

Answer (Vinz)

This is due to a limitation of Coq, when using induction on term that are not made only of variables. By doing your induction, Coq forgets about the fact that the first argument was a S of some n.

You can do the following instead:

Theorem le_Sn_m_ : forall X m, Le X m -> forall n, X = S n -> Le n m.forall X m : nat,
Le X m -> forall n : nat, X = S n -> Le n m

I think there is a dependent induction somewhere that could save you this intermediate lemma but I can't recall where.

Answer (Zimm i48)

Similar to @Vinz suggestion, but without changing the statement you are proving:

Theorem le_Sn_m : forall n m, Le (S n) m -> Le n m.forall n m : nat, Le (S n) m -> Le n m
Proof.forall n m : nat, Le (S n) m -> Le n m
  intros n m H.n, m: nat
H: Le (S n) m
Le n m remember (S n) as p.n, m, p: nat
Heqp: p = S n
H: Le p m
Le n m induction H; subst n0.n: nat
Le n (S n)
n, m: nat
IHLe: S n = S n -> Le n m
H: Le (S n) m
Le n (S m)
  -n: nat
Le n (S n) do 2 constructor.
  -n, m: nat
IHLe: S n = S n -> Le n m
H: Le (S n) m
Le n (S m) constructor.n, m: nat
IHLe: S n = S n -> Le n m
H: Le (S n) m
Le n m now apply IHLe.
Qed.

Using the remember tactic will introduce an equality in your context which will avoid losing this critical information.

Answer (Anton Trunov)

This is happening because Coq treats differently indices and parameters (see the accepted answer to this question for a very nice explanation). Your Le relation uses indices only, whereas the standard definition makes the first argument a parameter:

Inductive le (n : nat) : nat -> Prop :=
    le_n : n <= n
  | le_S : forall m : nat, n <= m -> n <= S m

Arguments le (_ _)%nat_scope
Arguments Peano.le_n _%nat_scope
Arguments Peano.le_S (_ _)%nat_scope _

I can recommend reading this blog post by James Wilcox. Here is a relevant excerpt:

When Coq performs a case analysis, it first abstracts over all indices. You may have seen this manifest as a loss of information when using destruct on predicates

So you can either (1) change your Le relation so it would use a parameter, or (2) use the remember tactic as was suggested by @Zimm i48, or (3) use the dependent induction tactic mentioned by @Vinz:

Require Import Coq.Program.Equality. (* for `dependent induction` *)

Inductive Le : nat -> nat -> Prop :=
| le_n : forall n, Le n n
| le_S : forall n m, Le n m -> Le n (S m).
Hint Constructors Le. (* so `auto` will work *)Adding and removing hints in the core database
implicitly is deprecated. Please specify a hint
database. [implicit-core-hint-db,deprecated]
The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]

Theorem le_Sn_m : forall n m, Le (S n) m -> Le n m.forall n m : nat, Le (S n) m -> Le n m
Proof.forall n m : nat, Le (S n) m -> Le n m
  intros n m H.n, m: nat
H: Le (S n) m
Le n m dependent induction H; auto.
Qed.