Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Delay monad interface and model #147

Draft
wants to merge 32 commits into
base: master
Choose a base branch
from
Draft
Changes from 5 commits
Commits
Show all changes
32 commits
Select commit Hold shift + click to select a range
d284233
add delay monad
Ryuji-Kawakami Jun 25, 2024
bdc9234
arrange the format of programs in example_delay.v
Ryuji-Kawakami Dec 9, 2024
c6a760e
modify the format of programs in example_delaystate.v
Ryuji-Kawakami Dec 9, 2024
eb81166
modify the parametric morphisms definition by using pointwise relation
Ryuji-Kawakami Dec 23, 2024
ccb11a7
change the space around commas and colons
Ryuji-Kawakami Jan 2, 2025
8cbd01c
remove some unnecessary Parentheses and spaces
Ryuji-Kawakami Jan 2, 2025
b27e099
replace fact and exp function using ssrnal library
Ryuji-Kawakami Jan 2, 2025
0ba600d
remove importing ssrnat and use the notation for factorial
Ryuji-Kawakami Jan 3, 2025
5f6b886
replace n + 1 and S n for n.+1
Ryuji-Kawakami Jan 3, 2025
d8eb6a3
renaming Bisim to strongBisim
Ryuji-Kawakami Jan 3, 2025
195c405
replace Oeq for wBisim and wBisim for wBisims
Ryuji-Kawakami Jan 3, 2025
68226d5
change the notation for wBisim and wBisims
Ryuji-Kawakami Jan 3, 2025
f126c23
instance the delay monad from wBisim laws
Ryuji-Kawakami Jan 3, 2025
985f389
replace the tactics case : _ = _ ... for have [|] := ...
Ryuji-Kawakami Jan 9, 2025
315a614
change the indent in example_delay.v and remove the lemma expE_aux
Ryuji-Kawakami Jan 9, 2025
56d0f75
remove the example section in hierarchy and mondify the proof in para…
Ryuji-Kawakami Jan 9, 2025
488f345
replace the tactics case: _ < _ for have [|] := ltnP _ _
Ryuji-Kawakami Jan 9, 2025
335c00e
change the indent in delay_monad_model.v
Ryuji-Kawakami Jan 11, 2025
e2071bb
change the indents
Ryuji-Kawakami Jan 12, 2025
d97ca57
change function definitions to use the projection function
Ryuji-Kawakami Jan 12, 2025
e45028a
share typed_store_universe
garrigue Jan 14, 2025
46f5a9c
modify the proof for factorial to be shorter
Ryuji-Kawakami Jan 15, 2025
4d9abaa
add the deprecated warning for strongBisim_eq axiom
Ryuji-Kawakami Jan 15, 2025
bddf8dd
add the typed universe file
Ryuji-Kawakami Jan 15, 2025
c0182d9
take in the typed_store_universe.v file
Ryuji-Kawakami Jan 15, 2025
1b5584b
add the definition of recursion using while operater
Ryuji-Kawakami Jan 15, 2025
dba404c
remove the wBisims part
Ryuji-Kawakami Jan 16, 2025
8dbd70a
give the proof of partial correctness when terminates
Ryuji-Kawakami Jan 16, 2025
c92c0b3
give the proof of partial correctness
Ryuji-Kawakami Jan 17, 2025
89fbf83
add the example of bubble sort using partial correctness
Ryuji-Kawakami Feb 4, 2025
7769aef
add the uniform law
Ryuji-Kawakami Feb 11, 2025
24696b8
modify the proof of factdts
Ryuji-Kawakami Feb 16, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 5 additions & 1 deletion _CoqProject
Original file line number Diff line number Diff line change
@@ -21,6 +21,10 @@ 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
@@ -34,4 +38,4 @@ theories/applications/example_transformer.v
theories/applications/category_ext.v
theories/all_monae.v

-R . monae
-R . monae
225 changes: 225 additions & 0 deletions theories/applications/example_delay.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,225 @@
From mathcomp Require Import all_ssreflect.
From mathcomp Require boolp.
Require Import hierarchy.
Require Import Lia.

Local Open Scope monae_scope.

Section delayexample.
Notation "a '≈' b" := (wBisim a b).
Variable M : delayMonad.

Fixpoint fact n : nat := match n with
Ryuji-Kawakami marked this conversation as resolved.
Show resolved Hide resolved
|O => 1
|S n' => n * fact n'
end.

