Partial correctness of partial functions

Stream: lean4

[Rish Vaishnav]

Partial functions in Lean are marked as opaque, so you can't prove any properties on their output (when they do happen to terminate). The new partial_fixpoint annotation lets you work around this when you are working with certain result types by reinterpreting the partial function as a fixpoint of the function with abstracted recursive calls. That lets you do some reasoning about the function's output without having to prove termination, using the autogenerated partial_correctness theorems.

I was wondering to what extent the machinery developed for partial_fixpoint could be adapted to generate partial_correctness theorems for all partial functions, even if we have no way of computing their fixpoint, in which case perhaps we could postulate the existence of a fixpoint as a hypothesis of the partial correctess theorem.

For example, suppose we make the List.findIndex function an actual partial function:

partial def List.findIndex? (xs : List α) (p : α → Bool) : Option Nat := do
  match xs with
  | [] => none
  | x::ys => do
    if p x then
      pure 0
    else
      let r ← List.findIndex? ys p
      pure (r + 1)
-- partial_fixpoint

#eval List.findIndex? ["a", "b", "c"] fun s => s == "b"
-- some 1

We could then perhaps generate a "fixpoint mapping" function that looks like this:

def List.findIndex?_fmap
   (f : (xs : List α) → (p : α → Bool) → Option Nat)
   (xs : List α) (p : α → Bool) : Option Nat := do
  match xs with
  | [] => none
  | x::ys =>
    if p x then
      pure 0
    else
      let r ← f ys p
      pure (r + 1)

along with a partial correctness theorem like this (note the new hf hypothesis):

def List.findIndex?_fmap.partial_correctness
  (motive : List α → (α → Bool) → Option Nat → Prop)
  (hf : ∃ f, List.findIndex?_fmap f = f)
  (h :
    ∀ (f : List α → (α → Bool) → Option Nat),
      (∀ (xs : List α) (p : α → Bool) (r : Option Nat), f xs p = r → motive xs p r) →
        ∀ (xs : List α) (p : α → Bool) (s : Unit) (r : Option Nat),
          List.findIndex?_fmap f xs p = r →
            motive xs p r)
  (xs : List α) (p : α → Bool) (r : Option Nat)
  : hf.choose xs p = r → motive xs p r := sorry

Would such a theorem be provable for partial functions in general? Even if not, I think it still would be quite convenient to be able to generate the theorem statements (perhaps on command), allowing you to get started on a partial correctness proof of a certain function without having to worry about first showing that it terminates, the proof of which might be much more difficult than a proof of partial correctness (if the function even is terminating in the first place). For instance, I was able to use such a theorem to prove the correctness of a monadic version of findIndex, and I would like to use simlar theorems for reasoning about other partial functions, but of course it would be much nicer if they could be automatically generated for me.

[Rish Vaishnav]

@Sebastian Graf gave me a pretty good idea here. If we do want to use this partial correctness function to also show the correctness of a provably terminating function corresponding to the partial function, we'd probably want to reframe it to not use the existential hypothesis, instead explicitly taking the fixpoint and fixpoint equality proofs as separate arguments:

def List.findIndex?_fmap.partial_correctness
  (motive : List α → (α → Bool) → Option Nat → Prop)
  (f : List α → (α → Bool) → Option Nat)
  (hf : List.findIndex?_fmap f = f)
  (h :
    ∀ (f : List α → (α → Bool) → Option Nat),
      (∀ (xs : List α) (p : α → Bool) (r : Option Nat), f xs p = r → motive xs p r) →
        ∀ (xs : List α) (p : α → Bool) (s : Unit) (r : Option Nat),
          List.findIndex?_fmap f xs p = r →
            motive xs p r)
  (xs : List α) (p : α → Bool) (r : Option Nat) : f xs p = r → motive xs p r := sorry

Now, if we have a provably terminating version of the function:

def List.findIndexT? (xs : List α) (p : α → Bool) : Option Nat := do
  match xs with
  | [] => none
  | x::ys => do
    if p x then
      pure 0
    else
      let r ← List.findIndexT? ys p
      pure (r + 1)

we can prove it equal to the fixpoint application by roughly following the code structure (this may not be the most concise proof):

theorem List.findIndexT?_eq_fmap :
  List.findIndex?_fmap (α := α) List.findIndexT? = List.findIndexT? := by
  ext xs p
  refine match xs with
  | [] => by rfl
  | x::ys =>
    if h : p x then
      by
        unfold findIndex?_fmap
        simp [h]
        unfold findIndexT?
        simp [h]
    else
      by
        unfold findIndex?_fmap
        simp [h]
        conv =>
          rhs
          unfold findIndexT?
          simp [h]

and then use this in our final proof of correctness:

-- main proof
def List.findIndex?_prf
  (f : List α → (α → Bool) → Option Nat)
  (xs : List α) (p : α → Bool) (r : Option Nat)
  (ih : ∀ (xs : List α) (p : α → Bool) (r : Option Nat),
    f xs p = r →
    match r with
    | some i => ∃ x, xs[i]? = some x ∧ p x = true
    | x => ∀ (i : Nat) (x : α), xs[i]? = some x → ¬p x = true)
  :
    if let some i := List.findIndex?_fmap f xs p then
      ∃x, xs[i]? = some x ∧ p x
    else
      ∀ (i : Nat) x, xs[i]? = some x → ¬ (p x) := by
  sorry

