feat(data/nat/basic): nat.le_rec_on

data/nat/basic.lean

@@ -27,6 +27,46 @@ succ_le_succ_iff
 lemma succ_le_iff {m n : ℕ} : succ m ≤ n ↔ m < n :=
 ⟨lt_of_succ_le, succ_le_of_lt⟩
 
+theorem of_le_succ {n m : ℕ} (H : n ≤ m.succ) : n ≤ m ∨ n = m.succ :=
+(lt_or_eq_of_le H).imp le_of_lt_succ id
+
+@[elab_with_expected_type]
+def le_rec_on {C : ℕ → Sort u} (next : Π {n}, C n → C (n+1)) : Π {n m : ℕ}, n ≤ m → C n → C m
+| n 0 H x := eq.rec_on (eq_zero_of_le_zero H) x
+| n (m+1) H x := or.by_cases (of_le_succ H) (λ h : n ≤ m, next $ le_rec_on h x) (λ h : n = m + 1, eq.rec_on h x)
+
+theorem le_rec_on_self {C : ℕ → Sort u} (next : Π n, C n → C (n+1)) {n h} (x : C n) : (le_rec_on next h x : C n) = x :=
+by cases n; unfold le_rec_on or.by_cases; rw [dif_neg n.not_succ_le_self, dif_pos rfl]
+
+theorem le_rec_on_succ {C : ℕ → Sort u} (next : Π n, C n → C (n+1)) {n m h2} (h1) (x : C n) :
+  (le_rec_on next h2 x : C (m+1)) = next m (le_rec_on next h1 x) :=
+by conv { to_lhs, rw [le_rec_on, or.by_cases, dif_pos h1] }
+
+theorem le_rec_on_succ' {C : ℕ → Sort u} (next : Π n, C n → C (n+1)) {n h} (x : C n) :
+  (le_rec_on next h x : C (n+1)) = next n x :=
+by rw [le_rec_on_succ next (le_refl n), le_rec_on_self]
+
+theorem le_rec_on_trans {C : ℕ → Sort u} (next : Π n, C n → C (n+1)) {n m k} (hnm : n ≤ m) (hmk : m ≤ k) (x : C n) :
+  (le_rec_on next (le_trans hnm hmk) x : C k) = le_rec_on next hmk (le_rec_on next hnm x) :=
+begin
+  induction hmk with k hmk ih, { rw le_rec_on_self },
+  rw [le_rec_on_succ _ (le_trans hnm hmk), ih, le_rec_on_succ]
+end
+
+theorem le_rec_on_injective {C : ℕ → Sort u} (next : Π n, C n → C (n+1)) (Hnext : ∀ n, function.injective (next n))
+  {n m} (hnm : n ≤ m) : function.injective (le_rec_on next hnm) :=
+begin
+  induction hnm with m hnm ih, { intros x y H, rwa [le_rec_on_self, le_rec_on_self] at H },
+  intros x y H, rw [le_rec_on_succ _ hnm, le_rec_on_succ _ hnm] at H, exact ih (Hnext _ H)
+end
+
+theorem le_rec_on_surjective {C : ℕ → Sort u} (next : Π n, C n → C (n+1)) (Hnext : ∀ n, function.surjective (next n))
+  {n m} (hnm : n ≤ m) : function.surjective (le_rec_on next hnm) :=
+begin
+  induction hnm with m hnm ih, { intros x, use x, rw le_rec_on_self },
+  intros x, rcases Hnext _ x with ⟨w, rfl⟩, rcases ih w with ⟨x, rfl⟩, use x, rw le_rec_on_succ
+end
+
 theorem pred_eq_of_eq_succ {m n : ℕ} (H : m = n.succ) : m.pred = n := by simp [H]
 
 theorem pred_sub (n m : ℕ) : pred n - m = pred (n - m) :=