Let fact_body a : M (nat + nat * nat)%type :=
match a with
|(O, a2) => Ret (inl a2)
|(S n', a2) => Ret (inr (n', a2 * (S n')))
end.

Let factdelay := fun nm => while fact_body nm.

Lemma eq_fact_factdelay : forall n m, factdelay (n, m) ≈ Ret (m * fact n).
Proof.
move => n.
rewrite /factdelay.
elim: n => [m | n IH m].
- by rewrite fixpointE bindretf muln1.
- by rewrite fixpointE bindretf/= IH 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))
Ryuji-Kawakami marked this conversation as resolved.
Show resolved Hide resolved
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 : forall m n p, delaymul p (collatzm m n) ≈ collatzm (p * m) n.
Proof.
move => m n p.
Ryuji-Kawakami marked this conversation as resolved.
Show resolved Hide resolved
rewrite /collatzm /delaymul naturalityE.
set x := (x in while x).
set y := collatzm_body (p*m).
have <-: x = y.
apply boolp.funext => q.
subst x y.
case_eq (q == 1) => Hs; rewrite /collatzm_body Hs//.
Ryuji-Kawakami marked this conversation as resolved.
Show resolved Hide resolved
+ by rewrite bindretf/= fmapE bindretf/=.
+ by case He: (q %% 2 == 0); rewrite bindretf/= fmapE bindretf/=.
done.
Qed.

Let minus1_body nm : M ((nat + nat * nat) + nat * nat)%type :=
match nm with
|(O, m) => match m with
|O => Ret (inl (inl O))
|S m' => Ret (inl (inr (m', m')))
Ryuji-Kawakami marked this conversation as resolved.
Show resolved Hide resolved
end
|(S n', m) => Ret (inr (n', m))
end.

Let minus1 := fun nm => while (while minus1_body) nm.

Let minus2_body nm : M (nat + nat * nat)%type :=
match nm with
|(O,m) => match m with
Ryuji-Kawakami marked this conversation as resolved.
Show resolved Hide resolved
|O => Ret (inl O)
|S m' => Ret (inr (m', m'))
end
|(S n', m) => Ret (inr (n',m))
end.

Let minus2 := fun nm => while minus2_body nm.

Lemma eq_minus : forall nm, minus1 nm ≈ minus2 nm.
Proof.
move => nm.
rewrite /minus1 /minus2 -codiagonalE.
apply: whilewB.
move => [n m].
case: n => [|n /=].
+ by case: m => //= [|n]; rewrite fmapE bindretf //.
+ by rewrite fmapE bindretf.
Qed.

Definition divide5_body (f : nat -> M nat) nm : M (nat + nat * nat)%type :=
match nm with (n, m) =>
if m %% 5 == 0 then Ret (inl m)
else f n >>= (fun x => Ret (inr (n.+1, x)))
end.

Let dividefac1 n := while (divide5_body (fun n => factdelay (n, 1))) (n, 1).

Let dividefac2 n := while (divide5_body (fun n => Ret (fact n))) (n, 1).

Lemma eq_dividefac : forall n, dividefac1 n ≈ dividefac2 n.
Proof.
move => n.
rewrite /dividefac1 /dividefac2.
apply whilewB.
move => [k l].
case/boolP: (l %% 5 == 0) => Hl /=.
- by rewrite Hl.
- rewrite !ifN // bindretf.
rewrite bindmwB; last by apply (eq_fact_factdelay k 1).
by rewrite 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).

Fixpoint exp n k := match n with |O => 1 | S n' => k * exp n' k end.
Ryuji-Kawakami marked this conversation as resolved.
Show resolved Hide resolved

Lemma expE_aux n : n <= n.*2.
Proof.
elim: n => //= n IH.
Ryuji-Kawakami marked this conversation as resolved.
Show resolved Hide resolved
rewrite doubleS ltnS.
by apply (leq_trans IH (leqnSn _)).
Qed.

Lemma expE : forall n m k, fastexp n m k ≈ Ret (m * expn k n).
Proof.
move => n.
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').
Copy link
Owner

@affeldt-aist affeldt-aist Dec 23, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Use - instead of ** (this breaks the indentation pattern of two characters otherwise)

** rewrite ltnS in Hmn.
rewrite leq_uphalf_double.
by apply (leq_trans Hmn (expE_aux _)).
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.
rewrite fixpointE /= ltnNge => Hmax. (*ltnNge.*)
rewrite ifN //.
rewrite 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.
case/boolP: (90 <= m).
- move => H89.
move: (conj H89 H101) => /andP Hm.
by rewrite mc91E_aux // mc91_101E.
- rewrite -leqNgt -ltnS.
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'.
Ryuji-Kawakami marked this conversation as resolved.
Show resolved Hide resolved
* rewrite mc91E_aux ?mc91_101E//; lia.
* rewrite -ltnNge in Hk'.
by rewrite (IH (k' - 11))//; lia.
Qed.
122 changes: 122 additions & 0 deletions theories/applications/example_delay_typed_store.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,122 @@
(* monae: Monadic equational reasoning in Coq *)
(* Copyright (C) 2023 monae authors, license: LGPL-2.1-or-later *)
Require Import ZArith Morphisms.
From mathcomp Require Import all_ssreflect.
From mathcomp Require boolp.
From infotheo Require Import ssrZ.
Require Import monad_model.
From HB Require Import structures.
Require Import preamble hierarchy monad_lib typed_store_lib.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Local Open Scope monae_scope.

(******************************************************************************)
(* generated by coqgen *)
(******************************************************************************)
Module MLTypes.
Inductive ml_type : Set :=
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This code, as well as other code below, is already present in example_typed_store.v. Could you come up with a way to share this code to avoid copy-pasting? (This is important for maintenance and this can only clarify your work.)

| 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.

Notation loc := (@loc _ monad_model.locT_nat).

Inductive rlist (a : Type) (a_1 : ml_type) :=
| Nil
| Cons (_ : a) (_ : loc (ml_rlist a_1)).

Definition ml_type_eq_mixin := hasDecEq.Build _ (comparePc MLTypes.ml_type_eq_dec).
HB.instance Definition ml_type_eqType := ml_type_eq_mixin.

End MLTypes.
(******************************************************************************)

Module CoqTypeNat.
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.

HB.instance Definition _ := @isML_universe.Build ml_type coq_type_nat ml_unit val_nonempty.

Definition delayTypedStoreMonad (N : monad) :=
delaytypedStoreMonad ml_type N monad_model.locT_nat.

Section factorial.
Variables (N : monad) (M : delayTypedStoreMonad N).
Local Notation coq_type := hierarchy.coq_type.
Local Open Scope do_notation.

Definition factdts_aux_body (r : loc ml_int) (n : nat) : M (unit + nat)%type :=
do v <- cget r;
match n with
|O => do _ <- cput r v; Ret (inl tt)
|S m => do _ <- cput r (n*v); Ret (inr m)
end.

Fixpoint fact n := match n with |O => 1 |m.+1 => n * fact m end.
Definition factn_aux (n: nat) (r : loc ml_int) :=
do s <- cget r;
do _ <- cput r (fact n * s); @ret M _ tt.
Definition factdts_aux (n : nat) (r : loc ml_int) := while (factdts_aux_body r) n.

Lemma factE_aux (n : nat) (r : loc ml_int) : factdts_aux n r ≈ factn_aux n r.
Proof.
rewrite/factdts_aux/factn_aux.
elim: n => /= [|n' IH].
rewrite fixpointE/= !bindA.
by under eq_bind => s do rewrite bindA bindretf/= -{1}(mul1n s).
rewrite fixpointE/= bindA.
under eq_bind => s do rewrite bindA bindretf/=.
setoid_rewrite IH.
by under eq_bind => x do rewrite cputget -bindA cputput mulnA (mulnC (fact n') _).
Qed.

Definition factdts n := do r <- cnew ml_int 1;
do _ <- factdts_aux n r ;
do v <- cget r; Ret v.
Definition factn n := do r <- cnew ml_int (fact n);
do v <- cget r; @ret M _ v.

Lemma factE n : factdts n ≈ factn n.
Proof.
rewrite/factdts/factn.
setoid_rewrite factE_aux.
under eq_bind => r.
rewrite bindA.
under eq_bind => x do rewrite bindA bindretf.
over.
by rewrite cnewget cnewput muln1.
Qed.
End factorial.
Loading

Unchanged files with check annotations Beta

Proof.
rewrite 10!compA.
Undo 1.
by rewrite !hom_compA.

Check warning on line 161 in theories/core/category.v

GitHub Actions / build (mathcomp/mathcomp:2.3.0-coq-8.19)

Command "Undo." is not recommended in batch mode. In particular,
(* rewrite !homcompA blocks id's from coming in, thanks to {hom _,_} conditions on arguments. *)
Abort.
Let choiceC (T : UU0) : forall p (a b : acto T), choice p _ a b = choice ((Prob.p p).~ %:pr) _ b a.
Proof. by move=> ? ?; exact: convC. Qed.
Let choicemm : forall (T : Type) p, idempotent (@choice p T).

Check warning on line 61 in theories/models/proba_monad_model.v

GitHub Actions / build (mathcomp/mathcomp:2.3.0-coq-8.19)

Notation idempotent is deprecated since mathcomp 2.3.0.
Proof. by move=> ? ? ?; exact: convmm. Qed.
Let choiceA : forall (T : Type) (p q r s : {prob R}) (a b c : acto T),
Set Bullet Behavior "Strict Subproofs".
Obligation Tactic := idtac.

Check warning on line 39 in theories/applications/smallstep.v

GitHub Actions / build (mathcomp/mathcomp:2.3.0-coq-8.19)

The default and global localities for this command outside sections
Reserved Notation "'p_do' x <- m ; e"
(at level 60, x name, m at level 200, e at level 60).