Using `partial_fixpoint`

Stream: lean4

[François G. Dorais]

How can I make this work?

def find (i : Nat) (p : Nat → Bool) : Nat :=
  if p i then i else find (i+1) p
partial_fixpoint

theorem find_eq_true_of_exists_ge (p : Nat → Bool) (i : Nat) (h : ∃ j ≥ i, p j) : p (find i p) = true := by
  rw [find]
  split
  · assumption
  · next hi =>
    have : ∃ j ≥ i+1, p j := by
      match h with
      | ⟨j, hj⟩ =>
        by_cases heq : i = j
        · exfalso
          apply hi
          rw [heq, hj.2]
        · exists j
          constructor
          · omega
          · exact hj.2
    exact find_eq_true_of_exists_ge p (i+1) this
partial_fixpoint -- doesn't work, what should I use?

[Kyle Miller]

I think partial_fixpoint only works if the type is inhabited, so for theorems it's not so useful

[François G. Dorais]

I understand that this is not the intended usage since find is not total but this is a natural use case, isn't it?

[François G. Dorais]

Kyle Miller said:

I think partial_fixpoint only works if the type is inhabited, so for theorems it's not so useful

Indeed, but there might be some mechanisms in place to reason about the domain of a partial_fixpoint function.

[Kyle Miller]

My understanding is that you'd need to prove the theorem first to prove that the theorem's type is inhabited, and then you'd be able to use partial_fixpoint on the theorem (defeating the purpose of trying to use partial_fixpoint in the first place). Just pointing this out given that your example ends with partial_fixpoint on a theorem.

Yes, it should be possible to reason about find.

[François G. Dorais]

Should it be? All functions are total in Lean's type theory, so perhaps Lean just assumes that find is not acceptable until I prove it is total? (It's not total, of course.)

[Kyle Miller]

Yeah, definitely provable:

def find (i : Nat) (p : Nat → Bool) : Nat :=
  if p i then i else find (i+1) p
partial_fixpoint

theorem find_eq_true_of_exists_ge (p : Nat → Bool) (i : Nat) (h : ∃ j ≥ i, p j) : p (find i p) = true := by
  obtain ⟨j, h, hpj⟩ := h
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
  clear h
  induction k generalizing i with
  | zero =>
    rw [Nat.add_zero] at hpj
    rw [find]
    simp [hpj]
  | succ k ih =>
    rw [find]
    split
    · assumption
    · apply ih
      simpa only [Nat.add_succ, Nat.succ_add] using hpj

[Kyle Miller]

You can see that the equation lemma find.eq_1 is very usable.

[François G. Dorais]

Very nice!

[François G. Dorais]

I'm still perplexed how to make sense of partial_fixpoint in Lean's type theory and things like find 0 fun _ => false being a closed term.

Note that Lean can now decide the halting problem and then some!

def find (i : Nat) (p : Nat → Bool) : Nat :=
  if p i then i else find (i+1) p
partial_fixpoint

theorem find_eq_true_of_exists_ge (p : Nat → Bool) (i : Nat) (h : ∃ j ≥ i, p j) : p (find i p) = true := by
  obtain ⟨j, h, hpj⟩ := h
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
  clear h
  induction k generalizing i with
  | zero =>
    rw [Nat.add_zero] at hpj
    rw [find]
    simp [hpj]
  | succ k ih =>
    rw [find]
    split
    · assumption
    · apply ih
      simpa only [Nat.add_succ, Nat.succ_add] using hpj

theorem find_eq_find_zero_of_forall_eq_false (hp : ∀ i, p i = false) : find i p = find 0 p := by
  induction i with
  | zero => rfl
  | succ i hi =>
    conv => rhs; rw [← hi, find]; simp [hp]

def test (p : Nat → Bool) : Bool := p (find 0 p)

theorem test_eq_true_of_exists (h : ∃ j, p j) : test p = true :=
  find_eq_true_of_exists_ge p 0 (let ⟨j, hj⟩ := h; ⟨j, Nat.zero_le _, hj⟩)

theorem test_eq_true_iff_exists : test p ↔ ∃ j, p j := by
  constructor
  · intro h
    rw [test] at h
    exists find 0 p
  · exact test_eq_true_of_exists

I can't tell whether this is neat or scary.

#print opaques find reveals the secret but that's not completely comforting either.

[James Gallicchio]

This is no worse than using Classical, though, right? Everything (including the halting problem) is already decidable in Prop.

[James Gallicchio]

And compiled Lean is only intended to have partial correctness wrt the type theory spec, e.g. panic! is non-total

[François G. Dorais]

It is using Classical.choice.

[François G. Dorais]

One danger is that one can write seemingly sensible code like this function that returns the minimum value of f : Nat → Nat:

def min (f : Nat → Nat) : Nat := f (find 0 fun i => !test fun j => f j < f i)

It's not difficult to prove that min is total and that min (fun _ => 0) = 0. One might reasonably expect that min (fun _ => 0) will return 0. However, min f never halts no matter what f is.