Extrinsic termination proofs for well-founded recursion

Stream: lean4

[Joachim Breitner]

I wrote a blog post about who well-founded recursion proofs could possibly also be done in Lean. This is a dead-end (hence exiled to my blog), but at least I found it interesting to ponder this:
https://www.joachim-breitner.de/blog/816-Extrinsic_termination_proofs_for_well-founded_recursion_in_Lean

[Robin Arnez]

I actually thought of a very similar concept but instead with the idea of not providing the proof directly in the declaration, so basically partial but you can still use it in proofs. I used something like this:

open scoped Classical

inductive Terminates {α : Sort u} {β : α → Sort v}
    (f : ((x : α) → β x) → ((x : α) → β x)) : (x : α) → β x → Prop where
  | intro (x : α) (y : β x) (p : α → Prop) (g : (y : α) → p y → β y)
    (h : ∀ y (h : p y), Terminates f y (g y h))
    (h2 : ∀ g' : (x : α) → β x, f (fun z => if h : p z then g z h else g' z) x = y) : Terminates f x y

@[specialize]
partial def computableFix {α : Sort u} {β : α → Sort v} [(x : α) → Nonempty (β x)]
    (f : ((x : α) → β x) → ((x : α) → β x)) : (x : α) → β x :=
  f (computableFix f)

@[implemented_by computableFix]
noncomputable def fix {α : Sort u} {β : α → Sort v} [(x : α) → Nonempty (β x)]
    (f : ((x : α) → β x) → ((x : α) → β x)) : (x : α) → β x := by
  intro x
  by_cases h : ∃ y, terminates f x y
  · exact h.choose
  · exact computableFix f x

That basically means that the functions doesn't need to be well-founded entirely, it can also have points that don't terminate but those are still opaque. I also had my own definition of callsOn which used ifs and yours is definitely much cleaner lol.

[Joachim Breitner]

Indeed, that’s neat. Note that this variant only works for types that inhabited a priori, which is a bit more restrictive.

Have you tried replacing the implemented_by with a computableFix?

@[csimp]
theorem fix_eq_computableFix : @fix = @computableFix :=by
  funext α β _ f x
  unfold fix
  split
  next h =>
    obtain ⟨y, hy⟩ := h
    induction hy with
    | intro x y p g ht heq ih =>
      sorry
  next =>
    rfl

Or, in other words, are you able to prove a fixedpiont equation for your fix, if it is terminating?

[Robin Arnez]

This was my original proof:

