val equiv : w1: AlgForAll.st_wp a -> w2: AlgForAll.st_wp a -> Prims.logical
let equiv #a (w1 w2 : st_wp a) = w1 `stronger` w2 /\ w2 `stronger` w1
module AlgForAll

open FStar.Calc
module FE = FStar.FunctionalExtensionality
module F = FStar.FunctionalExtensionality
module W = FStar.WellFounded
module T = FStar.Tactics.V2
module ID5 = ID5
open Alg

type rwtree a = Alg.tree a [Read; Write]
let tbind : #a:_ -> #b:_ -> rwtree a -> (a -> rwtree b) -> rwtree b = fun c f -> Alg.bind _ _ c f

let st_wp0 (a:Type) : Type = state -> (a & state -> Type0) -> Type0

let st_monotonic #a (w : st_wp0 a) : Type0 =
  //forall s0 p1 p2. (forall r. p1 r ==> p2 r) ==> w s0 p1 ==> w s0 p2
  // ^ this version seems to be less SMT-friendly
  forall s0 p1 p2. (forall x s1. p1 (x, s1) ==> p2 (x, s1)) ==> w s0 p1 ==> w s0 p2

let st_wp (a:Type) = wp:st_wp0 a{st_monotonic wp}

unfold
let return_wp #a x : st_wp a = fun s0 p -> p (x, s0)

unfold
let bind_wp #a #b (w : st_wp a) (wf : a -> st_wp b)
  : st_wp b
  = fun s0 p -> w s0 (fun (y, s1) -> wf y s1 p)

unfold
let read_wp : st_wp state = fun s0 p -> p (s0, s0)

unfold
let write_wp : state -> st_wp unit = fun s _ p -> p ((), s)

(* Also doable with handlers *)
let rec interp_as_wp #a (t : rwtree a) : st_wp a =
  match t with
  | Return x -> return_wp x
  | Op Read _ k ->
    bind_wp read_wp (fun s -> interp_as_wp (k s))
  | Op Write s k ->
    bind_wp (write_wp s) (fun (o:unit) -> interp_as_wp (k o))

(* With handlers. Can only be done into []? See the use of `run`. *)
let interp_as_wp2 #a (t : rwtree a) : Alg (st_wp a) [] =
  handle_with #a #(st_wp a) #[Read; Write] #[]
              (fun () -> Alg?.reflect t)
              (fun x -> return_wp x)
              (function Read  -> (fun i k -> bind_wp read_wp (fun s -> run (fun () -> k s)))
                      | Write -> (fun i k -> bind_wp (write_wp i) (fun _ -> run k)))

(* Bug: defining this as a FStar.Preorder.preorder
causes stupid failures ahead *)
val stronger : (#a:Type) -> st_wp a -> st_wp a -> Type0
let stronger w1 w2 = forall p s. w1 p s ==> w2 p s
/
prims.fst.checked ID5.fst.checked FStar.WellFounded.fst.checked FStar.Tactics.V2.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Pure.fst.checked FStar.FunctionalExtensionality.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked Alg.fst.checked
AlgForAll.fst
w1: AlgForAll.st_wp a -> w2: AlgForAll.st_wp a -> Prims.logical
AlgForAll.st_wp Prims.l_and AlgForAll.stronger Prims.logical
let equiv #a (w1: st_wp a) (w2: st_wp a) =
  
w1 `stronger` w2 /\ w2 `stronger` w1