relicensing, new version

affeldt-aist · Oct 31, 2020 · 837ccd9 · 837ccd9
1 parent cec5170
commit 837ccd9
Show file tree

Hide file tree

Showing 36 changed files with 581 additions and 12 deletions.
diff --git a/LICENSE.txt b/LICENSE.txt
diff --git a/README.org b/README.org
@@ -45,10 +45,7 @@ This library has been applied to other formalizations:
 - [[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_spark.v][example_spark.v]]: example of Spark aggregation
-- [[example_nqueens.v][example_nqueens.v]]: example of the n-queens puzzle
-- [[example_relabeling.v][example_relabeling.v]]: example of tree relabeling
-- [[example_monty.v][example_monty.v]]: examples of Monty Hall problem
+- 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
@@ -62,14 +59,14 @@ This library has been applied to other formalizations:
 
 *** Last stable version:
 
-Version 0.1.2:
+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.1.2 or 0.2
+- [[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
@@ -110,8 +107,12 @@ Once infotheo is installed:
 
 ** License
 
-GNU GPLv3
+LGPL-2.1-or-later
 
-** Reference
-   [[https://staff.aist.go.jp/reynald.affeldt/bib/bib_en.html#affeldt2019mpc][MPC 2019 paper]]
+(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
@@ -1,3 +1,5 @@
+(* monae: Monadic equational reasoning in Coq                                 *)
+(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 Require Import Reals.
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require Import boolp classical_sets.

diff --git a/category.v b/category.v
@@ -1,3 +1,5 @@
+(* 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.

diff --git a/example_array.v b/example_array.v
@@ -1,3 +1,5 @@
+(* 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 boolp.
 Require Import monae_lib hierarchy monad_lib fail_lib state_lib.

diff --git a/example_monad_transformer.v b/example_monad_transformer.v
@@ -1,3 +1,5 @@
+(* 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 monad_transformer.

diff --git a/example_monty.v b/example_monty.v
@@ -1,3 +1,5 @@
+(* monae: Monadic equational reasoning in Coq                                 *)
+(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 Require Import Reals Lra.
 From mathcomp Require Import all_ssreflect.
 From infotheo Require Import ssrR Reals_ext proba.

diff --git a/example_nqueens.v b/example_nqueens.v
@@ -1,3 +1,5 @@
+(* monae: Monadic equational reasoning in Coq                                 *)
+(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 Require Import ZArith.
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.

diff --git a/example_quicksort.v b/example_quicksort.v
@@ -1,3 +1,5 @@
+(* 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 boolp.
 Require Import monae_lib hierarchy monad_lib fail_lib.

diff --git a/example_relabeling.v b/example_relabeling.v
@@ -1,3 +1,5 @@
+(* monae: Monadic equational reasoning in Coq                                 *)
+(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 Require Import ZArith.
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.

diff --git a/example_spark.v b/example_spark.v
@@ -1,3 +1,5 @@
+(* 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 boolp.
 Require Import monae_lib hierarchy monad_lib fail_lib.

diff --git a/fail_lib.v b/fail_lib.v
@@ -1,3 +1,5 @@
+(* 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 boolp.
 Require Import monae_lib hierarchy monad_lib.

diff --git a/fmt_lifting.v b/fmt_lifting.v
@@ -1,3 +1,5 @@
+(* 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 boolp.
 Require Import monae_lib hierarchy monad_lib monad_transformer.

diff --git a/gcm_model.v b/gcm_model.v
@@ -1,3 +1,5 @@
+(* monae: Monadic equational reasoning in Coq                                 *)
+(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 Require Import Reals.
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require Import boolp classical_sets.

diff --git a/hierarchy.v b/hierarchy.v
@@ -1,3 +1,5 @@
+(* monae: Monadic equational reasoning in Coq                                 *)
+(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 Ltac typeof X := type of X.
 
 Require Import ssrmatching Reals.

diff --git a/impredicative_set/iexample_monad_transformer.v b/impredicative_set/iexample_monad_transformer.v
@@ -1,3 +1,5 @@
+(* 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
  imonad_transformer imonad_model.

diff --git a/impredicative_set/ifail_lib.v b/impredicative_set/ifail_lib.v
@@ -1,3 +1,5 @@
+(* 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.
 

diff --git a/impredicative_set/ifmt_lifting.v b/impredicative_set/ifmt_lifting.v
@@ -1,3 +1,5 @@
+(* 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 imonad_transformer.
 

diff --git a/impredicative_set/ihierarchy.v b/impredicative_set/ihierarchy.v
@@ -1,3 +1,5 @@
+(* monae: Monadic equational reasoning in Coq                                 *)
+(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 Ltac typeof X := type of X.
 
 Require Import ssrmatching.

diff --git a/impredicative_set/imonad_model.v b/impredicative_set/imonad_model.v
@@ -1,3 +1,5 @@
+(* 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 finmap.
 From mathcomp Require Import classical_sets.

diff --git a/impredicative_set/imonad_transformer.v b/impredicative_set/imonad_transformer.v
@@ -1,3 +1,5 @@
+(* 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.
 

diff --git a/impredicative_set/imonae_lib.v b/impredicative_set/imonae_lib.v
@@ -1,3 +1,5 @@
+(* monae: Monadic equational reasoning in Coq                                 *)
+(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
 Require FunctionalExtensionality ProofIrrelevance.
 

diff --git a/impredicative_set/iparametricity_codensity.v b/impredicative_set/iparametricity_codensity.v
@@ -1,3 +1,5 @@
+(* monae: Monadic equational reasoning in Coq                                 *)
+(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 Declare ML Module "paramcoq".
 
 From mathcomp Require Import all_ssreflect.

diff --git a/impredicative_set/istate_lib.v b/impredicative_set/istate_lib.v
@@ -1,3 +1,5 @@
+(* monae: Monadic equational reasoning in Coq                                 *)
+(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 Require Import ZArith.
 From mathcomp Require Import all_ssreflect.
 From infotheo Require Import ssrZ.

diff --git a/impredicative_set/itrace_lib.v b/impredicative_set/itrace_lib.v
@@ -1,3 +1,5 @@
+(* monae: Monadic equational reasoning in Coq                                 *)
+(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 Ltac typeof X := type of X.
 Require Import ZArith.
 From mathcomp Require Import all_ssreflect.

diff --git a/monad_composition.v b/monad_composition.v
@@ -1,3 +1,5 @@
+(* 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.
 

diff --git a/monad_lib.v b/monad_lib.v
@@ -1,3 +1,5 @@
+(* monae: Monadic equational reasoning in Coq                                 *)
+(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 Ltac typeof X := type of X.
 
 Require Import ssrmatching.

diff --git a/monad_transformer.v b/monad_transformer.v
@@ -1,3 +1,5 @@
+(* 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 boolp.
 Require Import monae_lib hierarchy monad_lib fail_lib state_lib.

diff --git a/monae_lib.v b/monae_lib.v
@@ -1,3 +1,5 @@
+(* 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 boolp.
 Require ProofIrrelevance FunctionalExtensionality.

diff --git a/opam b/opam
@@ -3,7 +3,7 @@ maintainer: "[email protected]"
 homepage: "https://github.com/affeldt-aist/monae"
 bug-reports: "https://github.com/affeldt-aist/monae/issues"
 dev-repo: "git+https://github.com/affeldt-aist/monae.git"
-license: "GPL-3.0-or-later"
+license: "LGPL-2.1-or-later"
 authors: [
   "Reynald Affeldt"
   "David Nowak"
@@ -22,7 +22,7 @@ install: [
 ]
 depends: [
   "coq" { >= "8.11" & < "8.13~" }
-  "coq-infotheo" { >= "0.1.2" & <= "0.2" }
+  "coq-infotheo" { >= "0.2" & < "0.3~" }
   "coq-paramcoq" { >= "1.1.2" & < "1.2~" }
 ]
 synopsis: "Monads and equational reasoning in Coq"
@@ -37,5 +37,5 @@ tags: [
   "keyword: probability"
   "keyword: nondeterminism"
   "logpath:monae"
-  "date:2020-08-13"
+  "date:2020-10-31"
 ]
diff --git a/parametricity_codensity.v b/parametricity_codensity.v
@@ -1,3 +1,5 @@
+(* monae: Monadic equational reasoning in Coq                                 *)
+(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 Declare ML Module "paramcoq".
 
 From mathcomp Require Import all_ssreflect.

diff --git a/proba_lib.v b/proba_lib.v
@@ -1,3 +1,5 @@
+(* monae: Monadic equational reasoning in Coq                                 *)
+(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 Require Import Reals Lra.
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.

diff --git a/proba_monad_model.v b/proba_monad_model.v
@@ -1,3 +1,5 @@
+(* 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 boolp.
 From infotheo Require Import Reals_ext ssr_ext fsdist.

diff --git a/smallstep.v b/smallstep.v
@@ -1,3 +1,5 @@
+(* monae: Monadic equational reasoning in Coq                                 *)
+(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 Require Import Eqdep JMeq List ssreflect.
 Import ListNotations.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.

diff --git a/state_lib.v b/state_lib.v
@@ -1,3 +1,5 @@
+(* monae: Monadic equational reasoning in Coq                                 *)
+(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 Require Import ZArith.
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.

diff --git a/trace_lib.v b/trace_lib.v
@@ -1,3 +1,5 @@
+(* monae: Monadic equational reasoning in Coq                                 *)
+(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 Ltac typeof X := type of X.
 Require Import ZArith.
 From mathcomp Require Import all_ssreflect.