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]