From 1659998cdf16a6ce9f0c18fd7a1609f7315205ba Mon Sep 17 00:00:00 2001 From: L Date: Sat, 8 Jun 2024 14:29:35 -0700 Subject: [PATCH] feat: `measureRec` for strong induction use cases (#829) * feat: `Nat.strongRecOnMeasure` Co-Authored-By: Joachim Breitner --- Batteries/Data/Nat/Basic.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Batteries/Data/Nat/Basic.lean b/Batteries/Data/Nat/Basic.lean index 9f7c7d8f36..a6e55a6ea2 100644 --- 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` -/