theorem Terminates.unique {α : Sort u} {β : α → Sort v} [(x : α) → Nonempty (β x)]
    (f : ((x : α) → β x) → ((x : α) → β x)) (x : α) (y1 : β x) (y2 : β x)
    (h1 : Terminates f x y1) (h2 : Terminates f x y2) : y1 = y2 := by
  induction h1 with
  | intro x y1 p1 g1 h1 h1' ih =>
    have ⟨_, _, p2, g2, h2, h2'⟩ := h2
    specialize h1' (fun z => if h : p2 z then g2 z h else Classical.ofNonempty)
    specialize h2' (fun z => if h : p1 z then g1 z h else Classical.ofNonempty)
    have : (fun z => if h : p1 z then g1 z h else if h : p2 z then g2 z h else Classical.ofNonempty)
        = (fun z => if h : p2 z then g2 z h else if h : p1 z then g1 z h else Classical.ofNonempty) := by
      ext z
      split
      · split
        · exact ih z _ _ (h2 z ‹_›)
        · rfl
      · rfl
    rw [this] at h1'
    rw [h1'] at h2'
    exact h2'

theorem fix_eq {α : Sort u} {β : α → Sort v} [(x : α) → Nonempty (β x)]
    (f : ((x : α) → β x) → ((x : α) → β x)) (x : α) (h : ∃ y, Terminates f x y)
    : fix f x = f (fix f) x := by
  have ⟨y, _, _, p, g, h1, h2⟩ := h
  have hterm : Terminates f x y := ⟨_, _, p, g, h1, h2⟩
  specialize h2 (fix f)
  conv => lhs; unfold fix
  simp [h]
  have : (fun z => if h : p z then g z h else fix f z) = fix f := by
    ext z
    unfold fix
    split
    · have : ∃ y, Terminates f z y := ⟨_, (h1 z ‹_›)⟩
      simp [this]
      apply Terminates.unique
      · exact h1 z ‹_›
      · exact this.choose_spec
    · rfl
  rw [this] at h2
  rw [h2]
  apply Terminates.unique
  · exact h.choose_spec
  · exact hterm

[Robin Arnez]

I actually worked on it a bit more and made this work:

def log2Example : Nat → Nat :=
  Partial.fix (fun f x => if x ≤ 1 then 0 else f (x / 2) + 1)

def log2Example' : (Nat → Nat) × (Nat → Nat) :=
  Partial.fix (fun (f, g) => (
    fun x => if x ≤ 1 then 0 else g (x / 2) + 1, -- f
    fun x => if x ≤ 1 then 0 else f (x / 2) + 1  -- g
  ))

=> very simple declaration of normally and mutually recursive functions

Full code

variable {α : Sort u}
variable {β : α → Sort v}
variable {γ : Sort w}

noncomputable def unpartial [∀ a, Nonempty (β a)]
    {p : α → Prop} (f : (a : α) → p a → β a) : (a : α) → β a := by
  intro a
  by_cases h : p a
  · exact f a h
  · exact Classical.ofNonempty

@[simp]
theorem unpartial_pos [∀ a, Nonempty (β a)] {p : α → Prop} {f : (a : α) → p a → β a}
    {x : α} (h : p x) : unpartial f x = f x h := by
  simp only [unpartial, h, reduceDIte]

def CallsOn (P : α → Prop) (F : (∀ y, β y) → γ) :=
  ∃ (F' : (∀ y, P y → β y) → γ), ∀ f, F' (fun y _ => f y) = F f

theorem CallsOn.congr {P : α → Prop} {F : (∀ y, β y) → γ}
    (h : CallsOn P F) {f f'} (h' : ∀ x, P x → f x = f' x) : F f = F f' := by
  obtain ⟨F', hF'⟩ := h
  rw [← hF' f, ← hF' f']
  simp +contextual only [h']

theorem CallsOn.imp {P₁ P₂ : α → Prop} {F : (∀ y, β y) → γ}
    (h : ∀ {x}, P₁ x → P₂ x) : CallsOn P₁ F → CallsOn P₂ F := by
  intro ⟨F', hF'⟩
  refine ⟨?_, ?_⟩
  · intro g
    apply F'
    intro y hy
    exact g y (h hy)
  · exact hF'

theorem CallsOn.and [∀ a, Nonempty (β a)] {P₁ : α → Prop} {P₂ : α → Prop} {F : (∀ y, β y) → γ}
    (h₁ : CallsOn P₁ F) (h₂ : CallsOn P₂ F) : CallsOn (fun x => P₁ x ∧ P₂ x) F := by
  obtain ⟨F'₁, hF'₁⟩ := h₁
  obtain ⟨F'₂, hF'₂⟩ := h₂
  refine ⟨?_, ?_⟩
  · intro f
    apply F'₁
    intro a h
    by_cases h' : P₂ a
    · exact f a ⟨h, h'⟩
    · exact Classical.ofNonempty
  · intro f
    dsimp
    rw [hF'₁, ← hF'₂]
    simp +contextual only [reduceIte]
    rw [hF'₂]

inductive TerminatesIn (F : ((a : α) → β a) → (a : α) → β a) :
    (a : α) → β a → Prop where
  | intro' (p : α → Prop) (f : (a : α) → p a → β a)
    (h : ∀ a, (h : p a) → TerminatesIn F a (f a h))
    (x : α) (hx : CallsOn p (fun f => F f x)) :
    TerminatesIn F x (hx.choose f)

def Terminates (F : ((a : α) → β a) → (a : α) → β a) (x : α) : Prop :=
  ∃ y, TerminatesIn F x y

theorem TerminatesIn.terminates {F : ((a : α) → β a) → (a : α) → β a} {x : α} {y : β x}
    (h : TerminatesIn F x y) : Terminates F x := ⟨y, h⟩

@[specialize]
private unsafe def unsafeFix [∀ a, Nonempty (β a)]
    (F : ((a : α) → β a) → (a : α) → β a) : (a : α) → β a :=
  F (unsafeFix F)

@[implemented_by unsafeFix]
opaque opaqueFix [∀ a, Nonempty (β a)]
    (F : ((a : α) → β a) → (a : α) → β a) : (a : α) → β a

@[implemented_by unsafeFix]
noncomputable def fix [∀ a, Nonempty (β a)]
    (F : ((a : α) → β a) → (a : α) → β a) : (a : α) → β a := by
  intro x
  by_cases h : Terminates F x
  · exact h.choose
  · exact opaqueFix F x

variable [∀ a, Nonempty (β a)] in

theorem TerminatesIn.unique {F : ((a : α) → β a) → (a : α) → β a} {x : α}
    {y y' : β x} (h : TerminatesIn F x y) (h' : TerminatesIn F x y') : y = y' := by
  induction h with | intro' p₁ f₁ h₁ x hx₁ ih =>
  have ⟨p₂, f₂, h₂, _, hx₂⟩ := h'
  have hy₁ := hx₁.choose_spec
  have hy₂ := hx₂.choose_spec
  dsimp only at hy₁ hy₂
  have hy₁' := hy₁ (unpartial f₁)
  have hy₂' := hy₂ (unpartial f₂)
  simp +contextual at hy₁' hy₂'
  rw [hy₁', hy₂']
  apply (hx₁.and hx₂).congr
  simp +contextual only [unpartial_pos]
  intro a h
  exact ih a h.1 (h₂ a h.2)

theorem TerminatesIn.intro {F : ((a : α) → β a) → (a : α) → β a} {x : α}
    (h : CallsOn (Terminates F) (fun f => F f x)) :
    TerminatesIn F x (h.choose (fun _ h' => h'.choose)) := by
  constructor
  intro a h'
  exact h'.choose_spec

theorem Terminates.intro {F : ((a : α) → β a) → (a : α) → β a} {x : α}
    (h : CallsOn (Terminates F) (fun f => F f x)) :
    Terminates F x := by
  exact ⟨_, .intro h⟩

@[elab_as_elim, induction_eliminator]
theorem Terminates.induction {F : ((a : α) → β a) → (a : α) → β a}
    {motive : (x : α) → Terminates F x → Prop}
    (intro : ∀ x h, CallsOn (fun x => ∃ h, motive x h) (fun f => F f x) → motive x (.intro h))
    {x : α} (h : Terminates F x) : motive x h := by
  obtain ⟨y, hy⟩ := h
  induction hy with
  | intro' p f h x hx ih =>
    apply intro
    · exact CallsOn.imp (fun hx => (h _ hx).terminates) hx
    · apply CallsOn.imp ?_ hx
      intro x hx
      refine ⟨?_, ?_⟩
      · exact (h x hx).terminates
      · exact ih x hx

@[elab_as_elim, cases_eliminator]
theorem Terminates.cases {F : ((a : α) → β a) → (a : α) → β a}
    {motive : (x : α) → Terminates F x → Prop}
    (intro : ∀ x h, motive x (.intro h))
    {x : α} (h : Terminates F x) : motive x h := by
  induction h with
  | intro x h ih =>
    exact intro x h

@[elab_as_elim]
theorem Terminates.ndinduction {F : ((a : α) → β a) → (a : α) → β a}
    {motive : α → Prop}
    (intro : ∀ x, CallsOn motive (fun f => F f x) → motive x)
    {x : α} (h : Terminates F x) : motive x := by
  induction h with
  | intro x h ih =>
    apply intro
    exact ih.imp (·.2)

theorem fix.peq_def {F : ((a : α) → β a) → (a : α) → β a} [∀ a, Nonempty (β a)] {x : α}
    (h : Terminates F x) : fix F x = F (fix F) x := by
  unfold fix
  simp only [h, reduceDIte]
  have h' := h.choose_spec
  generalize h.choose = a at h'; clear h
  rcases h' with ⟨p, f, h, _, hx⟩
  have hF' := hx.choose_spec
  generalize hx.choose = F' at hF'; clear hx
  dsimp at hF'
  rw [← hF']
  congr; funext y hy
  specialize h y hy
  simp only [h.terminates, reduceDIte, h.unique h.terminates.choose_spec]

class Partial (α : Sort u) (β : outParam (Sort v)) where
  Out : β → Sort w
  [nonempty : ∀ x, Nonempty (Out x)]
  toFun : α → ((x : β) → Out x)
  ofFun : ((x : β) → Out x) → α
  toFun_ofFun : ∀ f x, toFun (ofFun f) x = f x

attribute [instance] Partial.nonempty

def Partial.fix {β : Sort v} (f : α → α) [inst : Partial α β] : α :=
  ofFun (_root_.fix fun g => toFun (f (ofFun g)))

def Partial.fix.dom {β : Sort v} (f : α → α) [inst : Partial α β] : β → Prop :=
  Terminates fun g => toFun (f (ofFun g))

def Partial.fix.peq_def {β : Sort v} (f : α → α) [inst : Partial α β]
    {x : β} (hx : dom f x) : toFun (fix f) x = toFun (f (fix f)) x := by
  unfold fix
  unfold dom at hx
  rw [toFun_ofFun, _root_.fix.peq_def hx]

instance (priority := low) [Nonempty α] : Partial α Unit where
  Out _ := α
  toFun x _ := x
  ofFun f := f ()
  toFun_ofFun _ _ := rfl

instance {γ : α → Sort w} [inst : ∀ a, Partial (β a) (γ a)] : Partial ((a : α) → β a) ((a : α) ×' γ a) where
  Out := fun ⟨a, b⟩ => (inst a).Out b
  toFun x := fun ⟨a, b⟩ => Partial.toFun (x a) b
  ofFun f := fun a => Partial.ofFun (fun b => f ⟨a, b⟩)
  toFun_ofFun _ _ := Partial.toFun_ofFun _ _

instance {α₁ β₁ α₂ β₂ : Sort _} [inst1 : Partial α₁ β₁] [inst2 : Partial α₂ β₂] :
    Partial (α₁ × α₂) (β₁ ⊕' β₂) where
  Out
    | .inl x => inst1.Out x
    | .inr x => inst2.Out x
  nonempty
    | .inl _ => inferInstance
    | .inr _ => inferInstance
  toFun x
    | .inl y => inst1.toFun x.1 y
    | .inr y => inst2.toFun x.2 y
  ofFun f := (inst1.ofFun (fun x => f (.inl x)), inst2.ofFun (fun x => f (.inr x)))
  toFun_ofFun _
    | .inl _ => Partial.toFun_ofFun _ _
    | .inr _ => Partial.toFun_ofFun _ _

instance {α₁ β₁ α₂ β₂ : Sort _} [inst1 : Partial α₁ β₁] [inst2 : Partial α₂ β₂] :
    Partial (α₁ ×' α₂) (β₁ ⊕' β₂) where
  Out
    | .inl x => inst1.Out x
    | .inr x => inst2.Out x
  nonempty
    | .inl _ => inferInstance
    | .inr _ => inferInstance
  toFun x
    | .inl y => inst1.toFun x.1 y
    | .inr y => inst2.toFun x.2 y
  ofFun f := ⟨inst1.ofFun (fun x => f (.inl x)), inst2.ofFun (fun x => f (.inr x))⟩
  toFun_ofFun _
    | .inl _ => Partial.toFun_ofFun _ _
    | .inr _ => Partial.toFun_ofFun _ _

def log2Example : Nat → Nat :=
  Partial.fix (fun f x => if x ≤ 1 then 0 else f (x / 2) + 1)

def log2Example' : (Nat → Nat) × (Nat → Nat) :=
  Partial.fix (fun (f, g) => (
    fun x => if x ≤ 1 then 0 else g (x / 2) + 1, -- f
    fun x => if x ≤ 1 then 0 else f (x / 2) + 1  -- g
  ))

[Robin Arnez]

The proof for it being equivalent to Nat.log2 is possible, although a bit cumbersome:

example : log2Example = Nat.log2 := by
  unfold log2Example
  have : ∀ x, Partial.fix.dom (fun f x => if x ≤ 1 then 0 else f (x / 2) + 1) x := by
    intro ⟨x, ()⟩
    simp only [Partial.fix.dom, Partial.toFun, Partial.ofFun]
    fun_induction Nat.log2 x with
    | case1 x hx ih =>
      apply Terminates.intro
      apply CallsOn.of_forall_ite_eq (fun f g => ?_)
      simp only [ih, reduceIte]
    | case2 x hx =>
      apply Terminates.intro
      apply CallsOn.of_forall_ite_eq (fun f g => ?_)
      have : x ≤ 1 := by omega
      simp [this]
  rw [Partial.fix_eq this]
  funext x
  fun_induction Nat.log2 x with
  | case1 x hx ih =>
    rw [Partial.fix_eq this]
    have : ¬x ≤ 1 := by omega
    conv => rhs; unfold Nat.log2
    simp only [ih, this, reduceIte, hx]
  | case2 x hx =>
    have : x ≤ 1 := by omega
    conv => rhs; unfold Nat.log2
    simp only [this, reduceIte, hx]

[Robin Arnez]

Funnily enough I also thought of a similar concept once:

Robin Arnez schrieb:

I actually thought of a very similar concept but instead with the idea of not providing the proof directly in the declaration, so basically partial but you can still use it in proofs. I used something like this:

open scoped Classical

inductive Terminates {α : Sort u} {β : α → Sort v}
    (f : ((x : α) → β x) → ((x : α) → β x)) : (x : α) → β x → Prop where
  | intro (x : α) (y : β x) (p : α → Prop) (g : (y : α) → p y → β y)
    (h : ∀ y (h : p y), Terminates f y (g y h))
    (h2 : ∀ g' : (x : α) → β x, f (fun z => if h : p z then g z h else g' z) x = y) : Terminates f x y

@[specialize]
partial def computableFix {α : Sort u} {β : α → Sort v} [(x : α) → Nonempty (β x)]
    (f : ((x : α) → β x) → ((x : α) → β x)) : (x : α) → β x :=
  f (computableFix f)

@[implemented_by computableFix]
noncomputable def fix {α : Sort u} {β : α → Sort v} [(x : α) → Nonempty (β x)]
    (f : ((x : α) → β x) → ((x : α) → β x)) : (x : α) → β x := by
  intro x
  by_cases h : ∃ y, terminates f x y
  · exact h.choose
  · exact computableFix f x

That basically means that the functions doesn't need to be well-founded entirely, it can also have points that don't terminate but those are still opaque. I also had my own definition of callsOn which used ifs and yours is definitely much cleaner lol.

[Sebastian Graf]

Robin, were you perhaps trying to quote reply in #lean4 > Partial correctness of partial functions?

Either way, here's one way starting from Joachim's callsOn idea to provide the termination proof (aka Acc R x) extrinsically and for each point individually. Specifically, fix_eq' generalizes Joachim's fix_eq and takes a proof of termination hacc : Acc R x for the particular x to reduce instead of one big WellFounded R upfront (which is ∀ x, Acc R x):

variable {α : Sort u}
variable {β : α → Sort v}
variable {γ : Sort w}

def callsOn (P : α → Prop) (F : (∀ y, β y) → γ) :=
  ∃ (F': (∀ y, P y → β y) → γ), ∀ f, F' (fun y _ => f y) = F f

variable (F : (∀ y, β y) → (∀ x, β x))
variable (R : α → α → Prop)

local infix:50 " ≺ " => R

def recursesVia : Prop := ∀ x, callsOn (· ≺ x) (fun f => F f x)

noncomputable def fix (wf : WellFounded R) (h : recursesVia F R) : (∀ x, β x) :=
  wf.fix (fun x => (h x).choose)

def fix_eq (wf : WellFounded R) h x :
    fix F R wf h x = F (fix F R wf h) x := by
  unfold fix
  rw [wf.fix_eq]
  apply (h x).choose_spec

open Classical in
noncomputable def fix' (x : α) (R : α → α → Prop) (ne : (y : α) → ¬Acc R y → Nonempty (β y)) (hvia : recursesVia F R) : β x :=
  if h : Acc R x
  then WellFounded.fixF (fun x => (hvia x).choose) x h
  else Classical.choice (ne x h)

def fix_eq' x R ne hvia (hacc : Acc R x) :
    fix' F x R ne hvia = F (fun x => fix' F x R ne hvia) x := by
  unfold fix'
  have ⟨F', hcall⟩ := hvia x
  simp only [hacc, ↓reduceDIte]
  rw [WellFounded.fixFEq]
  simp only [←(hvia x).choose_spec]
  simp +contextual [hacc.inv]

I rearranged parameters so that x comes before R to signify that it is valid to prove termination of different x with different Rs, supplied at call sites rather than definition sites.
Regarding the Nonempty proof obligation: In case that WellFounded R, ne is provable by contradiction.

Now decreasing_by etc. could produce a particular WellFounded R, but if that fails we could still elaborate to the "partially applied" fix_eq' version where the user specifies an R, recursesVia F R and Acc R x after the fact.

Still, there's the fun induction rewriting caveat. But it "feels" to me like the solution to that problem should be independent of the termination proof.

[Robin Arnez]

Hmm if I understand it correctly that would imply thinking of a relation before-hand, no?

[Robin Arnez]

My idea was to only assume nonemptiness on the entire domain and then simply allow any relation to be used later

[Paul Reichert]

I also got hooked by this problem, so here's yet another approach to extrinsically prove partial termination of recursive functions:

• It uses partial_fixpoint with a special CCPO monad FilterT
• It works with the McCarthy f91 function and Tree.map (haven't tried the log2 example yet, but I see no obstructions)
• It also works in some monadic settings where the chain of recursive calls isn't well-founded
• The recursive function can either be defined using a Nonempty instance or by requiring a partial well-definedness proof in the function signature

It's a bit tedious to do the termination proofs right now, but I hope a better library could help with that.

The main idea is to consider what happens if we break the potentially infinite recursion by inserting "holes" after finitely many recursive calls. We're allowed to let the holes return arbitrary values. The deeper down these holes are inserted, the smaller the set of possible return values. A function call f x is considered well-defined if there's exactly one return value that's possible no matter how we place the holes.

[Sebastian Graf]

Awesome!! I was wondering what would turn out more usable: An idealized solution based on well-founded recursion that allows users to specify the accessibility proof or a nonemptiness proof for a partial def at call sites or some generic PartialT moand based on partial_fixpoint. You FilterT brings the latter idea to its conclusion. Bravo!

Unfortunately, that requires us to prove that our partial fixpoint is "not too large", something
that requires us to unseal the fixpoint definition of f91 and use coinduction (hidden in
FilterT.isProper_fix_of_preserves_isProper).

I only see a use of fixpoint induction which is not technically coinduction. I think it computes the least fixpoint of the functional. Lean.Order.iterates is not unlike Acc.

It appears your approach may be related to the filter model of denotational semantics (1983, also used in PLFA).

(Also, techically the IsProper obligation is quite like the NonEmpty obligation, no?)

[Paul Reichert]

Happy to hear that it seems potentially useful to you! I'm not familiar with the filter model of denotational semantics, hopefully I find the time to take a look soon.

Sebastian Graf said:

(Also, techically the IsProper obligation is quite like the NonEmpty obligation, no?)

This seems like a subtle point to me. If m α is empty while m β is not and x : FilterT m α, g : α → FilterT m β, then x >>= f : FilterT m β will not be proper even if m β is nonempty. (Such x might be the result of some fixpoint equation.) So at least I don't think we could just replace IsProper with Nonempty.

(On another note, it occurred to me that I should try to prove some lemmas about the interaction of pure and get!/get in order to make sure that the unsafe implementations are "sound", so all is not well yet. I still fear that empty types like m α might get us into trouble in this regard.)

[Paul Reichert]

Oh no -- indeed, I was able to prove False using native_decide, showing that the implemented_by-based computable implementation is unsound, at least in combination with partial_fixpoint and native_decide. So this approach at least needs some adjusting. I wonder what exactly caused the contradiction in here...

Perhaps the issue is related to get! = Classical.ofNonempty and one needs to assign a different (opaque) value depending on the parameters like Robin did above. I'm not quite sure how that would fit into the CCPO monad, though.

[Paul Reichert]

Found a way to fix the issue at hand by forbidding filters to contain the empty set (except for empty types). This increases the weirdness of the bind implementation. The examples needed only minimal adjustments.

However, it's possible that there is another False proof I couldn't conceive of. One really needs to be extremely cautious with unsafely implemented CCPO monads; it doesn't seem reasonable to use one in production.

A paradox using the more reasonable, simpler but unsafe CCPO monad Partial (= always-some Option)

One quite plausible CCPO monad I've wish we had is Partial. Semantically, it is just Option, but there's no computable none constructor. It's implemented unsafely by assuming that none never happens because we never construct none at runtime. Sadly, this also leads to a paradox:

def Partial α := Option α

unsafe def Partial.pureUnsafe (a : α) : Partial α :=
  unsafeCast a

@[implemented_by pureUnsafe]
def Partial.pureImpl (a : α) : Partial α :=
  some a

unsafe def Partial.bindUnsafe (x : Partial α) (f : α → Partial β) : Partial β :=
  let x : α := unsafeCast x
  let f a : β := unsafeCast (f a)
  unsafeCast (f x)

@[implemented_by bindUnsafe]
def Partial.bindImpl (x : Partial α) (f : α → Partial β) : Partial β:=
  Option.bind x f

unsafe def Partial.getUnsafe! [Inhabited α] (x : Partial α) : α :=
  unsafeCast x

@[implemented_by getUnsafe!]
def Partial.get! [Inhabited α] (x : Partial α) : α :=
  Option.get! x

instance : Monad Partial where
  pure := Partial.pureImpl
  bind := Partial.bindImpl

noncomputable instance : Lean.Order.CCPO (Partial α) :=
  inferInstanceAs <| Lean.Order.CCPO (Option α)

instance : Lean.Order.MonoBind Partial :=
  inferInstanceAs <| Lean.Order.MonoBind Option

def f (n : Nat) : Partial Nat := do
  match n with
  | 0 => f 0
  | n + 1 =>
    let _ ← f n
    return n
partial_fixpoint

unseal f

theorem t₁ : f 0 = none := by
  apply Lean.Order.fix_induct f._proof_1 (motive := fun f => f 0 = none)
  · intro f hcf h
    simp only [Lean.Order.CCPO.csup, Lean.Order.fun_csup, Lean.Order.flat_csup]
    rw [dif_neg]
    simp
    exact h
  · intro f h0
    simp
    exact h0

theorem t₂ : (f 2).get! = 0 := by
  rw [f, f]
  simp [t₁, Partial.get!]

theorem t₃ : (f 2).get! = 1 := by native_decide

theorem oh_no : False := by
  suffices h : 0 = 1 by omega
  rw [← t₂, t₃]

[Joachim Breitner]

I have been musing about this variant as well; thanks for showing how to break it

[Paul Reichert]

Actually, you musing about it in front of me was how I got hooked by the idea ;)

[Joachim Breitner]

So the unsoundness comes from the fact that compiled code can be more defined than what the kernel thinks it is.

[Edward van de Meent]

or, rephrasing, from the fact that the elaboration results in a function which is too undefined?

[Edward van de Meent]

i have to say, to me the t₂ result was more surprising than the t₃ result

[Joachim Breitner]

Would

theorem t₂ : f 2 = none  := by

be less surprising? (given that there is a recursive call and the function looks nonterminating)

[Edward van de Meent]

well, i expected the recursive call to be ignored because it's never used

[Edward van de Meent]

maybe this is a remnant from when i did haskell, where evaluation is lazy

[Joachim Breitner]

Even Haskell wouldn’t ignore it, depending on the monad. Note that’s it not a pure let but a monadic bind

[Edward van de Meent]

ah, that's true...

[Sebastian Graf]

Here's another attempt based on well-founded recursion. I managed to completely get rid of R, instead taking "the unique smallest R" as the call relation. My hope is that it could be used to

1. Elaborate total, well-founded definition by termination_by to, just as today
2. Elaborate partial def to. Unlike what we have today, this new elaboration would allow reasoning about a function call given a proof of its termination via Acc (Calls F) x. I demonstrate this below using a function that computes a variant of the collatz function. Unfolding these calls is presently quite unwieldy, but I'm hopeful it can be automated much more.

variable {α : Sort u}
variable {β : α → Sort v}

variable (F : (∀ y, β y) → (∀ x, β x))
variable (R : α → α → Prop)

/-- `infR S` is the smallest relation `R` satisfying `S R`. -/
def infR (S : (α → α → Prop) → Prop) : α → α → Prop :=
  fun x y => ∀ R, S R → R x y

/-- If `IsElab F R F'`, then `F'` elaborates calls to the functional `f y` in `F f x` with a proof
that `R y x`, such that `F' x (fun y (_ : R y x) => f y) = F f x`. -/
def IsElab (F' : ∀ x, (∀ y, R y x → β y) → β x) : Prop :=
  ∀ f x, F' x (fun y _ => f y) = F f x

/--
  `Calls F y x` iff `F f x` calls `f` on `y`.
-/
def Calls : α → α → Prop :=
  infR fun R => ∃ (F' : ∀ x, (∀ y, R y x → β y) → β x), IsElab F R F'

def HasElab : Prop := ∃ F', IsElab F (Calls F) F'

-- The following function could be generalized from `Nat` to any type `β y` with at least two elements.
-- (TODO: If there are fewer elements then we should be able to prove that `¬Calls F y x`.)
open Classical in
theorem mkCallReturningNat {F : (α → Nat) → (α → Nat)} {m n : α}
  (h : ∀ (ys : α → α → Prop), ¬ys m n → ¬F (fun y => if ys y n then 1 else 2) n = F (fun x => 1) n) :
    Calls F m n := by
  intro ys ⟨F', helab⟩
  false_or_by_contra
  next hys =>
  have h₁ := helab (fun y => if ys y n then 1 else 2) n
  have h₂ := helab (fun x => 1) n
  simp +contextual at h₁
  exact h ys hys (h₁.symm.trans h₂)

def collatz_len'.functional (f : Nat → Nat) (n : Nat) : Nat :=
  if n = 1 then 1
  else if n % 2 = 0
  then 1 + f (n / 2)
  else 1 + f (3 * n + 1)

example : Calls collatz_len'.functional 2 4 := mkCallReturningNat fun ys hys => by
  simp [collatz_len'.functional, hys]

example : Calls collatz_len'.functional 22 7 := mkCallReturningNat fun ys hys => by
  simp [collatz_len'.functional, hys]

theorem collatz_len'.functional.Calls_one :
    ¬Calls collatz_len'.functional n 1 := fun hcall => by
  apply hcall (fun y x => ¬(y = n ∧ x = 1))
  · exists fun x f => collatz_len'.functional (fun y => if h : y = n ∧ x = 1 then 1 else f y h) x
    simp [IsElab, functional]
    intro f x
    split
    · rfl
    · split
      · simp [*]
      · simp [*]
  · trivial

theorem collatz_len'.functional.Calls_even (h : n % 2 = 0) :
    Calls collatz_len'.functional (n / 2) n := mkCallReturningNat fun ys hys => by
  have : ¬n = 1 := by omega
  simp [collatz_len'.functional, *]

theorem collatz_len'.functional.Calls_odd (h₁ : ¬n = 1) (h₂ : ¬(n % 2 = 0)) :
    Calls collatz_len'.functional (3 * n + 1) n := mkCallReturningNat fun ys hys => by
  simp [collatz_len'.functional, *]

def collatz_len'.functional.elab (n : Nat) (f : (m : Nat) → Calls collatz_len'.functional m n → Nat) : Nat :=
  if hone : n = 1 then 1
  else if hmod : n % 2 = 0
  then 1 + f (n / 2) (collatz_len'.functional.Calls_even hmod)
  else 1 + f (3 * n + 1) (collatz_len'.functional.Calls_odd hone hmod)

theorem collatz_len'.functional.HasElab : HasElab collatz_len'.functional := by
  exists fun n f => collatz_len'.functional.elab n f
  simp [IsElab, «elab», functional]

/--
  The following definition could be used to elaborate `partial` functions as well as well-founded
  definitions using, e.g., `termination_by`.
  The key is to provide `HasElab F` that is used to perform the actual recursion.
-/
noncomputable def partial_fix (helab : HasElab F) (x : α) (hne : ¬Acc (Calls F) x → Nonempty (β x)) : β x :=
  open Classical in
  if hacc : Acc (Calls F) x
  then WellFounded.fixF helab.choose x hacc
  else Classical.choice (hne hacc)

/--
  This is essentially what `partial def collatz_len` generates today; some function the result of
  which is indeterminate.

  Requires `NonEmpty Nat`. A "smarter" version would shift the proof obligation of
  `¬Acc (Calls F) n → Nonempty Nat` to call sites `n` (which is nonsensical for `Nat`).
-/
-- TODO: `csimp` or `implemented_by`
noncomputable def collatz_len (n : Nat) : Nat :=
  partial_fix collatz_len'.functional collatz_len'.functional.HasElab n (fun _ => inferInstance)

/--
  `partial_fix` can be unrolled at `x` as long as we can prove that `x` is
  accessible in `Calls F`.
-/
-- TODO: It is annoying that we need `hne` in the RHS. We are lacking the proof for
-- `Acc (Calls F) y`/`Calls F y x` in the call to `partial_fix`. Thus we effectively forget that we
-- keep descending the same chain of calls.
theorem partial_fix_nonempty_acc_eq x (hne : ∀y, ¬Acc (Calls F) y → Nonempty (β y)) (hacc : Acc (Calls F) x) :
    partial_fix F helab x (fun h => (h hacc).elim) = F (fun y => partial_fix F helab y (hne y)) x := by
  unfold partial_fix
  simp only [hacc, ↓reduceDIte]
  rw [WellFounded.fixFEq, ←helab.choose_spec]
  simp +contextual [hacc.inv]

/--
  In contrast to the usual `partial` definition, we can actually reason about this one
  and peel off layer by layer!
-/
example : collatz_len 5 = 6 := by
  have hacc : Acc (Calls collatz_len'.functional) 5 := sorry
  have hne : ∀y, ¬Acc (Calls collatz_len'.functional) y → Nonempty Nat := fun _ => inferInstance
  simp [collatz_len, partial_fix_nonempty_acc_eq]
  rw [partial_fix_nonempty_acc_eq _ _ hne hacc]
  simp [collatz_len'.functional]
  have hacc := hacc.inv (collatz_len'.functional.Calls_odd (by omega) (by omega))
  rw [partial_fix_nonempty_acc_eq _ _ hne hacc]
  simp [collatz_len'.functional]
  have hacc := hacc.inv (collatz_len'.functional.Calls_even (by omega))
  rw [partial_fix_nonempty_acc_eq _ _ hne hacc]
  simp [collatz_len'.functional]
  have hacc := hacc.inv (collatz_len'.functional.Calls_even (by omega))
  rw [partial_fix_nonempty_acc_eq _ _ hne hacc]
  simp [collatz_len'.functional]
  have hacc := hacc.inv (collatz_len'.functional.Calls_even (by omega))
  rw [partial_fix_nonempty_acc_eq _ _ hne hacc]
  simp [collatz_len'.functional]
  have hacc := hacc.inv (collatz_len'.functional.Calls_even (by omega))
  rw [partial_fix_nonempty_acc_eq _ _ hne hacc]
  simp [collatz_len'.functional]

/-!
  The same elaboration mechanism works for total well-founded definitions as well.
-/

theorem not_acc_nonempty_of_wellFounded {R} (wf : WellFounded R) :
    ∀y, ¬Acc R y → Nonempty (β y) := by
  intro y hnacc
  exfalso
  exact hnacc (wf.apply y)

noncomputable def total_fix (helab : HasElab F) (wf : WellFounded (Calls F)) : ∀ x, β x := fun x =>
  partial_fix F helab x (not_acc_nonempty_of_wellFounded wf x)

theorem total_fix_wf_eq (helab : HasElab F) (wf : WellFounded (Calls F)) x :
    total_fix F helab wf x = F (fun x => total_fix F helab wf x) x :=
  partial_fix_nonempty_acc_eq F x (not_acc_nonempty_of_wellFounded wf) (wf.apply x)

[Joachim Breitner]

Skimming this on my phone. When would HasElab F not hold for a F?

[Edward van de Meent]

also, the description of infR is kinda wrong... i don't think that infR S itself will satisfy S in general...

[Edward van de Meent]

if S is something like ∃! (x,y), R x y, this is not true i think.

[Edward van de Meent]

(assuming that the type α is not a singleton)

[Sebastian Graf]

Joachim Breitner said:

Skimming this on my phone. When would HasElab F not hold for a F?

The intention is that it always holds and can be derived mechanically, driven by syntax. Note that IsElab is very much like your callsOn predicate, and HasElab F is like recursesVia (Calls F) F (only that HasElab carries a single elaboration F' rather than one per initial point x). I imagine a proof that is similar to your callsOn_map proof in the blog post. "Elaboration" here refers to F', which elaborates the recursive call sites of F f x with a proof for Calls F y x. I actually think that callsOn was a better and non-ambiguous name, but it was the first term that came to mind.

Edward van de Meent said:

if S is something like ∃! (x,y), R x y, this is not true i think.

Can you perhaps try and produce a counter-example? (live)
I tried to stay close to the definition of InfSet.

[Sebastian Graf]

Found a way to get by without infR using an equivalent inductive predicate per functional and wrote up a blog post about my solution: https://fixpt.de/blog/2025-06-08-partially-well-founded-definitions.html

[Joachim Breitner]

Hmm, is this a win? Now you have to define three inductive predicates. I was actually more intrigued by the CallsOn definitions that extract that relation from any functorial. What do we gain over that?

[Edward van de Meent]

Sebastian Graf said:

Edward van de Meent said:

if S is something like ∃! (x,y), R x y, this is not true i think.

Can you perhaps try and produce a counter-example? (live)
I tried to stay close to the definition of InfSet.

variable {α : Sort u}

/-- `infR S` is the smallest relation `R` satisfying `S R`. -/
def infR (S : (α → α → Prop) → Prop) : α → α → Prop :=
  fun x y => ∀ R, S R → R x y

/-- the verbose spelling of `∃! c, R c.1 c.2` -/
def S (R : α → α → Prop) := ∃ (c : α ×' α), (∀ c', (R c'.1 c'.2) ↔ c = c')

example (h : ∀ a : α, ∃ a', a ≠ a') : ¬ S (infR (α := α) S) := by
  dsimp [S]
  rintro ⟨⟨x,y⟩,hc⟩
  have : infR S x y := (hc ⟨x,y⟩).mpr rfl
  obtain ⟨y',hy'⟩ := h y
  dsimp [infR] at this
  specialize this (x = · ∧ y' = ·) (⟨⟨x,y'⟩,fun ⟨_,_⟩ => by
    simp⟩)
  apply hy'
  exact this.right.symm

so infR S will not always satisfy S

[Edward van de Meent]

the proof is basically, when there is not a unique pair in the entire set, for every pair there is a relation satisfying S that does not relate the pair, meaning the infimum does not relate them either.

[Sebastian Graf]

so infR S will not always satisfy S

Right, the infimum of a set S might not be an element of S.

Joachim Breitner said:

Hmm, is this a win? Now you have to define three inductive predicates. I was actually more intrigued by the CallsOn definitions that extract that relation from any functorial. What do we gain over that?

Here's a version that uses your CallsOn but retains the ability to define partial_fix: live

(I'm hopeful but unsure whether the compositional CallsOn lemma approach is actually sufficient to elaborate every WF def.)

I suppose the elaboration algorithm has to continually refine the particular P to supply at the call site of callsOn_base, taking into account path conditions as it descends into ifs/matches etc.
That is basically what collatzLen.Calls encodes; since it's a non-rec inductive we could just write it as a bunch of \ors and \ands.

[Edward van de Meent]

Sebastian Graf said:

Right, the infimum of a set S might not be an element of S.

indeed, but if you say "the smallest X that satisfies P", that means it satisfies P. which it doesn't in this case.

[Paul Reichert]

Having so many interesting approaches, I've created a matrix comparing them: https://cryptpad.fr/sheet/#/2/sheet/edit/APVkPXJpJ6A0eRgAceGRjM2a/

I filled many cells based on ad-hoc reasoning, so feel free to correct any parts that seem wrong! I'm also happy with others adding more columns or rows to the table. I'm sure I forgot to mention the upsides of some approaches in the table.

[Paul Reichert]

Sebastian Graf said:

Here's another attempt based on well-founded recursion. I managed to completely get rid of R, instead taking "the unique smallest R" as the call relation. My hope is that it could be used to

1. Elaborate total, well-founded definition by termination_by to, just as today
2. Elaborate partial def to. Unlike what we have today, this new elaboration would allow reasoning about a function call given a proof of its termination via Acc (Calls F) x. I demonstrate this below using a function that computes a variant of the collatz function. Unfolding these calls is presently quite unwieldy, but I'm hopeful it can be automated much more.

Do you mean by this that this approach is better able to generalize/unify well-founded and partial functions compared to the other approaches, say, Robin's first approach? I would naïvely expect Robin's approach to be flexible enough for this, too. I find your approach interesting either way, just trying to understand better how the approaches compare.

[Sebastian Graf]

TBH, I didn't quite understand Robin's Terminates on first read. Now that I have paged in all the tricks encoded in CallsOn and Acc it makes sense, but I still gravitate towards having the concepts decoupled.

I also thought that each constructor TerminatesIn.intro carrying its own p and f is overkill, but it appears that the f91 example proves that a "static" call relation R independent of the semantics of the function under definition is insufficient as well.

I would then conjecture that constructing the call relation R while elaborating the functional (through a CallsOn-like approach) seems infeasible to define f91, because I fail to see how to evaluate nested calls to define R. TerminatesIn seems to achieve this (I should check but don't feel like it ^^') by interleaving the termination proof with constructing the call relation for each point.

I suppose there is the option of starting with an R that is too large, saying that a nested call f91 (f91 (x+11)) gives rise to R (x+11) x and R y x for any y and then taking the infimum of the descending chain you get by resolving nested calls that are known to terminate given this too large R; for example when x+11 > 100 you'll be able to prove Acc R (x+11), compute f91 (x+11) = x+1 and thus refine R y x to R (x+1) x.
I don't know how to implement this to get an enjoyable system... After all, users are expected to prove membership in this R. I suppose the infR to defining the Calls relation ("Sebastian v0") does something quite like this and is an example of this experience; I would hope it could be used to define f91 but haven't checked because it's extraordinarily tedious to prove membership in Calls F.

[Paul Reichert]

Personally, I think it is fine if termination_by doesn't support f91 and consorts, as long as there's an escape hatch to do a more manual extrinsic termination proof if that does not suffice.

One could define fix according to a maximally general (sound) concept of termination and then provide a convenient frontend for it. Both of these parts seem worthy of investigation if you ask me.

I need to sleep now, but I agree with what you said above; it seems difficult to elaborate a nice wf recursion scheme for f91.

[Mario Carneiro]

I just want to cross reference #lean4 > lean-pipes: could someone help me finish? @ 💬 which does a termination proof via a "most general" inductive relation. It would be great if there was some way to generate this induction proof goal without having to define the inductive type myself.

[Paul Reichert]

@Mario Carneiro Interesting example and nice solution!

(Side note: I could imagine that the proof would also look very nice with more extrinsic termination proof support using a similar strategy like with the f91 termination proof using partial_fixpoint, where the relation used never needs to be written down explicitly. Following your well-foundedness proof, that would amount to first proving by induction that pushR will always terminate and then that go will, relying on the first theorem. (partial-fixpoint itself unfortunately doesn't seem to work here.))

[Paul Reichert]

Here is a new attempt to build a foundation that is as general as possible while adhering to what I believe to be the compiler semantics of partial. It has a "small kernel" in the sense that there is exacly one implemented_by annotation on the fix operator and the rest of the code is safe Lean.

It is general enough to handle all of the examples in the table. Having a nice termination_by frontend was out of scope for this prototype, but there already is a library for fixpoints by well-founded recursion on top of fix, which is also used in some of the examples. Generally, all of the elaborator stuff is missing. It might be nice to implement CallsOn and consorts in the future.

One could also think of it as a less complicated (and probably less unsound) version of the earlier FilterT + partial_fixpoint approach.

[Paul Reichert]

I found a fixpoint combinator that does not rely on unsafe/implemented_by and still allows partial and extrinsic well-foundedness proofs. You can also verify f91 with it! The magic trick is to use a partial function returning a subtype, encoding the expected properties of its return values in the subtype.

Caution: Giving a "termination proof" doesn't mean that the function will actually terminate; that information is no extensional property of the functional. (One can ameliorate this by requiring a call relation up front if desired.)

[Mirek Olšák]

Interesting. If I understand correctly, you use the uniqueness-based definition of a fixpoint, and fit the partial def inside such predicate. I thought your approach with evaluation trees was strictly more general though. The same trick cannot be done with them?

[Mirek Olšák]

I understand that then consistency is not guaranteed. We know that both inner and outer function have some plausible value but that doesn't guarantee the recursion formula, on the other hand, it should guarantee the recursion formula if there is exactly one plausible value (which should be still stronger than recursive uniqueness).

[Paul Reichert]

Mirek Olšák said:

Interesting. If I understand correctly, you use the uniqueness-based definition of a fixpoint, and fit the partial def inside such predicate. I thought your approach with evaluation trees was strictly more general though. The same trick cannot be done with them?

Monads such as StateM Nat are function types. Their efficiency relies on the compiler treating a function α -> StateM Nat Bool as a function α -> Nat -> Bool × Nat taking two arguments and returning Bool × Nat instead of taking one argument and returning lambda functions Nat -> Bool × Nat -- the latter is much less efficient and sometimes breaks tail recursion. Because the fixpoint combinator uses a function α -> Subtype (fun _ : StateM Nat Bool => _), the compiler no longer applies this optimization. This is why it is too inefficient for monadic loops.

The other problem: The old call tree approach simply defined on which inputs the function is well-defined and made it opaque on all other values. However:

  -- from the definition of `fixAttach`
  ⟨F (fixAttach F · |>.val) a, by sorry⟩

In order to provide the sorried proof of type Pred F a (F (fixAttach F ·).val a), we use the proofs (fixAttach F a').property : Pred F a' (fixAttach F a').val. If we simply set Pred F a' _ := True on the non-well-defined inputs, we might need to weaken the Pred F a _ predicate so that the proof is still possible. Admittedly, this is all a bit technical. The old library's definition of partial fixpoint doesn't seem to fit in neatly and I haven't figured out which predicates I need to weaken or strengthen so that it all fits together in a simple and canonical way.

Mirek Olšák said:

I understand that then consistency is not guaranteed. We know that both inner and outer function have some plausible value but that doesn't guarantee the recursion formula, on the other hand, it should guarantee the recursion formula if there is exactly one plausible value (which should be still stronger than recursive uniqueness).

I have problems understanding the meaning of "consistency" and of "inner/outer function". Are you speaking of the old or new approach here?