feat: measureRec for strong induction use cases (leanprover-communi…

…ty#829) * feat: `Nat.strongRecOnMeasure` Co-Authored-By: Joachim Breitner <[email protected]>
FR-vdash-bot · Jun 8, 2024 · 1659998 · 1659998
1 parent f93c3a7
commit 1659998
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/Batteries/Data/Nat/Basic.lean b/Batteries/Data/Nat/Basic.lean
@@ -28,6 +28,15 @@ protected def strongRec {motive : Nat → Sort _} (ind : ∀ n, (∀ m, m < n
 protected def strongRecOn (t : Nat) {motive : Nat → Sort _}
   (ind : ∀ n, (∀ m, m < n → motive m) → motive n) : motive t := Nat.strongRec ind t
 
+/--
+  Strong recursor via a `Nat`-valued measure
+-/
+@[elab_as_elim]
+def strongRecMeasure (f : α → Nat) {motive : α → Sort _}
+    (ind : ∀ x, (∀ y, f y < f x → motive y) → motive x) (x : α) : motive x :=
+  ind x fun y _ => strongRecMeasure f ind y
+termination_by f x
+
 /--
   Simple diagonal recursor for `Nat`
 -/