Delay monad interface and model

_CoqProject

@@ -21,17 +21,22 @@ theories/models/proba_monad_model.v
 theories/models/gcm_model.v
 theories/models/altprob_model.v
 theories/models/typed_store_model.v
+theories/models/delay_monad_model.v
+theories/models/delayexcept_model.v
+theories/models/delaystate_model.v
+theories/models/typed_store_transformer.v
 theories/applications/monad_composition.v
 theories/applications/example_spark.v
 theories/applications/example_nqueens.v
 theories/applications/example_relabeling.v
 theories/applications/example_quicksort.v
 theories/applications/example_iquicksort.v
 theories/applications/example_monty.v
+theories/applications/typed_store_universe.v
 theories/applications/example_typed_store.v
 theories/applications/smallstep.v
 theories/applications/example_transformer.v
 theories/applications/category_ext.v
 theories/all_monae.v
 
--R . monae
+-R . monae

theories/applications/example_delay.v

@@ -0,0 +1,172 @@
+From mathcomp Require Import all_ssreflect.
+From mathcomp Require boolp.
+Require Import hierarchy.
+Require Import Lia.
+
+Local Open Scope monae_scope.
+
+Section delayexample.
+Variable M : delayMonad.
+
+Let fact_body a : M (nat + nat * nat)%type :=
+  if a.1 is m.+1 then Ret (inr (m, a.2 * m.+1)) else Ret (inl a.2).
+Let factdelay := fun nm => while fact_body nm.
+
+Lemma eq_fact_factdelay : forall n m, factdelay (n, m) ≈ Ret (m * n`!).
+Proof.
+move => n.
+rewrite /factdelay.
+elim: n => [m | n IH m]; rewrite fixpointE bindretf/=.
+  by rewrite muln1.
+by rewrite mulnA.
+Qed.
+
+Let collatzm_body m n : M (nat + nat)%type :=
+  if n == 1 then Ret (inl m)
+  else if n %% 2 == 0 then Ret (inr n./2)
+       else Ret (inr ((3 * n).+1)).
+Let collatzm m := fun n => while (collatzm_body m) n.
+Let delaymul m d : M nat := d >>= (fun n => Ret (m * n)).
+
+Lemma collatzmwB m n p : delaymul p (collatzm m n) ≈ collatzm (p * m) n.
+Proof.
+rewrite /collatzm /delaymul naturalityE.
+apply: whilewB => q.
+have [Hs|Hns] := eqVneq q 1.
+  by rewrite Hs bindretf/= fmapE bindretf/=.
+rewrite /collatzm_body !(ifN_eq _ _ Hns).
+by have [|] := eqVneq (q %% 2) 0; rewrite bindretf/= fmapE bindretf.
+Qed.
+
+Let minus1_body nm : M ((nat + nat * nat) + nat * nat)%type :=
+  if nm.1 is n'.+1 then Ret (inr (n', nm.2))
+                   else if nm.2 is m'.+1 then Ret (inl (inr (m', m')))
+                                         else Ret (inl (inl  O)).
+Let minus1 := fun nm => while (while minus1_body) nm.
+Let minus2_body nm : M (nat + nat * nat)%type :=
+  if nm.1 is n'.+1 then Ret (inr (n', nm.2))
+                   else if nm.2 is m'.+1 then Ret (inr (m', m'))
+                                         else Ret (inl 0).
+Let minus2 := fun nm => while minus2_body nm.
+
+Lemma eq_minus nm : minus1 nm ≈ minus2 nm.
+Proof.
+rewrite /minus1 /minus2 -codiagonalE.
+apply: whilewB.
+move => [n m].
+case: n => [|n /=].
+  by case: m => //= [|n]; rewrite fmapE bindretf //.
+by rewrite fmapE bindretf.
+Qed.
+
+Let divide5_body (f : nat -> M nat) nm : M (nat + nat * nat)%type :=
+    if nm.2 %% 5 == 0 then Ret (inl nm.2)
+    else f nm.1 >>= (fun x => Ret (inr (nm.1.+1, x))).
+Let dividefac1 n := while (divide5_body (fun n => factdelay (n, 1))) (n, 1).
+Let dividefac2 n := while (divide5_body (fun n => Ret n`!)) (n, 1).
+
+Lemma eq_dividefac n : dividefac1 n ≈ dividefac2 n.
+Proof.
+rewrite /dividefac1/dividefac2/divide5_body.
+apply: whilewB.
+move => [k l].
+have [Hl|Hln] := eqVneq (l %% 5) 0 => //.
+by rewrite eq_fact_factdelay !bindretf mul1n.
+Qed.
+
+Let fastexp_body nmk : M (nat + nat * nat * nat)%type :=
+  match nmk with (n, m, k) =>
+    if n == 0 then Ret (inl m)
+    else (if odd n then Ret (inr (n.-1 , m * k, k))
+          else Ret (inr (n./2, m, k * k) ))
+  end.
+Let fastexp n m k := while fastexp_body (n, m, k).
+
+Lemma expE n: forall m k, fastexp n m k ≈ Ret (m * expn k n).
+Proof.
+rewrite /fastexp /fastexp_body.
+elim: n {-2}n (leqnn n) => n.
+  rewrite leqn0 => /eqP H0 m k.
+  by rewrite H0 fixpointE /= bindretf /= expn0 mulnS muln0 addn0.
+move => IH [|m'] Hmn m k.
+  by rewrite fixpointE /= bindretf /= mulnS muln0 addn0.
+case/boolP: (odd (m'.+1)) => Hm'.
+  by rewrite fixpointE Hm' bindretf/= IH//= expnSr (mulnC (k^m') k) mulnA.
+rewrite fixpointE ifN //= bindretf /= IH.
+  by rewrite uphalfE mulnn -expnM mul2n (even_halfK Hm').
+rewrite ltnS in Hmn.
+rewrite leq_uphalf_double.
+apply: (leq_trans Hmn).
+rewrite -addnn.
+by apply: leq_addr.
+Qed.
+
+Let mc91_body nm : M (nat + nat * nat)%type :=
+  match nm with (n, m) => if n == 0 then Ret (inl m)
+                          else if m > 100 then Ret (inr (n.-1, m - 10))
+                                          else Ret (inr (n.+1, m + 11))
+  end.
+Let mc91 n m := while mc91_body (n.+1, m).
+
+Lemma mc91succE n m : 90 <= m < 101 -> mc91 n m ≈ mc91 n (m.+1).
+Proof.
+move => /andP [Hmin].
+rewrite /mc91 fixpointE /= ltnNge => Hmax.
+rewrite ifN // bindretf /= fixpointE /=.
+have -> : 100 = 89 + 11 by [].
+rewrite ltn_add2r ifT //.
+rewrite bindretf fixpointE /= fixpointE.
+have -> // : m + 11 - 10 = m.+1.
+by rewrite -addnBA // addn1.
+Qed.
+Lemma mc91E_aux m n : 90 <= m <= 101 -> mc91 n m ≈ mc91 n 101.
+Proof.
+move => /andP [Hmin Hmax].
+case/boolP: (m < 101).
+  move/ltnW/subnKC.
+  set k:= 101 - m.
+  clearbody k.
+  move: m Hmin Hmax.
+  elim: k.
+    move => m Hmin Hmax.
+    by rewrite addn0 => ->.
+  move => l IH m Hmin.
+  rewrite leq_eqVlt => /orP [/eqP H101 | Hm].
+    by rewrite H101 => _.
+  rewrite -addn1 (addnC l 1) addnA mc91succE ?Hmin // addn1.
+  apply IH => //.
+  by apply: leq_trans.
+rewrite -leqNgt => H100.
+have -> //: m = 101.
+apply anti_leq => //.
+by rewrite Hmax.
+Qed.
+Lemma mc91_101E n : mc91 n 101 ≈ Ret 91.
+Proof.
+elim: n => [|n IH]; rewrite/mc91/mc91_body fixpointE bindretf/=.
+  by rewrite fixpointE bindretf.
+by rewrite -/mc91_body // -/(mc91 n 91) mc91E_aux // IH.
+Qed.
+Lemma mc91E n m : m <= 101 -> mc91 n m ≈ Ret 91.
+Proof.
+move => H101.
+have [H89|] := leqP 90 m.
+  move: (conj H89 H101) => /andP Hm.
+  by rewrite mc91E_aux // mc91_101E.
+move/ltnW/subnKC.
+set k:= 90 - m.
+clearbody k.
+elim: k {-2}k (leqnn k) n m {H101} => k.
+  rewrite leqn0 => /eqP H0 n m.
+  rewrite H0 (addn0 m) => ->.
+  by rewrite mc91E_aux// mc91_101E.
+move =>IH k' Hk n m Hm.
+have ->: m = 90 - k' by rewrite -Hm addnK.
+rewrite/mc91/mc91_body fixpointE //=.
+rewrite ifF; last by rewrite ltn_subRL addnC.
+rewrite bindretf/= -/mc91_body -/(mc91 _ _).
+case/boolP: (k' <= 11) => Hk'.
+  by rewrite mc91E_aux ?mc91_101E//; lia.
+rewrite -ltnNge in Hk'.
+by rewrite (IH (k' - 11))//; lia.
+Qed.

theories/applications/example_delay_typed_store.v

@@ -0,0 +1,58 @@
+(* monae: Monadic equational reasoning in Coq                                 *)
+(* Copyright (C) 2023 monae authors, license: LGPL-2.1-or-later               *)
+Require Import Morphisms.
+From mathcomp Require Import all_ssreflect.
+From HB Require Import structures.
+Require Import preamble hierarchy monad_lib typed_store_lib.
+Require Import typed_store_universe.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope monae_scope.
+
+Module CoqTypeNat.
+Import MLTypes CoqTypeNat.
+
+Definition delayTypedStoreMonad (N : monad) :=
+  delaytypedStoreMonad ml_type N nat.
+
+Section factorial.
+Variables (N : monad) (M : delayTypedStoreMonad N).
+
+Local Notation coq_type := hierarchy.coq_type.
+Local Open Scope do_notation.
+
+Let factdts_body (r : loc ml_int) n : M (unit + nat)%type :=
+  do v <- cget r;
+  if n is m.+1 then do _ <- cput r (n * v); Ret (inr m)
+               else Ret (inl tt).
+
+Let while_factdtsE n r :
+  while (factdts_body r) n ≈ do s <- cget r; cput r (n`! * s).
+Proof.
+elim: n => /= [|n' IH].
+  rewrite fixpointE/= !bindA.
+  under [x in _ ≈ x]eq_bind => s do rewrite fact0 mul1n.
+  rewrite cgetputskip.
+  by under eq_bind do rewrite bindretf.
+rewrite fixpointE/= bindA.
+under eq_bind => s do rewrite bindA bindretf/=.
+setoid_rewrite IH.
+by under eq_bind do rewrite cputget cputput mulnA (mulnC n'`! _).
+Qed.
+
+Definition factdts n :=
+  do r <- cnew ml_int 1;
+  do _ <- while (factdts_body r) n ;
+  cget r.
+
+Lemma factdtsE n : factdts n ≈ cnew ml_int n`! >> Ret n`!.
+Proof.
+rewrite/factdts.
+setoid_rewrite factdts_loopE.
+under eq_bind do rewrite bindA.
+by rewrite cnewget cnewput muln1 cnewgetret.
+Qed.
+End factorial.

theories/applications/example_delayexcept.v

@@ -0,0 +1,112 @@
+From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import boolp.
+Require Import preamble hierarchy monad_lib fail_lib state_lib.
+
+Local Open Scope monae_scope.
+
+Section delayexcept_example.
+
+Variable M : delayExceptMonad.
+
+Definition select l := let max := \max_(i <- l) i in (max, rem max l).
+
+Definition muloflistover10d_body ln : M (nat + (seq nat) * nat)%type :=
+  match ln with (l, n) =>
+                  match l with
+                    |[::] => Ret (inl n)
+                    |h::tl => let (m, res) := select l in catch (if m <= 10 then fail else Ret (inr (res, m * n))) (Ret (inl n))
+                  end
+  end.
+
+Definition muloflistover10d := while muloflistover10d_body.
+
+Definition muloflistover10 l := foldr (fun x z => if 10 < x then x * z else z) 1 l.
+
+Lemma all_under10 l : (forall i, i \in l -> i <= 10) -> muloflistover10 l = 1.
+Proof.
+elim: l => //= n l' Hl H.
+have [H10|_] := ltnP 10 n.
+  contradict H10.
+  apply/negP.
+  rewrite -leqNgt.
+  apply H.
+  by rewrite in_cons eq_refl.
+apply Hl => m Hl'.
+apply H.
+by rewrite in_cons Hl' orbT.
+Qed.
+
+Lemma muloflistover10_aux(l : seq nat) (k : nat): 10 < k -> k \in l -> k * muloflistover10 (rem k l) = muloflistover10 l.
+move => Hk Hink.
+rewrite/muloflistover10.
+elim: l Hink => //= n l' IH Hink.
+have  [Hnk|/negPf Hnk] := eqVneq n k.
+  have [|?] := ltnP 10 n.
+    by rewrite Hnk.
+  contradict Hk.
+  rewrite -Hnk.
+  apply/negP.
+  by rewrite -ltnNge.
+have Hkl': k \in l'.
+  move: Hink.
+  by rewrite in_cons eq_sym Hnk/=.
+have [Hn|HnN] := ltnP 10 n.
+  rewrite -(IH Hkl')/= Hn.
+  by rewrite mulnA (mulnC k n) -mulnA.
+by rewrite -(IH Hkl')/= ltnNge HnN/=.
+Qed.
+
+Lemma maxinseq (l : seq nat): ~~(nilp l) -> \max_(i <- l) i \in l.
+Proof.
+move => Hn.
+rewrite -(in_tupleE l) big_tuple.
+case: (eq_bigmax (tnth (in_tuple l))) => [|x ->].
+  by rewrite cardT size_enum_ord lt0n.
+by rewrite mem_tnth.
+Qed.
+
+Lemma muloflistover10E (l : seq nat) (n : nat) : muloflistover10d (l, n) ≈ Ret (n * (muloflistover10 l)).
+Proof.
+move Hlen: (size l) => len.
+move: n.
+elim: len l Hlen.
+- move => l /eqP/nilP Hl n.
+  by rewrite/muloflistover10/muloflistover10d/muloflistover10d_body Hl /= fixpointE /= bindretf /= mulnS muln0 addn0.
+move => m IH l' Hs n.
+rewrite/muloflistover10d/muloflistover10d_body fixpointE /=.
+elim: l' Hs => //= [h l''] _ Hs.
+case: Hs => Hs.
+have [/bigmax_leqP_seq Hm10|Hm10] := leqP (\max_(i <- (h :: l'')) i) 10.
+  rewrite catchfailm bindretf /=.
+  have -> : (10 < h) = false.
+    apply/negP/negP.
+    rewrite -leqNgt.
+    apply Hm10 => //=.
+    by rewrite in_cons eq_refl.
+  rewrite all_under10.
+    by rewrite mulnS muln0 addn0.
+  move => i Hini.
+  apply Hm10 => //=.
+  by rewrite in_cons Hini orbT.
+rewrite catchret bindretf /=.
+rewrite -/muloflistover10d_body -/muloflistover10d.
+have [Ht|Hf] := eqVneq h (\max_(i <- (h :: l'')) i).
+  by rewrite {2}Ht (ifT _ _ Hm10) (IH l'' Hs) -Ht (mulnC h n) mulnA.
+move: Hm10.
+set k := \max_(i <- (h :: l'')) i => Hk.
+have Hmaxin : k \in (h :: l'').
+  subst k.
+  by apply maxinseq.
+rewrite IH/=.
+  rewrite /= (mulnC k n) -mulnA fun_if.
+  rewrite (mulnA k h _) (mulnC k h) -mulnA (muloflistover10_aux _ _ Hk) //.
+  by move: Hmaxin; rewrite in_cons eq_sym (negPf Hf) /=.
+subst k.
+rewrite  size_rem.
+  case: l'' Hs Hf Hk Hmaxin => [? contr|h' l'''  Hs ? ?].
+    contradict contr.
+    by rewrite big_cons big_nil maxn0 eq_refl.
+  by rewrite prednK //=.
+move: Hmaxin.
+by rewrite in_cons eq_sym (negPf Hf) /=.
+Qed.