proving values of a `partial def`

Stream: new members

[llllvvuu]

Consider the following example. I can run #eval on the partial def version, but I cannot prove anything about it. I can prove things about the noncomputable def version, but I cannot run #eval on it.

I have a few questions:

1. What would go wrong if we were allowed to unfold a partial def?
2. Is there any way in Lean to define such a function in a way that supports both running the code and proving? If not, is it theoretically possible for a proof assistant to support it?
3. If not, is there an easier way to define the provable version?

open scoped Classical

partial def collatz (n : Nat) : List Nat :=
  if n == 1 then [1]
  else if n % 2 == 0 then n :: collatz (n / 2)
  else n :: collatz (3 * n + 1)

#eval collatz 10

theorem collatz_1 : collatz 1 = [1] := by
  fail_if_success unfold collatz
  sorry

noncomputable def collatz_wf_fix (n : Nat) (r : Nat → Nat → Prop) (rwf : WellFounded r) :
    Option (List Nat) :=
  WellFounded.fix rwf (fun n ih =>
    if n == 1 then some [1]
    else if n % 2 == 0 then
      if h : r (n / 2) n then (ih (n / 2) h).map (.cons n) else none
    else
      if h : r (3 * n  + 1) n then (ih (3 * n + 1) h).map (.cons n) else none
  ) n

noncomputable def collatz_wf (n : Nat) : Option (List Nat) :=
  if h : ∃ r : Nat → Nat → Prop, ∃ rwf : WellFounded r, (collatz_wf_fix n r rwf).isSome then
    let r := h.choose
    let rwf := h.choose_spec.choose
    collatz_wf_fix n r rwf
  else
    none

-- #eval collatz_wf 10

theorem collatz_wf_1 : collatz_wf 1 = [1] := by
  unfold collatz_wf
  split
  · simp [collatz_wf_fix, WellFounded.fix_eq]
  next h =>
    refine (h ⟨(· < ·), Nat.lt_wfRel.wf, ?_⟩).elim
    simp [collatz_wf_fix, WellFounded.fix_eq]

[Kyle Miller]

Here's an example for 1:

partial def bad (_ : Unit) : Bool := !bad ()

[Kyle Miller]

For collatz_wf, that doesn't look right to me, since you're choosing an arbitrary well-founded relation on Nat and hoping that it supports the recursive function. Likely, collatz_wf could just return none in all cases but the first . I think collatz_wf 1 = [1] is the only thing you can prove about it.

[Kyle Miller]

This doesn't solve not being able to #eval, but at least it's possible to create a relation for the function and prove things about that:

inductive collatz : Nat → List Nat → Prop where
  | one : collatz 1 [1]
  | even (k : Nat) (res : List Nat) (h : collatz k res) :
    collatz (2 * k) (2 * k :: res)
  | odd (k : Nat) (res : List Nat) (h : collatz (3 * (2 * k + 3) + 1) res) :
    collatz (2 * k + 3) ((2 * k + 3) :: res)

(Question: what's collatz 0 supposed to be? Your function infinite loops.)

[llllvvuu]

Ah yes my bad, I didn't get this toy example exactly right, the un-#xy is basically suppose we wanted to write a VM in lean, and wanted to prove VM(input) = output for some input, in spite of some VM(input') not halting. Or to translate a loop from another language into a Lean tail-recursive function and prove loop invariants, but the loop halting is dependent on the initial state.

Maybe a similar trick as what you've just showed would work in those cases too. I'll think about it, thanks!

[Kyle Miller]

At least you can define a small-step function and iterate it

[Joachim Breitner]

If the function is proper tail-recursive and has an inhabited type, nothing would go wrong. This feature would be https://github.com/leanprover/lean4/issues/3119

But yes, iterating a small-step function or relation is a good way to model this for now.

[Tyler Josephson ⚛️]

Our solution to 2) (at least for pure functions) is polymorphism. If you have a function over real numbers (hence, noncomputable) and you want to compute things with it, you can define it with a generic type. Then, you can write proofs about the function when it takes real arguments, and perform calculations when it takes floating point arguments.

Check out Lecture 8 here (recording, slides, code): https://leanprover.zulipchat.com/#narrow/stream/445230-Lean-for-Scientists-and-Engineers-2024

