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 1 commit
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
Prev Previous commit
Next Next commit
remove importing ssrnat and use the notation for factorial
  • Loading branch information
Ryuji-Kawakami committed Jan 3, 2025

Unverified

No user is associated with the committer email.
commit 0ba600d33e02fedef8617ee8aa813c5e4a29cda2
6 changes: 3 additions & 3 deletions theories/applications/example_delay.v
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
From mathcomp Require Import all_ssreflect ssrnat.
From mathcomp Require Import all_ssreflect.
From mathcomp Require boolp.
Require Import hierarchy.
Require Import Lia.
@@ -17,7 +17,7 @@ Let fact_body a : M (nat + nat * nat)%type :=

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

Lemma eq_fact_factdelay : forall n m, factdelay (n, m) ≈ Ret (m * factorial n).
Lemma eq_fact_factdelay : forall n m, factdelay (n, m) ≈ Ret (m * n`!).
Proof.
move => n.
rewrite /factdelay.
@@ -90,7 +90,7 @@ Definition divide5_body (f : nat -> M nat) nm : M (nat + nat * nat)%type :=

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).
Let dividefac2 n := while (divide5_body (fun n => Ret n`!)) (n, 1).

Lemma eq_dividefac : forall n, dividefac1 n ≈ dividefac2 n.
Proof.
8 changes: 4 additions & 4 deletions theories/applications/example_delay_typed_store.v
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(* 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 ssrnat.
From mathcomp Require Import all_ssreflect.
From mathcomp Require boolp.
From infotheo Require Import ssrZ.
Require Import monad_model.
@@ -87,7 +87,7 @@ Definition factdts_aux_body (r : loc ml_int) (n : nat) : M (unit + nat)%type :=

Definition factn_aux (n: nat) (r : loc ml_int) :=
do s <- cget r;
do _ <- cput r (factorial n * s); @ret M _ tt.
do _ <- cput r (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.
@@ -99,13 +99,13 @@ elim: n => /= [|n' IH].
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 (factorial n') _).
by under eq_bind => x do rewrite cputget -bindA cputput mulnA (mulnC 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 (factorial n);
Definition factn n := do r <- cnew ml_int n`!;
do v <- cget r; @ret M _ v.

Lemma factE n : factdts n ≈ factn n.
Loading