Delay monad interface and model (#147)

Co-authored-by: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Co-authored-by: Takafumi Saikawa <tscompor@gmail.com>

Author: 4 people

_CoqProject

@@ -18,10 +18,13 @@ theories/lib/trace_lib.v
 theories/lib/proba_lib.v
 theories/lib/typed_store_lib.v
 theories/models/monad_model.v
-theories/models/proba_monad_model.v
+theories/models/proba_model.v
 theories/models/gcm_model.v
 theories/models/altprob_model.v
 theories/models/typed_store_model.v
+theories/models/delay_model.v
+theories/models/elgot_model.v
+theories/models/typed_store_transformer.v
 theories/applications/monad_composition.v
 theories/applications/example_fastprod.v
 theories/applications/example_spark.v
@@ -30,11 +33,13 @@ theories/applications/example_relabeling.v
 theories/applications/example_quicksort.v
 theories/applications/example_iquicksort.v
 theories/applications/example_monty.v
+theories/applications/example_elgot.v
+theories/applications/typed_store_universe.v
 theories/applications/example_typed_store.v
 theories/applications/smallstep.v
 theories/applications/example_transformer.v
 theories/applications/counterexample_altconvexdr.v
 theories/applications/category_ext.v
 theories/all_monae.v
 
--R . monae
+-R . monae

coq-monae.opam

@@ -18,7 +18,7 @@ in several examples of monadic equational reasoning."""
 build: [make "-j%{jobs}%"]
 install: [make "install_full"]
 depends: [
-  "coq" { (>= "8.20" & < "9.1~") }
+  "coq" { (>= "9.0" & < "9.1~") }
   "coq-mathcomp-ssreflect" { (>= "2.4.0") }
   "coq-mathcomp-fingroup" { (>= "2.4.0") }
   "coq-mathcomp-algebra" { (>= "2.4.0") }

theories/all_monae.v

@@ -9,7 +9,7 @@ Require Export proba_lib.
 Require Export typed_store_lib.
 Require Export monad_composition.
 Require Export monad_model.
-Require Export proba_monad_model.
+Require Export proba_model.
 Require Export category.
 Require Export gcm_model.
 Require Export altprob_model.

theories/applications/counterexample_altconvexdr.v

@@ -1,4 +1,4 @@
-(* monae: Monadic equational reasoning in Coq                                 *)
+(* monae: Monadic equational reasoning in Rocq                                *)
 (* Copyright (C) 2025 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum finmap.
 From mathcomp Require Import boolp classical_sets reals.