reasoning about the outcome of `partial_fixpoint`

Stream: Program verification

[Jonathan Protzenko]

@Son Ho @Josh Clune @Michael Naehrig and I are looking at partial_fixpoint... does partial_fixpoint expose an induction principle that would allow reasoning about the terminating case without necessarily proving properties about the divergent case? we can provide a minimal example if that helps... @Joachim Breitner pinging you as the author of partial_fixpoint

[Robin Arnez]

I don't think there's anything builtin but you can pretty easily make your own inductive predicate to prove things with:

def myFn (a b : Int) : Int :=
  if a = 0 then b
  else myFn (a - 2) (b + 1)
partial_fixpoint

inductive myFn.dom : (a b : Int) → Prop where
  | case1 (a b : Int) : a = 0 → myFn.dom a b
  | case2 (a b : Int) : a ≠ 0 → myFn.dom (a - 2) (b + 1) → myFn.dom a b

theorem myFn.dom_two_mul_natCast {a : Nat} {b : Int} : myFn.dom (2 * a) b := by
  induction a generalizing b with
  | zero => apply myFn.dom.case1; rfl
  | succ k ih =>
    apply myFn.dom.case2
    · omega
    · simpa [Int.mul_add] using ih

theorem le_myFn (h : myFn.dom a b) : b ≤ myFn a b := by
  induction h with
  | case1 a b h => simp [h, myFn]
  | case2 a b h h' ih =>
    rw [myFn, if_neg h]
    exact Int.le_of_lt ih

example {a : Nat} {b : Int} : b ≤ myFn (2 * a) b := le_myFn myFn.dom_two_mul_natCast

[Aaron Liu]

If you use a monad you also get a partial correctness theorem:

def myFn (a b : Int) : Option Int :=
  if a = 0 then some b
  else myFn (a - 2) (b + 1)
partial_fixpoint

#check myFn.partial_correctness

[Aaron Liu]

After staring at the type of myFn.partial_correctness for a while, this looks like it might be what you want.

[Son Ho]

Aaron Liu said:

After staring at the type of myFn.partial_correctness for a while, this looks like it might be what you want.

Yes, this looks exactly like what we need, thanks!
Here is a minimal example:

import Lean

/- `flip` models a random tape -/
def flipCoin (flip : Nat → Bool) (i : Nat) : Option Nat :=
  if flip i then some i
  else flipCoin flip (i + 2)
partial_fixpoint

theorem flipCoin_thm (flip : Nat → Bool) (i : Nat) :
  flipCoin flip 0 = some i → flip i := by
  apply flipCoin.partial_correctness flip (fun _ r => flip r)
  intros flipCoin' hi i r
  split
  . intro; simp_all
  . apply hi

[Joachim Breitner]

I think the hive mind answered the questions already, but I don’t want to appear as if I'm not taking care of my users:

For every partial_fixpoint definition you get a fixpoint induction principle (.fixpoint_induct). This is likely only useful and of interest if you have defined your own CCPO (e.g. when defining probability distributions recursively)

For those partial_fixpoint definitions that produce an Option you get a partial_correctness theorem (derived from the fixpoint_induct theorem). It allows you to prove statements of the form “if the function, given arguments x, y… returns successfully with result r , then some predicate holds for x,y,z.

(This could be generalized to other result types possibly, let me know if you run into this.)

def myFn (a b : Int) : Option Int :=
  if a = 0 then some b
  else myFn (a - 2) (b + 1)
partial_fixpoint

/--
info: myFn.fixpoint_induct (motive : (Int → Int → Option Int) → Prop) (adm : Lean.Order.admissible motive)
  (h :
    ∀ (myFn : Int → Int → Option Int), motive myFn → motive fun a b => if a = 0 then some b else myFn (a - 2) (b + 1)) :
  motive myFn
-/
#guard_msgs in
#check myFn.fixpoint_induct

/--
info: myFn.partial_correctness (motive : Int → Int → Int → Prop)
  (h :
    ∀ (myFn : Int → Int → Option Int),
      (∀ (a b r : Int), myFn a b = some r → motive a b r) →
        ∀ (a b r : Int), (if a = 0 then some b else myFn (a - 2) (b + 1)) = some r → motive a b r)
  (a b r✝ : Int) : myFn a b = some r✝ → motive a b r✝