theorem List.findIndex?_fmap_implies_pred
  (f : List α → (α → Bool) → Option Nat)
  (hf : List.findIndex?_fmap f = f)
  (xs : List α) (p : α → Bool) :
  f xs p = r →
  if let some i := r then
    ∃x, xs[i]? = some x ∧ p x
  else
    ∀ (i : Nat) x, xs[i]? = some x → ¬ (p x)
  := by
    refine List.findIndex?_fmap.partial_correctness (fun xs p r =>
      if let some i := r then
        ∃x, xs[i]? = some x ∧ p x
      else
        ∀ (i : Nat) x, xs[i]? = some x → ¬ (p x)
      ) f hf (fun f ih => ?_) xs p r
    intros xs p s r h
    subst r
    exact List.findIndex?_prf f xs p r ih

theorem List.findIndexT?_implies_pred
  (xs : List α) (p : α → Bool) :
  (findIndexT? xs p) = r →
  if let some i := r then
    ∃x, xs[i]? = some x ∧ p x
  else
    ∀ (i : Nat) x, xs[i]? = some x → ¬ (p x)
  := List.findIndex?_fmap_implies_pred List.findIndexT? List.findIndexT?_eq_fmap xs p

The benefit here is that in our main proof List.findIndex?_prf, we've abstracted away the low-level details of termination, such as whether we use structural or well-founded recursion, making for a proof state that should be simpler to work with.

So I guess the things to do here would be to:

1. Find a way to autogenerate partial_correctness theorems like the one above for all partial functions, where we hypothesize the existence of a fixpoint.
2. Auto-generate fixpoint equality proofs like List.findIndexT?_eq_fmap above after we prove the termination of a (previously partial) function, recovering the original partial function in the process to generate the _fmap function (in which we can also try to erase any details that are specific to termination).
3. Also generate some of the scaffolding above (from List.findIndexT?_implies_pred and List.findIndex?_fmap_implies_pred) so that we can focus on the main details of the proof in List.findIndex?_prf.

[Rish Vaishnav]

Having thought about this a bit more, I suppose that the answer to the question of whether we can generate partial_correctness lemmas for all partial functions is no, because that would be pretty similar to assuming something like this, which you can use to prove False:

axiom fixpoint_rec (F : α → α) (f : α) (hf : F f = f) (motive : α → Prop)
  (ih : ∀ (g : α), motive g → motive (F g)) : motive f
example : False := by
  refine fixpoint_rec (fun x => x) 0 rfl (fun _ => False) fun _ h => h

You really need to have more assumptions in the lemma, like a CCPO instance for the output type, amissibility of the motive and monotonicity of the functorial. I suppose an interesting question, however, is whether these requirements may be able to be relaxed at all if we just want to reason about the behavior of a hypothetical fixpoint, rather than a concrete one computed by Lean.Order.fix. Could we extend it to stateful and exception-throwing monads, perhaps? The following fails the monotonicity check, for example:

def List.findIndex! (xs : List α) (p : α → Bool) : EStateM Unit Unit Nat := do
  match xs with
  | [] => throw ()
  | x::ys => do
    if p x then
      pure 0
    else
      let r ← List.findIndex! ys p -- error
      pure (r + 1)
partial_fixpoint

But I wonder if a partial_correctness lemma like this would still be provable:

def List.findIndex!_fmap
  (f : (xs : List α) → (p : α → Bool) → EStateM Unit Unit Nat)
  (xs : List α) (p : α → Bool) : EStateM Unit Unit Nat := do
  match xs with
  | [] => throw ()
  | x::ys =>
    if p x then
      pure 0
    else
      let r ← f ys p
      pure (r + 1)

def List.findIndex!_fmap.partial_correctness (motive : List α → (α → Bool) → Unit → _ → Prop)
  (f : List α → (α → Bool) → EStateM Unit Unit Nat)
  (hf : List.findIndex!_fmap f = f)
  (h :
    ∀ (f : List α → (α → Bool) → EStateM Unit Unit Nat),
      (∀ (xs : List α) (p : α → Bool) (s : Unit) (r : _), (f xs p).run s = r → motive xs p s r) →
        ∀ (xs : List α) (p : α → Bool) (s : Unit) (r : _),
          (List.findIndex!_fmap f xs p).run s = r →
            motive xs p s r)
  (xs : List α) (p : α → Bool) (s : Unit) (r : _) : (f xs p).run s = r → motive xs p s r := sorry

Or if not, whether assuming it actually leads to soundness issues like we had with fixpoint_rec above.

[Sebastian Graf]

One problem with piggy-backing on the Option result type of findIndex? to generate the partial correctness theorem is that you will not be able to prove anything about the circumstances under which findIndex? returns none. IIRC, since the motive must be admissible for proof by fixpoint induction, the motive must return True for none.

Perhaps you like my answer here? #lean4 > Extrinsic termination proofs for well-founded recursion @ 💬

[Rish Vaishnav]

Hmm, my first idea to get around this was to have the function return an Option (Option A) rather than just an Option A so that we could separate the return value indications of possible non-termination (return value of none) from failure (return value of some none), but this doesn't pass the monotonicity check:

def List.findIndex? (xs : List α) (p : α → Bool) : OptionT (OptionT Id) Nat := do
  match xs with
  | [] => some none
  | x::ys => do
    if p x then
      pure 0
    else
      let r ← List.findIndex? ys p -- error
      pure (r + 1)
partial_fixpoint

However, it seems to me that this may be tied to the fact that I use OptionT instead of Option so that the do notation works as we expect. Perhaps this is something that could work in principle, however?

But anyways, this was also part of what I was trying to address with all of this. We ideally wouldn't want the return value semantics to be conflated with non-termination. You'll notice in my partial_correctness axioms I don't have any requirements on the shape of the return value of the fixpoint. My hope is that this becomes possible when we reason about an abstract fixpoint function, rather than one that was actually computed by Lean.Order.fix.