diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 30e53157..07d18eb4 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,7 +17,9 @@ jobs: strategy: matrix: image: + - 'mathcomp/mathcomp:1.16.0-coq-8.16' - 'mathcomp/mathcomp:1.16.0-coq-8.17' + - 'mathcomp/mathcomp:1.17.0-coq-8.16' - 'mathcomp/mathcomp:1.17.0-coq-8.17' fail-fast: false steps: diff --git a/README.md b/README.md index 1e56bce3..826eaca2 100644 --- a/README.md +++ b/README.md @@ -26,7 +26,7 @@ in several examples of monadic equational reasoning. - Celestine Sauvage - Kazunari Tanaka - License: [LGPL-2.1-or-later](LICENSE) -- Compatible Coq versions: Coq 8.17 +- Compatible Coq versions: Coq 8.16-8.17 - Additional dependencies: - [MathComp ssreflect](https://math-comp.github.io) - [MathComp fingroup](https://math-comp.github.io) diff --git a/_CoqProject b/_CoqProject index 66bb9250..a541dec3 100644 --- a/_CoqProject +++ b/_CoqProject @@ -13,6 +13,7 @@ state_lib.v array_lib.v trace_lib.v proba_lib.v +typed_store_lib.v monad_composition.v monad_model.v proba_monad_model.v @@ -20,12 +21,14 @@ category.v gcm_model.v altprob_model.v monad_transformer.v +typed_store_model.v example_spark.v example_nqueens.v example_relabeling.v example_quicksort.v example_iquicksort.v example_monty.v +example_typed_store.v smallstep.v example_transformer.v category_ext.v diff --git a/coq-monae.opam b/coq-monae.opam index 202e1a6d..3b86d8b9 100644 --- a/coq-monae.opam +++ b/coq-monae.opam @@ -15,10 +15,10 @@ description: """ This Coq library contains a hierarchy of monads with their laws used in several examples of monadic equational reasoning.""" -build: [make "-j%{jobs}%" ] +build: [make "-j%{jobs}%"] install: [make "install_full"] depends: [ - "coq" { (>= "8.17" & < "8.18~") | (= "dev") } + "coq" { (>= "8.16" & < "8.18~") | (= "dev") } "coq-mathcomp-ssreflect" { (>= "1.16.0" & < "1.18~") | (= "dev") } "coq-mathcomp-fingroup" { (>= "1.16.0" & < "1.18~") | (= "dev") } "coq-mathcomp-algebra" { (>= "1.16.0" & < "1.18~") | (= "dev") } diff --git a/example_typed_store.v b/example_typed_store.v new file mode 100644 index 00000000..ae8a0514 --- /dev/null +++ b/example_typed_store.v @@ -0,0 +1,543 @@ +(* monae: Monadic equational reasoning in Coq *) +(* Copyright (C) 2023 monae authors, license: LGPL-2.1-or-later *) +Require Import ZArith. +From mathcomp Require Import all_ssreflect. +From mathcomp Require boolp. +From infotheo Require Import ssrZ. +Require monad_model. +Require Import monae_lib hierarchy monad_lib typed_store_lib. + +(******************************************************************************) +(* Typed store examples *) +(* *) +(* Inductive ml_type == generated by coqgen *) +(* *) +(* Module MLTypesNat *) +(* coq_type_nat == adapted from code generated by coqgen *) +(* coq_type_nat0 == coq_type_nat with identity monad *) +(* Definition cycle *) +(* Fixpoint fact_ref *) +(* Definition fact_for *) +(* Fixpoint fibo_ref *) +(* *) +(* Module MLtypes63 *) +(* Fixpoint coq_type63 == generated type translation function *) +(* Definition fact_for63 *) +(******************************************************************************) + +Local Open Scope monae_scope. + +(******************************************************************************) +(* generated by coqgen *) +(******************************************************************************) +Module MLTypes. +Inductive ml_type : Set := + | ml_int + | ml_bool + | ml_unit + | ml_ref (_ : ml_type) + | ml_arrow (_ : ml_type) (_ : ml_type) + | ml_rlist (_ : ml_type). + +Definition ml_type_eq_dec (T1 T2 : ml_type) : {T1=T2}+{T1<>T2}. +revert T2; induction T1; destruct T2; + try (right; intro; discriminate); try (now left); + try (case (IHT1_5 T2_5); [|right; injection; intros; contradiction]); + try (case (IHT1_4 T2_4); [|right; injection; intros; contradiction]); + try (case (IHT1_3 T2_3); [|right; injection; intros; contradiction]); + try (case (IHT1_2 T2_2); [|right; injection; intros; contradiction]); + (case (IHT1 T2) || case (IHT1_1 T2_1)); try (left; now subst); + right; injection; intros; contradiction. +Defined. + +Definition val_nonempty (M : UU0 -> UU0) := tt. + +Definition locT := [eqType of nat]. + +Notation loc := (@loc _ locT). + +Inductive rlist (a : Type) (a_1 : ml_type) := + | Nil + | Cons (_ : a) (_ : loc (ml_rlist a_1)). + +Definition ml_type_eq_mixin := comparableMixin MLTypes.ml_type_eq_dec. +Canonical ml_type_eqType := Eval hnf in EqType _ ml_type_eq_mixin. + +End MLTypes. +(******************************************************************************) + +Module MLTypesNat. +Import MLTypes. + +Section with_monad. +Context [M : Type -> Type]. + +Fixpoint coq_type_nat (T : ml_type) : Type := + match T with + | ml_int => nat + | ml_bool => bool + | ml_unit => unit + | ml_arrow T1 T2 => coq_type_nat T1 -> M (coq_type_nat T2) + | ml_ref T1 => loc T1 + | ml_rlist T1 => rlist (coq_type_nat T1) T1 + end. +End with_monad. + +(* use coq_type_nat (typed_store_model.v) *) +Canonical MLU := @Build_ML_universe _ coq_type_nat ml_unit val_nonempty. + +(* alternative: use coq_type_nat0 (monad_model.v) *) +(* +Definition coq_type_nat0 := @coq_type_nat idfun. +Canonical MLU := @monad_model.MLU _ coq_type_nat0 ml_unit (val_nonempty idfun). +*) + +Section cyclic. +Variables (M : typedStoreMonad MLU MLTypes.locT). +Local Notation coq_type := (hierarchy.coq_type (MonadTypedStore.sort M)). +Local Open Scope do_notation. + +Definition cycle (T : ml_type) (a b : coq_type T) + : M (coq_type (ml_rlist T)) := + do r <- cnew (ml_rlist T) (Nil (coq_type T) T); + do l <- + (do v <- cnew (ml_rlist T) (Cons (coq_type T) T b r); + Ret (Cons (coq_type T) T a v)); + do _ <- cput r l; Ret l. + +Definition hd (T : ml_type) (def : coq_type T) + (param : coq_type (ml_rlist T)) : coq_type T := + match param with | Nil => def | Cons a _ => a end. + +Lemma hd_is_true : + crun (do l <- cycle ml_bool true false; Ret (hd ml_bool false l)) = Some true. +Proof. +rewrite bindA. +under eq_bind => tl. + rewrite !bindA. + under eq_bind do rewrite !bindA bindretf !bindA bindretf /=. + rewrite -bindA. + over. +rewrite -bindA crunret // -bindA_uncurry /= crungetput // bindA. +under eq_bind => tl. + rewrite !bindA. + under eq_bind do rewrite bindretf /=. + over. +by rewrite crungetnew // -(bindskipf (_ >>= _)) crunnewget // crunskip. +Qed. +End cyclic. + +Section factorial. +Variable M : typedStoreMonad MLU MLTypes.locT. +Notation coq_type := (@coq_type M). + +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. +End factorial. + +Section fact_for. +Variable M : typedStoreMonad MLU MLTypes.locT. +Local Notation coq_type := (hierarchy.coq_type (MonadTypedStore.sort M)). +Local Open Scope do_notation. + +Definition fact_for (n : coq_type ml_int) : M (coq_type ml_int) := + do v <- cnew ml_int 1; + do _ <- + (do u <- Ret 1; + do v_1 <- Ret n; + forloop u v_1 + (fun i => + do v_1 <- (do v_1 <- cget v; Ret (v_1 * i)); + cput v v_1)); + cget v. + +Theorem fact_for_ok n : crun (fact_for n) = Some (fact_rec n). +Proof. +rewrite /fact_for. +under eq_bind do rewrite !bindA !bindretf. +transitivity (crun (cnew ml_int (fact_rec n) >> Ret (fact_rec n) : M _)); + last by rewrite crunret // crunnew0. +congr crun. +rewrite -{1}/(fact_rec 0). +pose m := n. +have -> : 0 = n - m by rewrite subnn. +have : m <= n by []. +elim: m => [|m IH] mn. + rewrite subn0. + under eq_bind do rewrite forloop0 ?leqnn // bindretf -cgetret. + by rewrite cnewget. +rewrite subnSK //. +under eq_bind do (rewrite forloopS; last by apply leq_subr). +under eq_bind do rewrite !bindA. +rewrite cnewget. +under eq_bind do rewrite bindretf. +rewrite cnewput -IH; last by apply ltnW. +by rewrite subnS mulnC -(@prednK (n-m)) // lt0n subn_eq0 -ltnNge. +Qed. +End fact_for. + +Section fibonacci. +Variable M : typedStoreMonad MLU MLTypes.locT. +Local Notation coq_type := (hierarchy.coq_type (MonadTypedStore.sort M)). + +Fixpoint fibo_rec n := + if n is m.+1 then + if m is k.+1 then fibo_rec k + fibo_rec m else 1 + else 1. + +Fixpoint fibo_ref n (a b : loc ml_int) : M unit := + if n is n.+1 then + cget a >>= (fun x => cget b >>= fun y => cput a y >> cput b (x + y)) + >> fibo_ref n a b + else skip. + +Theorem fibo_ref_ok n : + crun (cnew ml_int 1 >>= + (fun a => cnew ml_int 1 >>= fun b => fibo_ref n a b >> cget a)) + = Some (fibo_rec n). +Proof. +set x := 1. +pose y := x. +rewrite -{2}/y. +pose i := n. +rewrite -[in LHS]/i. +have : (x, y) = (fibo_rec (n - i), fibo_rec (n.+1 - i)). + by rewrite subnn -addn1 addKn. +have : i <= n by []. +elim: i x y => [|i IH] x y Hi. + rewrite !subn0 => -[-> ->]. + rewrite -/(fibo_rec n.+1). + under eq_bind do under eq_bind do rewrite /= bindskipf. + rewrite -cnewchk. + under eq_bind do rewrite -cgetret cchknewget. + by rewrite cnewget -bindA crunret // crunnew // crunnew0. +rewrite subSS => -[] Hx Hy. +rewrite -(IH y (x + y) (ltnW Hi)); last first. + rewrite {}Hx {}Hy; congr pair. + rewrite subSn 1?ltnW//. + case: n {IH} => // n in Hi *. + by rewrite [in RHS]subSn -1?ltnS// subSS subSn -1?ltnS. +rewrite /=. +under eq_bind do under eq_bind do rewrite !bindA. +rewrite -cnewchk. +under eq_bind do rewrite cchknewget. +rewrite cnewget. +under eq_bind do under eq_bind do rewrite !bindA. +under eq_bind do rewrite cnewget. +under eq_bind do under eq_bind do rewrite !bindA. +rewrite -[in LHS]cnewchk. +under eq_bind do rewrite cchknewput. +rewrite cnewput. +by under eq_bind do rewrite cnewput. +Qed. +End fibonacci. + +End MLTypesNat. + +Require Import PrimInt63. +Require Sint63. + +Section Int63. +Definition uint2N (n : int) : nat := + if Uint63.to_Z n is Zpos pos then Pos.to_nat pos else 0. +Definition N2int n := Uint63.of_Z (Z.of_nat n). + +Lemma ltsbNlesb m n : ltsb m n = ~~ lesb n m. +Proof. +case/boolP: (lesb n m) => /Sint63.lebP nm; apply/Sint63.ltbP => /=; + by [apply Z.le_ngt | apply Z.nle_gt]. +Qed. + +Lemma ltsbW m n : ltsb m n -> lesb m n. +Proof. move/Sint63.ltbP/Z.lt_le_incl => mn; by apply/Sint63.lebP. Qed. + +Lemma lesb_ltsbS_eq m n : lesb m n -> ltsb n (Uint63.succ m) -> m = n. +Proof. +move/Sint63.lebP => mn /Sint63.ltbP nSm. +move: (nSm). +rewrite Sint63.succ_of_Z -Sint63.is_int; last first. + split. + apply Z.le_le_succ_r. + by case: (Sint63.to_Z_bounded m). + apply Zlt_le_succ, (Z.le_lt_trans _ _ _ mn), (Z.lt_le_trans _ _ _ nSm). + by case: (Sint63.to_Z_bounded (Uint63.succ m)). +move/Zlt_le_succ/Zsucc_le_reg => nm. +by apply Sint63.to_Z_inj, Zle_antisym. +Qed. + +(* The opposite is not true ! (n = max_int) *) +Lemma ltsbS_lesb m n : ltsb m (Uint63.succ n) -> lesb m n. +Proof. +rewrite -[lesb _ _]negbK -ltsbNlesb => nSm; apply/negP => /[dup] /ltsbW nm. +by rewrite (lesb_ltsbS_eq n m) // => /Sint63.ltbP /Z.lt_irrefl. +Qed. + +Lemma uint63_min n : (0 <= Uint63.to_Z n)%Z. +Proof. by case: (Uint63.to_Z_bounded n). Qed. + +Lemma uint63_max n : (Uint63.to_Z n < Uint63.wB)%Z. +Proof. by case: (Uint63.to_Z_bounded n). Qed. + +Lemma uint2N_pred n : n <> 0%int63 -> uint2N n = (uint2N (Uint63.pred n)).+1. +Proof. +move=> Hn. +rewrite /uint2N Uint63.pred_spec. +case HnZ: (Uint63.to_Z n) => [|m|m]. +- rewrite (_ : 0 = Uint63.to_Z 0)%Z // in HnZ. + move/Uint63.to_Z_inj in HnZ. + by elim Hn. +- have Hm1 : (0 <= Z.pos m - 1 < Uint63.wB)%Z. + split. by apply leZsub1, Pos2Z.is_pos. + apply (Z.lt_trans _ (Z.pos m)). + by apply leZsub1, Z.le_refl. + rewrite -HnZ; by apply uint63_max. + rewrite Zmod_small //. + case HmZ: (Z.pos m - 1)%Z => [|p|p]. + + by move/Z.sub_move_r: HmZ => /= [] ->. + + apply Nat2Z.inj => /=. + rewrite positive_nat_Z Pos2SuccNat.id_succ Pos2Z.inj_succ -HmZ. + by rewrite (Z.succ_pred (Z.pos m)). + + by destruct m. +- move: (uint63_min n). + rewrite HnZ => /Zle_not_lt; elim. + by apply Zlt_neg_0. +Qed. + +Lemma lesb_sub_bounded m n : + lesb m n -> (0 <= Sint63.to_Z n - Sint63.to_Z m < Uint63.wB)%Z. +Proof. +move/Sint63.lebP => mn. +split. by apply Zle_minus_le_0. +apply + (Z.le_lt_trans _ (Sint63.to_Z Sint63.max_int - Sint63.to_Z Sint63.min_int))%Z. + apply leZ_sub. + by case: (Sint63.to_Z_bounded n). + by case: (Sint63.to_Z_bounded m). +done. +Qed. + +Lemma ltsb_neq m n : ltsb m n -> m <> n. +Proof. by move/Sint63.ltbP/[swap]/(f_equal Sint63.to_Z)-> =>/Z.lt_irrefl. Qed. + +(* +Lemma sub0_eq m n : sub m n = 0%int63 -> m = n. +Proof. +rewrite Sint63.sub_of_Z => /(f_equal Uint63.to_Z). +rewrite Uint63.of_Z_spec. +move/Sint63.ltbP in mn. +rewrite Zmod_small. + rewrite Z.sub_move_r /= => nm. + rewrite nm in mn. + by move/Z.lt_irrefl in mn. +by apply /lesb_sub_bounded /Sint63.lebP /Z.lt_le_incl. +Qed. +*) + +Lemma ltsb_sub_neq0 m n : ltsb m n -> sub n m <> 0%int63. +Proof. +move=> mn. +rewrite Sint63.sub_of_Z => /(f_equal Uint63.to_Z). +rewrite Uint63.of_Z_spec. +move/Sint63.ltbP in mn. +rewrite Zmod_small. + rewrite Z.sub_move_r /= => nm. + rewrite nm in mn. + by move/Z.lt_irrefl in mn. +by apply /lesb_sub_bounded /Sint63.lebP /Z.lt_le_incl. +Qed. + +Lemma sub_succ_pred m n : sub n (Uint63.succ m) = Uint63.pred (sub n m). +Proof. +apply Uint63.to_Z_inj. +rewrite Uint63.sub_spec Uint63.succ_spec Uint63.pred_spec Uint63.sub_spec. +rewrite Zminus_mod Zmod_mod -Zminus_mod Z.sub_add_distr. +apply/esym. +by rewrite Zminus_mod Zmod_mod -Zminus_mod. +Qed. + +Lemma uint2N_sub_succ m n : ltsb m n -> + uint2N (sub n m) = (uint2N (sub n (Uint63.succ m))).+1. +Proof. move/ltsb_sub_neq0 => mn. by rewrite sub_succ_pred uint2N_pred. Qed. + +Lemma N2int_succ : {morph N2int : x / x.+1 >-> Uint63.succ x}. +Proof. +move=> x; apply Uint63.to_Z_inj; rewrite Uint63.succ_spec !Uint63.of_Z_spec. +by rewrite Zplus_mod /= Zpos_P_of_succ_nat /Z.succ Zplus_mod Zmod_mod. +Qed. + +Lemma N2int_mul : {morph N2int : x y / x * y >-> mul x y}. +Proof. +move=> x y; apply Uint63.to_Z_inj. +by rewrite Uint63.mul_spec !Uint63.of_Z_spec Nat2Z.inj_mul Zmult_mod. +Qed. + +Lemma N2int_bounded n : + (Z.of_nat n <= Sint63.to_Z Sint63.max_int)%Z -> + (Sint63.to_Z Sint63.min_int <= Z.of_nat n <= Sint63.to_Z Sint63.max_int)%Z. +Proof. +split => //. +apply (Z.le_trans _ 0). + rewrite -[0%Z]/(Sint63.to_Z 0). + by case: (Sint63.to_Z_bounded 0). +by apply Zle_0_nat. +Qed. +End Int63. + +Module MLtypes63. +Import MLTypes. + +(******************************************************************************) +(* generated by coqgen *) +(******************************************************************************) +Section with_monad. +Context [M : Type -> Type]. +Fixpoint coq_type63 (T : ml_type) : Type := + match T with + | ml_int => int + | ml_bool => bool + | ml_unit => unit + | ml_arrow T1 T2 => coq_type63 T1 -> M (coq_type63 T2) + | ml_ref T1 => loc T1 + | ml_rlist T1 => rlist (coq_type63 T1) T1 + end. +End with_monad. +(******************************************************************************) + +Canonical ml_type63 := @Build_ML_universe _ coq_type63 ml_unit val_nonempty. + +Section fact_for_int63. +Variable M : typedStoreMonad ml_type63 MLTypes.locT. +Local Notation coq_type := (hierarchy.coq_type (MonadTypedStore.sort M)). +Local Open Scope do_notation. + +Section forloop63. +Definition forloop63 (n_1 n_2 : int) (b : int -> M unit) : M unit := + if Sint63.ltb n_2 n_1 then Ret tt else + iter (uint2N (sub n_2 n_1)).+1 + (fun (m : M int) => do i <- m; do _ <- b i; Ret (Uint63.succ i)) + (Ret n_1) >> Ret tt. + +Lemma forloop63S m n (f : int -> M unit) : + ltsb m n -> forloop63 m n f = f m >> forloop63 (Uint63.succ m) n f. +Proof. +rewrite /forloop63 => mn. +rewrite ltsbNlesb (ltsbW _ _ mn) /=. +case: ifPn => nSm. + by move: mn; rewrite ltsbNlesb => /negP; elim; apply ltsbS_lesb. +rewrite ltsbNlesb negbK in nSm. +rewrite uint2N_sub_succ //. +by rewrite iterSr bindretf !bindA iter_bind !bindA. +Qed. + +Lemma forloop631 m (f : int -> M unit) : + forloop63 m m f = f m. +Proof. rewrite /forloop63. +case: (Sint63.ltbP m m) => [/Z.lt_irrefl // | _]. +rewrite /= bindA. +rewrite /uint2N Uint63.sub_spec Z.sub_diag Zmod_0_l /=. +by rewrite !(bindretf,bindA) bindmskip. +Qed. + +Lemma forloop630 m n (f : int -> M unit) : + ltsb n m -> forloop63 m n f = skip. +Proof. by rewrite /forloop63 => ->. Qed. +End forloop63. + +Definition fact_for63 (n : coq_type ml_int) : M (coq_type ml_int) := + do v <- cnew ml_int 1%int63; + do _ <- + (do u <- Ret 1%int63; + do v_1 <- Ret n; + forloop63 u v_1 + (fun i => + do v_1 <- (do v_1 <- cget v; Ret (mul v_1 i)); + cput v v_1)); + cget v. + +Section fact_for63_ok. +Variable n : nat. +(* Note: assuming n < max_int rather than n <= max_int is not strictly + needed, but it simplifies reasoning about loops in concrete code *) +Hypothesis Hn : (Z.of_nat n < Sint63.to_Z Sint63.max_int)%Z. + +Let n_bounded : + (Sint63.to_Z Sint63.min_int <= Z.of_nat n <= Sint63.to_Z Sint63.max_int)%Z. +Proof. by apply N2int_bounded, Z.lt_le_incl. Qed. + +Lemma ltsb_succ : ltsb (N2int n) (Uint63.succ (N2int n)). +Proof. +apply/Sint63.ltbP. +rewrite Sint63.succ_spec Sint63.cmod_small. + by apply/Zle_lt_succ/Z.le_refl. +split. + apply leZ_addr => //; by case: (Sint63.to_Z_bounded (N2int n)). +apply Z.lt_add_lt_sub_r; by rewrite -Sint63.is_int. +Qed. + +Lemma ltsb_subr m : m.+1 < n -> ltsb (N2int (n - m.+1)) (N2int n). +Proof. +move=> Smn. +apply/Sint63.ltbP. +have Hm : n - m.+1 < n. + rewrite ltn_subLR. + by rewrite addSn ltnS leq_addl. + by apply ltnW. +rewrite /N2int -!Sint63.is_int //. +- by apply/inj_lt/ltP. +- move/ltP/inj_lt in Hm. + by split; apply N2int_bounded, Z.lt_le_incl, (Z.lt_trans _ _ _ Hm). +Qed. + +Theorem fact_for63_ok : crun (fact_for63 (N2int n)) = Some (N2int (fact_rec n)). +Proof. +rewrite /fact_for63. +under eq_bind do rewrite !bindA !bindretf. +set fn := N2int (fact_rec n). +transitivity (crun (cnew ml_int fn >> Ret fn : M _)); + last by rewrite crunret // crunnew0. +congr crun. +have {1}-> : (1 = N2int 1)%int63 by []. +rewrite -/(fact_rec 0). +have -> : (1 = Uint63.succ (N2int 0))%int63 by []. +pose m := n. +have -> : 0 = n - m by rewrite subnn. +have : m <= n by []. +elim: m => [|m IH] mn. + rewrite subn0. + under eq_bind do rewrite forloop630 (ltsb_succ,bindretf) // -cgetret. + by rewrite cnewget. +rewrite -N2int_succ subnSK //. +case: m IH mn => [|m] IH mn. + under eq_bind do rewrite subn0 forloop631 !(ltsb_subr,bindA) //. + rewrite cnewget. + under eq_bind do rewrite bindretf -cgetret. + rewrite cnewput -N2int_mul mulnC -{1}(prednK mn) cnewget subn1. + by rewrite -/(fact_rec n.-1.+1) prednK. +under eq_bind do rewrite forloop63S !(ltsb_subr,bindA) //. +rewrite cnewget. +under eq_bind do rewrite bindretf. +rewrite cnewput -IH (ltnW,subnS) // -N2int_mul mulnC -(@prednK (n-m.+1)) //. +by rewrite lt0n subn_eq0 -ltnNge. +Qed. +End fact_for63_ok. +End fact_for_int63. + +End MLtypes63. diff --git a/hierarchy.v b/hierarchy.v index 0edb9016..4da4c461 100644 --- a/hierarchy.v +++ b/hierarchy.v @@ -2,7 +2,7 @@ (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later *) Ltac typeof X := type of X. -Require Import ssrmatching Reals. +Require Import ssrmatching Reals JMeq. From mathcomp Require Import all_ssreflect. From mathcomp Require boolp. From infotheo Require Import Reals_ext. @@ -65,6 +65,11 @@ From HB Require Import structures. (* arrayMonad == array monad *) (* plusArrayMonad == plus monad + array monad *) (* *) +(* ML_universe == a type with decidable equality to represent an *) +(* OCaml type together with its Coq representation *) +(* in the type of a Tarski universe *) +(* typedStoreMonad == A monad for OCaml computations *) +(* *) (* Trace monads: *) (* traceMonad == trace monad *) (* traceReifyMonad == trace + reify *) @@ -83,8 +88,10 @@ From HB Require Import structures. (* failFreshMonad == freshMonad + failure *) (* *) (* references: *) +(* - R. Affeldt, J. Garrigue, T. Saikawa, Environment-friendly monadic *) +(* equational reasoning for OCaml, The Coq Workshop 2023 *) (* - R. Affeldt, D. Nowak, Extending Equational Monadic Reasoning with Monad *) -(* Transformers, https://arxiv.org/abs/2011.03463 *) +(* Transformers, TYPES 2020, https://arxiv.org/abs/2011.03463 *) (* - R. Affeldt, D. Nowak, T. Saikawa, A Hierarchy of Monadic Effects for *) (* Program Verification using Equational Reasoning, MPC 2019 *) (* - J. Gibbons, R. Hinze, Just do it: simple monadic equational reasoning, *) @@ -294,11 +301,11 @@ End join_laws. End JoinLaws. HB.mixin Record isMonad (F : UU0 -> UU0) of Functor F := { - ret : FId ~> [the functor of F] ; - join : [the functor of F \o F] ~> [the functor of F] ; + ret : FId ~> F ; + join : F \o F ~> F ; bind : forall (A B : UU0), F A -> (A -> F B) -> F B ; - bindE : forall (A B : UU0) (f : A -> F B) (m : F A), - bind A B m f = join B (([the functor of F] # f) m) ; + __bindE : forall (A B : UU0) (f : A -> F B) (m : F A), + bind A B m f = join B ((F # f) m) ; joinretM : JoinLaws.left_unit ret join ; joinMret : JoinLaws.right_unit ret join ; joinA : JoinLaws.associativity join }. @@ -311,6 +318,10 @@ Notation Join := (@join _ _). Arguments bind {s A B} : simpl never. Notation "m >>= f" := (bind m f) : monae_scope. +Lemma bindE (F : monad) (A B : UU0) (f : A -> F B) (m : F A) : + m >>= f = join B ((F # f) m). +Proof. by rewrite __bindE. Qed. + Lemma eq_bind (M : monad) (A B : UU0) (m : M A) (f1 f2 : A -> M B) : f1 =1 f2 -> m >>= f1 = m >>= f2. Proof. by move=> f12; congr bind; apply boolp.funext. Qed. @@ -1076,6 +1087,97 @@ HB.structure Definition MonadArray (S : UU0) (I : eqType) := HB.structure Definition MonadPlusArray (S : UU0) (I : eqType) := { M of MonadPlus M & isMonadArray S I M}. +Variant loc (ml_type : Type) (locT : eqType) : ml_type -> Type := + mkloc T : locT -> loc locT T. +Definition loc_id (ml_type : Type) (locT : eqType) {T : ml_type} (l : loc locT T) : locT := + let: mkloc _ n := l in n. + +Structure ML_universe := { + ml_type :> eqType ; + coq_type : forall M : Type -> Type, ml_type -> Type ; + ml_nonempty : ml_type ; + val_nonempty : forall M, coq_type M ml_nonempty }. + +HB.mixin Record isMonadTypedStore (MLU : ML_universe) (locT : eqType) (M : UU0 -> UU0) + of Monad M := { + cnew : forall {T : MLU}, coq_type M T -> M (loc locT T) ; + cget : forall {T}, loc locT T -> M (coq_type M T) ; + cput : forall {T}, loc locT T -> coq_type M T -> M unit ; + crun : forall {A : UU0}, M A -> option A ; (* execute in empty store *) + cnewget : forall T (s : coq_type M T) A (k : loc locT T -> coq_type M T -> M A), + cnew s >>= (fun r => cget r >>= k r) = cnew s >>= (fun r => k r s) ; + cnewput : forall T (s t : coq_type M T) A (k : loc locT T -> M A), + cnew s >>= (fun r => cput r t >> k r) = cnew t >>= k ; + cgetput : forall T (r : loc locT T) (s : coq_type M T), + cget r >> cput r s = cput r s ; + cgetputskip : forall T (r : loc locT T), cget r >>= cput r = cget r >> skip ; + cgetget : + forall T (r : loc locT T) (A : UU0) (k : coq_type M T -> coq_type M T -> M A), + cget r >>= (fun s => cget r >>= k s) = cget r >>= fun s => k s s ; + cputget : + forall T (r : loc locT T) (s : coq_type M T) (A : UU0) (k : coq_type M T -> M A), + cput r s >> (cget r >>= k) = cput r s >> k s ; + cputput : forall T (r : loc locT T) (s s' : coq_type M T), + cput r s >> cput r s' = cput r s' ; + cgetC : + forall T1 T2 (r1 : loc locT T1) (r2 : loc locT T2) (A : UU0) + (k : coq_type M T1 -> coq_type M T2 -> M A), + cget r1 >>= (fun u => cget r2 >>= (fun v => k u v)) = + cget r2 >>= (fun v => cget r1 >>= (fun u => k u v)) ; + cgetnewD : + forall T T' (r : loc locT T) (s : coq_type M T') A + (k : loc locT T' -> coq_type M T -> coq_type M T -> M A), + cget r >>= (fun u => cnew s >>= (fun r' => cget r >>= k r' u)) = + cget r >>= (fun u => cnew s >>= (fun r' => k r' u u)) ; + cgetnewE : forall T1 T2 (r1 : loc locT T1) (s : coq_type M T2) (A : UU0) + (k1 k2 : loc locT T2 -> M A), + (forall r2 : loc locT T2, loc_id r1 != loc_id r2 -> k1 r2 = k2 r2) -> + cget r1 >> (cnew s >>= k1) = cget r1 >> (cnew s >>= k2) ; + cgetputC : forall T1 T2 (r1 : loc locT T1) (r2 : loc locT T2) (s : coq_type M T2), + cget r1 >> cput r2 s = cput r2 s >> cget r1 >> skip ; + cputC : + forall T1 T2 (r1 : loc locT T1) (r2 : loc locT T2) (s1 : coq_type M T1) + (s2 : coq_type M T2) (A : UU0), + loc_id r1 != loc_id r2 \/ JMeq s1 s2 -> + cput r1 s1 >> cput r2 s2 = cput r2 s2 >> cput r1 s1 ; + cputgetC : + forall T1 T2 (r1 : loc locT T1) (r2 : loc locT T2) (s1 : coq_type M T1) + (A : UU0) (k : coq_type M T2 -> M A), + loc_id r1 != loc_id r2 -> + cput r1 s1 >> cget r2 >>= k = + cget r2 >>= (fun v => cput r1 s1 >> k v) ; + cputnewC : + forall T T' (r : loc locT T) (s : coq_type M T) (s' : coq_type M T') A + (k : loc locT T' -> M A), + cget r >> (cnew s' >>= fun r' => cput r s >> k r') = + cput r s >> (cnew s' >>= k) ; + crunret : forall (A B : UU0) (m : M A) (s : B), + crun m -> crun (m >> Ret s) = Some s ; + crunskip : + crun skip = Some tt ; + crunnew : forall (A : UU0) T (m : M A) (s : A -> coq_type M T), + crun m -> crun (m >>= fun x => cnew (s x)) ; + crunnewget : forall (A : UU0) T (m : M A) (s : A -> coq_type M T), + crun m -> crun (m >>= fun x => cnew (s x) >>= cget) ; + crungetnew : forall (A : UU0) T1 T2 (m : M A) (r : A -> loc locT T1) + (s : A -> coq_type M T2), + crun (m >>= fun x => cget (r x)) -> + crun (m >>= fun x => cnew (s x) >> cget (r x)) ; + crungetput : forall (A : UU0) T (m : M A) (r : A -> loc locT T) + (s : A -> coq_type M T), + crun (m >>= fun x => cget (r x)) -> + crun (m >>= fun x => cput (r x) (s x)) ; + }. + +#[short(type=typedStoreMonad)] +HB.structure Definition MonadTypedStore (ml_type : ML_universe) (locT : eqType) := + { M of isMonadTypedStore ml_type locT M & isMonad M & isFunctor M }. + +Arguments cnew {ml_type locT s}. +Arguments cget {ml_type locT s} [T]. +Arguments cput {ml_type locT s} [T]. +Arguments crun {ml_type locT s} [A]. + HB.mixin Record isMonadTrace (T : UU0) (M : UU0 -> UU0) of Monad M := { mark : T -> M unit }. diff --git a/impredicative_set/ihierarchy.v b/impredicative_set/ihierarchy.v index c881f9a4..6d1478f0 100644 --- a/impredicative_set/ihierarchy.v +++ b/impredicative_set/ihierarchy.v @@ -2,7 +2,7 @@ (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later *) Ltac typeof X := type of X. -Require Import ssrmatching. +Require Import ssrmatching JMeq. From mathcomp Require Import all_ssreflect. Require Import imonae_lib. From HB Require Import structures. @@ -283,11 +283,11 @@ End join_laws. End JoinLaws. HB.mixin Record isMonad (F : UU0 -> UU0) of Functor F := { - ret : FId ~> [the functor of F] ; - join : [the functor of F \o F] ~> [the functor of F] ; + ret : FId ~> F ; + join : F \o F ~> F ; bind : forall (A B : UU0), F A -> (A -> F B) -> F B ; - bindE : forall (A B : UU0) (f : A -> F B) (m : F A), - bind A B m f = join B (([the functor of F] # f) m) ; + __bindE : forall (A B : UU0) (f : A -> F B) (m : F A), + bind A B m f = join B ((F # f) m) ; joinretM : JoinLaws.left_unit ret join ; joinMret : JoinLaws.right_unit ret join ; joinA : JoinLaws.associativity join }. @@ -300,6 +300,10 @@ Notation Join := (@join _ _). Arguments bind {s A B} : simpl never. Notation "m >>= f" := (bind m f) : monae_scope. +Lemma bindE (F : monad) (A B : UU0) (f : A -> F B) (m : F A) : + m >>= f = join B ((F # f) m). +Proof. by rewrite __bindE. Qed. + Lemma eq_bind (M : monad) (A B : UU0) (m : M A) (f1 f2 : A -> M B) : f1 =1 f2 -> m >>= f1 = m >>= f2. Proof. by move=> f12; congr bind; apply funext. Qed. @@ -1065,6 +1069,11 @@ HB.structure Definition MonadArray (S : UU0) (I : eqType) := HB.structure Definition MonadPlusArray (S : UU0) (I : eqType) := { M of MonadPlus M & isMonadArray S I M}. +Variant loc (ml_type : Type) (locT : eqType) : ml_type -> Type := + mkloc T : locT -> loc locT T. +Definition loc_id (ml_type : Type) (locT : eqType) {T : ml_type} (l : loc locT T) : locT := + let: mkloc _ n := l in n. + HB.mixin Record isMonadTrace (T : UU0) (M : UU0 -> UU0) of Monad M := { mark : T -> M unit }. diff --git a/impredicative_set/imonad_lib.v b/impredicative_set/imonad_lib.v index 6c20f468..c77c41c4 100644 --- a/impredicative_set/imonad_lib.v +++ b/impredicative_set/imonad_lib.v @@ -34,6 +34,7 @@ Require Import ihierarchy. (* commute m n f := (m >>= n >>= f) = (n >>= m >>= f) *) (* (ref: definition 4.2, mu2019tr3) *) (* rep n mx == mx >> mx >> ... >> mx, n times *) +(* forloop n1 n2 (b : nat -> M unit) : M unit := for-loop *) (* *) (******************************************************************************) @@ -150,6 +151,16 @@ HB.instance Definition _ X := Definition uncurry_F X : functor := [the functor of @uncurry_M X]. End uncurry_functor. +Lemma bind_uncurry (M : monad) (A B C : UU0) (f : A -> M B) (g : A -> B -> M C) x : + (f x >>= fun y => Ret (x, y)) >>= (fun xy => g xy.1 xy.2) = + (f x >>= g x). +Proof. by rewrite bindA; under eq_bind do rewrite bindretf. Qed. + +Lemma bindA_uncurry (M : monad) (A B C : UU0) (m : M A) (f : A -> M B) (g : A -> B -> M C) : + (m >>= fun x => f x >>= fun y => Ret (x, y)) >>= (fun xy => g xy.1 xy.2) = + (m >>= fun x => f x >>= g x). +Proof. by rewrite bindA; by under eq_bind do rewrite bind_uncurry. Qed. + Section exponential_functor. Variable A : UU0. Definition exponential_M (X : UU0) := A -> X. @@ -696,3 +707,40 @@ by rewrite -subn1 addnBA ?expn_gt0 // addnn -muln2 -expnSr subn1. Qed. End MonadCount. + +Lemma iteri_bind {M : monad} n (f : nat -> M unit) (m1 m2 : M unit) : + iteri n (fun i (m : M unit) => m >> f i) (m1 >> m2) = + m1 >> iteri n (fun i (m : M unit) => m >> f i) m2. +Proof. by elim: n m2 => // n IH m2; rewrite iteriS IH !bindA. Qed. + +Lemma iter_bind {M : monad} (T : UU0) n (f : T -> M T) (m1 : M unit) m2 : + iter n (fun (m : M T) => m >>= f) (m1 >> m2) = + m1 >> iter n (fun (m : M T) => m >>= f) m2. +Proof. by elim: n m2 => // n IH m2; rewrite iterS IH !bindA. Qed. + +Section forloop. +Variable M : monad. + +Definition forloop (n_1 n_2 : nat) (b : nat -> M unit) : M unit := + if n_2 < n_1 then Ret tt else + iteri (n_2.+1 - n_1) + (fun i (m : M unit) => m >> b (n_1 + i)) + skip. + +Lemma forloopS m n (f : nat -> M unit) : + m <= n -> forloop m n f = f m >> forloop m.+1 n f. +Proof. +rewrite /forloop => mn. +rewrite ltnNge mn /= subSS subSn // iteriSr bindskipf. +rewrite -[f _]bindmskip iteri_bind addn0 ltnS -subn_eq0. +case: (n-m) => //= k. +rewrite addSnnS; apply eq_bind => _; congr bind. +apply eq_iteri => i x; by rewrite addSnnS. +Qed. + +Lemma forloop0 m n (f : nat -> M unit) : + m > n -> forloop m n f = skip. +Proof. by rewrite /forloop => ->. Qed. + +End forloop. +Arguments forloop {M}. diff --git a/impredicative_set/imonae_lib.v b/impredicative_set/imonae_lib.v index 84c49abb..97bb1c39 100644 --- a/impredicative_set/imonae_lib.v +++ b/impredicative_set/imonae_lib.v @@ -5,7 +5,8 @@ Require ProofIrrelevance FunctionalExtensionality. Definition proof_irr := @ProofIrrelevance.proof_irrelevance. -Definition eq_rect_eq := @ProofIrrelevance.ProofIrrelevanceTheory.Eq_rect_eq.eq_rect_eq. +Definition eq_rect_eq := + @ProofIrrelevance.ProofIrrelevanceTheory.Eq_rect_eq.eq_rect_eq. Definition funext := @FunctionalExtensionality.functional_extensionality. @@ -138,3 +139,70 @@ Lemma compidf A B (f : A -> B) : id \o f = f. Proof. by []. Qed. Lemma compE A B C (g : B -> C) (f : A -> B) a : (g \o f) a = g (f a). Proof. by []. Qed. + +Lemma if_pair A B b (x : A) y (u : A) (v : B) : + (if b then (x, y) else (u, v)) = (if b then x else u, if b then y else v). +Proof. by case: ifPn. Qed. + +Lemma iteriSr T n (f : nat -> T -> T) x : + iteri n.+1 f x = iteri n (f \o succn) (f 0 x). +Proof. by elim: n x => // n IH x /=; rewrite -IH. Qed. + +Lemma iteriD T n m (f : nat -> T -> T) x : + iteri (n + m) f x = iteri m (f \o addn n) (iteri n f x). +Proof. by elim: n x f => // n IH x f; rewrite addSn iteriSr IH iteriSr. Qed. + +Section nth_error. +Context [T : Type] (def : T) (st : seq T). + +(* Basic lemmas for standard library's nth_error *) +Local Notation nth_error := List.nth_error. + +Lemma nth_error_set_nth n x : nth_error (set_nth def st n x) n = Some x. +Proof. +elim: n st => [|z IH] [] // {IH}. +elim: z.+1 => [|n <-] //=. +by rewrite set_nth_nil. +Qed. + +Lemma nth_error_rcons_size b : nth_error (rcons st b) (size st) = Some b. +Proof. by elim: st. Qed. + +Lemma nth_error_rcons_some n a b : + nth_error st n = Some a -> nth_error (rcons st b) n = Some a. +Proof. by elim: n st => [|n IH] []. Qed. + +Lemma nth_error_set_nth_id n a : + nth_error st n = Some a -> set_nth def st n a = st. +Proof. by elim: n st => [|n IH] [] //= b st'; [case=> -> | move/IH ->]. Qed. + +Lemma nth_error_set_nth_other m n a b : + m != n -> + nth_error st m = Some a -> + nth_error (set_nth def st n b) m = Some a. +Proof. +elim: m st n => [|m IH] [|c st'] [|n] //=; rewrite eqSS => *; exact: IH. +Qed. + +Lemma nth_error_set_nth_none m n a b : + nth_error st m = None -> + nth_error st n = Some a -> + nth_error (set_nth def st n b) m = None. +Proof. by elim: m st n => [|m IH] [|c st'] [|n] //=; apply IH. Qed. + +Lemma nth_error_size n a : nth_error st n = Some a -> n < size st. +Proof. by elim: n st => [|n IH] [|c st'] //= /IH. Qed. + +Lemma nth_error_size_set_nth n a b : + nth_error st n = Some a -> size (set_nth def st n b) = size st. +Proof. by rewrite size_set_nth => /nth_error_size /maxn_idPr. Qed. + +Lemma set_nth_rcons a b : set_nth def (rcons st a) (size st) b = rcons st b. +Proof. by elim: st => //= c st' ->. Qed. + +Lemma nth_error_set_nth_rcons n a b c : + nth_error st n = Some a -> + set_nth def (rcons st c) n b = rcons (set_nth def st n b) c. +Proof. by elim: n st => [|n IH] [|d st'] //= /IH ->. Qed. +End nth_error. +Arguments nth_error_size {T st n a}. diff --git a/meta.yml b/meta.yml index 45c127e9..c30903f4 100644 --- a/meta.yml +++ b/meta.yml @@ -35,12 +35,16 @@ license: file: LICENSE supported_coq_versions: - text: Coq 8.17 - opam: '{ (>= "8.17" & < "8.18~") | (= "dev") }' + text: Coq 8.16-8.17 + opam: '{ (>= "8.16" & < "8.18~") | (= "dev") }' tested_coq_opam_versions: +- version: '1.16.0-coq-8.16' + repo: 'mathcomp/mathcomp' - version: '1.16.0-coq-8.17' repo: 'mathcomp/mathcomp' +- version: '1.17.0-coq-8.16' + repo: 'mathcomp/mathcomp' - version: '1.17.0-coq-8.17' repo: 'mathcomp/mathcomp' diff --git a/monad_lib.v b/monad_lib.v index 1b504a5d..1968c035 100644 --- a/monad_lib.v +++ b/monad_lib.v @@ -37,6 +37,7 @@ Require Import hierarchy. (* preserves f g := the monadic function f : A -> M A preserves *) (* the value of the function g : A -> B *) (* rep n mx == mx >> mx >> ... >> mx, n times *) +(* forloop n1 n2 (b : nat -> M unit) : M unit := for-loop *) (* *) (******************************************************************************) @@ -153,6 +154,16 @@ HB.instance Definition _ X := Definition uncurry_F X : functor := [the functor of @uncurry_M X]. End uncurry_functor. +Lemma bind_uncurry (M : monad) (A B C : UU0) (f : A -> M B) (g : A -> B -> M C) x : + (f x >>= fun y => Ret (x, y)) >>= (fun xy => g xy.1 xy.2) = + (f x >>= g x). +Proof. by rewrite bindA; under eq_bind do rewrite bindretf. Qed. + +Lemma bindA_uncurry (M : monad) (A B C : UU0) (m : M A) (f : A -> M B) (g : A -> B -> M C) : + (m >>= fun x => f x >>= fun y => Ret (x, y)) >>= (fun xy => g xy.1 xy.2) = + (m >>= fun x => f x >>= g x). +Proof. by rewrite bindA; by under eq_bind do rewrite bind_uncurry. Qed. + Section exponential_functor. Variable A : UU0. Definition exponential_M (X : UU0) := A -> X. @@ -586,7 +597,7 @@ Proof. by []. Qed. Lemma naturality_mpair (M : monad) (A B : UU0) (f : A -> B) (g : A -> M A): (M # f^`2) \o (mpair \o g^`2) = mpair \o ((M # f) \o g)^`2. Proof. -rewrite boolp.funeqE => -[a0 a1]. +apply boolp.funext => -[a0 a1]. rewrite compE fmap_bind. rewrite compE mpairE compE bind_fmap; bind_ext => a2. rewrite fcompE fmap_bind 2!compE bind_fmap; bind_ext => a3. @@ -699,3 +710,40 @@ by rewrite -subn1 addnBA ?expn_gt0 // addnn -muln2 -expnSr subn1. Qed. End MonadCount. + +Lemma iteri_bind {M : monad} n (f : nat -> M unit) (m1 m2 : M unit) : + iteri n (fun i (m : M unit) => m >> f i) (m1 >> m2) = + m1 >> iteri n (fun i (m : M unit) => m >> f i) m2. +Proof. by elim: n m2 => // n IH m2; rewrite iteriS IH !bindA. Qed. + +Lemma iter_bind {M : monad} (T : UU0) n (f : T -> M T) (m1 : M unit) m2 : + iter n (fun (m : M T) => m >>= f) (m1 >> m2) = + m1 >> iter n (fun (m : M T) => m >>= f) m2. +Proof. by elim: n m2 => // n IH m2; rewrite iterS IH !bindA. Qed. + +Section forloop. +Variable M : monad. + +Definition forloop (n_1 n_2 : nat) (b : nat -> M unit) : M unit := + if n_2 < n_1 then Ret tt else + iteri (n_2.+1 - n_1) + (fun i (m : M unit) => m >> b (n_1 + i)) + skip. + +Lemma forloopS m n (f : nat -> M unit) : + m <= n -> forloop m n f = f m >> forloop m.+1 n f. +Proof. +rewrite /forloop => mn. +rewrite ltnNge mn /= subSS subSn // iteriSr bindskipf. +rewrite -[f _]bindmskip iteri_bind addn0 ltnS -subn_eq0. +case: (n-m) => //= k. +rewrite addSnnS; apply eq_bind => _; congr bind. +apply eq_iteri => i x; by rewrite addSnnS. +Qed. + +Lemma forloop0 m n (f : nat -> M unit) : + m > n -> forloop m n f = skip. +Proof. by rewrite /forloop => ->. Qed. + +End forloop. +Arguments forloop {M}. diff --git a/monad_model.v b/monad_model.v index fc73811c..d1b97c39 100644 --- a/monad_model.v +++ b/monad_model.v @@ -1,3 +1,4 @@ +Require Import JMeq. From mathcomp Require Import all_ssreflect. From mathcomp Require Import finmap. From mathcomp Require boolp. @@ -20,7 +21,7 @@ Require Import monad_transformer. (* ListMonad == list monad seq *) (* SetMonad == set monads using classical_sets *) (* ExceptMonad == exception monad E + A *) -(* option_monad == notation for ExceptMonad.acto unit *) +(* option_monad == alias for ExceptMonad.acto unit *) (* OutputMonad == output monad X * seq L *) (* EnvironmentMonad == environment monad E -> A *) (* StateMonad == state monad S -> A * S *) @@ -62,6 +63,8 @@ Require Import monad_transformer. (* Module ModelMonadStateRun == stateRunMonad for MS *) (* Module ModelMonadExceptStateRun == exceptStateRunMonad *) (* *) +(* Module ModelTypedStore == model for typed store *) +(* *) (* references: *) (* - Wadler, P. Monads and composable continuations. LISP and Symbolic *) (* Computation 7, 39–55 (1994) *) @@ -232,7 +235,8 @@ Lemma except_bindE (E A B : UU0) (M := ExceptMonad.acto E) m >>= f = match m with inl z => inl z | inr b => f b end. Proof. by []. Qed. -Notation option_monad := (ExceptMonad.acto unit). +Definition option_monad := ExceptMonad.acto unit. +HB.instance Definition _ := Monad.on option_monad. Module OutputMonad. Section output. @@ -799,6 +803,7 @@ Section fail. Definition option_fail : forall A, option_monad A := fun A => @throw unit A tt. Let option_bindfailf : BindLaws.left_zero (@bind _) option_fail. Proof. by []. Qed. +HB.instance Definition _ := Monad.on option_monad. HB.instance Definition _ := @isMonadFail.Build option_monad option_fail option_bindfailf. @@ -820,7 +825,7 @@ HB.export Fail. Module Except. Section except. -Let M : failMonad := [the failMonad of ExceptMonad.acto unit]. +Let M : failMonad := option_monad. Definition handle : forall A, M A -> M A -> M A := fun A m1 m2 => @handle_op unit _ (m1, (fun _ => m2)). Lemma handleE : handle = (fun A m m' => if m is inr x then m else m'). @@ -833,7 +838,7 @@ Let catchA : forall A, ssrfun.associative (@handle A). Proof. by move=> A; case. Qed. Let catchret : forall A x, @left_zero (M A) (M A) (Ret x) (@handle A). Proof. by move=> A x; case. Qed. -HB.instance Definition _ := isMonadExcept.Build (ExceptMonad.acto unit) +HB.instance Definition _ := isMonadExcept.Build option_monad catchmfail catchfailm catchA catchret. End except. End Except. @@ -1656,6 +1661,524 @@ End modelplusarray. End ModelPlusArray. HB.export ModelPlusArray. +Definition locT_nat := [eqType of nat]. + +Module ModelTypedStore. + +Section ModelTypedStore. +Variables (ml_type0 : eqType) (coq_type0 : ml_type0 -> Type) + (ml_nonempty0 : ml_type0) (val_nonempty0 : coq_type0 ml_nonempty0). + +Definition MLU : ML_universe := + @Build_ML_universe (ml_type0) (fun M => @coq_type0) + (ml_nonempty0) (fun M => val_nonempty0). + +Record binding (M : Type -> Type) := + mkbind { bind_type : MLU; bind_val : coq_type M bind_type }. +Arguments mkbind {M}. + +Definition acto : UU0 -> UU0 := MS (seq (binding idfun)) [the monad of option_monad]. +Local Notation M := acto. + +Local Notation coq_type' := (@coq_type MLU idfun). + +Definition def : binding idfun := mkbind (ml_nonempty MLU) (val_nonempty MLU idfun). + +Local Notation nth_error := List.nth_error. + +Notation loc := (@loc MLU locT_nat). + +Definition cnew T (v : coq_type M T) : M (loc T) := + fun st => let n := size st in + Ret (mkloc T n, rcons st (mkbind T (v : coq_type' T))). + +Definition cget T (r : loc T) : M (coq_type M T) := + fun st => + if nth_error st (loc_id r) is Some (mkbind T' v) then + if coerce T v is Some u then Ret (u, st) else fail + else fail. + +Definition cput T (r : loc T) (v : coq_type M T) : M unit := + fun st => + let n := loc_id r in + if nth_error st n is Some (mkbind T' _) then + if coerce T' v is Some u then + Ret (tt, set_nth def st n (mkbind T' (u : coq_type' _))) + else fail + else fail. + +Definition crun (A : UU0) (m : M A) : option A := + match m nil with + | inl _ => None + | inr (a, _) => Some a + end. + +Definition Env := seq (binding idfun). + +Definition fresh_loc (T : MLU) (e : Env) := mkloc T (size e). + +Section mkbind. +Local Notation mkbind := (@mkbind idfun). + +Definition extend_env T (v : coq_type M T) (e : Env) := + rcons e (mkbind T v). + +Variant nth_error_spec (T : MLU) (e : Env) (r : loc T) : Type := + | NthError : forall s : coq_type M T, + nth_error e (loc_id r) = Some (mkbind T s) -> nth_error_spec e r + | NthError_nocoerce : forall T' (s' : coq_type M T'), + nth_error e (loc_id r) = Some (mkbind T' s') -> ~ coerce T s' -> + nth_error_spec e r + | NthError_None : nth_error e (loc_id r) = None -> nth_error_spec e r. + +Lemma ntherrorP (T : MLU) (e : Env) (r : loc T) : nth_error_spec e r. +Proof. +case H : (nth_error e (loc_id r)) => [[T' s']|]. + have [Ts'|Ts'] := boolp.pselect (coerce T s'). + have ? := coerce_eq Ts'; subst T'. + exact: NthError H. + exact: NthError_nocoerce H Ts'. +exact: NthError_None. +Qed. + +Lemma bind_cnew T (s : coq_type M T) A (k : loc T -> M A) e : + (cnew s >>= k) e = k (fresh_loc T e) (extend_env s e). +Proof. by case: e. Qed. + +Lemma Some_cget T (r : loc T) (s : coq_type M T) e (A : UU0) (f : coq_type M T -> M A) : + nth_error e (loc_id r) = Some (mkbind T s) -> + (cget r >>= f) e = f s e. +Proof. by move=> H; rewrite MS_bindE /cget H coerce_Some. Qed. +Arguments Some_cget {T r} s. + +Lemma cnewget T (s : coq_type M T) A (k : loc T -> coq_type M T -> M A) : + cnew s >>= (fun r => cget r >>= k r) = cnew s >>= (fun r => k r s). +Proof. +apply/boolp.funext => e. +by rewrite bind_cnew (Some_cget s)// nth_error_rcons_size. +Qed. + +Lemma cnewput T (s t : coq_type M T) A (k : loc T -> M A) : + cnew s >>= (fun r => cput r t >> k r) = cnew t >>= k. +Proof. +apply/boolp.funext => e. +rewrite bind_cnew 2!MS_bindE. +by rewrite /cput/= nth_error_rcons_size coerce_Some set_nth_rcons. +Qed. + +Lemma nocoerce_cget T (r : loc T) T' (s' : coq_type M T') e : + nth_error e (loc_id r) = Some (mkbind T' s') -> + ~ coerce T s' -> + cget r e = fail. +Proof. by move=> H Ts'; rewrite /cget H; case: coerce Ts'. Qed. + +Lemma nocoerce_cput T (r : loc T) (s : coq_type M T) T' (s' : coq_type M T') e : + nth_error e (loc_id r) = Some (mkbind T' s') -> + ~ coerce T s' -> + cput r s e = fail. +Proof. +move=> H Ts'; rewrite /cput H. +have {}Ts' : ~ coerce T' s by apply: contra_not Ts'; exact: coerce_sym. +by case: coerce Ts'. +Qed. + +Lemma None_cget T (r : loc T) e : + nth_error e (loc_id r) = None -> cget r e = fail. +Proof. by move=> H; rewrite /cget H. Qed. + +Lemma None_cput T (r : loc T) (s : coq_type M T) e : + nth_error e (loc_id r) = None -> cput r s e = fail. +Proof. by move=> H; rewrite /cput H. Qed. + +Definition cgetput T (r : loc T) (s : coq_type M T) : + cget r >> cput r s = cput r s. +Proof. +apply/boolp.funext => e. +have [s' H|T' s' H Ts'|H] := ntherrorP e r. +- by rewrite (Some_cget s'). +- by rewrite MS_bindE (nocoerce_cget H)// (nocoerce_cput _ H). +- by rewrite MS_bindE None_cget// None_cput. +Qed. + +Lemma Some_cput T (r : loc T) (s : coq_type M T) e : + nth_error e (loc_id r) = Some (mkbind T s) -> + cput r s e = (@skip M) e. +Proof. +by move=> H; rewrite /cput/= H coerce_Some/= nth_error_set_nth_id. +Qed. + +Lemma cgetputskip T (r : loc T) : cget r >>= cput r = cget r >> skip. +Proof. +apply/boolp.funext => e /=. +have [s' H|T' s' H Ts'|H] := ntherrorP e r. +- by rewrite (Some_cget s')// (Some_cget s')// (Some_cput H). +- by rewrite !MS_bindE (nocoerce_cget H). +- by rewrite !MS_bindE None_cget. +Qed. + +Lemma cgetget T (r : loc T) (A : UU0) + (k : coq_type M T -> coq_type M T -> M A) : + cget r >>= (fun s => cget r >>= k s) = cget r >>= fun s => k s s. +Proof. +apply/boolp.funext => e /=. +have [s' H|T' s' H Ts'|H] := ntherrorP e r. +- by do 3 rewrite (Some_cget s')//. +- by rewrite !MS_bindE (nocoerce_cget H). +- by rewrite !MS_bindE None_cget. +Qed. + +Lemma Some_cputE T (r : loc T) (s s' : coq_type M T) e : + nth_error e (loc_id r) = Some (mkbind T s') -> + cput r s e = inr (tt, set_nth def e (loc_id r) (mkbind T s)). +Proof. by move=> H; rewrite /cput/= H coerce_Some. Qed. + +Lemma Some_cputget T (s' s : coq_type M T) (r : loc T) A (k : coq_type M T -> M A) + (e : Env) : + nth_error e (loc_id r) = Some (mkbind T s') -> + (cput r s >> (cget r >>= k)) e = (cput r s >> k s) e. +Proof. +move=> H. +rewrite 2!MS_bindE (Some_cputE _ H). +by rewrite bindE/= (Some_cget s)// nth_error_set_nth. +Qed. +Arguments Some_cputget {T} s'. + +Lemma cputget T (r : loc T) (s : coq_type M T) (A : UU0) + (k : coq_type M T -> M A) : + cput r s >> (cget r >>= k) = cput r s >> k s. +Proof. +apply/boolp.funext => e /=. +have [s' H|T' s' H Ts'|H] := ntherrorP e r. +- by rewrite (Some_cputget s'). +- by rewrite !MS_bindE (nocoerce_cput _ H). +- by rewrite 2!MS_bindE None_cput. +Qed. + +Lemma Some_cputput (T : MLU) (r : loc T) (s s' : coq_type M T) + (e : Env) (s'' : coq_type M T) : + nth_error e (loc_id r) = Some (mkbind T s'') -> + (cput r s >> cput r s') e = cput r s' e. +Proof. +move=> H. +rewrite MS_bindE/=. +rewrite [in LHS](Some_cputE _ H)//. +rewrite [in RHS](Some_cputE _ H)//. +rewrite bindE/= /cput. +rewrite nth_error_set_nth coerce_Some/=. +by rewrite set_set_nth eqxx. +Qed. + +Lemma cputput T (r : loc T) (s s' : coq_type M T) : + cput r s >> cput r s' = cput r s'. +Proof. +apply/boolp.funext => e. +have [s'' H|T'' s'' H Ts''|H] := ntherrorP e r. +- by rewrite (Some_cputput _ _ H). +- by rewrite !MS_bindE (nocoerce_cput _ H)// (nocoerce_cput _ H). +- by rewrite MS_bindE !None_cput. +Qed. + +Lemma cgetC T1 T2 (r1 : loc T1) (r2 : loc T2) (A : UU0) + (k : coq_type M T1 -> coq_type M T2 -> M A) : + cget r1 >>= (fun u => cget r2 >>= (fun v => k u v)) = + cget r2 >>= (fun v => cget r1 >>= (fun u => k u v)). +Proof. +apply/boolp.funext => e /=. +have [u Hr1|u T1' Hr1 T1u|Hr1] := ntherrorP e r1. +- rewrite (Some_cget u)//. + have [v Hr2|v T2' Hr2 T2v|Hr2] := ntherrorP e r2. + + by rewrite (Some_cget v)// (Some_cget v)// (Some_cget u). + + by rewrite 2!MS_bindE (nocoerce_cget Hr2)// bindfailf. + + by rewrite !MS_bindE None_cget. +- rewrite MS_bindE (nocoerce_cget Hr1)// bindfailf. + have [v Hr2|v T2' Hr2 T2v|Hr2] := ntherrorP e r2. + + by rewrite (Some_cget v)// MS_bindE (nocoerce_cget Hr1). + + by rewrite MS_bindE (nocoerce_cget Hr2). + + by rewrite MS_bindE None_cget. +- rewrite MS_bindE None_cget// bindfailf. + have [v Hr2|v T2' Hr2 T2v|Hr2] := ntherrorP e r2. + + by rewrite (Some_cget v)// MS_bindE None_cget. + + by rewrite MS_bindE (nocoerce_cget Hr2). + + by rewrite MS_bindE !None_cget. +Qed. + +(* NB: this is similar to the cnewget law *) +Lemma cnewgetD_helper e T T' r v (s : coq_type M T') A (k : loc T' -> coq_type M T -> M A) : + nth_error e (loc_id r) = Some (mkbind T v) -> + (cnew s >>= (fun r' => cget r >>= k r')) e = (cnew s >>= (fun r => k r v)) e. +Proof. +move=> H. +rewrite bind_cnew//. +by rewrite (Some_cget v) // (nth_error_rcons_some _ H). +Qed. + +Lemma cgetnewD T T' (r : loc T) (s : coq_type M T') A + (k : loc T' -> coq_type M T -> coq_type M T -> M A) : + cget r >>= (fun u => cnew s >>= fun r' => cget r >>= k r' u) = + cget r >>= (fun u => cnew s >>= fun r' => k r' u u). +Proof. +apply/boolp.funext => e. +have [u Hr|u T1 Hr T1u|Hr] := ntherrorP e r. +- by rewrite (Some_cget u)// (Some_cget u)// (cnewgetD_helper _ _ Hr)//. +- by rewrite !MS_bindE (nocoerce_cget Hr). +- by rewrite !MS_bindE None_cget. +Qed. + +Lemma cgetnewE T1 T2 (r1 : loc T1) (s : coq_type M T2) (A : UU0) + (k1 k2 : loc T2 -> M A) : + (forall r2 : loc T2, loc_id r1 != loc_id r2 -> k1 r2 = k2 r2) -> + cget r1 >> (cnew s >>= k1) = cget r1 >> (cnew s >>= k2). +Proof. +move=> Hk. +apply/boolp.funext => e. +have [u r1u|T' s' Hr1 T1s'|Hr] := ntherrorP e r1. +- rewrite (Some_cget u)// (Some_cget u)// !bind_cnew Hk// neq_ltn. +- by move: r1u => /= /nth_error_size ->. +- by rewrite !MS_bindE (nocoerce_cget Hr1). +- by rewrite !MS_bindE None_cget. +Qed. + +Lemma cgetputC T1 T2 (r1 : loc T1) (r2 : loc T2) (s : coq_type M T2) : + cget r1 >> cput r2 s = cput r2 s >> cget r1 >> skip. +Proof. +apply/boolp.funext => e /=. +have [u r1u|T1' v1 Hr1 T1v1|Hr1] := ntherrorP e r1. +- rewrite (Some_cget u)// [in RHS]bindA MS_bindE. + have [v r2v|T' v r2v T2v|Hr2] := ntherrorP e r2. + + rewrite (Some_cputE _ r2v) [in RHS]bindE/=. + have [r12|r12] := eqVneq (loc_id r1) (loc_id r2). + move: r2v; rewrite -r12 r1u => -[?] _; subst T2. + by rewrite MS_bindE /cget nth_error_set_nth// coerce_Some. + by rewrite (Some_cget u)// (nth_error_set_nth_other _ _ r12 r1u). + + by rewrite (nocoerce_cput _ _ T2v). + + by rewrite None_cput. +- rewrite MS_bindE [RHS]MS_bindE bindA. + have [v r2v|T' v r2v T2v|Hr2] := ntherrorP e r2. + + rewrite {1}/cget Hr1. + have [?|T1'T1] := eqVneq T1' T1. + * subst T1'; rewrite coerce_Some. + rewrite [in LHS]bindE/= (Some_cputE _ r2v) [in RHS]bindE/=. + have [Hr|Hr] := eqVneq (loc_id r1) (loc_id r2). + move: r2v; rewrite -Hr Hr1 => -[?] _; subst T2. + by rewrite /cget nth_error_set_nth coerce_Some. + by rewrite /cget (nth_error_set_nth_other _ _ Hr Hr1) coerce_Some. + * rewrite coerce_None//= bindfailf (Some_cputE _ r2v) [in RHS]bindE/=. + have [r12|r12] := eqVneq (loc_id r1) (loc_id r2). + move: r2v; rewrite -r12 Hr1 => -[?] _; subst T1'. + by rewrite /cget nth_error_set_nth coerce_None. + by rewrite /cget (nth_error_set_nth_other _ _ r12 Hr1) coerce_None. + + by rewrite (nocoerce_cget _ T1v1)// bindfailf (nocoerce_cput _ _ T2v). + + by rewrite (nocoerce_cget _ T1v1)// None_cput// bindfailf. +- rewrite MS_bindE None_cget// bindfailf bindA MS_bindE. + have [v r2v|T' v r2v T2v|Hr2] := ntherrorP e r2. + + rewrite (Some_cputE _ r2v)/=. + rewrite bindE/=. + rewrite MS_bindE None_cget/= ?bindfailf//. + by rewrite (nth_error_set_nth_none _ _ Hr1 r2v). + + by rewrite (nocoerce_cput _ r2v). + + by rewrite None_cput. +Qed. + +Lemma cput_then_fail T1 T2 T1' e (s1' : coq_type M T1') + (r2 : loc T2) (s2 : coq_type M T2) + (r1 : loc T1) (s1 : coq_type M T1) : + nth_error e (loc_id r1) = Some (mkbind T1' s1') -> + ~ coerce T1 s1' -> + (cput r2 s2 >> cput r1 s1) e = fail. +Proof. +move=> Hr1 T1s'. +have [v Hr2|T2' v Hr2 T2v|Hr2] := ntherrorP e r2; last first. +- by rewrite MS_bindE None_cput. +- by rewrite MS_bindE (nocoerce_cput _ _ T2v). +- rewrite MS_bindE (Some_cputE _ Hr2). + rewrite bindE/=. + have [Hr|Hr] := eqVneq (loc_id r1) (loc_id r2). + + rewrite {1}/cput -Hr /= nth_error_set_nth. + have [HT|HT] := eqVneq T1 T2; last by rewrite coerce_None. + subst T2. + rewrite coerce_Some//=. + move: Hr1; rewrite Hr Hr2 => -[?]; subst T1' => _. + by rewrite coerce_Some // in T1s'. + + rewrite (nocoerce_cput _ _ T1s')//=. + by rewrite (@nth_error_set_nth_other _ _ _ _ _ (mkbind T1' s1')). +Qed. + +Lemma cputC T1 T2 (r1 : loc T1) (r2 : loc T2) (s1 : coq_type M T1) + (s2 : coq_type M T2) (A : UU0) : + loc_id r1 != loc_id r2 \/ JMeq s1 s2 -> + cput r1 s1 >> cput r2 s2 = cput r2 s2 >> cput r1 s1. +Proof. +move=> H; apply/boolp.funext => e /=. +have [u Hr1|T1' s'd Hr1 T1s'|Hr1] := ntherrorP e r1; last first. + rewrite MS_bindE None_cput// bindfailf. + have [v Hr2|T2' s' Hr2 T2s'|Hr2] := ntherrorP e r2; last first. + by rewrite MS_bindE None_cput. + + by rewrite MS_bindE (nocoerce_cput _ _ T2s'). + + rewrite MS_bindE (Some_cputE _ Hr2). + rewrite bindE/=. + by rewrite None_cput// (nth_error_set_nth_none _ _ Hr1 Hr2). +- rewrite MS_bindE (nocoerce_cput _ _ T1s')// bindfailf. + by rewrite (cput_then_fail _ _ _ Hr1). +- rewrite MS_bindE (Some_cputE _ Hr1)/=. + rewrite bindE/=. + case/boolP: (loc_id r1 == loc_id r2) H => [/eqP|] Hr /=. + + case => // H. + rewrite MS_bindE. + rewrite {2}/cput -Hr Hr1. + case/boolP: (T1 == T2) => [/eqP HT|HT]; last first. + rewrite coerce_None//; last by rewrite eq_sym. + by rewrite /cput/= Hr nth_error_set_nth// coerce_None// eq_sym. + subst T2. + rewrite coerce_Some bindE/=. + have ? := JMeq_eq H; subst s2. + by rewrite /cput -Hr. + + move=> _. + have [v r2v|T2' s Hr2 T2s|Hr2] := ntherrorP e r2; last first. + * rewrite MS_bindE None_cput/=; last first. + by rewrite (nth_error_set_nth_none _ _ Hr2 Hr1). + by rewrite None_cput. + * rewrite MS_bindE. + rewrite [in RHS](nocoerce_cput _ _ T2s)// bindfailf. + rewrite (nocoerce_cput _ _ T2s)//=. + by rewrite (nth_error_set_nth_other _ _ _ Hr2) 1?eq_sym. + * rewrite MS_bindE. + rewrite [in RHS](Some_cputE _ r2v). + rewrite {1}/cput/=. + rewrite (nth_error_set_nth_other _ _ _ r2v) 1?eq_sym//. + rewrite coerce_Some. + rewrite bindE/=. + rewrite /cput (nth_error_set_nth_other _ _ Hr Hr1). + rewrite coerce_Some. + by rewrite set_set_nth (negbTE Hr). +Qed. + +Lemma cputgetC T1 T2 (r1 : loc T1) (r2 : loc T2) (s1 : coq_type M T1) + (A : UU0) (k : coq_type M T2 -> M A) : + loc_id r1 != loc_id r2 -> + cput r1 s1 >> cget r2 >>= k = cget r2 >>= (fun v => cput r1 s1 >> k v). +Proof. +move=> Hr. +apply/boolp.funext => e /=. +rewrite !bindA. +rewrite bindE /= /bindS MS_mapE /= fmapE /= bindA /=. +rewrite [in RHS]bindE /= /bindS MS_mapE /= fmapE /= bindA /= /cput /cget. +case Hr1: (nth_error _ _) => [[T1' u]|]; last first. + rewrite bindfailf. + case Hr2: (nth_error _ _) => [[T2' v]|]; last by rewrite bindfailf. + case Hc: (coerce T2 v) => [u|]; last by rewrite bindfailf. + by rewrite !bindE /= !bindE /= /bindS MS_mapE /= fmapE Hr1 bindfailf. +case Hr2: (nth_error _ _) => [[T2' v]|]; last first. + rewrite bindfailf. + case Hc: (coerce T1' s1) => [v|]; last by rewrite bindfailf. + rewrite !bindE /= !bindE /= /bindS MS_mapE /= fmapE. + by rewrite (nth_error_set_nth_none _ _ Hr2 Hr1) bindfailf. +case: (eqVneq T1 T1') => HT1; last first. + rewrite coerce_None//. + rewrite bindfailf. + case: (eqVneq T2' T2) => HT2; last by rewrite coerce_None// bindfailf. + subst T2'. + rewrite coerce_Some. + rewrite bindE/= bindE/= bindE/= /bindS /= MS_mapE /= fmapE Hr1. + by rewrite coerce_None. +subst T1'. +rewrite coerce_Some//. +rewrite bindE /= bindE /= bindE /= /bindS /= MS_mapE /= fmapE. +rewrite (nth_error_set_nth_other _ _ _ Hr2) 1?eq_sym//. +case: (eqVneq T2' T2) => HT2'; last by rewrite coerce_None. +subst T2'. +rewrite coerce_Some bindE /= bindE /= bindE /= bindE /=. +rewrite /bindS /= MS_mapE /= fmapE Hr1. +by rewrite coerce_Some. +Qed. + +Lemma cputnewC T T' (r : loc T) (s : coq_type M T) (s' : coq_type M T') A + (k : loc T' -> M A) : + cget r >> (cnew s' >>= fun r' => cput r s >> k r') = + cput r s >> (cnew s' >>= k). +Proof. +apply/boolp.funext => e /=. +rewrite bindE /= /bindS MS_mapE /= fmapE /= bindA /=. +rewrite [in RHS]bindE /= /bindS MS_mapE /= fmapE /= bindA /= /cget /cput. +case Hr: (nth_error _ _) => [[T1 u]|]; last by rewrite bindfailf. +case: (eqVneq T1 T) => H //=; last by rewrite coerce_None// 1?eq_sym// coerce_None// eq_sym. +subst T1. +rewrite [in LHS]coerce_Some//. +rewrite bindE /= /bindS /= bindE /= bindE /= /bindS /= MS_mapE /= fmapE /=. +rewrite bindE /= /bindS /= bindE /= bindE /= /bindS /= MS_mapE /= fmapE /=. +rewrite (nth_error_rcons_some _ Hr). +rewrite coerce_Some. +rewrite bindE /= /bindS /= bindE /= bindE /= /bindS /= MS_mapE /= fmapE /=. +rewrite bindE /= /bindS /=. +rewrite /fresh_loc/=. +rewrite (nth_error_size_set_nth _ _ Hr). +by rewrite (nth_error_set_nth_rcons _ _ _ Hr). +Qed. + +Definition crunret (A B : UU0) (m : M A) (s : B) : + crun m -> crun (m >> Ret s) = Some s. +Proof. +rewrite /crun /= bindE /= /bindS MS_mapE /= fmapE /= bindA /=. +by case Hm: (m [::]). +Qed. + +Definition crunskip : crun skip = Some tt. +Proof. by []. Qed. + +Definition crunnew (A : UU0) T (m : M A) (s : A -> coq_type M T) : + crun m -> crun (m >>= fun x => cnew (s x)). +Proof. +rewrite /crun /= bindE /= /bindS MS_mapE /= fmapE /= bindA /=. +by case Hm: (m [::]). +Qed. + +Definition crunnewget (A : UU0) T (m : M A) (s : A -> coq_type M T) : + crun m -> crun (m >>= fun x => cnew (s x) >>= @cget T). +Proof. +rewrite /crun /= bindE /= /bindS MS_mapE /= fmapE /= bindA /=. +case Hm: (m [::]) => [|[a b]] // _. +by rewrite bindE /= bindE /= -(bindmret (_ >>= _)) bindA cnewget bindE. +Qed. + +Definition crungetnew (A : UU0) T1 T2 (m : M A) (r : A -> loc T1) + (s : A -> coq_type M T2) : + crun (m >>= fun x => cget (r x)) -> + crun (m >>= fun x => cnew (s x) >> cget (r x)). +Proof. +rewrite /crun /= !bindE /= /bindS !MS_mapE /= !fmapE /= !bindA /=. +case Hm: (m [::]) => [|[a b]] //. +rewrite !bindE /= !bindE /= /bindS MS_mapE /= fmapE /= bindA. +rewrite !bindE /= !bindE /= /cget. +case Hnth: nth_error => [[]|] //. +rewrite (nth_error_rcons_some _ Hnth). +by case Hcoe: coerce. +Qed. + +Definition crungetput (A : UU0) T (m : M A) (r : A -> loc T) + (s : A -> coq_type M T) : + crun (m >>= fun x => cget (r x)) -> + crun (m >>= fun x => cput (r x) (s x)). +Proof. +rewrite /crun /= !bindE /= /bindS !MS_mapE /= !fmapE /= !bindA /=. +case Hm: (m _) => [|[a b]] //=. +rewrite !bindE /= !bindE /= /cget /cput /=. +case Hnth: nth_error => [[T' v]|] //. +case: (eqVneq T' T) => T'T; last first. + by rewrite coerce_None// 1?eq_sym// coerce_None. +subst T'. +by rewrite !coerce_Some. +Qed. + +HB.instance Definition _ := Monad.on M. +HB.instance Definition isMonadTypedStoreModel := + isMonadTypedStore.Build MLU locT_nat M cnewget cnewput cgetput cgetputskip + cgetget cputget cputput cgetC cgetnewD cgetnewE cgetputC cputC + cputgetC cputnewC + crunret crunskip crunnew crunnewget crungetnew crungetput. + +End mkbind. +End ModelTypedStore. +End ModelTypedStore. + (* TODO? (* result of a discussion with Maxime and Enrico on 2019-09-12 *) (* Equality between monads from the hierarchy and their counterparts built *) @@ -1858,7 +2381,7 @@ End examples_of_algebraic_lifting. Module ModelMonadStateRun. Section modelmonadstaterun. Variable S : UU0. -Let N : monad := [the monad of ExceptMonad.acto unit]. +Let N : monad := option_monad. Definition M : stateMonad S := [the stateMonad S of stateT S N]. Let runStateT : forall A : UU0, M A -> S -> N (A * S)%type := fun A : UU0 => id. @@ -1891,7 +2414,7 @@ HB.export ModelMonadStateRun. Module ModelMonadExceptStateRun. Section modelmonadexceptstaterun. Variable S : UU0. -Let N : exceptMonad := [the exceptMonad of ExceptMonad.acto unit]. +Let N : exceptMonad := option_monad. Definition M : stateRunMonad S N := [the stateRunMonad S N of MS S N]. Definition failure : forall A, MS S N A := fun A => liftS (@fail N A). diff --git a/monad_transformer.v b/monad_transformer.v index 487b26a3..6e6c3ba2 100644 --- a/monad_transformer.v +++ b/monad_transformer.v @@ -145,14 +145,18 @@ by rewrite [in RHS]bindretf. Qed. HB.instance Definition _ := isMonadM_ret_bind.Build - M [the monad of MS] liftS retliftS bindliftS. + M MS liftS retliftS bindliftS. End state_monad_transformer. +Lemma MS_bindE [S : UU0] [M : monad] [A B : UU0] (m : MS S M A) (f : A -> MS S M B) s : + (m >>= f) s = m s >>= uncurry f. +Proof. by []. Qed. + Definition stateT (S : UU0) := fun M => [the monad of MS S M]. HB.instance Definition _ (S : UU0) := isMonadT.Build - (stateT S) (fun M => [the monadM _ _ of @liftS S M]). + (stateT S) (@liftS S). Definition mapStateT2 (A S : UU0) (N1 N2 N3 : monad) (f : N1 (A * S)%type -> N2 (A * S)%type -> N3 (A * S)%type) diff --git a/monae_lib.v b/monae_lib.v index 81dc4417..8075f59a 100644 --- a/monae_lib.v +++ b/monae_lib.v @@ -6,16 +6,18 @@ Require ProofIrrelevance. Definition proof_irr := boolp.Prop_irrelevance. -Definition eq_rect_eq := @ProofIrrelevance.ProofIrrelevanceTheory.Eq_rect_eq.eq_rect_eq. +Definition eq_rect_eq := + @ProofIrrelevance.ProofIrrelevanceTheory.Eq_rect_eq.eq_rect_eq. Definition funext_dep := boolp.functional_extensionality_dep. (******************************************************************************) (* Shared notations and easy definitions/lemmas of general interest *) (* *) -(* foldr1 *) -(* curry/uncurry == currying for pairs *) -(* curry3/uncurry3 == currying for triples *) +(* foldr1 *) +(* curry/uncurry == currying for pairs *) +(* curry3/uncurry3 == currying for triples *) +(* coerce T1 (v : f T1) == some (f T2) if T1 = T2 and None o.w. *) (* *) (******************************************************************************) @@ -141,3 +143,90 @@ Proof. by []. Qed. Lemma if_pair A B b (x : A) y (u : A) (v : B) : (if b then (x, y) else (u, v)) = (if b then x else u, if b then y else v). Proof. by case: ifPn. Qed. + +Lemma iteriSr T n (f : nat -> T -> T) x : + iteri n.+1 f x = iteri n (f \o succn) (f 0 x). +Proof. by elim: n x => // n IH x /=; rewrite -IH. Qed. + +Lemma iteriD T n m (f : nat -> T -> T) x : + iteri (n + m) f x = iteri m (f \o addn n) (iteri n f x). +Proof. by elim: n x f => // n IH x f; rewrite addSn iteriSr IH iteriSr. Qed. + +Section nth_error. +Context [T : Type] (def : T) (st : seq T). + +(* Basic lemmas for standard library's nth_error *) +Local Notation nth_error := List.nth_error. + +Lemma nth_error_set_nth n x : nth_error (set_nth def st n x) n = Some x. +Proof. +elim: n st => [|z IH] [] // {IH}. +elim: z.+1 => [|n <-] //=. +by rewrite set_nth_nil. +Qed. + +Lemma nth_error_rcons_size b : nth_error (rcons st b) (size st) = Some b. +Proof. by elim: st. Qed. + +Lemma nth_error_rcons_some n a b : + nth_error st n = Some a -> nth_error (rcons st b) n = Some a. +Proof. by elim: n st => [|n IH] []. Qed. + +Lemma nth_error_set_nth_id n a : + nth_error st n = Some a -> set_nth def st n a = st. +Proof. by elim: n st => [|n IH] [] //= b st'; [case=> -> | move/IH ->]. Qed. + +Lemma nth_error_set_nth_other m n a b : + m != n -> + nth_error st m = Some a -> + nth_error (set_nth def st n b) m = Some a. +Proof. +elim: m st n => [|m IH] [|c st'] [|n] //=; rewrite eqSS => *; exact: IH. +Qed. + +Lemma nth_error_set_nth_none m n a b : + nth_error st m = None -> + nth_error st n = Some a -> + nth_error (set_nth def st n b) m = None. +Proof. by elim: m st n => [|m IH] [|c st'] [|n] //=; apply IH. Qed. + +Lemma nth_error_size n a : nth_error st n = Some a -> n < size st. +Proof. by elim: n st => [|n IH] [|c st'] //= /IH. Qed. + +Lemma nth_error_size_set_nth n a b : + nth_error st n = Some a -> size (set_nth def st n b) = size st. +Proof. by rewrite size_set_nth => /nth_error_size /maxn_idPr. Qed. + +Lemma set_nth_rcons a b : set_nth def (rcons st a) (size st) b = rcons st b. +Proof. by elim: st => //= c st' ->. Qed. + +Lemma nth_error_set_nth_rcons n a b c : + nth_error st n = Some a -> + set_nth def (rcons st c) n b = rcons (set_nth def st n b) c. +Proof. by elim: n st => [|n IH] [|d st'] //= /IH ->. Qed. +End nth_error. +Arguments nth_error_size {T st n a}. + +Section coerce. +Variables (X : eqType) (f : X -> Type). + +Definition coerce (T1 T2 : X) (v : f T1) : option (f T2) := + if @eqP _ T1 T2 is ReflectT H then Some (eq_rect _ _ v _ H) else None. + +Lemma coerce_sym (T T' : X) (s : f T) (s' : f T') : coerce T' s -> coerce T s'. +Proof. +by rewrite /coerce; case: eqP => //= h; case: eqP => //; rewrite h; auto. +Qed. + +Lemma coerce_Some (T : X) (s : f T) : coerce T s = Some s. +Proof. +by rewrite /coerce; case: eqP => /= [?|]; [rewrite -eq_rect_eq|auto]. +Qed. + +Lemma coerce_eq (T T' : X) (s : f T) : coerce T' s -> T = T'. +Proof. by rewrite /coerce; case: eqP. Qed. + +Lemma coerce_None (T T' : X) (s : f T) : T != T' -> coerce T' s = None. +Proof. by rewrite /coerce; case: eqP. Qed. + +End coerce. diff --git a/typed_store_lib.v b/typed_store_lib.v new file mode 100644 index 00000000..4a3b2cbe --- /dev/null +++ b/typed_store_lib.v @@ -0,0 +1,103 @@ +(* monae: Monadic equational reasoning in Coq *) +(* Copyright (C) 2023 monae authors, license: LGPL-2.1-or-later *) +Ltac typeof X := type of X. + +Require Import ssrmatching Reals JMeq. +From mathcomp Require Import all_ssreflect. +From mathcomp Require boolp. +From infotheo Require Import Reals_ext. +Require Import monae_lib hierarchy. + +(******************************************************************************) +(* Lemmas using the typed store monad *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope monae_scope. + +Section cchk. +Variables (MLU : ML_universe) (locT : eqType) (M : typedStoreMonad MLU locT). +Notation loc := (@loc MLU locT). +Definition cchk T (r : loc T) : M unit := cget r >> skip. + +Lemma cnewchk T s (A : UU0) (k : loc T -> M A) : + cnew T s >>= (fun r => cchk r >> k r) = cnew T s >>= k. +Proof. +under eq_bind do rewrite bindA. +rewrite cnewget. +by under eq_bind do rewrite bindskipf. +Qed. + +Lemma cchknewC T1 T2 (r : loc T1) s (A : UU0) (k : loc T2 -> M A) : + cchk r >> (cnew T2 s >>= fun r' => cchk r >> k r') = + cchk r >> (cnew T2 s >>= k). +Proof. +rewrite !(bindA,bindskipf). +under eq_bind do under eq_bind do rewrite bindA. +rewrite cgetnewD. +by under eq_bind do under eq_bind do rewrite bindskipf. +Qed. + +Lemma cchkgetC T1 T2 (r1: loc T1) (r2: loc T2) (A: UU0) + (k: coq_type M T2 -> M A) : + cchk r1 >> (cget r2 >>= k) = cget r2 >>= (fun s => cchk r1 >> k s). +Proof. +under [in RHS]eq_bind do rewrite bindA bindskipf. +by rewrite !(bindA,bindskipf) cgetC. +Qed. + +Lemma cchknewE T1 T2 (r1 : loc T1) s (A : UU0) (k1 k2 : loc T2 -> M A) : + (forall r2 : loc T2, loc_id r1 != loc_id r2 -> k1 r2 = k2 r2) -> + cchk r1 >> (cnew T2 s >>= k1) = cchk r1 >> (cnew T2 s >>= k2). +Proof. move=> Hk; rewrite !(bindA,bindskipf); exact: cgetnewE. Qed. + +Lemma cchknewget T T' (r : loc T) s (A : UU0) k : + cchk r >> (cnew T' s >>= fun r' => cget r >>= k r') = + cget r >>= (fun u => cnew T' s >>= k ^~ u) :> M A. +Proof. by rewrite bindA bindskipf cgetnewD. Qed. + +Lemma cchknewput T T' (r : loc T) s s' (A : UU0) k : + cchk r >> (cnew T' s' >>= fun r' => cput r s >> k r') = + cput r s >> (cnew T' s' >>= k) :> M A. +Proof. by rewrite bindA bindskipf cputnewC. Qed. + +Lemma cchkget T (r : loc T) (A: UU0) (k : coq_type M T -> M A) : + cchk r >> (cget r >>= k) = cget r >>= k. +Proof. by rewrite bindA bindskipf cgetget. Qed. + +Lemma cgetchk T (r : loc T) (A: UU0) (k : coq_type M T -> M A) : + cget r >>= (fun s => cchk r >> k s) = cget r >>= k. +Proof. under eq_bind do rewrite bindA bindskipf; by rewrite cgetget. Qed. + +Lemma cchkputC T1 T2 (r1 : loc T1) (r2 : loc T2) (s : coq_type M T2) : + cchk r1 >> cput r2 s = cput r2 s >> cchk r1. +Proof. by rewrite bindA bindskipf cgetputC bindA. Qed. + +Lemma cchkput T (r : loc T) (s : coq_type M T) : + cchk r >> cput r s = cput r s. +Proof. by rewrite bindA bindskipf cgetput. Qed. + +Lemma cputchk T (r : loc T) (s : coq_type M T) : + cput r s >> cchk r = cput r s. +Proof. by rewrite cputget bindmskip. Qed. + +Lemma cchkC T1 T2 (r1: loc T1) (r2: loc T2) : + cchk r1 >> cchk r2 = cchk r2 >> cchk r1. +Proof. by rewrite !(bindA,bindskipf) cgetC. Qed. + +Lemma cchkdup T (r : loc T) : cchk r >> cchk r = cchk r. +Proof. by rewrite bindA bindskipf cgetget. Qed. + +Lemma cgetret T (r : loc T) : cget r >>= Ret = cget r :> M _. +Proof. by rewrite bindmret. Qed. + +Lemma crunnew0 T s : crun (cnew T s : M _). +Proof. by rewrite -(bindskipf (cnew T s)) crunnew // crunskip. Qed. + +Lemma cnewgetret T s : cnew T s >>= @cget _ _ _ _ = cnew T s >> Ret s :> M _. +Proof. under eq_bind do rewrite -cgetret; by rewrite cnewget. Qed. +End cchk. +Arguments cchk {MLU locT M} [T]. diff --git a/typed_store_model.v b/typed_store_model.v new file mode 100644 index 00000000..fc6d738c --- /dev/null +++ b/typed_store_model.v @@ -0,0 +1,569 @@ +(* monae: Monadic equational reasoning in Coq *) +(* Copyright (C) 2023 monae authors, license: LGPL-2.1-or-later *) +Require Import JMeq. +From mathcomp Require Import all_ssreflect finmap. +From mathcomp Require boolp. +#[local] Remove Hints boolp.Prop_irrelevance : core. +Require Import monae_lib. +From HB Require Import structures. +Require Import hierarchy monad_lib fail_lib state_lib trace_lib. +Require Import monad_transformer monad_model. + +(******************************************************************************) +(* Model for typed store *) +(* *) +(* Separate file as it requires disabling various sanity checks. *) +(* Reuses coerce and locT_nat from monad_model.v. *) +(* Similarities with ModelTypedStore from monad_model.v *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope monae_scope. + +Section ModelTypedStore. +Variable MLU : ML_universe. + +Record binding (M : Type -> Type) := + mkbind { bind_type : MLU; bind_val : coq_type M bind_type }. +Arguments mkbind {M bind_type}. + +Definition M0 Env (T : UU0) := MS Env option_monad T. + +End ModelTypedStore. + +#[bypass_check(positivity)] +Inductive Env (MLU : ML_universe) := + mkEnv : seq (binding MLU (M0 (Env _))) -> Env _. + +Section ModelTypedStore_contd. +Variable MLU : ML_universe. + +Definition ofEnv (e : Env MLU) := let: mkEnv e := e in e. +Definition sizeEnv e := size (ofEnv e). + +Local Notation mkEnv := (@mkEnv MLU). +Local Notation Env := (@Env MLU). + +Definition acto : UU0 -> UU0 := MS Env option_monad. +Local Notation M := acto. + +Local Notation coq_type := (@coq_type MLU M). + +Local Notation val_nonundef := (val_nonempty MLU). + +Definition def := mkbind (val_nonempty MLU M). + +Local Notation nth_error := List.nth_error. + +Definition extend_env T (v : coq_type T) (e : Env) := + mkEnv (rcons (ofEnv e) (mkbind v)). +Definition fresh_loc (T : MLU) (e : Env) := mkloc T (sizeEnv e). + +Local Notation loc := (@loc MLU locT_nat). + +Definition cnew T (v : coq_type T) : M (loc T) := + fun e => inr (fresh_loc T e, extend_env v e). + +Definition cget T (r : loc T) : M (coq_type T) := + fun st => + if nth_error (ofEnv st) (loc_id r) is Some (mkbind T' v) then + if coerce T v is Some u then inr (u, st) else inl tt + else inl tt. + +Definition cput T (r : loc T) (v : coq_type T) : M unit := + fun st => + let n := loc_id r in + if nth_error (ofEnv st) n is Some (mkbind T' _) then + if coerce T' v is Some u then + let b := mkbind (u : coq_type T') in + inr (tt, mkEnv (set_nth def (ofEnv st) n b)) + else inl tt + else inl tt. + +Definition crun (A : UU0) (m : M A) : option A := + match m (mkEnv nil) with + | inl _ => None + | inr (a, _) => Some a + end. + +Lemma bind_cnew T (s : coq_type T) A (k : loc T -> M A) e : + (cnew s >>= k) e = k (fresh_loc T e) (extend_env s e). +Proof. by case: e. Qed. + +Lemma Some_cget T (r : loc T) (s : coq_type T) e (A : UU0) (f : coq_type T -> M A) : + nth_error (ofEnv e) (loc_id r) = Some (mkbind s) -> + (cget r >>= f) e = f s e. +Proof. by move=> H; rewrite MS_bindE /cget H coerce_Some. Qed. +Arguments Some_cget {T r} s. + +Lemma nocoerce_cget T (r : loc T) T' (s' : coq_type T') e : + nth_error (ofEnv e) (loc_id r) = Some (mkbind s') -> + ~ coerce T s' -> + cget r e = fail. +Proof. by move=> H Ts'; rewrite /cget H; case: coerce Ts'. Qed. + +Lemma None_cget T (r : loc T) e : + nth_error (ofEnv e) (loc_id r) = None -> + cget r e = fail. +Proof. by move=> H; rewrite /cget H. Qed. + +(* Prove the laws *) +Lemma cnewget T (s : coq_type T) A (k : loc T -> coq_type T -> M A) : + cnew s >>= (fun r => cget r >>= k r) = cnew s >>= (fun r => k r s). +Proof. +apply/boolp.funext => e. +by rewrite bind_cnew (Some_cget s)// nth_error_rcons_size. +Qed. + +Lemma nocoerce_cput T (r : loc T) (s : coq_type T) T' (s' : coq_type T') e : + nth_error (ofEnv e) (loc_id r) = Some (mkbind s') -> + ~ coerce T s' -> + cput r s e = fail. +Proof. +move=> H Ts'; move: e H => [e] H; rewrite /cput H. +have {}Ts' : ~ coerce T' s by apply: contra_not Ts'; exact: coerce_sym. +by case: coerce Ts'. +Qed. + +Lemma None_cput T (r : loc T) (s : coq_type T) e : + nth_error (ofEnv e) (loc_id r) = None -> + cput r s e = fail. +Proof. by move=> H; move: e H => [e] H; rewrite /cput H. Qed. + +Lemma cnewput T (s t : coq_type T) A (k : loc T -> M A) : + cnew s >>= (fun r => cput r t >> k r) = cnew t >>= k. +Proof. +apply/boolp.funext => e. +rewrite bind_cnew 2!MS_bindE. +by rewrite /cput/= nth_error_rcons_size coerce_Some set_nth_rcons. +Qed. + +(* +Definition permutable T1 T2 (A : UU0) (k : loc T1 -> loc T2 -> M A) := + forall (n1 n2 : nat) (b1 b2 : binding M) (st : seq (binding M)), + k (mkloc T1 n1) (mkloc T2 n2) + (mkEnv (set_nth def (set_nth def st n1 b1) n2 b2)) = + k (mkloc T1 n2) (mkloc T2 n1) + (mkEnv (set_nth def (set_nth def st n2 b1) n1 b2)). + +Lemma cnewC T1 T2 (s : coq_type T1) (t : coq_type T2) + A (k : loc T1 -> loc T2 -> M A) : + permutable k -> + cnew s >>= (fun r => cnew t >>= k r) = + cnew t >>= (fun r => cnew s >>= k^~ r). +Proof. +move=> pmk. +apply/boolp.funext => -[st]. +rewrite !bind_cnew /fresh_loc /extend_env /= size_rcons. +Abort. +*) + +Variant nth_error_spec (T : MLU) (e : Env) (r : loc T) : Type := + | NthError : forall s : coq_type T, + nth_error (ofEnv e) (loc_id r) = Some (mkbind s) -> nth_error_spec e r + | NthError_nocoerce : forall T' (s' : coq_type T'), + nth_error (ofEnv e) (loc_id r) = Some (mkbind s') -> ~ coerce T s' -> + nth_error_spec e r + | NthError_None : nth_error (ofEnv e) (loc_id r) = None -> nth_error_spec e r. + +Lemma ntherrorP (T : MLU) (e : Env) (r : loc T) : nth_error_spec e r. +Proof. +case H : (nth_error (ofEnv e) (loc_id r)) => [[T' s']|]. + have [Ts'|Ts'] := boolp.pselect (coerce T s'). + have ? := coerce_eq Ts'; subst T'. + exact: NthError H. + exact: NthError_nocoerce H Ts'. +exact: NthError_None. +Qed. + +Lemma cgetput T (r : loc T) (s : coq_type T) : cget r >> cput r s = cput r s. +Proof. +apply/boolp.funext => e. +have [s' H|T' s' H Ts'|H] := ntherrorP e r. +- by rewrite (Some_cget s'). +- by rewrite MS_bindE (nocoerce_cget H)// (nocoerce_cput _ H). +- by rewrite MS_bindE None_cget// None_cput. +Qed. + +(* TODO: at least rename *) +Lemma Some_cputE T (r : loc T) (s s' : coq_type T) e : + nth_error (ofEnv e) (loc_id r) = Some (mkbind s') -> + cput r s e = inr (tt, mkEnv (set_nth def (ofEnv e) (loc_id r) (mkbind s))). +Proof. by move=> H; rewrite /cput/= H coerce_Some. Qed. + +Lemma Some_cput T (r : loc T) (s : coq_type T) e : + nth_error (ofEnv e) (loc_id r) = Some (mkbind s) -> + cput r s e = (@skip M) e. +Proof. +move=> H. +rewrite /cput/= H coerce_Some/= nth_error_set_nth_id//. +by destruct e. +Qed. + +Lemma Some_cputget T (s' s : coq_type T) (r : loc T) A (k : coq_type T -> M A) + (e : Env) : + nth_error (ofEnv e) (loc_id r) = Some (mkbind s') -> + (cput r s >> (cget r >>= k)) e = (cput r s >> k s) e. +Proof. +move=> H. +rewrite 2!MS_bindE (Some_cputE _ H). +by rewrite bindE/= (Some_cget s)// nth_error_set_nth. +Qed. +Arguments Some_cputget {T} s'. + +Lemma cgetputskip T (r : loc T) : cget r >>= cput r = cget r >> skip. +Proof. +apply/boolp.funext => e /=. +have [s' H|T' s' H Ts'|H] := ntherrorP e r. +- by rewrite (Some_cget s')// (Some_cget s')// (Some_cput H). +- by rewrite !MS_bindE (nocoerce_cget H). +- by rewrite !MS_bindE None_cget. +Qed. + +Lemma cgetget T (r : loc T) (A : UU0) (k : coq_type T -> coq_type T -> M A) : + cget r >>= (fun s => cget r >>= k s) = cget r >>= fun s => k s s. +Proof. +apply/boolp.funext => e /=. +have [s' H|T' s' H Ts'|H] := ntherrorP e r. +- by do 3 rewrite (Some_cget s')//. +- by rewrite !MS_bindE (nocoerce_cget H). +- by rewrite !MS_bindE None_cget. +Qed. + +Lemma cputget T (r : loc T) (s: coq_type T) (A: UU0) (k: coq_type T -> M A) : + cput r s >> (cget r >>= k) = cput r s >> k s. +Proof. +apply/boolp.funext => e /=. +have [s' H|T' s' H Ts'|H] := ntherrorP e r. +- by rewrite (Some_cputget s'). +- by rewrite !MS_bindE (nocoerce_cput _ H). +- by rewrite 2!MS_bindE None_cput. +Qed. + +Lemma Some_cputput (T : MLU) (r : loc T) (s s' : coq_type T) + (e : Env) (s'' : coq_type T) : + nth_error (ofEnv e) (loc_id r) = Some (mkbind s'') -> + (cput r s >> cput r s') e = cput r s' e. +Proof. +move=> H. +rewrite MS_bindE/=. +rewrite [in LHS](Some_cputE _ H)//. +rewrite [in RHS](Some_cputE _ H)//. +rewrite bindE/= /cput. +rewrite nth_error_set_nth coerce_Some/=. +by rewrite set_set_nth eqxx. +Qed. + +Lemma cputput T (r : loc T) (s s' : coq_type T) : + cput r s >> cput r s' = cput r s'. +Proof. +apply/boolp.funext => e. +have [s'' H|T'' s'' H Ts''|H] := ntherrorP e r. +- by rewrite (Some_cputput _ _ H). +- by rewrite !MS_bindE (nocoerce_cput _ H)// (nocoerce_cput _ H). +- by rewrite MS_bindE !None_cput. +Qed. + +Lemma cgetC T1 T2 (r1 : loc T1) (r2 : loc T2) (A : UU0) + (k : coq_type T1 -> coq_type T2 -> M A) : + cget r1 >>= (fun u => cget r2 >>= (fun v => k u v)) = + cget r2 >>= (fun v => cget r1 >>= (fun u => k u v)). +Proof. +apply/boolp.funext => e /=. +have [u Hr1|u T1' Hr1 T1u|Hr1] := ntherrorP e r1. +- rewrite (Some_cget u)//. + have [v Hr2|v T2' Hr2 T2v|Hr2] := ntherrorP e r2. + + by rewrite (Some_cget v)// (Some_cget v)// (Some_cget u). + + by rewrite 2!MS_bindE (nocoerce_cget Hr2)// bindfailf. + + by rewrite !MS_bindE None_cget. +- rewrite MS_bindE (nocoerce_cget Hr1)// bindfailf. + have [v Hr2|v T2' Hr2 T2v|Hr2] := ntherrorP e r2. + + by rewrite (Some_cget v)// MS_bindE (nocoerce_cget Hr1). + + by rewrite MS_bindE (nocoerce_cget Hr2). + + by rewrite MS_bindE None_cget. +- rewrite MS_bindE None_cget// bindfailf. + have [v Hr2|v T2' Hr2 T2v|Hr2] := ntherrorP e r2. + + by rewrite (Some_cget v)// MS_bindE None_cget. + + by rewrite MS_bindE (nocoerce_cget Hr2). + + by rewrite MS_bindE !None_cget. +Qed. + +(* NB: this is similar to the cnewget law *) +Lemma cnewgetD_helper e T T' r v (s : coq_type T') A (k : loc T' -> coq_type T -> M A) : + nth_error (ofEnv e) (loc_id r) = Some (mkbind v) -> + (cnew s >>= (fun r' => cget r >>= k r')) e = (cnew s >>= (fun r => k r v)) e. +Proof. +move=> H. +rewrite bind_cnew//. +by rewrite (Some_cget v) // (nth_error_rcons_some _ H). +Qed. + +Lemma cgetnewD T T' (r : loc T) (s : coq_type T') A + (k : loc T' -> coq_type T -> coq_type T -> M A) : + cget r >>= (fun u => cnew s >>= fun r' => cget r >>= k r' u) = + cget r >>= (fun u => cnew s >>= fun r' => k r' u u). +Proof. +apply/boolp.funext => e. +have [u Hr|u T1 Hr T1u|Hr] := ntherrorP e r. +- by rewrite (Some_cget u)// (Some_cget u)// (cnewgetD_helper _ _ Hr)//. +- by rewrite !MS_bindE (nocoerce_cget Hr). +- by rewrite !MS_bindE None_cget. +Qed. + +Lemma cgetnewE T1 T2 (r1 : loc T1) (s : coq_type T2) (A : UU0) + (k1 k2 : loc T2 -> M A) : + (forall r2 : loc T2, loc_id r1 != loc_id r2 -> k1 r2 = k2 r2) -> + cget r1 >> (cnew s >>= k1) = cget r1 >> (cnew s >>= k2). +Proof. +move=> Hk. +apply/boolp.funext => e. +have [u r1u|T' s' Hr1 T1s'|Hr] := ntherrorP e r1. +- rewrite (Some_cget u)// (Some_cget u)// !bind_cnew Hk// neq_ltn. + by case: e r1u => /= e /nth_error_size ->. +- by rewrite !MS_bindE (nocoerce_cget Hr1). +- by rewrite !MS_bindE None_cget. +Qed. + +(* TODO: do not rely on bindE to pass option and do not unfold cget *) +Lemma cgetputC T1 T2 (r1 : loc T1) (r2 : loc T2) (s : coq_type T2) : + cget r1 >> cput r2 s = cput r2 s >> cget r1 >> skip. +Proof. +apply/boolp.funext => e /=. +have [u r1u|T1' v1 Hr1 T1v1|Hr1] := ntherrorP e r1. +- rewrite (Some_cget u)// [in RHS]bindA MS_bindE. + have [v r2v|T' v r2v T2v|Hr2] := ntherrorP e r2. + + rewrite (Some_cputE _ r2v) [in RHS]bindE/=. + have [r12|r12] := eqVneq (loc_id r1) (loc_id r2). + move: r2v; rewrite -r12 r1u => -[?] _; subst T2. + by rewrite MS_bindE /cget nth_error_set_nth// coerce_Some. + by rewrite (Some_cget u)// (nth_error_set_nth_other _ _ r12 r1u). + + by rewrite (nocoerce_cput _ _ T2v). + + by rewrite None_cput. +- rewrite MS_bindE [RHS]MS_bindE bindA. + have [v r2v|T' v r2v T2v|Hr2] := ntherrorP e r2. + + rewrite {1}/cget Hr1. + have [?|T1'T1] := eqVneq T1' T1. + * subst T1'; rewrite coerce_Some. + rewrite [in LHS]bindE/= (Some_cputE _ r2v) [in RHS]bindE/=. + have [Hr|Hr] := eqVneq (loc_id r1) (loc_id r2). + move: r2v; rewrite -Hr Hr1 => -[?] _; subst T2. + by rewrite /cget nth_error_set_nth coerce_Some. + by rewrite /cget (nth_error_set_nth_other _ _ Hr Hr1) coerce_Some. + * rewrite coerce_None//= bindfailf (Some_cputE _ r2v) [in RHS]bindE/=. + have [r12|r12] := eqVneq (loc_id r1) (loc_id r2). + move: r2v; rewrite -r12 Hr1 => -[?] _; subst T1'. + by rewrite /cget nth_error_set_nth coerce_None. + by rewrite /cget (nth_error_set_nth_other _ _ r12 Hr1) coerce_None. + + by rewrite (nocoerce_cget _ T1v1)// bindfailf (nocoerce_cput _ _ T2v). + + by rewrite (nocoerce_cget _ T1v1)// None_cput// bindfailf. +- rewrite MS_bindE None_cget// bindfailf bindA MS_bindE. + have [v r2v|T' v r2v T2v|Hr2] := ntherrorP e r2. + + rewrite (Some_cputE _ r2v)/=. + rewrite bindE/=. + rewrite MS_bindE None_cget/= ?bindfailf//. + by rewrite (nth_error_set_nth_none _ _ Hr1 r2v). + + by rewrite (nocoerce_cput _ r2v). + + by rewrite None_cput. +Qed. + +Lemma cput_then_fail T1 T2 T1' e (s1' : coq_type T1') + (r2 : loc T2) (s2 : coq_type T2) + (r1 : loc T1) (s1 : coq_type T1) : + nth_error (ofEnv e) (loc_id r1) = Some (mkbind s1') -> + ~ coerce T1 s1' -> + (cput r2 s2 >> cput r1 s1) e = fail. +Proof. +move=> Hr1 T1s'. +have [v Hr2|T2' v Hr2 T2v|Hr2] := ntherrorP e r2; last first. +- by rewrite MS_bindE None_cput. +- by rewrite MS_bindE (nocoerce_cput _ _ T2v). +- rewrite MS_bindE (Some_cputE _ Hr2). + rewrite bindE/=. + have [Hr|Hr] := eqVneq (loc_id r1) (loc_id r2). + + rewrite {1}/cput -Hr /= nth_error_set_nth. + have [HT|HT] := eqVneq T1 T2; last by rewrite coerce_None. + subst T2. + rewrite coerce_Some//=. + move: Hr1; rewrite Hr Hr2 => -[?]; subst T1' => _. + by rewrite coerce_Some // in T1s'. + + rewrite (nocoerce_cput _ _ T1s')//=. + by rewrite (@nth_error_set_nth_other _ _ _ _ _ (mkbind s1')). +Qed. + +Lemma cputC T1 T2 (r1 : loc T1) (r2 : loc T2) (s1 : coq_type T1) + (s2 : coq_type T2) (A : UU0) : + loc_id r1 != loc_id r2 \/ JMeq s1 s2 -> + cput r1 s1 >> cput r2 s2 = cput r2 s2 >> cput r1 s1. +Proof. +move=> H; apply/boolp.funext => e /=. +have [u Hr1|T1' s'd Hr1 T1s'|Hr1] := ntherrorP e r1; last first. + rewrite MS_bindE None_cput// bindfailf. + have [v Hr2|T2' s' Hr2 T2s'|Hr2] := ntherrorP e r2; last first. + by rewrite MS_bindE None_cput. + + by rewrite MS_bindE (nocoerce_cput _ _ T2s'). + + rewrite MS_bindE (Some_cputE _ Hr2). + rewrite bindE/=. + by rewrite None_cput// (nth_error_set_nth_none _ _ Hr1 Hr2). +- rewrite MS_bindE (nocoerce_cput _ _ T1s')// bindfailf. + by rewrite (cput_then_fail _ _ _ Hr1). +- rewrite MS_bindE (Some_cputE _ Hr1)/=. + rewrite bindE/=. + case/boolP: (loc_id r1 == loc_id r2) H => [/eqP|] Hr /=. + + case => // H. + rewrite MS_bindE. + rewrite {2}/cput -Hr Hr1. + case/boolP: (T1 == T2) => [/eqP HT|HT]; last first. + rewrite coerce_None//; last by rewrite eq_sym. + by rewrite /cput/= Hr nth_error_set_nth// coerce_None// eq_sym. + subst T2. + rewrite coerce_Some bindE/=. + have ? := JMeq_eq H; subst s2. + by rewrite /cput -Hr. + + move=> _. + have [v r2v|T2' s Hr2 T2s|Hr2] := ntherrorP e r2; last first. + * rewrite MS_bindE None_cput/=; last first. + by rewrite (nth_error_set_nth_none _ _ Hr2 Hr1). + by rewrite None_cput. + * rewrite MS_bindE. + rewrite [in RHS](nocoerce_cput _ _ T2s)// bindfailf. + rewrite (nocoerce_cput _ _ T2s)//=. + by rewrite (nth_error_set_nth_other _ _ _ Hr2) 1?eq_sym. + * rewrite MS_bindE. + rewrite [in RHS](Some_cputE _ r2v). + rewrite {1}/cput/=. + rewrite (nth_error_set_nth_other _ _ _ r2v) 1?eq_sym//. + rewrite coerce_Some. + rewrite bindE/=. + rewrite /cput (nth_error_set_nth_other _ _ Hr Hr1). + rewrite coerce_Some. + by rewrite set_set_nth (negbTE Hr). +Qed. + +Lemma cputgetC T1 T2 (r1 : loc T1) (r2 : loc T2) (s1 : coq_type T1) + (A : UU0) (k : coq_type T2 -> M A) : + loc_id r1 != loc_id r2 -> + cput r1 s1 >> cget r2 >>= k = cget r2 >>= (fun v => cput r1 s1 >> k v). +Proof. +move=> Hr. +apply/boolp.funext => e /=. +rewrite !bindA. +rewrite bindE /= /bindS MS_mapE /= fmapE /= bindA /=. +rewrite [in RHS]bindE /= /bindS MS_mapE /= fmapE /= bindA /= /cput /cget. +case Hr1: (nth_error _ _) => [[T1' u]|]; last first. + rewrite bindfailf. + case Hr2: (nth_error _ _) => [[T2' v]|]; last by rewrite bindfailf. + case Hc: (coerce T2 v) => [u|]; last by rewrite bindfailf. + by rewrite !bindE /= !bindE /= /bindS MS_mapE /= fmapE Hr1 bindfailf. +case Hr2: (nth_error _ _) => [[T2' v]|]; last first. + rewrite bindfailf. + case Hc: (coerce T1' s1) => [v|]; last by rewrite bindfailf. + rewrite !bindE /= !bindE /= /bindS MS_mapE /= fmapE. + by rewrite (nth_error_set_nth_none _ _ Hr2 Hr1) bindfailf. +case: (eqVneq T1 T1') => HT1; last first. + rewrite coerce_None//. + rewrite bindfailf. + case: (eqVneq T2' T2) => HT2; last by rewrite coerce_None// bindfailf. + subst T2'. + rewrite coerce_Some. + rewrite bindE/= bindE/= bindE/= /bindS /= MS_mapE /= fmapE Hr1. + by rewrite coerce_None. +subst T1'. +rewrite coerce_Some//. +rewrite bindE /= bindE /= bindE /= /bindS /= MS_mapE /= fmapE. +rewrite (nth_error_set_nth_other _ _ _ Hr2) 1?eq_sym//. +case: (eqVneq T2' T2) => HT2'; last by rewrite coerce_None. +subst T2'. +rewrite coerce_Some bindE /= bindE /= bindE /= bindE /=. +rewrite /bindS /= MS_mapE /= fmapE Hr1. +by rewrite coerce_Some. +Qed. + +Lemma cputnewC T T' (r : loc T) (s : coq_type T) (s' : coq_type T') A + (k : loc T' -> M A) : + cget r >> (cnew s' >>= fun r' => cput r s >> k r') = + cput r s >> (cnew s' >>= k). +Proof. +apply/boolp.funext => e /=. +rewrite bindE /= /bindS MS_mapE /= fmapE /= bindA /=. +rewrite [in RHS]bindE /= /bindS MS_mapE /= fmapE /= bindA /= /cget /cput. +case Hr: (nth_error _ _) => [[T1 u]|]; last by rewrite bindfailf. +case: (eqVneq T1 T) => H //=; last by rewrite coerce_None// 1?eq_sym// coerce_None// eq_sym. +subst T1. +rewrite [in LHS]coerce_Some//. +rewrite bindE /= /bindS /= bindE /= bindE /= /bindS /= MS_mapE /= fmapE /=. +rewrite bindE /= /bindS /= bindE /= bindE /= /bindS /= MS_mapE /= fmapE /=. +rewrite (nth_error_rcons_some _ Hr). +rewrite coerce_Some. +rewrite bindE /= /bindS /= bindE /= bindE /= /bindS /= MS_mapE /= fmapE /=. +rewrite bindE /= /bindS /=. +rewrite /fresh_loc/=. +rewrite /sizeEnv/=. +rewrite (nth_error_size_set_nth _ _ Hr). +by rewrite (nth_error_set_nth_rcons _ _ _ Hr). +Qed. + +Lemma crunret (A B : UU0) (m : M A) (s : B) : + crun m -> crun (m >> Ret s) = Some s. +Proof. +rewrite /crun /= bindE /= /bindS MS_mapE /= fmapE /= bindA /=. +by case Hm: (m (mkEnv [::])). +Qed. + +Lemma crunskip : crun skip = Some tt. +Proof. by []. Qed. + +Lemma crunnew (A : UU0) T (m : M A) (s : A -> coq_type T) : + crun m -> crun (m >>= fun x => cnew (s x)). +Proof. +rewrite /crun /= bindE /= /bindS MS_mapE /= fmapE /= bindA /=. +by case Hm: (m _). +Qed. + +Lemma crunnewget (A : UU0) T (m : M A) (s : A -> coq_type T) : + crun m -> crun (m >>= fun x => cnew (s x) >>= @cget T). +Proof. +rewrite /crun /= bindE /= /bindS MS_mapE /= fmapE /= bindA /=. +case Hm: (m _) => [|[a b]] // _. +by rewrite bindE /= bindE /= -(bindmret (_ >>= _)) bindA cnewget bindE. +Qed. + +Lemma crungetnew (A : UU0) T1 T2 (m : M A) (r : A -> loc T1) + (s : A -> coq_type T2) : + crun (m >>= fun x => cget (r x)) -> + crun (m >>= fun x => cnew (s x) >> cget (r x)). +Proof. +rewrite /crun /= !bindE /= /bindS !MS_mapE /= !fmapE /= !bindA /=. +case Hm: (m _) => [|[a b]] //. +rewrite !bindE /= !bindE /= /bindS MS_mapE /= fmapE /= bindA. +rewrite !bindE /= !bindE /= /cget. +case Hnth: nth_error => [[]|] //. +rewrite (nth_error_rcons_some _ Hnth). +by case Hcoe: coerce. +Qed. + +Lemma crungetput (A : UU0) T (m : M A) (r : A -> loc T) (s : A -> coq_type T) : + crun (m >>= fun x => cget (r x)) -> + crun (m >>= fun x => cput (r x) (s x)). +Proof. +rewrite /crun /= !bindE /= /bindS !MS_mapE /= !fmapE /= !bindA /=. +case Hm: (m _) => [|[a [b]]] //=. +rewrite !bindE /= !bindE /= /cget /cput /=. +case Hnth: nth_error => [[T' v]|] //. +case: (eqVneq T' T) => T'T; last first. + by rewrite coerce_None// 1?eq_sym// coerce_None. +subst T'. +by rewrite !coerce_Some. +Qed. + +HB.instance Definition _ := Monad.on M. +HB.instance Definition isMonadTypedStoreModel := + isMonadTypedStore.Build _ _ M cnewget cnewput cgetput cgetputskip + cgetget cputget cputput cgetC cgetnewD cgetnewE cgetputC cputC + cputgetC cputnewC + crunret crunskip crunnew crunnewget crungetnew crungetput. + +End ModelTypedStore_contd.