proposition: Lemma iappend_correct m l1 l2 : crun (do p : rlist nat ml_int * rlist nat ml_int <- m; let (rl1, rl2) := p in do a <- is_int_list l1 rl1; do b <- is_int_list l2 rl2; do rs1 <- loc_ids_rlist l1 rl1; do rs2 <- loc_ids_rlist l2 rl2; Ret (a && b && (allrel (fun r1 r2 => r1 != r2) rs1 rs2))) = Some true-> crun (do p : rlist nat ml_int * rlist nat ml_int <- m; let (rl1, rl2) := p in do rl <- iappend (size l1).+1 rl1 rl2; is_int_list (l1 ++ l2) rl) = Some true.
proof: Proof. Abort. End cyclic. Module eval_cyclic. Section eval. Import monad_model.ModelTypedStore. Definition M := [the typedStoreMonad idfun of @acto ml_type idfun]. Definition Env := Env ml_type idfun. Definition empty_env : Env := [::]. Definition W (A : UU0) : UU0 := monad_model.option_monad (A * Env). Definition Restart [A B] (r : W A) (f : M B) : W B := if r is inr (_, env) then f env else inl tt. Definition FromW [A] (r : W A) : M A := fun env => if r is inr (a, _) then inr (a, env) else inl tt. Definition it0 : W unit := inr (tt, empty_env). Local Open Scope do_notation. Local Notation mkloc := (mkloc (locT:=monad_model.locT_nat)). Local Notation coq_type := (coq_type _). Definition incr (l : loc ml_int) : M nat := do x <- cget l; do _ <- cput l (succn x); Ret (succn x). Definition l : W (loc ml_int) := Restart it0 (cnew ml_int 3). Eval vm_compute in l. Definition it1 := Restart l (do l <- FromW l; incr l). Eval vm_compute in it1. Definition it2 := Restart it1 (do l <- FromW l; incr l). Eval vm_compute in it2. Local Notation cycle := (cycle idfun M). Local Notation rhd := (rhd idfun M). Local Notation rtl := (rtl idfun M). Definition it3 := Restart it2 (cycle ml_bool true false). Eval vm_compute in crun (FromW it3). Definition it4 := Restart it3 (do l <- FromW it3; Ret (rhd ml_bool false l)). Definition it5 := Restart it4 (do l0 <- FromW it3; do l1 <- rtl _ l0; do l2 <- rtl _ l1; Ret (rhd ml_bool false l2)). End eval. End eval_cyclic. Section factorial. Variable (N : monad) (M : typedStoreMonad N). Fixpoint fact_ref (r : loc ml_int) (n : nat) : M unit := if n is m.+1 then cget r >>= fun p => cput r (n * p) >> fact_ref r m else skip. Theorem fact_ref_ok n : crun (cnew ml_int 1 >>= fun r => fact_ref r n >> cget r) = Some (fact_rec n). Proof. set fn := fact_rec n. set m := n. set s := 1. have smn : s * fact_rec m = fn by rewrite mul1n. elim: m s smn => [|m IH] s /= smn. rewrite /fact_ref -smn muln1. under eq_bind do rewrite bindskipf. by rewrite cnewgetret crunret // crunnew0. under eq_bind do rewrite bindA. rewrite cnewget. under eq_bind do rewrite bindA. by rewrite cnewput IH // (mulnC m.+1) -mulnA. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib