Subdirs

README.md

@@ -94,36 +94,44 @@ This library has been applied to other formalizations:
 
 ## Files
 
-- basics:
-  + [monae_lib.v](./monae_lib.v): simple additions to base libraries
-  + [hierarchy.v](./hierarchy.v): hierarchy of monadic effects
-  + [category.v](./category.v): formalization of concrete categories (generalization of the bottom layers of `hierarchy.v`)
-  + [monad_transformer.v](./monad_transformer.v): monad transformers
+- core:
+  + [monae_lib.v](./theories/core/monae_lib.v): simple additions to base libraries
+  + [hierarchy.v](./theories/core/hierarchy.v): hierarchy of monadic effects
+  + [category.v](./theories/core/category.v): formalization of concrete categories (generalization of the bottom layers of `hierarchy.v`)
+  + [monad_transformer.v](./theories/core/monad_transformer.v): monad transformers
     * completed by `ifmt_lifting.v` and `iparametricty_codensity.v` in the directory `impredicative_set`
       - the directory `impredicative_set` contains a lighter version of Monae where monads live in `Set` and that compiles with `impredicative-set`
-- utility lemmas:  
-  + [monad_lib.v](./monad_lib.v): basic lemmas about monads
-  + [fail_lib.v](./fail_lib.v): lemmas about the fail monad and related monads
-  + [state_lib.v](./state_lib.v): lemmas about state-related monads
-  + [array_lib.v](./array_lib.v): lemmas about the array monad
-  + [trace_lib.v](./trace_lib.v): lemmas about about the state-trace monad
-  + [proba_lib.v](./proba_lib.v): lemmas about the probability monad
-  + [typed_store_lib.v](./typed_store_lib.v): derived definitions and lemmas about about the typed store monad
+- libraries for each monad theory:  
+  + [monad_lib.v](./theories/lib/monad_lib.v): basic lemmas about monads
+  + [fail_lib.v](./theories/lib/fail_lib.v): lemmas about the fail monad and related monads
+  + [state_lib.v](./theories/lib/state_lib.v): lemmas about state-related monads
+  + [array_lib.v](./theories/lib/array_lib.v): lemmas about the array monad
+  + [trace_lib.v](./theories/lib/trace_lib.v): lemmas about about the state-trace monad
+  + [proba_lib.v](./theories/lib/proba_lib.v): lemmas about the probability monad
+  + [typed_store_lib.v](./theories/lib/typed_store_lib.v): derived definitions and lemmas about about the typed store monad
 - models of monads:
