Why can't we reason about general recursion?

Stream: Type theory

[Will Bradley]

The Lean 3 changes document says that

Finally, since we "seal" the auxiliary definition using an opaque constant, we cannot reason about partial definitions.

If we were allowed to reason about partial definitions, what unsoundness could occur? I am thinking specifically of the following example:

partial def silly n :=
  if n % 2 = 0 then n
  else silly (n + 1)

def silly' n :=
  if n % 2 = 0 then n
  else silly (n + 1)

(It seems like partial doesn't make opaque a definition that doesn't actually recurse, like example : x = 3 := rfl where partial def x := 3.) Could it be possible to, in a future version of Lean 4, prove that silly = silly'?

[Horațiu Cheval]

I think the idea behind not be able to reason about a (true) partial function is that it's definition cannot be expressed as a term in Lean's type theory, which is the basic level at which proofs happen. So even if it can be compiled and run, there is nothing to reason about, so to speak. Of course, in this example, silly is actually total, so it can be expressed in Lean's type theory,

def silly n :=
  if n % 2 = 0 then n
  else silly' (n + 1)
  termination_by n % 2

example : silly 3 = 4 := by
  simp [silly]

But what would reasoning about partial def loop (n : Nat) : Nat := loop (n + 1) look like?

[Marcus Rossel]

While I don't understand how it works, @Joachim Breitner introduced some reasoning capabilities for partial functions in the recent Lean FRO talk (starting at 34:50).

[Will Bradley]

I should've read a little further:

We are aware that proof assistants such as Isabelle provide a framework for defining partial functions that does not prevent users from proving properties about them. This kind of framework can be implemented in Lean 4. Actually, it can be implemented by users since Lean 4 is an extensible system. The developers current have no plans to implement this kind of support for Lean 4. However, we remark that users can implement it using a function that traverses the auxiliary unsafe definition generated by Lean, and produces a safe one using an approach similar to the one used in Isabelle.

@Marcus Rossel that's pretty much what I was wondering about— if there's a library function marked partial or opaque that can provably terminate (maybe with some extra hypotheses), then users are sort of locked out from showing that. I think String.splitAux used to be like that, and that's what prompted my question.

[Marcus Rossel]

Oh, well if the function provably terminates, but the library authors marked it as partial, that's just bad luck. What Joachim's work is on, is reasoning about functions which truely don't terminate on all inputs.

[Kyle Miller]

Yeah, if the function can provably terminate, then the expectation is that you don't mark it partial. That's how you ensure you can reason about the function without any unsoundness.

[Kyle Miller]

Otherwise, how would Lean know that a function like

partial def bad (b : Bool) := ¬ bad b

is or isn't something you can reason about without soundness issues?

[Kyle Miller]

Joachim's neat new feature handles a special case of partial functions where reasoning is sound.

[Kyle Miller]

(We don't need Lean to tell us this, but this example is definitely something that can't be reasoned about soundly:)

axiom bad : Bool → Bool
axiom bad.eq_1 (b : Bool) : bad b = ¬ bad b

example : False := by
  have := bad.eq_1 true
  revert this
  cases bad true <;> simp

[Kevin Buzzard]

The natural d(t) telling you how long it took for the 3n+1 problem to terminate starting at t would be another interesting example.

[Will Bradley]

@Marcus Rossel ah I see. I'm watching the video now, thanks. In the simpler case where an opaque function actually does terminate (provably), is there any way to attach a proof that it terminates, removing the opaque attribute?

[Kyle Miller]

In the Lean lingo, opaque isn't an attribute, it's a kind of constant. (The kinds of constants are axioms, definitions, theorems, opaques, quotient axioms, inductives, constructors, and recursors.) There's no mechanism to change the kind of a constant to another kind.

If you can prove an opaque function terminates, then you should make a definition instead and prove it terminates.

[Kyle Miller]

