mvgen run rule for Option

Stream: general

[Frederick Pu]

Is there something analagous to Std.Do.Id.of_wp_run_eq for Option? ie given prog x : Option T, x = some b if |-s[[x]] (\down _ out => out = b))

[Frederick Pu]

a simple mwe of when this might be useful would be proving something like this:

theorem womp (a c : Option Nat) (b : Nat → Option Nat) (p : Nat → Prop) : (do let x ← a; some <| p (← b x)) = some True → (do let x ← a; let y ← c; some <| p (← b x)) = some True := sorry

[Frederick Pu]

without having to explicitly unfold and do casework on all of the do notation

[Sebastian Graf]

The following theorem will be part of 4.29. This is the proof for <4.29:

/--
Adequacy lemma for `Option`.
Useful if you want to prove a property about a complex expression `prog : Option α` that you have
generalized to a variable `x` and you want to use `mvcgen` to reason about `prog`.
-/
theorem Std.Do.Option.of_wp_eq {α} {x prog : Option α} (h : prog = x) (P : Option α → Prop) :
    (⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (some a)⌝, fun _ => ⌜P none⌝⟩) → P x := by
  subst h
  intro hspec
  simp only [wp, Id.run, PredTrans.pushOption_apply, PredTrans.pure_apply, SPred.entails_nil,
    SPred.down_pure] at hspec
  split at hspec <;> exact hspec True.intro

[Frederick Pu]

is 4.29 out yet?

[Frederick Pu]

oh ig not

[Frederick Pu]

also what do i do after i get here:

import Std.Tactic.Do

open Std Do
/--
Adequacy lemma for `Option`.
Useful if you want to prove a property about a complex expression `prog : Option α` that you have
generalized to a variable `x` and you want to use `mvcgen` to reason about `prog`.
-/
theorem Std.Do.Option.of_wp_eq {α} {x prog : Option α} (h : prog = x) (P : Option α → Prop) :
    (⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (some a)⌝, fun _ => ⌜P none⌝⟩) → P x := by
  subst h
  intro hspec
  simp only [wp, Id.run, PredTrans.pushOption_apply, PredTrans.pure_apply, SPred.entails_nil,
    SPred.down_pure] at hspec
  split at hspec <;> exact hspec True.intro

theorem womp (a c : Option Nat) (b : Nat → Option Nat) (p : Nat → Prop) : (do let x ← a; some <| p (← b x)) = some True → (do let x ← a; let y ← c; some <| p (← b x)) = some True := by
  intro h
  apply Option.of_wp_eq rfl (· = some True)
  /-
    a c : Option Nat
    b : Nat → Option Nat
    p : Nat → Prop
    h : (do
        let x ← a
        let __do_lift ← b x
        some (p __do_lift)) =
      some True
    ⊢ ⊢ₛ
      wp⟦do
          let x ← a
          let _ ← c
          let __do_lift ← b x
          some (p __do_lift)⟧
        (fun a => ⌜some a = some True⌝, fun x => ⌜none = some True⌝, ())
  -/

[Frederick Pu]

how do bring the lets out of the do?

[Eric Wieser]

The (h : prog = x) assumption in that theorem seems quite strange to me

[Frederick Pu]

yeah, all of the of_wp theorems do that for some reason tho

[Eric Wieser]

Also, your theorem is false, consider c = none

[Frederick Pu]

good point. the mwe should be more like :

theorem womp (a c : Option Nat) (b : Nat → Option Nat) (p : Nat → Prop) : (do let x ← a; some <| p (← b x)) = some True → c.isSome → (do let x ← a; let y ← c; some <| p (← b x)) = some True := by sorry

[Frederick Pu]

so appparently you can just do:

theorem womp (a c : Option Nat) (b : Nat → Option Nat) (p : Nat → Prop) : (do let x ← a; some <| p (← b x)) = some True → c.isSome → (do let x ← a; let y ← c; some <| p (← b x)) = some True := by
  intro h h1
  simp [Option.bind_eq_some_iff, Option.isSome_iff_exists] at *
  grind

[Sebastian Graf]

I'm not sure that mvcgen will be of much help to prove that two imperative programs ((do let x ← a; some <| p (← b x)) and (do let x ← a; let y ← c; some <| p (← b x)) are equivalent. You want a relational Hoare Logic for that; mvcgen currently supports only unary Hoare Logic. Also your proposition is about open programs without any spec attached to them.

So yes, use equational reasoning and grind.