feat: custom recursors for Nat

Std/Data/Nat/Basic.lean

@@ -7,6 +7,100 @@ import Std.Classes.Dvd
 
 namespace Nat
 
+/--
+  Recursor identical to `Nat.rec` but uses notations `0` for `Nat.zero` and `·+1` for `Nat.succ`
+-/
+@[elab_as_elim]
+protected def recAux {motive : Nat → Sort _} (zero : motive 0) (succ : ∀ n, motive n → motive (n+1)) :
+    (t : Nat) → motive t
+  | 0 => zero
+  | _+1 => succ _ (Nat.recAux zero succ _)
+
+/--
+  Recursor identical to `Nat.recOn` but uses notations `0` for `Nat.zero` and `·+1` for `Nat.succ`
+-/
+@[elab_as_elim]
+protected def recAuxOn {motive : Nat → Sort _} (t : Nat) (zero : motive 0)
+  (succ : ∀ n, motive n → motive (n+1)) : motive t := Nat.recAux zero succ t
+
+/--
+  Recursor identical to `Nat.casesOn` but uses notations `0` for `Nat.zero` and `·+1` for `Nat.succ`
+-/
+@[elab_as_elim]
+protected def casesAuxOn {motive : Nat → Sort _} (t : Nat) (zero : motive 0)
+  (succ : ∀ n, motive (n+1)) : motive t := Nat.recAux zero (fun n _ => succ n) t
+
+/--
+  Strong recursor for `Nat`
+-/
+@[elab_as_elim]
+protected def strongRec {motive : Nat → Sort _} (ind : ∀ n, (∀ m, m < n → motive m) → motive n)
+  (t : Nat) : motive t := ind t fun m _ => Nat.strongRec ind m
+
+/--
+  Strong recursor for `Nat`
+-/
+@[elab_as_elim]
+protected def strongRecOn (t : Nat) {motive : Nat → Sort _}
+  (ind : ∀ n, (∀ m, m < n → motive m) → motive n) : motive t := Nat.strongRec ind t
+
+/--
+  Simple diagonal recursor for `Nat`
+-/
+@[elab_as_elim]
+protected def recDiagAux {motive : Nat → Nat → Sort _}
+  (zero_left : ∀ n, motive 0 n)
+  (zero_right : ∀ m, motive m 0)
+  (succ_succ : ∀ m n, motive m n → motive (m+1) (n+1)) :
+    (m n : Nat) → motive m n
+  | 0, _ => zero_left _
+  | _, 0 => zero_right _
+  | _+1, _+1 => succ_succ _ _ (Nat.recDiagAux zero_left zero_right succ_succ _ _)
+
+/--
+  Diagonal recursor for `Nat`
+-/
+@[elab_as_elim]
+protected def recDiag {motive : Nat → Nat → Sort _}
+  (zero_zero : motive 0 0)
+  (zero_succ : ∀ n, motive 0 n → motive 0 (n+1))
+  (succ_zero : ∀ m, motive m 0 → motive (m+1) 0)
+  (succ_succ : ∀ m n, motive m n → motive (m+1) (n+1)) :
+    (m n : Nat) → motive m n := Nat.recDiagAux left right succ_succ
+where
+  /-- Left leg for `Nat.recDiag` -/
+  left : ∀ n, motive 0 n
+  | 0 => zero_zero
+  | _+1 => zero_succ _ (left _)
+  /-- Right leg for `Nat.recDiag` -/
+  right : ∀ m, motive m 0
+  | 0 => zero_zero
+  | _+1 => succ_zero _ (right _)
+
+/--
+  Diagonal recursor for `Nat`
+-/
+@[elab_as_elim]
+protected def recDiagOn {motive : Nat → Nat → Sort _} (m n : Nat)
+  (zero_zero : motive 0 0)
+  (zero_succ : ∀ n, motive 0 n → motive 0 (n+1))
+  (succ_zero : ∀ m, motive m 0 → motive (m+1) 0)
+  (succ_succ : ∀ m n, motive m n → motive (m+1) (n+1)) :
+    motive m n := Nat.recDiag zero_zero zero_succ succ_zero succ_succ m n
+
+/--
+  Diagonal recursor for `Nat`
+-/
+@[elab_as_elim]
+protected def casesDiagOn {motive : Nat → Nat → Sort _} (m n : Nat)
+  (zero_zero : motive 0 0)
+  (zero_succ : ∀ n, motive 0 (n+1))
+  (succ_zero : ∀ m, motive (m+1) 0)
+  (succ_succ : ∀ m n, motive (m+1) (n+1)) :
+    motive m n :=
+  Nat.recDiag zero_zero (fun _ _ => zero_succ _) (fun _ _ => succ_zero _)
+    (fun _ _ _ => succ_succ _ _) m n
+
 /--
 Divisibility of natural numbers. `a ∣ b` (typed as `\|`) says that
 there is some `c` such that `b = a * c`.

