Proving Option monad programs with Std.Do

Stream: Program verification

[Zheyuan Wu]

Hey! Has anyone tried proving programs in the Option monad?
I’m trying out Std.Do, code works nicely with Id(thanks to Markus Himmel’s blog). Now I’m trying to verify something similar but with Option eg:

def list_max (l : List ℕ) : Option ℕ := do
  let mut max_num ← l.head?
  for x in l do
    max_num := max x max_num
  some max_num

If not, would it be reasonable and doable to extend the rules myself, following the existing WP pattern?

[Bhavik Mehta]

def pushOption (x : Option β) : PredTrans (PostShape.except PUnit PostShape.pure) β where
  apply a := x.elim (a.2.1 ⟨⟩) a.1
  conjunctive := by
    simp [PredTrans.Conjunctive, Assertion, SPred, SVal, FailConds]
    grind [cases Option]

instance : WP Option (PostShape.except PUnit PostShape.pure) where
  wp := pushOption

[Bhavik Mehta]

Here are the wp lemmas for that instance:

@[simp]
theorem wp_none : wp⟦none : Option α⟧ Q = Q.2.1 () := rfl

@[simp]
theorem wp_some {x} : wp⟦some x : Option α⟧ Q = Q.1 x := rfl

[Bhavik Mehta]

I wrote these back in July with a similar aim as you, so sharing them here to save you the time :) (but while they compiled in July, I haven't checked that they compile now!)

[Sebastian Graf]

I recently added the instances for Option and OptionT: lean4#9932 They will be part of the next RC.