Another thing worth pointing out is that Lean doesn't work with termination proofs, so attaching a termination proof isn't something you can do exactly.

Instead, the system is that recursive definitions are "derecursified" using a couple strategies. The "derecursified" definition then goes through a process where equation lemmas are proved about it, where the equations come from the original recursive definition.

[Kyle Miller]

(Strategy 1: structural recursion, i.e. construct recursor applications. Strategy 2: well-founded recursion)

[Will Bradley]

@Kevin Buzzard Would something like this work? It's noncomputable but we can still reason about it

def collatz n :=
  if n % 2 = 0 then n / 2 else 3 * n + 1

def rpt (f: α → α) (x: α): ℕ → α
| 0 => x
| k + 1 => rpt f (f x) k

noncomputable def stoppingTime (n: ℕ): Option ℕ :=
  let p := ∃ i, rpt collatz n i = 1
  have := Classical.propDecidable -- instance for Or.by_cases'
  (Classical.em p).by_cases'
    (fun hp => some (Classical.choose hp))
    (fun _ => none)

[Kevin Buzzard]

Sure that looks mathematically correct and avoids partial but instead relies on Option which in the presence of noncomputability is very close to partial.

[Kevin Buzzard]

"if it terminates that's fine and if not then bail, and it must either terminate or not because of LEM"

[Joachim Breitner]

On lean nightly, you can use partial_fixpoint to define that Option-valued stopping time more directly, run it with #eval, and do proofs about it (although simp [stoppingTime] does not work well, as that loops, hence repeat and rw)

def collatz n :=
  if n % 2 = 0 then n / 2 else 3 * n + 1

def stoppingTime (n : Nat) : Option Nat := do
  if n = 1 then return 0 else return 1 + (← stoppingTime (collatz n))
partial_fixpoint

/--
info: stoppingTime.eq_def (n : Nat) :
  stoppingTime n =
    if n = 1 then pure 0
    else do
      let __do_lift ← stoppingTime (collatz n)
      pure (1 + __do_lift)
-/
#guard_msgs in
#check stoppingTime.eq_def

/-- info: some 6 -/
#guard_msgs in
#eval stoppingTime 10

example : stoppingTime 10 = some 6 := by
  repeat (rw [stoppingTime]; simp +arith [Option.bind_eq_some, collatz])

[Yakov Pechersky]

What does stoppingTime 0 do? :boom:

[Aaron Liu]

example : stoppingTime 0 = none := by
  apply Option.eq_none_iff_forall_not_mem.mpr
  intro a
  apply mt Option.mem_iff.mp
  intro h
  have h' := h
  rw [stoppingTime, if_neg Nat.zero_ne_one] at h'
  rw [collatz, if_pos rfl, Nat.zero_div, h] at h'
  rw [Option.bind_eq_bind, Option.some_bind] at h'
  rw [Option.pure_def, Option.some.injEq] at h'
  simp at h'

-- stack overflow
#eval stoppingTime 0

[Kyle Miller]

Here's another proof:

example : stoppingTime 0 = none := by
  cases h : stoppingTime 0
  · rfl
  · have h0 := stoppingTime.eq_1 0
    simp [collatz, h] at h0

It's a bit awkward mentioning the equation lemma directly though.

[Will Bradley]

I did this last night but didn't upload it. @Kevin Buzzard what is the problem with Option and noncomputability? Is it that Option lives in Type u?

lemma not_stops_zero: ¬(stops 0) := by
  rw [stops, not_exists]
  intro x
  induction x with
  | zero => decide
  | succ k ih => rwa [rpt, show collatz 0 = 0 by decide]

theorem stoppingTime_zero : stoppingTime 0 = none := by
  simp [stoppingTime, Or.by_cases', not_stops_zero]

[Kevin Buzzard]

Oh I don't have any problems with anything, I never use option or partial in my work, I was just observing that you used option instead of partial

[Will Bradley]

Ah ok thanks!