Std/Data/Nat/Lemmas.lean

@@ -10,7 +10,127 @@ import Std.Data.Nat.Basic
 
 namespace Nat
 
-/-! ## le/lt -/
+/-! ### rec/cases -/
+
+@[simp] theorem recAux_zero {motive : Nat → Sort _} (zero : motive 0)
+    (succ : ∀ n, motive n → motive (n+1)) :
+    Nat.recAux zero succ 0 = zero := rfl
+
+theorem recAux_succ {motive : Nat → Sort _} (zero : motive 0)
+    (succ : ∀ n, motive n → motive (n+1)) (n) :
+    Nat.recAux zero succ (n+1) = succ n (Nat.recAux zero succ n) := rfl
+
+@[simp] theorem recAuxOn_zero {motive : Nat → Sort _} (zero : motive 0)
+    (succ : ∀ n, motive n → motive (n+1)) :
+    Nat.recAuxOn 0 zero succ = zero := rfl
+
+theorem recAuxOn_succ {motive : Nat → Sort _} (zero : motive 0)
+    (succ : ∀ n, motive n → motive (n+1)) (n) :
+    Nat.recAuxOn (n+1) zero succ = succ n (Nat.recAuxOn n zero succ) := rfl
+
+@[simp] theorem casesAuxOn_zero {motive : Nat → Sort _} (zero : motive 0)
+    (succ : ∀ n, motive (n+1)) :
+    Nat.casesAuxOn 0 zero succ = zero := rfl
+
+@[simp] theorem casesAuxOn_succ {motive : Nat → Sort _} (zero : motive 0)
+    (succ : ∀ n, motive (n+1)) (n) :
+    Nat.casesAuxOn (n+1) zero succ = succ n := rfl
+
+theorem strongRec_eq {motive : Nat → Sort _} (ind : ∀ n, (∀ m, m < n → motive m) → motive n)
+    (t : Nat) : Nat.strongRec ind t = ind t fun m _ => Nat.strongRec ind m := by
+  conv => lhs; unfold Nat.strongRec
+
+theorem strongRecOn_eq {motive : Nat → Sort _} (ind : ∀ n, (∀ m, m < n → motive m) → motive n)
+    (t : Nat) : Nat.strongRecOn t ind = ind t fun m _ => Nat.strongRecOn m ind := Nat.strongRec_eq ..
+
+@[simp] theorem recDiagAux_zero_left {motive : Nat → Nat → Sort _}
+    (zero_left : ∀ n, motive 0 n) (zero_right : ∀ m, motive m 0)
+    (succ_succ : ∀ m n, motive m n → motive (m+1) (n+1)) (n) :
+    Nat.recDiagAux zero_left zero_right succ_succ 0 n = zero_left n := by cases n <;> rfl
+
+@[simp] theorem recDiagAux_zero_right {motive : Nat → Nat → Sort _}
+    (zero_left : ∀ n, motive 0 n) (zero_right : ∀ m, motive m 0)
+    (succ_succ : ∀ m n, motive m n → motive (m+1) (n+1)) (m)
+    (h : zero_left 0 = zero_right 0 := by first | assumption | trivial) :
+    Nat.recDiagAux zero_left zero_right succ_succ m 0 = zero_right m := by cases m; exact h; rfl
+
+theorem recDiagAux_succ_succ {motive : Nat → Nat → Sort _}
+    (zero_left : ∀ n, motive 0 n) (zero_right : ∀ m, motive m 0)
+    (succ_succ : ∀ m n, motive m n → motive (m+1) (n+1)) (m n) :
+    Nat.recDiagAux zero_left zero_right succ_succ (m+1) (n+1)
+      = succ_succ m n (Nat.recDiagAux zero_left zero_right succ_succ m n) := rfl
+
+@[simp] theorem recDiag_zero_zero {motive : Nat → Nat → Sort _} (zero_zero : motive 0 0)
+    (zero_succ : ∀ n, motive 0 n → motive 0 (n+1)) (succ_zero : ∀ m, motive m 0 → motive (m+1) 0)
+    (succ_succ : ∀ m n, motive m n → motive (m+1) (n+1)) :
+    Nat.recDiag (motive:=motive) zero_zero zero_succ succ_zero succ_succ 0 0 = zero_zero := rfl
+
+theorem recDiag_zero_succ {motive : Nat → Nat → Sort _} (zero_zero : motive 0 0)
+    (zero_succ : ∀ n, motive 0 n → motive 0 (n+1)) (succ_zero : ∀ m, motive m 0 → motive (m+1) 0)
+    (succ_succ : ∀ m n, motive m n → motive (m+1) (n+1)) (n) :
+    Nat.recDiag zero_zero zero_succ succ_zero succ_succ 0 (n+1)
+      = zero_succ n (Nat.recDiag zero_zero zero_succ succ_zero succ_succ 0 n) := by
+  simp [Nat.recDiag]; rfl
+
+theorem recDiag_succ_zero {motive : Nat → Nat → Sort _} (zero_zero : motive 0 0)
+    (zero_succ : ∀ n, motive 0 n → motive 0 (n+1)) (succ_zero : ∀ m, motive m 0 → motive (m+1) 0)
+    (succ_succ : ∀ m n, motive m n → motive (m+1) (n+1)) (m) :
+    Nat.recDiag zero_zero zero_succ succ_zero succ_succ (m+1) 0
+      = succ_zero m (Nat.recDiag zero_zero zero_succ succ_zero succ_succ m 0) := by
+  simp [Nat.recDiag]; cases m <;> rfl
+
+theorem recDiag_succ_succ {motive : Nat → Nat → Sort _} (zero_zero : motive 0 0)
+    (zero_succ : ∀ n, motive 0 n → motive 0 (n+1)) (succ_zero : ∀ m, motive m 0 → motive (m+1) 0)
+    (succ_succ : ∀ m n, motive m n → motive (m+1) (n+1)) (m n) :
+    Nat.recDiag zero_zero zero_succ succ_zero succ_succ (m+1) (n+1)
+      = succ_succ m n (Nat.recDiag zero_zero zero_succ succ_zero succ_succ m n) := rfl
+
+@[simp] theorem recDiagOn_zero_zero {motive : Nat → Nat → Sort _} (zero_zero : motive 0 0)
+    (zero_succ : ∀ n, motive 0 n → motive 0 (n+1)) (succ_zero : ∀ m, motive m 0 → motive (m+1) 0)
+    (succ_succ : ∀ m n, motive m n → motive (m+1) (n+1)) :
+    Nat.recDiagOn (motive:=motive) 0 0 zero_zero zero_succ succ_zero succ_succ = zero_zero := rfl
+
+theorem recDiagOn_zero_succ {motive : Nat → Nat → Sort _} (zero_zero : motive 0 0)
+    (zero_succ : ∀ n, motive 0 n → motive 0 (n+1)) (succ_zero : ∀ m, motive m 0 → motive (m+1) 0)
+    (succ_succ : ∀ m n, motive m n → motive (m+1) (n+1)) (n) :
+    Nat.recDiagOn 0 (n+1) zero_zero zero_succ succ_zero succ_succ
+      = zero_succ n (Nat.recDiagOn 0 n zero_zero zero_succ succ_zero succ_succ) :=
+  Nat.recDiag_zero_succ ..
+
+theorem recDiagOn_succ_zero {motive : Nat → Nat → Sort _} (zero_zero : motive 0 0)
+    (zero_succ : ∀ n, motive 0 n → motive 0 (n+1)) (succ_zero : ∀ m, motive m 0 → motive (m+1) 0)
+    (succ_succ : ∀ m n, motive m n → motive (m+1) (n+1)) (m) :
+    Nat.recDiagOn (m+1) 0 zero_zero zero_succ succ_zero succ_succ
+      = succ_zero m (Nat.recDiagOn m 0 zero_zero zero_succ succ_zero succ_succ) :=
+  Nat.recDiag_succ_zero ..
+
+theorem recDiagOn_succ_succ {motive : Nat → Nat → Sort _} (zero_zero : motive 0 0)
+    (zero_succ : ∀ n, motive 0 n → motive 0 (n+1)) (succ_zero : ∀ m, motive m 0 → motive (m+1) 0)
+    (succ_succ : ∀ m n, motive m n → motive (m+1) (n+1)) (m n) :
+    Nat.recDiagOn (m+1) (n+1) zero_zero zero_succ succ_zero succ_succ
+      = succ_succ m n (Nat.recDiagOn m n zero_zero zero_succ succ_zero succ_succ) := rfl
+
+@[simp] theorem casesDiagOn_zero_zero {motive : Nat → Nat → Sort _} (zero_zero : motive 0 0)
+    (zero_succ : ∀ n, motive 0 (n+1)) (succ_zero : ∀ m, motive (m+1) 0)
+    (succ_succ : ∀ m n, motive (m+1) (n+1)) :
+    Nat.casesDiagOn 0 0 (motive:=motive) zero_zero zero_succ succ_zero succ_succ = zero_zero := rfl
+
+@[simp] theorem casesDiagOn_zero_succ {motive : Nat → Nat → Sort _} (zero_zero : motive 0 0)
+    (zero_succ : ∀ n, motive 0 (n+1)) (succ_zero : ∀ m, motive (m+1) 0)
+    (succ_succ : ∀ m n, motive (m+1) (n+1)) (n) :
+    Nat.casesDiagOn 0 (n+1) zero_zero zero_succ succ_zero succ_succ = zero_succ n := rfl
+
+@[simp] theorem casesDiagOn_succ_zero {motive : Nat → Nat → Sort _} (zero_zero : motive 0 0)
+    (zero_succ : ∀ n, motive 0 (n+1)) (succ_zero : ∀ m, motive (m+1) 0)
+    (succ_succ : ∀ m n, motive (m+1) (n+1)) (m) :
+    Nat.casesDiagOn (m+1) 0 zero_zero zero_succ succ_zero succ_succ = succ_zero m := rfl
+
+@[simp] theorem casesDiagOn_succ_succ {motive : Nat → Nat → Sort _} (zero_zero : motive 0 0)
+    (zero_succ : ∀ n, motive 0 (n+1)) (succ_zero : ∀ m, motive (m+1) 0)
+    (succ_succ : ∀ m n, motive (m+1) (n+1)) (m n) :
+    Nat.casesDiagOn (m+1) (n+1) zero_zero zero_succ succ_zero succ_succ = succ_succ m n := rfl
+
+/-! ### le/lt -/
 
 theorem ne_of_gt {a b : Nat} (h : b < a) : a ≠ b := (ne_of_lt h).symm