Induction over relations

2
votes

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?

3
coqcoq-tactic
IMHO this example could sever as an exercise on Coq inductives types and indexes; however, if what you plan to do is to formalize the <= relation, this is total overkill and will give you many headaches. I suggest indeed you define your relation as a function nat -> nat -> bool. – ejgallego

3 Answers

4
votes

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.
3
votes

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.

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

3
votes

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

Proof.
  intros n m H.
  remember (S n) as p.
  induction H.

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