[Eric Wieser]

Does making collatz return a lazy list help here?

[Eric Wieser]

(docs#MLList, docs#LazyList)

[Yuyang Zhao]

You can use docs#PFun, but I'm not sure there's an easy way to use it.

[Yuyang Zhao]

import Mathlib.Data.PFun

def step : Nat × List Nat → List Nat ⊕ (Nat × List Nat)
  | ⟨n, l⟩ =>
    if n == 1 then .inl (1 :: l)
    else if n % 2 == 0 then .inr (n / 2, n :: l)
    else .inr (3 * n + 1, n :: l)

def collatz : Nat →. List Nat :=
  fun n ↦ (PFun.fix (.lift step) ⟨n, []⟩).map List.reverse

#eval! collatz.fn 3 sorry -- [3, 10, 5, 16, 8, 4, 2, 1]

[Yuyang Zhao]

import Batteries.Data.List.Lemmas
import Mathlib.Data.PFun

def step : Nat × List Nat → List Nat ⊕ (Nat × List Nat)
  | ⟨n, l⟩ =>
    if n == 1 then .inl (1 :: l)
    else if n % 2 == 0 then .inr (n / 2, n :: l)
    else .inr (3 * n + 1, n :: l)

def collatz : Nat →. List Nat :=
  fun n ↦ (PFun.fix (.lift step) ⟨n, []⟩).map List.reverse

lemma PFun.mem_fix_iff' {α β : Type*} {f : α →. β ⊕ α} {a : α} {b : β} :
    b ∈ f.fix a ↔ ∃ (l : List α),
      l.Chain (fun a a' ↦ .inr a' ∈ f a) a ∧ .inl b ∈ f ((a :: l).getLast (by simp)) := by
  constructor
  · intro h
    refine PFun.fixInduction' h (fun a h ↦ ⟨[], .nil, h⟩) ?_
    rintro a a' - ha ⟨l, hl, hb⟩
    use a' :: l
    rw [List.chain_cons]
    exact ⟨⟨ha, hl⟩, hb⟩
  · rintro ⟨l, hl, hb⟩
    induction l generalizing a with
    | nil => exact PFun.fix_stop hb
    | cons a' l ih =>
      rw [List.chain_cons] at hl
      rw [PFun.fix_fwd_eq hl.1]
      exact ih hl.2 hb

lemma PFun.fix_dom_iff {α β : Type*} {f : α →. β ⊕ α} {a : α} :
    (f.fix a).Dom ↔ ∃ (l : List α) (b : β),
      l.Chain (fun a a' ↦ .inr a' ∈ f a) a ∧ .inl b ∈ f ((a :: l).getLast (by simp)) := by
  simp_rw [Part.dom_iff_mem, PFun.mem_fix_iff']
  exact exists_comm

def collatz_3_dom : (collatz 3).Dom := by
  unfold collatz
  simp only [PFun.dom_mk, Part.map_Dom, setOf]
  rw [PFun.fix_dom_iff]
  use [(10, [3]), (5, [10, 3]), (16, [5, 10, 3]), (8, [16, 5, 10, 3]), (4, [8, 16, 5, 10, 3]), (2, [4, 8, 16, 5, 10, 3]), (1, [2, 4, 8, 16, 5, 10, 3])], [1, 2, 4, 8, 16, 5, 10, 3]
  simp; decide

def collatz_3 : [3, 10, 5, 16, 8, 4, 2, 1] ∈ collatz 3 := by
  unfold collatz
  simp
  rw [PFun.mem_fix_iff']
  use [(10, [3]), (5, [10, 3]), (16, [5, 10, 3]), (8, [16, 5, 10, 3]), (4, [8, 16, 5, 10, 3]), (2, [4, 8, 16, 5, 10, 3]), (1, [2, 4, 8, 16, 5, 10, 3])]
  simp; decide

#eval collatz.fn 3 collatz_3_dom -- [3, 10, 5, 16, 8, 4, 2, 1]

[Yuyang Zhao]

Maybe there should be some way to make functions easier to define and rewrite.

[Yuyang Zhao]

and a tactic to prove termination and evaluation.

[Eric Wieser]

PFun presumably doesn't let you prove something about the start of the sequence without first claiming it terminates, unlike LazyLizt