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.

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.
  intros n m H. induction H.

1 subgoal
n, n0 : nat
______________________________________(1/1)
Le n n0

...in which case I am blocked.

How should I proceed instead?

Answer 1

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

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 *)

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