-/
#guard_msgs in
#check myFn.partial_correctness

[Joachim Breitner]

And I know it’s not what people are used to yet, but the reference manual even talks about it:
https://lean-lang.org/doc/reference/latest/Definitions/Recursive-Definitions/#partial-correctness-theorem

[Michael Sammler]

This looks very cool. Where does this partial_correctness theorem come from? Is that something that the partial_fixpoint implementation hardcodes for option or can I have a custom partial_correctness theorem for my custom monad?

[Son Ho]

Joachim Breitner said:

(This could be generalized to other result types possibly, let me know if you run into this.)

I would love to be able to do this. For instance I have a type :

inductive Result a where
| ok (x : a) | fail | div

where div is the default value used for the divergent case. I would like to be able to derive a partial correctness theorem for the ok and fail cases.

[Joachim Breitner]

Michael Sammler schrieb:

This looks very cool. Where does this partial_correctness theorem come from? Is that something that the partial_fixpoint implementation hardcodes for option or can I have a custom partial_correctness theorem for my custom monad?

It's currently hardcoded

[Joachim Breitner]

Looking at https://github.com/leanprover/lean4/blob/338456e765807b088f44b1205a7743a215e331a1/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean#L304 you can try to define your Result a := Option (a + Unit) and make the CCPO instance defeq to the one from option. Maybe that's sufficient already? (Although maybe the code above needs to replace isAppOfArity with defeq checks for that to work).

[Son Ho]

It actually doesn't work because the order instance of Result is not equivalent to the order instance of Option (a + Unit) (if a computation evaluates to fail, we need to abort). But I note that the partial_correctness theorems are actually derived from the quite general fixpoint_induct theorems, which are all we need: it is enough to instantiate fixpoint_induct with the proper motive, and proving that this motive is admissible is straightforward with the following theorem (inspired by Option.admissible_eq_some) :

theorem Result.admissible_neq_div {α : Type u} (P : Prop) (r : Result α) :
  Lean.Order.admissible fun (x : Result α) => x = r → r ≠ .div → P := by
  apply Lean.Order.admissible_flatOrder; simp +contextual

In particular, I managed to wrote the following version of flipCoin which uses the Result type:

def flipCoin' (flip : Nat → Bool) (i : Nat) : Result Nat :=
  if flip i then .ok i
  else flipCoin' flip (i + 2)
partial_fixpoint

and prove the corresponding partial correctness theorem:

theorem flipCoin'.partial_correctness (flip : Nat → Bool) (motive : Nat → Result Nat → Prop)
  (h :
    ∀ (flipCoin' : Nat → Result Nat),
      (∀ (i : Nat) (r : Result Nat), flipCoin' i = r → r ≠ Result.div  → motive i r) →
        ∀ (i : Nat) (r : Result Nat),
          (if flip i = true then .ok i else flipCoin' (i + 2)) = r → r ≠ Result.div → motive i r)
  (i : Nat) (r : Result Nat) : flipCoin' flip i = r → r ≠ Result.div → motive i r

I'm going to define an attribute to automatically generate this kind of theorems for partial functions defined with the Result type, and it will be enough for my use case.

[Aaron Liu]

Son Ho said:

(if a computation evaluates to fail, we need to abort)

Does this impact the order instance?

[Aaron Liu]

which order are you thinking of?

[Son Ho]

Sorry, I was confused: it has an impact on the MonoBind instance that is required by the partial_fixpoint.

[Joachim Breitner]

Son Ho schrieb:

But I note that the partial_correctness theorems are actually derived from the quite general fixpoint_induct theorem

Yes, it’s only a thin convenience wrapper around it, so at least for advanced users (that’s you) it should be possible to use the fixpoint_induct directly. Good to know that that’s actually the case!

I’d wait wait generalizing this feature in Lean proper until we have more use cases and understand better which kind of Monads and which kind of partial correctness theorems people expect.

[Son Ho]

Joachim Breitner said:

I’d wait wait generalizing this feature in Lean proper until we have more use cases and understand better which kind of Monads and which kind of partial correctness theorems people expect.

I think having the fixpoint_induct theorem is already super nice. :)