Library Eqle.le_inv

Author: Jean-François Monin, Verimag, Université Grenoble Alpes

Require Import Utf8 Eqdep_dec Arith.

Basic small inversion of le, with 0 / S discrimination and linear heads

We then actually use the injective small inversion trick as if le was defined as: Inductive le n : nat → Prop := | le_e m : n = m → le n m | le_S m : n ≤ m → le n (S m).

Or better, in order to discriminate on the last argument:

Inductive le n : nat → Prop := | le_e_0 : n = 0 → le n O | le_e_S m : n = S m → le n (S m) | le_S m : n ≤ m → le n (S m).

However the auxiliary inductive for the latter can directly be used on le, as illustrated below.

Definition eq_le {n m} (e : n = m) : n ≤ m :=
  match e with eq_refl ⇒ le_n n end.

Inductive le_0 [n] : n ≤ 0 → Prop :=
| le_0_e : ∀ e , le_0 (eq_le e).

Inductive le_Sm [m n] : n ≤ S m → Prop :=
| le_Sm_e : ∀ e , le_Sm (eq_le e)
| le_Sm_S : ∀ l , le_Sm (le_S n m l).

Lemma le_inv {n m} (l : le n m) :
  match m with
  | O ⇒ le_0
  | S m ⇒ @le_Sm m
  end n l.
Proof.
  destruct l as [ | m l].
  - exact (match n with 0 ⇒ le_0_e eq_refl | S _ ⇒ le_Sm_e eq_refl end).
  - constructor.
Qed.

Inversion lemmas based on the original structure of le

Lemma eq_is_le_n {n} (e : n = n) : le_n n = eq_le e.
Proof. rewrite (UIP_refl_nat n e). reflexivity. Qed.

Lemma lenn_unique {n} (l : n ≤ n) : le_n n = l.
Proof.
  destruct n as [ | n]; destruct (le_inv l); try apply eq_is_le_n.
  case (lt_irrefl _ l).
Qed.

Inductive is_le_S {n m} : n ≤ S m → Prop :=
| is_le_S_intro : ∀ l , is_le_S (le_S n m l).

Lemma leS_is_le_S {n m} (lS : n ≤ S m) : n ≤ m → is_le_S lS.
Proof.
  destruct (le_inv lS) as [ e | ll ]; intro l; try constructor.
  exfalso; rewrite e in l; apply (lt_irrefl _ l).
Qed.

Fixpoint le_unique {n m} (p : n ≤ m) : ∀ q , p = q.
Proof.
  destruct p as [ | m p]; intro q; cbn.
  - destruct (lenn_unique q); reflexivity.
  - destruct (leS_is_le_S q p). apply f_equal, le_unique.
Qed.