From 3542061110d5634859eca11144777b030e6b0136 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 15 Dec 2020 17:48:47 +0900 Subject: [PATCH] compatibility with infotheo 0.2.1 --- .github/workflows/docker-action.yml | 32 +++++ README.md | 125 ++++++++++++++++++ README.org | 118 ----------------- altprob_model.v | 2 +- coq-monae.opam | 50 ++++++++ dune | 7 + dune-project | 6 + gcm_model.v | 15 +-- index.md | 52 ++++++++ meta.yml | 192 ++++++++++++++++++++++++++++ monad_model.v | 9 +- 11 files changed, 476 insertions(+), 132 deletions(-) create mode 100644 .github/workflows/docker-action.yml create mode 100644 README.md delete mode 100644 README.org create mode 100644 coq-monae.opam create mode 100644 dune create mode 100644 dune-project create mode 100644 index.md create mode 100644 meta.yml diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml new file mode 100644 index 00000000..28a63e62 --- /dev/null +++ b/.github/workflows/docker-action.yml @@ -0,0 +1,32 @@ +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. +name: Docker CI + +on: + push: + branches: + - master + pull_request: + branches: + - '**' + +jobs: + build: + # the OS must be GNU/Linux to be able to use the docker-coq-action + runs-on: ubuntu-latest + strategy: + matrix: + image: + - 'mathcomp/mathcomp:1.11.0-coq-8.11' + - 'mathcomp/mathcomp:1.11.0-coq-8.12' + fail-fast: false + steps: + - uses: actions/checkout@v2 + - uses: coq-community/docker-coq-action@v1 + with: + opam_file: 'coq-monae.opam' + custom_image: ${{ matrix.image }} + +# See also: +# https://github.com/coq-community/docker-coq-action#readme +# https://github.com/erikmd/docker-coq-github-action-demo diff --git a/README.md b/README.md new file mode 100644 index 00000000..e03e8374 --- /dev/null +++ b/README.md @@ -0,0 +1,125 @@ + +# Monadic effects and equational reasonig in Coq + +[![Docker CI][docker-action-shield]][docker-action-link] + +[docker-action-shield]: https://github.com/affeldt-aist/monae/workflows/Docker%20CI/badge.svg?branch=master +[docker-action-link]: https://github.com/affeldt-aist/monae/actions?query=workflow:"Docker%20CI" + + + + +This Coq library contains a hierarchy of monads with their laws used +in several examples of monadic equational reasoning. + +## Meta + +- Author(s): + - Reynald Affeldt (initial) + - David Nowak (initial) + - Takafumi Saikawa (initial) + - Jacques Garrigue + - Celestine Sauvage + - Kazunari Tanaka +- License: [LGPL-2.1-or-later](LICENSE) +- Compatible Coq versions: Coq 8.11 to 8.12 +- Additional dependencies: + - [MathComp ssreflect 1.11](https://math-comp.github.io) + - [MathComp fingroup 1.11](https://math-comp.github.io) + - [MathComp algebra 1.11](https://math-comp.github.io) + - [MathComp solvable 1.11](https://math-comp.github.io) + - [MathComp field 1.11](https://math-comp.github.io) + - [MathComp analysis 0.3.4](https://github.com/math-comp/analysis) + - [Infotheo 0.2.1](https://github.com/affeldt-aist/infotheo) + - [Paramcoq 0.1.2](https://github.com/coq-community/paramcoq) +- Coq namespace: `monae` +- Related publication(s): + - [A hierarchy of monadic effects for program verification using equational reasoning](https://staff.aist.go.jp/reynald.affeldt/documents/monae.pdf) doi:[10.1007/978-3-030-33636-3_9](https://doi.org/10.1007/978-3-030-33636-3_9) + - [A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism](https://arxiv.org/abs/2003.09993) + +## Building and installation instructions + +The easiest way to install the latest released version of Monadic effects and equational reasonig in Coq +is via [OPAM](https://opam.ocaml.org/doc/Install.html): + +```shell +opam repo add coq-released https://coq.inria.fr/opam/released +opam install coq-monae +``` + +To instead build and install manually, do: +``` shell +git clone https://github.com/affeldt-aist/monae.git +cd monae +make -j 4 +make sect5 +make -C impredicative_set +make install +``` + +## Overview + +This repository contains a formalization of monads including examples +of monadic equational reasoning and several models (in particular, a +model for a monad that mixes non-deterministic choice and +probabilistic choice). This corresponds roughly to the formalization +of the following papers: +- [Gibbons and Hinze, Just do It: Simple Monadic Equational Reasoning, ICFP 2011] (except Sect. 10.2) +- [Gibbons, Unifying Theories of Programming with Monads, UTP 2012] (up to Sect. 7.2) +- [Mu, Equational Reasoning for Non-determinism Monad: A Case study of Spark Aggregation, TR-IIS-19-002, Academia Sinica] +- [Mu, Calculating a Backtracking Algorithm: An exercise in Monadic Program Derivation, TR-IIS-29-003, Academia Sinica] +- [Mu, Functional Pearls: Reasoning and Derivation of Monadic Programs, A case study of non-determinism and state, 2017] + + This is a draft paper. In the first release, we formalized this draft up to Sect. 5. + The contents have been since superseded by [mu2019tr2] and [mu2019tr3]. + +This library has been applied to other formalizations: +- application to program semantics (see file `smallstep.v`) +- formalization of monad composition [Jones and Duponcheel, Composing Monads, Yale RR 1993] (Sections 2 and 3) +- formalization of monad transformers [Jaskelioff, Modular Monad Transformers, ESOP 2009] (up to Sect. 4) + + completed with details from [Jaskelioff, Lifting of Operations in Modular Monadic Semantics, PhD 2009] + + see directory `impredicative_set` for the formalization of [Jaskelioff, Modular Monad Transformers, ESOP 2009] up to Sect. 5 +- formalization of the geometrically convex monad (main reference: + [Cheung, Distributive Interaction of Algebraic Effects, PhD Thesis, U. Oxford, 2017]) + +![Available monads](./hier.png "Available Monads") + +## FIles. + + - [monae_lib.v](./monae_lib.v): simple additions to base libraries +- [hierarchy.v](./hierarchy.v): hierarchy of monadic effects +- [monad_lib.v](./monad_lib.v): basic lemmas about monads +- [category.v](./category.v): formalization of categories (generalization of ~hierarchy.v~) +- [fail_lib.v](./fail_lib.v): lemmas about fail monad and related monads +- [state_lib.v](./state_lib.v): lemmas about state-related monads +- [trace_lib.v](./trace_lib.v): lemmas about about the state-trace monad +- [proba_lib.v](./proba_lib.v): about the probability monad +- [monad_composition.v](./monad_composition.v): composing monads +- [monad_transformer.v](./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 `impredicate-set` +- [monad_model.v](./monad_model.v): concrete models of monads (up to state and trace monads) +- [proba_monad_model.v](./proba_monad_model.v): concrete 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 +- example_*.v: various examples (Spark aggregation, the n-queens puzzle, tree relabeling, Monty Hall problem, monad transformers, etc.) +- [smallstep.v](./smallstep.v): semantics for an imperative language, with equivalence operational semantics/denotation and sample imperative programs + +## About Installation with Windows 10 + +Installation of monae on Windows is less simple. +First install infotheo following the [instructions for Windows 10](https://github.com/affeldt-aist/infotheo). +Once infotheo is installed: +1. If opam is available, do + + `opam install coq-monae` or `git clone git@github.com:affeldt-aist/monae.git; opam install .` +2. If opam is not available (i.e., installation of MathComp using unzip, untar, cd, make, make install), + do: + + `git clone git@github.com:affeldt-aist/monae.git` + + `coq_makefile -o Makefile -f _CoqProject` + + `make` + +## Original License + +Before version 0.2, monae was distributed under the terms of the `GPL-3.0-or-later` license diff --git a/README.org b/README.org deleted file mode 100644 index 3e883f2b..00000000 --- a/README.org +++ /dev/null @@ -1,118 +0,0 @@ -* Monadic equational reasoning in Coq - -[[https://travis-ci.com/affeldt-aist/monae][file:https://travis-ci.com/affeldt-aist/monae.svg?branch=master]] - -This repository contains a formalization of monads including examples -of monadic equational reasoning and several models (in particular, a -model for a monad that mixes non-deterministic choice and -probabilistic choice). This corresponds roughly to the formalization -of the following papers: -- [Gibbons and Hinze, Just do It: Simple Monadic Equational Reasoning, ICFP 2011] (except Sect. 10.2) -- [Gibbons, Unifying Theories of Programming with Monads, UTP 2012] (up to Sect. 7.2) -- [Mu, Equational Reasoning for Non-determinism Monad: A Case study of Spark Aggregation, TR-IIS-19-002, Academia Sinica] -- [Mu, Calculating a Backtracking Algorithm: An exercise in Monadic Program Derivation, TR-IIS-29-003, Academia Sinica] -- [Mu, Functional Pearls: Reasoning and Derivation of Monadic Programs, A case study of non-determinism and state, 2017] - + This is a draft paper. In the first release, we formalized this draft up to Sect. 5. - The contents have been since superseded by [mu2019tr2] and [mu2019tr3]. - -This library has been applied to other formalizations: -- application to program semantics (see file ~smallstep.v~) -- formalization of monad composition [Jones and Duponcheel, Composing Monads, Yale RR 1993] (Sections 2 and 3) -- formalization of monad transformers [Jaskelioff, Modular Monad Transformers, ESOP 2009] (up to Sect. 4) - + completed with details from [Jaskelioff, Lifting of Operations in Modular Monadic Semantics, PhD 2009] - + see directory ~impredicative_set~ for the formalization of [Jaskelioff, Modular Monad Transformers, ESOP 2009] up to Sect. 5 -- formalization of the geometrically convex monad (main reference: - [Cheung, Distributive Interaction of Algebraic Effects, PhD Thesis, U. Oxford, 2017]) - -** Available monads - [[hier.png]] - -** Files - -- [[monae_lib.v][monae_lib.v]]: simple additions to base libraries -- [[hierarchy.v][hierarchy.v]]: hierarchy of monadic effects -- [[monad_lib.v][monad_lib.v]]: basic lemmas about monads -- [[category.v][category.v]]: formalization of categories (generalization of ~hierarchy.v~) -- [[fail_lib.v][fail_lib.v]]: lemmas about fail monad and related monads -- [[state_lib.v][state_lib.v]]: lemmas about state-related monads -- [[trace_lib.v][trace_lib.v]]: lemmas about about the state-trace monad -- [[proba_lib.v][proba_lib.v]]: about the probability monad -- [[monad_composition.v][monad_composition.v]]: composing monads -- [[monad_transformer.v][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 ~impredicate-set~ -- [[monad_model.v][monad_model.v]]: concrete models of monads (up to state and trace monads) -- [[proba_monad_model.v][proba_monad_model.v]]: concrete 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 -- example_*.v: various examples (Spark aggregation, the n-queens puzzle, tree relabeling, Monty Hall problem, monad transformers, etc.) -- [[smallstep.v][smallstep.v]]: semantics for an imperative language, with equivalence operational semantics/denotation and sample imperative programs - -** Installation - - The preferred way to install monae is with opam because it takes - care of the dependencies with other libraries. If not already done, - add the repository for Coq libraries to opam and update: - -1. ~opam repo add coq-released https://coq.inria.fr/opam/released~ -2. ~opam update~ - -*** Last stable version: - -Version 0.2: -3. ~opam install coq-monae~ - -**** Requirements - -- [[https://coq.inria.fr][Coq]] 8.11 or 8.12 -- [[https://github.com/math-comp/math-comp][Mathematical Components library]] 1.11.0 -- [[https://github.com/affeldt-aist/infotheo][infotheo]] 0.2 - + which requires [[https://github.com/math-comp/analysis][MathComp-Analysis]] 0.3.2 - * which requires - - [[https://github.com/math-comp/finmap][finmap]] 1.5.0 - -All versions available from opam. - -*** Development version (git master): - -With Coq 8.11 or 8.12 and the last stable release of infotheo -(the ~impredicative_set~ directory (as well as `make sect5`) require ParamCoq). - -3. ~git clone git@github.com:affeldt-aist/monae.git~ -4. ~cd monae~ - -If opam is installed, do: - -5. ~opam install .~ - -opam takes care of the dependencies. - -If opam is not installed but if the requirements are met, do: - -1. ~make~ -2. ~make install~ - -*** About Windows 10 - -Installation of monae on Windows is less simple. -First install infotheo following the [[https://github.com/affeldt-aist/infotheo][instructions for Windows 10]]. -Once infotheo is installed: -1. If opam is available, do - + ~opam install coq-monae~ or ~git clone git@github.com:affeldt-aist/monae.git; opam install .~ -2. If opam is not available (i.e., installation of MathComp using unzip, untar, cd, make, make install), - do: - + ~git clone git@github.com:affeldt-aist/monae.git~ - + ~coq_makefile -o Makefile -f _CoqProject~ - + ~make~ - -** License - -LGPL-2.1-or-later - -(Before version 0.2, monae was distributed under the terms of the -~GPL-3.0-or-later~ license.) - -** References -- [[https://staff.aist.go.jp/reynald.affeldt/bib/bib_en.html#affeldt2019mpc][MPC 2019 paper]] -- [[https://arxiv.org/abs/2003.09993][A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism]] (arXiv 2020) - diff --git a/altprob_model.v b/altprob_model.v index 518a39a8..9e34efc8 100644 --- a/altprob_model.v +++ b/altprob_model.v @@ -311,7 +311,7 @@ rewrite /necset_convType.pre_pre_conv /=. Local Open Scope convex_scope. set mk1d := fun b : choice_of_Type bool => FSDist1.d b. move/(f_equal (fun x : FSDist.t _ -> _ => x (mk1d true <|p|> mk1d false))). -set tmp := ex _. +rewrite /mkset; set tmp := ex _. move=> Heq. have: tmp -> tmp by []. rewrite {2}Heq /tmp {Heq tmp}. diff --git a/coq-monae.opam b/coq-monae.opam new file mode 100644 index 00000000..2cd08e14 --- /dev/null +++ b/coq-monae.opam @@ -0,0 +1,50 @@ +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. + +opam-version: "2.0" +maintainer: "Reynald Affeldt " +version: "dev" + +homepage: "https://github.com/affeldt-aist/monae" +dev-repo: "git+https://github.com/affeldt-aist/monae.git" +bug-reports: "https://github.com/affeldt-aist/monae/issues" +license: "LGPL-2.1-or-later" + +synopsis: "Monads and equational reasoning in Coq" +description: """ +This Coq library contains a hierarchy of monads with their laws used +in several examples of monadic equational reasoning.""" + +build: [ + [make "-j%{jobs}%"] + [make "sect5"] + [make "-C" "impredicative_set"] +] +install: [make "install"] +depends: [ + "coq" { (>= "8.11" & < "8.13~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "1.11.0" & < "1.12~") } + "coq-mathcomp-fingroup" { (>= "1.11.0" & < "1.12~") } + "coq-mathcomp-algebra" { (>= "1.11.0" & < "1.12~") } + "coq-mathcomp-solvable" { (>= "1.11.0" & < "1.12~") } + "coq-mathcomp-field" { (>= "1.11.0" & < "1.12~") } + "coq-mathcomp-analysis" { (= "0.3.4") } + "coq-infotheo" { >= "0.2.1" } + "coq-paramcoq" { >= "1.1.2" & < "1.2~" } +] + +tags: [ + "keyword:monae" + "keyword:effect" + "keyword:probability" + "keyword:nondeterminism" + "logpath:monae" +] +authors: [ + "Reynald Affeldt" + "David Nowak" + "Takafumi Saikawa" + "Jacques Garrigue" + "Celestine Sauvage" + "Kazunari Tanaka" +] diff --git a/dune b/dune new file mode 100644 index 00000000..c07e504d --- /dev/null +++ b/dune @@ -0,0 +1,7 @@ +; This file was generated from `meta.yml`, please do not edit manually. +; Follow the instructions on https://github.com/coq-community/templates to regenerate. + +(coq.theory + (name monae) + (package coq-monae) + (synopsis "Monads and equational reasoning in Coq")) diff --git a/dune-project b/dune-project new file mode 100644 index 00000000..5c03c91e --- /dev/null +++ b/dune-project @@ -0,0 +1,6 @@ +; This file was generated from `meta.yml`, please do not edit manually. +; Follow the instructions on https://github.com/coq-community/templates to regenerate. + +(lang dune 2.5) +(using coq 0.2) +(name monae) diff --git a/gcm_model.v b/gcm_model.v index 08357949..0c2d822d 100644 --- a/gcm_model.v +++ b/gcm_model.v @@ -504,7 +504,7 @@ move=> F. rewrite /eps1''. transitivity (|_| (lub_op @` ((fun X : necset_semiCompSemiLattType L => (X : neset _)) @` F))%:ne); last first. - congr (|_| _). - apply/neset_ext/eqEsubset => x [] x0 Fx0 <-. + apply/neset_ext; rewrite eqEsubset; split => x [] x0 Fx0 <-. + by case: Fx0 => x1 Fx1 <-; exists x1. + by exists x0 => // ; exists x0. transitivity (|_| (hull (\bigcup_(x in F) x))%:ne); @@ -518,8 +518,7 @@ move=> X Y p. rewrite /affine_function_at /eps1''. transitivity (|_| (X :<| p |>: Y)%:ne); last by rewrite lub_op_conv_setD. congr (|_| _%:ne); apply/neset_ext => /=. -rewrite conv_setE necset_convType.convE. -apply eqEsubset=> u. +rewrite conv_setE necset_convType.convE eqEsubset; split=> u. - case=> x [] y [] xX [] yY ->. exists x; first by rewrite -in_setE. by rewrite conv_pt_setE; exists y; first by rewrite -in_setE. @@ -555,7 +554,7 @@ Definition eta1'' (C : convType) (x : C) : necset_convType C := necset1 x. Lemma eta1''_affine (C : convType) : affine_function (@eta1'' C). Proof. move=> a b p; rewrite /affine_function_at /eta1'' /=. -apply/necset_ext/eqEsubset=> x /=. +apply/necset_ext; rewrite eqEsubset; split=> x /=. - move->; rewrite necset_convType.convE. by exists a, b; rewrite !asboolE /necset1 /=. - rewrite necset_convType.convE => -[] a0 [] b0. @@ -585,12 +584,11 @@ Proof. move=> c; apply funext=> x /=; apply/necset_ext=> /=. rewrite eps1E eta1E' /= free_semiCompSemiLattConvType_morE' /= /eta1'' /=. rewrite -[in RHS](hull_cset x); congr hull. -apply/eqEsubset=> a /=. +rewrite eqEsubset; split=> a /=. - case=> y [] b xb <-. by rewrite necset1E => ->. - move=> xa. - exists (necset1 a); last by rewrite necset1E. - by exists a. + by exists (necset1 a); [exists a | rewrite necset1E]. Qed. Lemma triR1 : TriangularLaws.right eta1 eps1. Proof. @@ -720,8 +718,7 @@ rewrite -(bigcup_image (fun x => if x \in necset_join.F1join0 X then NECSet.car x else set0) idfun). simpl. congr hull. -rewrite /bigsetU. -apply/eqEsubset => y [i Xi iy]. +rewrite /bigsetU eqEsubset; split => y [i Xi iy]. - exists i; last exact: iy. exists i => //. by move/asboolP : Xi; rewrite asboolE -in_setE => ->. diff --git a/index.md b/index.md new file mode 100644 index 00000000..68b79e01 --- /dev/null +++ b/index.md @@ -0,0 +1,52 @@ +--- +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. +title: Monadic effects and equational reasonig in Coq +lang: en +header-includes: + - | + + + + + +--- + +
+View the project on GitHub +
+ +## About + +Welcome to the Monadic effects and equational reasonig in Coq project website! + +This Coq library contains a hierarchy of monads with their laws used +in several examples of monadic equational reasoning. + +This is an open source project, licensed under the LGPL-2.1-or-later. + +## Get the code + +The current stable release of Monadic effects and equational reasonig in Coq can be [downloaded from GitHub](https://github.com/affeldt-aist/monae/releases). + +## Documentation + + +Related publications, if any, are listed below. + +- [A hierarchy of monadic effects for program verification using equational reasoning](https://staff.aist.go.jp/reynald.affeldt/documents/monae.pdf) doi:[10.1007/978-3-030-33636-3_9](https://doi.org/10.1007/978-3-030-33636-3_9) +- [A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism](https://arxiv.org/abs/2003.09993) + +## Help and contact + +- Report issues on [GitHub](https://github.com/affeldt-aist/monae/issues) + +## Authors and contributors + +- Reynald Affeldt +- David Nowak +- Takafumi Saikawa +- Jacques Garrigue +- Celestine Sauvage +- Kazunari Tanaka + diff --git a/meta.yml b/meta.yml new file mode 100644 index 00000000..58786b43 --- /dev/null +++ b/meta.yml @@ -0,0 +1,192 @@ +fullname: Monadic effects and equational reasonig in Coq +shortname: monae +organization: affeldt-aist +opam_name: coq-monae +community: false +action: true +coqdoc: false + +synopsis: >- + Monads and equational reasoning in Coq +description: |- + This Coq library contains a hierarchy of monads with their laws used + in several examples of monadic equational reasoning. +authors: +- name: Reynald Affeldt + initial: true +- name: David Nowak + initial: true +- name: Takafumi Saikawa + initial: true +- name: Jacques Garrigue + initial: false +- name: Celestine Sauvage + initial: false +- name: Kazunari Tanaka + initial: false + +opam-file-maintainer: Reynald Affeldt + +license: + fullname: LGPL-2.1-or-later + identifier: LGPL-2.1-or-later + file: LICENSE + +supported_coq_versions: + text: Coq 8.11 to 8.12 + opam: '{ (>= "8.11" & < "8.13~") | (= "dev") }' + +tested_coq_opam_versions: +- version: '1.11.0-coq-8.11' + repo: 'mathcomp/mathcomp' +- version: '1.11.0-coq-8.12' + repo: 'mathcomp/mathcomp' + +dependencies: +- opam: + name: coq-mathcomp-ssreflect + version: '{ (>= "1.11.0" & < "1.12~") }' + description: |- + [MathComp ssreflect 1.11](https://math-comp.github.io) +- opam: + name: coq-mathcomp-fingroup + version: '{ (>= "1.11.0" & < "1.12~") }' + description: |- + [MathComp fingroup 1.11](https://math-comp.github.io) +- opam: + name: coq-mathcomp-algebra + version: '{ (>= "1.11.0" & < "1.12~") }' + description: |- + [MathComp algebra 1.11](https://math-comp.github.io) +- opam: + name: coq-mathcomp-solvable + version: '{ (>= "1.11.0" & < "1.12~") }' + description: |- + [MathComp solvable 1.11](https://math-comp.github.io) +- opam: + name: coq-mathcomp-field + version: '{ (>= "1.11.0" & < "1.12~") }' + description: |- + [MathComp field 1.11](https://math-comp.github.io) +- opam: + name: coq-mathcomp-analysis + version: '{ (= "0.3.4") }' + description: |- + [MathComp analysis 0.3.4](https://github.com/math-comp/analysis) +- opam: + name: coq-infotheo + version: '{ >= "0.2.1" }' + description: |- + [Infotheo 0.2.1](https://github.com/affeldt-aist/infotheo) +- opam: + name: coq-paramcoq + version: '{ >= "1.1.2" & < "1.2~" }' + description: |- + [Paramcoq 0.1.2](https://github.com/coq-community/paramcoq) + +namespace: monae + +keywords: +- name: monae +- name: effect +- name: probability +- name: nondeterminism + +publications: +- pub_url: https://staff.aist.go.jp/reynald.affeldt/documents/monae.pdf + pub_title: A hierarchy of monadic effects for program verification using equational reasoning + pub_doi: 10.1007/978-3-030-33636-3_9 +- pub_url: https://arxiv.org/abs/2003.09993 + pub_title: A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism + +#make_target: [ +# [make "-j%{jobs}%"] +# [make "sect5"] +# [make "-C" "impredicative_set"] +#] + +build: |- + ## Building and installation instructions + + The easiest way to install the latest released version of Monadic effects and equational reasonig in Coq + is via [OPAM](https://opam.ocaml.org/doc/Install.html): + + ```shell + opam repo add coq-released https://coq.inria.fr/opam/released + opam install coq-monae + ``` + + To instead build and install manually, do: + ``` shell + git clone https://github.com/affeldt-aist/monae.git + cd monae + make -j 4 + make sect5 + make -C impredicative_set + make install + ``` + +documentation: |- + ## Overview + + This repository contains a formalization of monads including examples + of monadic equational reasoning and several models (in particular, a + model for a monad that mixes non-deterministic choice and + probabilistic choice). This corresponds roughly to the formalization + of the following papers: + - [Gibbons and Hinze, Just do It: Simple Monadic Equational Reasoning, ICFP 2011] (except Sect. 10.2) + - [Gibbons, Unifying Theories of Programming with Monads, UTP 2012] (up to Sect. 7.2) + - [Mu, Equational Reasoning for Non-determinism Monad: A Case study of Spark Aggregation, TR-IIS-19-002, Academia Sinica] + - [Mu, Calculating a Backtracking Algorithm: An exercise in Monadic Program Derivation, TR-IIS-29-003, Academia Sinica] + - [Mu, Functional Pearls: Reasoning and Derivation of Monadic Programs, A case study of non-determinism and state, 2017] + + This is a draft paper. In the first release, we formalized this draft up to Sect. 5. + The contents have been since superseded by [mu2019tr2] and [mu2019tr3]. + + This library has been applied to other formalizations: + - application to program semantics (see file `smallstep.v`) + - formalization of monad composition [Jones and Duponcheel, Composing Monads, Yale RR 1993] (Sections 2 and 3) + - formalization of monad transformers [Jaskelioff, Modular Monad Transformers, ESOP 2009] (up to Sect. 4) + + completed with details from [Jaskelioff, Lifting of Operations in Modular Monadic Semantics, PhD 2009] + + see directory `impredicative_set` for the formalization of [Jaskelioff, Modular Monad Transformers, ESOP 2009] up to Sect. 5 + - formalization of the geometrically convex monad (main reference: + [Cheung, Distributive Interaction of Algebraic Effects, PhD Thesis, U. Oxford, 2017]) + + ![Available monads](./hier.png "Available Monads") + + ## FIles. + + - [monae_lib.v](./monae_lib.v): simple additions to base libraries + - [hierarchy.v](./hierarchy.v): hierarchy of monadic effects + - [monad_lib.v](./monad_lib.v): basic lemmas about monads + - [category.v](./category.v): formalization of categories (generalization of ~hierarchy.v~) + - [fail_lib.v](./fail_lib.v): lemmas about fail monad and related monads + - [state_lib.v](./state_lib.v): lemmas about state-related monads + - [trace_lib.v](./trace_lib.v): lemmas about about the state-trace monad + - [proba_lib.v](./proba_lib.v): about the probability monad + - [monad_composition.v](./monad_composition.v): composing monads + - [monad_transformer.v](./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 `impredicate-set` + - [monad_model.v](./monad_model.v): concrete models of monads (up to state and trace monads) + - [proba_monad_model.v](./proba_monad_model.v): concrete 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 + - example_*.v: various examples (Spark aggregation, the n-queens puzzle, tree relabeling, Monty Hall problem, monad transformers, etc.) + - [smallstep.v](./smallstep.v): semantics for an imperative language, with equivalence operational semantics/denotation and sample imperative programs + + ## About Installation with Windows 10 + + Installation of monae on Windows is less simple. + First install infotheo following the [instructions for Windows 10](https://github.com/affeldt-aist/infotheo). + Once infotheo is installed: + 1. If opam is available, do + + `opam install coq-monae` or `git clone git@github.com:affeldt-aist/monae.git; opam install .` + 2. If opam is not available (i.e., installation of MathComp using unzip, untar, cd, make, make install), + do: + + `git clone git@github.com:affeldt-aist/monae.git` + + `coq_makefile -o Makefile -f _CoqProject` + + `make` + + ## Original License + + Before version 0.2, monae was distributed under the terms of the `GPL-3.0-or-later` license diff --git a/monad_model.v b/monad_model.v index 2a41ec85..24b062e9 100644 --- a/monad_model.v +++ b/monad_model.v @@ -166,7 +166,7 @@ Qed. Definition ret : FId ~> functor := Natural.Pack (Natural.Mixin naturality_ret). Lemma left_neutral : @BindLaws.left_neutral functor (fun A B => @bigsetU B A) ret. -Proof. move=> ? ? ? ?; exact: classical_sets_ext.bigcup_set1. Qed. +Proof. move=> ? ? ? ?; exact: bigcup_set1. Qed. Lemma right_neutral : @BindLaws.right_neutral functor (fun A B => @bigsetU B A) ret. Proof. move=> ? ?; exact: bigsetU1. Qed. @@ -788,7 +788,7 @@ Lemma setUDl : @BindLaws.left_distributive ModelMonad.SetMonad.functor (fun I A Proof. move=> A B /= p q r; rewrite boolp.funeqE => b; rewrite boolp.propeqE; split. move=> -[a [?|?] ?]; by [left; exists a | right; exists a]. -rewrite /setU => -[[a ? ?]|[a ? ?]]; exists a; tauto. +by rewrite /setU => -[[a ? ?]|[a ? ?]]; exists a => //; [left|right]. Qed. Section set. @@ -838,8 +838,9 @@ Local Obligation Tactic := idtac. Program Definition set_class := @MonadNondet.Class _ ModelFail.set_class (MonadAlt.mixin ModelAlt.set_class) _. Next Obligation. -apply: MonadNondet.Mixin => //= A p; rewrite boolp.funeqE => a; - rewrite boolp.propeqE; rewrite /Fail /= /set0 /setU; split; tauto. +by apply: MonadNondet.Mixin => //= A p; rewrite boolp.funeqE => a; + rewrite boolp.propeqE; rewrite /Fail /= /set0 /setU; split=> [[] // |pa]; + [right|left]. Qed. Definition set := MonadNondet.Pack list_class. End set.