From b548cf38b623bff7c05359640512a8dbbb518f0f Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Wed, 25 Feb 2026 13:43:39 +0100
Subject: [PATCH] feat: enable partial termination proofs about
 `WellFounded.extrinsicFix` (#12430)

This PR provides `WellFounded.partialExtrinsicFix`, which makes it
possible to implement and verify partially terminating functions, safely
building on top of the seemingly less general `extrinsicFix` (which is
now called `totalExtrinsicFix`). A proof of termination is only
necessary in order to formally verify the behavior of
`partialExtrinsicFix`.
---
 src/Init/WFExtrinsicFix.lean | 287 +++++++++++++++++++++++++++++++++++
 1 file changed, 287 insertions(+)

diff --git a/src/Init/WFExtrinsicFix.lean b/src/Init/WFExtrinsicFix.lean
index c94dbfafed..f9767eba7e 100644
--- a/src/Init/WFExtrinsicFix.lean
+++ b/src/Init/WFExtrinsicFix.lean
@@ -30,6 +30,7 @@ variable {α : Sort _} {β : α → Sort _} {γ : (a : α) → β a → Sort _}
 set_option doc.verso true
 
 namespace WellFounded
+open Relation
 
 /--
 The function implemented as the loop {lean}`opaqueFix R F a = F a (fun a _ => opaqueFix R F a)`.
@@ -85,6 +86,23 @@ public theorem extrinsicFix_eq_apply [∀ a, Nonempty (C a)] {R : α → α →
   simp only [extrinsicFix, dif_pos h]
   rw [WellFounded.fix_eq]
 
+public theorem extrinsicFix_invImage {α' : Sort _} [∀ a, Nonempty (C a)] (R : α → α → Prop) (f : α' → α)
+    (F : ∀ a, (∀ a', R a' a → C a') → C a) (F' : ∀ a, (∀ a', R (f a') (f a) → C (f a')) → C (f a))
+    (h : ∀ a r, F (f a) r = F' a fun a' hR => r (f a') hR) (a : α') (h : WellFounded R) :
+    extrinsicFix (C := (C <| f ·)) (InvImage R f) F' a = extrinsicFix (C := C) R F (f a) := by
+  have h' := h
+  rcases h with ⟨h⟩
+  specialize h (f a)
+  have : Acc (InvImage R f) a := InvImage.accessible _ h
+  clear h
+  induction this
+  rename_i ih
+  rw [extrinsicFix_eq_apply, extrinsicFix_eq_apply, h]
+  · congr; ext a x
+    rw [ih _ x]
+  · assumption
+  · exact InvImage.wf _ ‹_›
+
 /--
 A fixpoint combinator that allows for deferred proofs of termination.
 
@@ -242,4 +260,273 @@ nontrivial properties about it.
 -/
 add_decl_doc extrinsicFix₃
 
+/--
+A fixpoint combinator that can be used to construct recursive functions with an
+*extrinsic, partial* proof of termination.
+
+Given a relation {name}`R` and a fixpoint functional {name}`F` which must be decreasing with respect
+to {name}`R`, {lean}`partialExtrinsicFix R F` is the recursive function obtained by having {name}`F` call
+itself recursively.
+
+For each input {given}`a`, {lean}`partialExtrinsicFix R F a` can be verified given a *partial* termination
+proof. The precise semantics are as follows.
+
+If {lean}`Acc R a` does not hold, {lean}`partialExtrinsicFix R F a` might run forever. In this case,
+nothing interesting can be proved about the recursive function; it is opaque and behaves like a
+recursive function with the `partial` modifier.
+
+If {lean}`Acc R a` _does_ hold, {lean}`partialExtrinsicFix R F a` is equivalent to
+{lean}`F a (fun a' _ => partialExtrinsicFix R F a')`, both logically and regarding its termination behavior.
+
+In particular, if {name}`R` is well-founded, {lean}`partialExtrinsicFix R F a` is equivalent to
+{lean}`WellFounded.fix _ F`.
+-/
+@[inline]
+public def partialExtrinsicFix [∀ a, Nonempty (C a)] (R : α → α → Prop)
+    (F : ∀ a, (∀ a', R a' a → C a') → C a) (a : α) : C a :=
+  extrinsicFix (α := { a' : α // a' = a ∨ TransGen R a' a }) (C := (C ·.1))
+      (fun p q => R p.1 q.1)
+      (fun a recur => F a.1 fun a' hR => recur ⟨a', by
+        rcases a.property with ha | ha
+        · exact Or.inr (TransGen.single (ha ▸ hR))
+        · apply Or.inr
+          apply TransGen.trans ?_ ‹_›
+          apply TransGen.single
+          assumption⟩ ‹_›) ⟨a, Or.inl rfl⟩
+
+public theorem partialExtrinsicFix_eq_apply_of_acc [∀ a, Nonempty (C a)] {R : α → α → Prop}
+    {F : ∀ a, (∀ a', R a' a → C a') → C a} {a : α} (h : Acc R a) :
+    partialExtrinsicFix R F a = F a (fun a' _ => partialExtrinsicFix R F a') := by
+  simp only [partialExtrinsicFix]
+  rw [extrinsicFix_eq_apply]
+  congr; ext a' hR
+  let f (x : { x : α // x = a' ∨ TransGen R x a' }) : { x : α // x = a ∨ TransGen R x a } :=
+    ⟨x.val, by
+      cases x.property
+      · rename_i h
+        rw [h]
+        exact Or.inr (.single hR)
+      · rename_i h
+        apply Or.inr
+        refine TransGen.trans h ?_
+        exact .single hR⟩
+  have := extrinsicFix_invImage (C := (C ·.val)) (R := (R ·.1 ·.1)) (f := f)
+    (F := fun a r => F a.1 fun a' hR => r ⟨a', Or.inr (by rcases a.2 with ha | ha; exact .single (ha ▸ hR); exact .trans (.single hR) ‹_›)⟩ hR)
+    (F' := fun a r => F a.1 fun a' hR => r ⟨a', by rcases a.2 with ha | ha; exact .inr (.single (ha ▸ hR)); exact .inr (.trans (.single hR) ‹_›)⟩ hR)
+  unfold InvImage at this
+  rw [this]
+  · simp +zetaDelta
+  · constructor
+    intro x
+    refine InvImage.accessible _ ?_
+    cases x.2 <;> rename_i hx
+    · rwa [hx]
+    · exact h.inv_of_transGen hx
+  · constructor
+    intro x
+    refine InvImage.accessible _ ?_
+    cases x.2 <;> rename_i hx
+    · rwa [hx]
+    · exact h.inv_of_transGen hx
+
+public theorem partialExtrinsicFix_eq_apply [∀ a, Nonempty (C a)] {R : α → α → Prop}
+    {F : ∀ a, (∀ a', R a' a → C a') → C a} {a : α} (wf : WellFounded R) :
+    partialExtrinsicFix R F a = F a (fun a' _ => partialExtrinsicFix R F a') :=
+  partialExtrinsicFix_eq_apply_of_acc (wf.apply _)
+
+public theorem partialExtrinsicFix_eq_fix [∀ a, Nonempty (C a)] {R : α → α → Prop}
+    {F : ∀ a, (∀ a', R a' a → C a') → C a}
+    (wf : WellFounded R) {a : α} :
+    partialExtrinsicFix R F a = wf.fix F a := by
+  have h := wf.apply a
+  induction h with | intro a' h ih
+  rw [partialExtrinsicFix_eq_apply_of_acc (Acc.intro _ h), WellFounded.fix_eq]
+  congr 1; ext a'' hR
+  exact ih _ hR
+
+/--
+A 2-ary fixpoint combinator that can be used to construct recursive functions with an
+*extrinsic, partial* proof of termination.
+
+Given a relation {name}`R` and a fixpoint functional {name}`F` which must be decreasing with respect
+to {name}`R`, {lean}`partialExtrinsicFix₂ R F` is the recursive function obtained by having {name}`F` call
+itself recursively.
+
+For each pair of inputs {given}`a` and {given}`b`, {lean}`partialExtrinsicFix₂ R F a b` can be verified
+given a *partial* termination proof. The precise semantics are as follows.
+
+If {lean}`Acc R ⟨a, b⟩ ` does not hold, {lean}`partialExtrinsicFix₂ R F a b` might run forever. In this
+case, nothing interesting can be proved about the recursive function; it is opaque and behaves like
+a recursive function with the `partial` modifier.
+
+If {lean}`Acc R ⟨a, b⟩` _does_ hold, {lean}`partialExtrinsicFix₂ R F a b` is equivalent to
+{lean}`F a b (fun a' b' _ => partialExtrinsicFix₂ R F a' b')`, both logically and regarding its
+termination behavior.
+
+In particular, if {name}`R` is well-founded, {lean}`partialExtrinsicFix₂ R F a b` is equivalent to
+a well-foundesd fixpoint.
+-/
+@[inline]
+public def partialExtrinsicFix₂ [∀ a b, Nonempty (C₂ a b)]
+    (R : (a : α) ×' β a → (a : α) ×' β a → Prop)
+    (F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b)
+    (a : α) (b : β a) :
+    C₂ a b :=
+  extrinsicFix₂ (α := α) (β := fun a' => { b' : β a' // (PSigma.mk a' b') = (PSigma.mk a b) ∨ TransGen R ⟨a', b'⟩ ⟨a, b⟩ })
+      (C₂ := (C₂ · ·.1))
+      (fun p q => R ⟨p.1, p.2.1⟩ ⟨q.1, q.2.1⟩)
+      (fun a b recur => F a b.1 fun a' b' hR => recur a' ⟨b', Or.inr (by
+        rcases b.property with hb | hb
+        · exact .single (hb ▸ hR)
+        · apply TransGen.trans ?_ ‹_›
+          apply TransGen.single
+          assumption)⟩ ‹_›) a ⟨b, Or.inl rfl⟩
+
+public theorem partialExtrinsicFix₂_eq_partialExtrinsicFix [∀ a b, Nonempty (C₂ a b)]
+    {R : (a : α) ×' β a → (a : α) ×' β a → Prop}
+    {F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b}
+    {a : α} {b : β a} (h : Acc R ⟨a, b⟩) :
+    partialExtrinsicFix₂ R F a b = partialExtrinsicFix (α := PSigma β) (C := fun a => C₂ a.1 a.2) R (fun p r => F p.1 p.2 fun a' b' hR => r ⟨a', b'⟩ hR) ⟨a, b⟩ := by
+  simp only [partialExtrinsicFix, partialExtrinsicFix₂, extrinsicFix₂]
+  let f (x : ((a' : α) ×' { b' // PSigma.mk a' b' = ⟨a, b⟩ ∨ TransGen R ⟨a', b'⟩ ⟨a, b⟩ })) : { a' // a' = ⟨a, b⟩ ∨ TransGen R a' ⟨a, b⟩ } :=
+    ⟨⟨x.1, x.2.1⟩, x.2.2⟩
+  have := extrinsicFix_invImage (C := fun a => C₂ a.1.1 a.1.2) (f := f) (R := (R ·.1 ·.1))
+    (F := fun a r => F a.1.1 a.1.2 fun a' b' hR => r ⟨⟨a', b'⟩, ?refine_a⟩ hR)
+    (F' := fun a r => F a.1 a.2.1 fun a' b' hR => r ⟨a', b', ?refine_b⟩ hR)
+    (a := ⟨a, b, ?refine_c⟩); rotate_left
+  · cases a.2 <;> rename_i heq
+    · rw [heq] at hR
+      exact .inr (.single hR)
+    · exact .inr (.trans (.single hR) heq)
+  · cases a.2.2 <;> rename_i heq
+    · rw [heq] at hR
+      exact .inr (.single hR)
+    · exact .inr (.trans (.single hR) heq)
+  · exact .inl rfl
+  unfold InvImage f at this
+  simp at this
+  rw [this]
+  constructor
+  intro x
+  apply InvImage.accessible
+  cases x.2 <;> rename_i heq
+  · rwa [heq]
+  · exact h.inv_of_transGen heq
+
+public theorem partialExtrinsicFix₂_eq_apply_of_acc [∀ a b, Nonempty (C₂ a b)]
+    {R : (a : α) ×' β a → (a : α) ×' β a → Prop}
+    {F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b}
+    {a : α} {b : β a} (wf : Acc R ⟨a, b⟩) :
+    partialExtrinsicFix₂ R F a b = F a b (fun a' b' _ => partialExtrinsicFix₂ R F a' b') := by
+  rw [partialExtrinsicFix₂_eq_partialExtrinsicFix wf, partialExtrinsicFix_eq_apply_of_acc wf]
+  congr 1; ext a' b' hR
+  rw [partialExtrinsicFix₂_eq_partialExtrinsicFix (wf.inv hR)]
+
+public theorem partialExtrinsicFix₂_eq_apply [∀ a b, Nonempty (C₂ a b)]
+    {R : (a : α) ×' β a → (a : α) ×' β a → Prop}
+    {F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b}
+    {a : α} {b : β a} (wf : WellFounded R) :
+    partialExtrinsicFix₂ R F a b = F a b (fun a' b' _ => partialExtrinsicFix₂ R F a' b') :=
+  partialExtrinsicFix₂_eq_apply_of_acc (wf.apply _)
+
+public theorem partialExtrinsicFix₂_eq_fix [∀ a b, Nonempty (C₂ a b)]
+    {R : (a : α) ×' β a → (a : α) ×' β a → Prop}
+    {F : ∀ a b, (∀ a' b', R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b}
+    (wf : WellFounded R) {a b} :
+    partialExtrinsicFix₂ R F a b = wf.fix (fun x G => F x.1 x.2 (fun a b h => G ⟨a, b⟩ h)) ⟨a, b⟩ := by
+  rw [partialExtrinsicFix₂_eq_partialExtrinsicFix (wf.apply _), partialExtrinsicFix_eq_fix wf]
+
+
+/--
+A 3-ary fixpoint combinator that can be used to construct recursive functions with an
+*extrinsic, partial* proof of termination.
+
+Given a relation {name}`R` and a fixpoint functional {name}`F` which must be decreasing with respect
+to {name}`R`, {lean}`partialExtrinsicFix₃ R F` is the recursive function obtained by having {name}`F` call
+itself recursively.
+
+For each pair of inputs {given}`a`, {given}`b` and {given}`c`, {lean}`partialExtrinsicFix₃ R F a b` can be
+verified given a *partial* termination proof. The precise semantics are as follows.
+
+If {lean}`Acc R ⟨a, b, c⟩ ` does not hold, {lean}`partialExtrinsicFix₃ R F a b` might run forever. In this
+case, nothing interesting can be proved about the recursive function; it is opaque and behaves like
+a recursive function with the `partial` modifier.
+
+If {lean}`Acc R ⟨a, b, c⟩` _does_ hold, {lean}`partialExtrinsicFix₃ R F a b` is equivalent to
+{lean}`F a b c (fun a' b' c' _ => partialExtrinsicFix₃ R F a' b' c')`, both logically and regarding its
+termination behavior.
+
+In particular, if {name}`R` is well-founded, {lean}`partialExtrinsicFix₃ R F a b c` is equivalent to
+a well-foundesd fixpoint.
+-/
+@[inline]
+public def partialExtrinsicFix₃ [∀ a b c, Nonempty (C₃ a b c)]
+    (R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop)
+    (F : (a : α) → (b : β a) → (c : γ a b) → ((a' : α) → (b' : β a') → (c' : γ a' b') → R ⟨a', b', c'⟩ ⟨a, b, c⟩ → C₃ a' b' c') → C₃ a b c)
+    (a : α) (b : β a) (c : γ a b) :
+    C₃ a b c :=
+  extrinsicFix₃ (α := α) (β := β) (γ := fun a' b' => { c' : γ a' b' // (⟨a', b', c'⟩ : (a : α) ×' (b : β a) ×' γ a b) = ⟨a, b, c⟩ ∨ TransGen R ⟨a', b', c'⟩ ⟨a, b, c⟩ })
+      (C₃ := (C₃ · · ·.1))
+      (fun p q => R ⟨p.1, p.2.1, p.2.2.1⟩ ⟨q.1, q.2.1, q.2.2.1⟩)
+      (fun a b c recur => F a b c.1 fun a' b' c' hR => recur a' b' ⟨c', Or.inr (by
+        rcases c.property with hb | hb
+        · exact .single (hb ▸ hR)
+        · apply TransGen.trans ?_ ‹_›
+          apply TransGen.single
+          assumption)⟩ ‹_›) a b ⟨c, Or.inl rfl⟩
+
+public theorem partialExtrinsicFix₃_eq_partialExtrinsicFix [∀ a b c, Nonempty (C₃ a b c)]
+    {R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop}
+    {F : (a : α) → (b : β a) → (c : γ a b) → ((a' : α) → (b' : β a') → (c' : γ a' b') → R ⟨a', b', c'⟩ ⟨a, b, c⟩ → C₃ a' b' c') → C₃ a b c}
+    {a : α} {b : β a} {c : γ a b} (h : Acc R ⟨a, b, c⟩) :
+    partialExtrinsicFix₃ R F a b c = partialExtrinsicFix (α := (a : α) ×' (b : β a) ×' γ a b) (C := fun a => C₃ a.1 a.2.1 a.2.2) R (fun p r => F p.1 p.2.1 p.2.2 fun a' b' c' hR => r ⟨a', b', c'⟩ hR) ⟨a, b, c⟩ := by
+  simp only [partialExtrinsicFix, partialExtrinsicFix₃, extrinsicFix₃]
+  let f (x : ((a' : α) ×' (b' : β a') ×' { c' // (⟨a', b', c'⟩ : (a : α) ×' (b : β a) ×' γ a b) = ⟨a, b, c⟩ ∨ TransGen R ⟨a', b', c'⟩ ⟨a, b, c⟩ })) : { a' // a' = ⟨a, b, c⟩ ∨ TransGen R a' ⟨a, b, c⟩ } :=
+    ⟨⟨x.1, x.2.1, x.2.2.1⟩, x.2.2.2⟩
+  have := extrinsicFix_invImage (C := fun a => C₃ a.1.1 a.1.2.1 a.1.2.2) (f := f) (R := (R ·.1 ·.1))
+    (F := fun a r => F a.1.1 a.1.2.1 a.1.2.2 fun a' b' c' hR => r ⟨⟨a', b', c'⟩, ?refine_a⟩ hR)
+    (F' := fun a r => F a.1 a.2.1 a.2.2.1 fun a' b' c' hR => r ⟨a', b', c', ?refine_b⟩ hR)
+    (a := ⟨a, b, c, ?refine_c⟩); rotate_left
+  · cases a.2 <;> rename_i heq
+    · rw [heq] at hR
+      exact .inr (.single hR)
+    · exact .inr (.trans (.single hR) heq)
+  · cases a.2.2.2 <;> rename_i heq
+    · rw [heq] at hR
+      exact .inr (.single hR)
+    · exact .inr (.trans (.single hR) heq)
+  · exact .inl rfl
+  unfold InvImage f at this
+  simp at this
+  rw [this]
+  constructor
+  intro x
+  apply InvImage.accessible
+  cases x.2 <;> rename_i heq
+  · rwa [heq]
+  · exact h.inv_of_transGen heq
+
+public theorem partialExtrinsicFix₃_eq_apply_of_acc [∀ a b c, Nonempty (C₃ a b c)]
+    {R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop}
+    {F : ∀ (a b c), (∀ (a' b' c'), R ⟨a', b', c'⟩ ⟨a, b, c⟩ → C₃ a' b' c') → C₃ a b c}
+    {a : α} {b : β a} {c : γ a b} (wf : Acc R ⟨a, b, c⟩) :
+    partialExtrinsicFix₃ R F a b c = F a b c (fun a b c _ => partialExtrinsicFix₃ R F a b c) := by
+  rw [partialExtrinsicFix₃_eq_partialExtrinsicFix wf, partialExtrinsicFix_eq_apply_of_acc wf]
+  congr 1; ext a' b' c' hR
+  rw [partialExtrinsicFix₃_eq_partialExtrinsicFix (wf.inv hR)]
+
+public theorem partialExtrinsicFix₃_eq_apply [∀ a b c, Nonempty (C₃ a b c)]
+    {R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop}
+    {F : ∀ (a b c), (∀ (a' b' c'), R ⟨a', b', c'⟩ ⟨a, b, c⟩ → C₃ a' b' c') → C₃ a b c}
+    {a : α} {b : β a} {c : γ a b} (wf : WellFounded R) :
+    partialExtrinsicFix₃ R F a b c = F a b c (fun a b c _ => partialExtrinsicFix₃ R F a b c) :=
+  partialExtrinsicFix₃_eq_apply_of_acc (wf.apply _)
+
+public theorem partialExtrinsicFix₃_eq_fix [∀ a b c, Nonempty (C₃ a b c)]
+    {R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop}
+    {F : ∀ a b c, (∀ a' b' c', R ⟨a', b', c'⟩ ⟨a, b, c⟩ → C₃ a' b' c') → C₃ a b c}
+    (wf : WellFounded R) {a b c} :
+    partialExtrinsicFix₃ R F a b c = wf.fix (fun x G => F x.1 x.2.1 x.2.2 (fun a b c h => G ⟨a, b, c⟩ h)) ⟨a, b, c⟩ := by
+  rw [partialExtrinsicFix₃_eq_partialExtrinsicFix (wf.apply _), partialExtrinsicFix_eq_fix wf]
+
 end WellFounded