-  + [monad_model.v](./monad_model.v): concrete models of monads
-  + [proba_monad_model.v](./proba_monad_model.v): model of the probability monad
-  + [gcm_model.v](./gcm_model.v): model of the geometrically convex monad
-  + [altprob_model.v](./altprob_model.v): model of a monad that mixes non-deterministic choice and probabilistic choice
-  + [typed_store_model.v](./typed_store_model.v): alternative model of the typed store monad
+  + [monad_model.v](./theories/models/monad_model.v): concrete models of monads
+  + [proba_monad_model.v](./theories/models//proba_monad_model.v): model of the probability monad
+  + [gcm_model.v](./theories/models//gcm_model.v): model of the geometrically convex monad
+  + [altprob_model.v](./theories/models//altprob_model.v): model of a monad that mixes non-deterministic choice and probabilistic choice
+  + [typed_store_model.v](./theories/models//typed_store_model.v): alternative model of the typed store monad
 - applications:
-  + [monad_composition.v](./monad_composition.v): composing monads
-  + [smallstep.v](./smallstep.v): semantics for an imperative language, with equivalence operational semantics/denotation and sample imperative programs
-  + example_*.v: various examples (Spark aggregation, the n-queens puzzle, tree relabeling,  Monty Hall problem, monad transformers, quicksort, OCaml programs, etc.)
-
-## About Installation with Windows 10 or 11
+  + [example_relabeling.v](./theories/applications/example_relabeling.v): tree relabeling
+  + [example_monty.v](./theories/applications/example_monty.v): Monty Hall problem
+  + [example_spark.v](./theories/applications/example_spark.v): Spark aggregation
+  + [example_iquicksort.v](./theories/applications/example_iquicksort.v): in-place quicksort
+  + [example_quicksort.v](./theories/applications/example_quicksort.v): functional quicksort
+  + [example_nqueens.v](./theories/applications/example_nqueens.v): the n-queens puzzle
+  + [example_typed_store.v](./theories/applications/example_typed_store.v): ML programs with references
+  + [example_transformer.v](./theories/applications/example_transformer.v): monad transformers
+  + [smallstep.v](./theories/applications/smallstep.v): semantics for an imperative language, with equivalence operational semantics/denotation and sample imperative programs
+  + [monad_composition.v](./theories/applications/monad_composition.v): composing monads
+  + [category_ext.v](./theories/applications/category_ext.v): experimental library about categories
+
+## About Installation with Windows 11
 
 Installation of monae on Windows is less simple.
-First install infotheo following the [instructions for Windows 10](https://github.com/affeldt-aist/infotheo).
+First install infotheo following the [instructions for Windows 11](https://github.com/affeldt-aist/infotheo).
 Once infotheo is installed (with opam), do:
 - `opam install coq-monae` or `git clone [email protected]:affeldt-aist/monae.git; opam install .`
 

_CoqProject

@@ -5,33 +5,33 @@
 -arg -w -arg -notation-incompatible-format
 -arg -w -arg -elpi.add-const-for-axiom-or-sectionvar
 
-monae_lib.v
-hierarchy.v
-monad_lib.v
-fail_lib.v
-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
-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
-all_monae.v
+theories/core/preamble.v
+theories/core/hierarchy.v
+theories/core/category.v
+theories/core/monad_transformer.v
+theories/lib/monad_lib.v
+theories/lib/fail_lib.v
+theories/lib/state_lib.v
+theories/lib/array_lib.v
+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/gcm_model.v
+theories/models/altprob_model.v
+theories/models/typed_store_model.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/example_typed_store.v
+theories/applications/smallstep.v
+theories/applications/example_transformer.v
+theories/applications/category_ext.v
+theories/all_monae.v
 
 -R . monae

coq-monae.opam

@@ -15,7 +15,7 @@ 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.18" & < "8.20~") | (= "dev") }

impredicative_set/_CoqProject

@@ -6,7 +6,7 @@
 -arg -w -arg -elpi.add-const-for-axiom-or-sectionvar
 -arg -impredicative-set
 
-imonae_lib.v
+ipreamble.v
 ihierarchy.v
 imonad_lib.v
 ifail_lib.v

impredicative_set/iexample_transformer.v

@@ -1,7 +1,7 @@
 (* monae: Monadic equational reasoning in Coq                                 *)
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
-Require Import imonae_lib ihierarchy imonad_lib ifail_lib istate_lib.
+Require Import ipreamble ihierarchy imonad_lib ifail_lib istate_lib.
 Require Import imonad_transformer.
 
 (******************************************************************************)

impredicative_set/ifail_lib.v

@@ -1,7 +1,7 @@
 (* monae: Monadic equational reasoning in Coq                                 *)
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
-Require Import imonae_lib.
+Require Import ipreamble.
 From HB Require Import structures.
 Require Import ihierarchy imonad_lib.
 From Equations Require Import Equations.

impredicative_set/ifmt_lifting.v

@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
 From HB Require Import structures.
-Require Import imonae_lib ihierarchy imonad_lib imonad_transformer.
+Require Import ipreamble ihierarchy imonad_lib imonad_transformer.
 
 (******************************************************************************)
 (*   Uniform Lifting of Sigma-operations Along Functorial Monad Transformers  *)

impredicative_set/ihierarchy.v

@@ -4,7 +4,7 @@ Ltac typeof X := type of X.
 
 Require Import ssrmatching JMeq.
 From mathcomp Require Import all_ssreflect.
-Require Import imonae_lib.
+Require Import ipreamble.
 From HB Require Import structures.
 
 (******************************************************************************)

impredicative_set/imonad_composition.v

@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
 From HB Require Import structures.
-Require Import imonae_lib ihierarchy imonad_lib.
+Require Import ipreamble ihierarchy imonad_lib.
 
 (******************************************************************************)
 (*                          Composing monads                                  *)

impredicative_set/imonad_lib.v

@@ -3,7 +3,7 @@
 Ltac typeof X := type of X.
 Require Import ssrmatching.
 From mathcomp Require Import all_ssreflect.
-Require Import imonae_lib.
+Require Import ipreamble.
 From HB Require Import structures.
 Require Import ihierarchy.
 

impredicative_set/imonad_model.v

@@ -1,5 +1,5 @@
 From mathcomp Require Import all_ssreflect.
-Require Import imonae_lib.
+Require Import ipreamble.
 From HB Require Import structures.
 Require Import ihierarchy imonad_lib ifail_lib istate_lib itrace_lib.
 Require Import imonad_transformer.

impredicative_set/imonad_transformer.v

@@ -1,7 +1,7 @@
 (* monae: Monadic equational reasoning in Coq                                 *)
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
-Require Import imonae_lib.
+Require Import ipreamble.
 From HB Require Import structures.
 Require Import ihierarchy imonad_lib ifail_lib istate_lib.
 

impredicative_set/iparametricity_codensity.v

@@ -4,7 +4,7 @@ From Param Require Import Param.
 
 From mathcomp Require Import all_ssreflect.
 From HB Require Import structures.
-Require Import imonae_lib ihierarchy imonad_lib ifmt_lifting imonad_model.
+Require Import ipreamble ihierarchy imonad_lib ifmt_lifting imonad_model.
 
 (******************************************************************************)
 (* Instantiations of uniform lifting (Theorem 27 of [Mauro Jaskelioff,        *)

impredicative_set/istate_lib.v

@@ -1,7 +1,7 @@
 (* monae: Monadic equational reasoning in Coq                                 *)
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
-Require Import imonae_lib.
+Require Import ipreamble.
 From HB Require Import structures.
 Require Import ihierarchy imonad_lib ifail_lib.
 

meta.yml

@@ -180,36 +180,44 @@ documentation: |-
 
   ## Files
 
-  - basics:
-    + [monae_lib.v](./monae_lib.v): simple additions to base libraries
-    + [hierarchy.v](./hierarchy.v): hierarchy of monadic effects
-    + [category.v](./category.v): formalization of concrete categories (generalization of the bottom layers of `hierarchy.v`)
-    + [monad_transformer.v](./monad_transformer.v): monad transformers
+  - core:
+    + [preamble.v](./theories/core/preamble.v): simple additions to base libraries
+    + [hierarchy.v](./theories/core/hierarchy.v): hierarchy of monadic effects
+    + [category.v](./theories/core/category.v): formalization of concrete categories (generalization of the bottom layers of `hierarchy.v`)
+    + [monad_transformer.v](./theories/core/monad_transformer.v): monad transformers
       * completed by `ifmt_lifting.v` and `iparametricty_codensity.v` in the directory `impredicative_set`
         - the directory `impredicative_set` contains a lighter version of Monae where monads live in `Set` and that compiles with `impredicative-set`
-  - utility lemmas:  
-    + [monad_lib.v](./monad_lib.v): basic lemmas about monads
-    + [fail_lib.v](./fail_lib.v): lemmas about the fail monad and related monads
-    + [state_lib.v](./state_lib.v): lemmas about state-related monads
-    + [array_lib.v](./array_lib.v): lemmas about the array monad
-    + [trace_lib.v](./trace_lib.v): lemmas about about the state-trace monad
-    + [proba_lib.v](./proba_lib.v): lemmas about the probability monad
-    + [typed_store_lib.v](./typed_store_lib.v): derived definitions and lemmas about about the typed store monad
+  - libraries for each monad theory:  
+    + [monad_lib.v](./theories/lib/monad_lib.v): basic lemmas about monads
+    + [fail_lib.v](./theories/lib/fail_lib.v): lemmas about the fail monad and related monads
+    + [state_lib.v](./theories/lib/state_lib.v): lemmas about state-related monads
+    + [array_lib.v](./theories/lib/array_lib.v): lemmas about the array monad
+    + [trace_lib.v](./theories/lib/trace_lib.v): lemmas about about the state-trace monad
+    + [proba_lib.v](./theories/lib/proba_lib.v): lemmas about the probability monad
+    + [typed_store_lib.v](./theories/lib/typed_store_lib.v): derived definitions and lemmas about about the typed store monad
   - models of monads:
-    + [monad_model.v](./monad_model.v): concrete models of monads
-    + [proba_monad_model.v](./proba_monad_model.v): model of the probability monad
-    + [gcm_model.v](./gcm_model.v): model of the geometrically convex monad
-    + [altprob_model.v](./altprob_model.v): model of a monad that mixes non-deterministic choice and probabilistic choice
-    + [typed_store_model.v](./typed_store_model.v): alternative model of the typed store monad
+    + [monad_model.v](./theories/models/monad_model.v): concrete models of monads
+    + [proba_monad_model.v](./theories/models//proba_monad_model.v): model of the probability monad
+    + [gcm_model.v](./theories/models//gcm_model.v): model of the geometrically convex monad
+    + [altprob_model.v](./theories/models//altprob_model.v): model of a monad that mixes non-deterministic choice and probabilistic choice
+    + [typed_store_model.v](./theories/models//typed_store_model.v): alternative model of the typed store monad
   - applications:
-    + [monad_composition.v](./monad_composition.v): composing monads
-    + [smallstep.v](./smallstep.v): semantics for an imperative language, with equivalence operational semantics/denotation and sample imperative programs
-    + example_*.v: various examples (Spark aggregation, the n-queens puzzle, tree relabeling,  Monty Hall problem, monad transformers, quicksort, OCaml programs, etc.)
-
-  ## About Installation with Windows 10 or 11
+    + [example_relabeling.v](./theories/applications/example_relabeling.v): tree relabeling
+    + [example_monty.v](./theories/applications/example_monty.v): Monty Hall problem
+    + [example_spark.v](./theories/applications/example_spark.v): Spark aggregation
+    + [example_iquicksort.v](./theories/applications/example_iquicksort.v): in-place quicksort
+    + [example_quicksort.v](./theories/applications/example_quicksort.v): functional quicksort
+    + [example_nqueens.v](./theories/applications/example_nqueens.v): the n-queens puzzle
+    + [example_typed_store.v](./theories/applications/example_typed_store.v): ML programs with references
+    + [example_transformer.v](./theories/applications/example_transformer.v): monad transformers
+    + [smallstep.v](./theories/applications/smallstep.v): semantics for an imperative language, with equivalence operational semantics/denotation and sample imperative programs
+    + [monad_composition.v](./theories/applications/monad_composition.v): composing monads
+    + [category_ext.v](./theories/applications/category_ext.v): experimental library about categories
+
+  ## About Installation with Windows 11
 
   Installation of monae on Windows is less simple.
-  First install infotheo following the [instructions for Windows 10](https://github.com/affeldt-aist/infotheo).
+  First install infotheo following the [instructions for Windows 11](https://github.com/affeldt-aist/infotheo).
   Once infotheo is installed (with opam), do:
   - `opam install coq-monae` or `git clone [email protected]:affeldt-aist/monae.git; opam install .`
 

all_monae.v → theories/all_monae.v

@@ -1,4 +1,4 @@
-Require Export monae_lib.
+Require Export preamble.
 Require Export hierarchy.
 Require Export monad_lib.
 Require Export fail_lib.

category_ext.v → theories/applications/category_ext.v

@@ -1,6 +1,8 @@
+(* monae: Monadic equational reasoning in Coq                                 *)
+(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require Import boolp.
-Require Import monae_lib category.
+Require Import preamble category.
 From HB Require Import structures.
 
 (******************************************************************************)

example_iquicksort.v → theories/applications/example_iquicksort.v

@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
-Require Import monae_lib hierarchy monad_lib fail_lib state_lib.
+Require Import preamble hierarchy monad_lib fail_lib state_lib.
 Require Import array_lib example_quicksort.
 From infotheo Require Import ssr_ext.
 

example_monty.v → theories/applications/example_monty.v

@@ -4,7 +4,7 @@ Require Import Reals Lra.
 From mathcomp Require Import all_ssreflect ssralg ssrnum.
 From mathcomp Require Import mathcomp_extra reals Rstruct.
 From infotheo Require Import ssrR realType_ext Reals_ext proba.
-Require Import monae_lib hierarchy monad_lib fail_lib proba_lib.
+Require Import preamble hierarchy monad_lib fail_lib proba_lib.
 
 (******************************************************************************)
 (*                            Monty Hall example                              *)

example_nqueens.v → theories/applications/example_nqueens.v

@@ -4,7 +4,7 @@ Require Import ZArith.
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
 From infotheo Require Import ssrZ.
-Require Import monae_lib hierarchy monad_lib fail_lib state_lib.
+Require Import preamble hierarchy monad_lib fail_lib state_lib.
 
 (******************************************************************************)
 (*                            N-queens example                                *)

example_quicksort.v → theories/applications/example_quicksort.v

@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
-Require Import monae_lib.
+Require Import preamble.
 Require Import hierarchy monad_lib fail_lib state_lib.
 From infotheo Require Import ssr_ext.
 Require Import Recdef.

example_relabeling.v → theories/applications/example_relabeling.v

@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
-Require Import monae_lib hierarchy monad_lib fail_lib state_lib.
+Require Import preamble hierarchy monad_lib fail_lib state_lib.
 
 (******************************************************************************)
 (*                           Tree relabeling                                  *)

example_spark.v → theories/applications/example_spark.v

@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
-Require Import monae_lib hierarchy monad_lib fail_lib.
+Require Import preamble hierarchy monad_lib fail_lib.
 
 (******************************************************************************)
 (*                              Spark example                                 *)

example_transformer.v → theories/applications/example_transformer.v

@@ -1,7 +1,7 @@
 (* monae: Monadic equational reasoning in Coq                                 *)
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
-Require Import monae_lib hierarchy monad_lib fail_lib state_lib.
+Require Import preamble hierarchy monad_lib fail_lib state_lib.
 Require Import monad_transformer.
 
 (******************************************************************************)