From 6f1dee653303245814417c863535dfbe4ef1ada5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 2 Jun 2023 15:15:44 +0200 Subject: [PATCH 01/10] test for step 0 of CoREACT --- _CoqProject.test-suite | 1 + tests/monoid_law_structure.v | 18 ++++++++++++++++++ 2 files changed, 19 insertions(+) create mode 100644 tests/monoid_law_structure.v diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index 98c20167e..80c32c4af 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -80,6 +80,7 @@ tests/hnf.v tests/fun_instance.v tests/issue284.v tests/issue287.v +tests/monoid_law_structure.v -R tests HB.tests -R examples HB.examples diff --git a/tests/monoid_law_structure.v b/tests/monoid_law_structure.v new file mode 100644 index 000000000..e43439164 --- /dev/null +++ b/tests/monoid_law_structure.v @@ -0,0 +1,18 @@ +From HB Require Import structures. + +HB.mixin Record isMonLaw T (e : T) (op : T -> T -> T) := { + opmA : forall a b c, op (op a b) c = op a (op b c); + op1m : forall x, op e x = x; + opm1 : forall x, op x e = x; +}. + +HB.structure Definition MonLaw T e := { op of isMonLaw T e op }. + +HB.mixin Record isPreMonoid T := { + zero : T; + add : T -> T -> T; +}. +HB.structure Definition PreMonoid := { T of isPreMonoid T }. + +HB.structure Definition Monoid := + { T of isPreMonoid T & isMonLaw T zero add }. From 1ceb6ea4c9e46836f37f712aaa1918db485309e2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 2 Jun 2023 15:38:25 +0200 Subject: [PATCH 02/10] update --- tests/monoid_law_structure.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/tests/monoid_law_structure.v b/tests/monoid_law_structure.v index e43439164..3d6f8e0d5 100644 --- a/tests/monoid_law_structure.v +++ b/tests/monoid_law_structure.v @@ -15,4 +15,6 @@ HB.mixin Record isPreMonoid T := { HB.structure Definition PreMonoid := { T of isPreMonoid T }. HB.structure Definition Monoid := - { T of isPreMonoid T & isMonLaw T zero add }. + { T of isPreMonoid T & + isMonLaw T zero add }. + (* isMonLaw T (@zero (PreMonoid.clone T _)) (@add (PreMonoid.clone T _))*) From f6c1970f4748fcff2fe4b1234ef3fb158d72e173 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 2 Jun 2023 15:52:10 +0200 Subject: [PATCH 03/10] more --- _CoqProject.test-suite | 1 + tests/monoid_law_structure.v | 4 +--- tests/monoid_law_structure_clone.v | 19 +++++++++++++++++++ 3 files changed, 21 insertions(+), 3 deletions(-) create mode 100644 tests/monoid_law_structure_clone.v diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index 80c32c4af..9661f9ac8 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -81,6 +81,7 @@ tests/fun_instance.v tests/issue284.v tests/issue287.v tests/monoid_law_structure.v +tests/monoid_law_structure_clone.v -R tests HB.tests -R examples HB.examples diff --git a/tests/monoid_law_structure.v b/tests/monoid_law_structure.v index 3d6f8e0d5..b78f06c69 100644 --- a/tests/monoid_law_structure.v +++ b/tests/monoid_law_structure.v @@ -15,6 +15,4 @@ HB.mixin Record isPreMonoid T := { HB.structure Definition PreMonoid := { T of isPreMonoid T }. HB.structure Definition Monoid := - { T of isPreMonoid T & - isMonLaw T zero add }. - (* isMonLaw T (@zero (PreMonoid.clone T _)) (@add (PreMonoid.clone T _))*) + { T of isPreMonoid T & isMonLaw T zero add }. diff --git a/tests/monoid_law_structure_clone.v b/tests/monoid_law_structure_clone.v new file mode 100644 index 000000000..5df341567 --- /dev/null +++ b/tests/monoid_law_structure_clone.v @@ -0,0 +1,19 @@ +From HB Require Import structures. + +HB.mixin Record isMonLaw T (e : T) (op : T -> T -> T) := { + opmA : forall a b c, op (op a b) c = op a (op b c); + op1m : forall x, op e x = x; + opm1 : forall x, op x e = x; +}. + +HB.structure Definition MonLaw T e := { op of isMonLaw T e op }. + +HB.mixin Record isPreMonoid T := { + zero : T; + add : T -> T -> T; +}. +HB.structure Definition PreMonoid := { T of isPreMonoid T }. + +HB.structure Definition Monoid := + { T of isPreMonoid T & + isMonLaw T (@zero (PreMonoid.clone T _)) (@add (PreMonoid.clone T _)) }. From 17d6561596115b759fa5c317a7e03cbca9342a33 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 2 Jun 2023 16:18:01 +0200 Subject: [PATCH 04/10] more --- tests/monoid_enriched_cat.v | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 tests/monoid_enriched_cat.v diff --git a/tests/monoid_enriched_cat.v b/tests/monoid_enriched_cat.v new file mode 100644 index 000000000..f0552a4e9 --- /dev/null +++ b/tests/monoid_enriched_cat.v @@ -0,0 +1,37 @@ +From HB Require Import structures. +From Coq Require Import ssreflect ssrfun. + +HB.mixin Record isQuiver Obj := { hom : Obj -> Obj -> Type }. + +HB.structure Definition Quiver := { Obj of isQuiver Obj }. + +HB.mixin Record isMon A := { + zero : A; + add : A -> A -> A; + addrA : associative add; + add0r : left_id zero add; + addr0 : right_id zero add; + }. + +HB.structure + Definition Monoid := { A of isMon A }. + +Fail HB.structure + Definition Monoid_enriched_quiver := + { Obj of isQuiver Obj & + (forall A B : Obj, isMon (@hom (Quiver.clone Obj _) A B)) }. + + +HB.mixin Record hom_isMon T of Quiver T := + { private : forall A B, isMon (@hom T A B) }. + +HB.structure + Definition Monoid_enriched_quiver := + { Obj of isQuiver Obj & hom_isMon Obj }. + +HB.instance Definition _ (T : Monoid_enriched_quiver.type) (A B : T) : isMon (@hom T A B) := + @private T A B. + + (* each instance of isMon should be tried as an instance of hom_isMon *) + + From d2bc00fb29bec805195af4123a8c44594cc09d19 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Mon, 19 Jun 2023 16:07:25 +0200 Subject: [PATCH 05/10] Update tests/monoid_enriched_cat.v --- tests/monoid_enriched_cat.v | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/tests/monoid_enriched_cat.v b/tests/monoid_enriched_cat.v index f0552a4e9..4aa63cd87 100644 --- a/tests/monoid_enriched_cat.v +++ b/tests/monoid_enriched_cat.v @@ -34,4 +34,9 @@ HB.instance Definition _ (T : Monoid_enriched_quiver.type) (A B : T) : isMon (@h (* each instance of isMon should be tried as an instance of hom_isMon *) - +HB.instance Definition _ := isQuiver.Build Type (fun A B => A -> B). +Fail HB.instance Definition homTypeMon (A B : Quiver.type) := isMon.Build (hom A B) (* ... *). +(* This last command should create a `Monoid_enriched_quiver`, in order to do so it should + automatically instanciate the wrapper `hom_isMon`: + HB.instance Definition _ := hom_isMon.Build Type homTypeMon. + *) From 6726472407ef61191d663e32f08a625ed8de3564 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Mon, 19 Jun 2023 16:10:12 +0200 Subject: [PATCH 06/10] Update tests/monoid_enriched_cat.v --- tests/monoid_enriched_cat.v | 3 +++ 1 file changed, 3 insertions(+) diff --git a/tests/monoid_enriched_cat.v b/tests/monoid_enriched_cat.v index 4aa63cd87..2a380990d 100644 --- a/tests/monoid_enriched_cat.v +++ b/tests/monoid_enriched_cat.v @@ -25,6 +25,9 @@ Fail HB.structure HB.mixin Record hom_isMon T of Quiver T := { private : forall A B, isMon (@hom T A B) }. +(* Step 2: at structure declaration, export the main and only projection + of each declared wrapper as an instance of the wrapped structure on + its subject *) HB.structure Definition Monoid_enriched_quiver := { Obj of isQuiver Obj & hom_isMon Obj }. From 0821793a406d2d5a725622c5cd1b381ad950a0f3 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Mon, 19 Jun 2023 16:10:18 +0200 Subject: [PATCH 07/10] Update tests/monoid_enriched_cat.v --- tests/monoid_enriched_cat.v | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/tests/monoid_enriched_cat.v b/tests/monoid_enriched_cat.v index 2a380990d..7b00b8913 100644 --- a/tests/monoid_enriched_cat.v +++ b/tests/monoid_enriched_cat.v @@ -22,6 +22,14 @@ Fail HB.structure (forall A B : Obj, isMon (@hom (Quiver.clone Obj _) A B)) }. +(* Step 0: define a wrapper predicate in coq-elpi *) +(* Step 1: add a wrapper attribute to declare wrappers, + they should index: + - the wrapped mixin (`isMon`) + - the wrapper mixin (`hom_isMon`) + - the new subject (`hom`) + *) +#[wrapper] HB.mixin Record hom_isMon T of Quiver T := { private : forall A B, isMon (@hom T A B) }. From 234e3f5d3b354ec0e849600f8507adccf06e59d6 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Mon, 19 Jun 2023 16:11:38 +0200 Subject: [PATCH 08/10] Update tests/monoid_enriched_cat.v --- tests/monoid_enriched_cat.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tests/monoid_enriched_cat.v b/tests/monoid_enriched_cat.v index 7b00b8913..16dc0091b 100644 --- a/tests/monoid_enriched_cat.v +++ b/tests/monoid_enriched_cat.v @@ -45,6 +45,8 @@ HB.instance Definition _ (T : Monoid_enriched_quiver.type) (A B : T) : isMon (@h (* each instance of isMon should be tried as an instance of hom_isMon *) +(* Step 3: for each instance of a wrapped mixin on a subject known + to be wrapped, automatically produce an instance of the wrapper mixin too. *) HB.instance Definition _ := isQuiver.Build Type (fun A B => A -> B). Fail HB.instance Definition homTypeMon (A B : Quiver.type) := isMon.Build (hom A B) (* ... *). (* This last command should create a `Monoid_enriched_quiver`, in order to do so it should From 92e1f685272a9817754121a719cf1b8816722d28 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Mon, 19 Jun 2023 16:24:58 +0200 Subject: [PATCH 09/10] Update tests/monoid_enriched_cat.v --- tests/monoid_enriched_cat.v | 3 +++ 1 file changed, 3 insertions(+) diff --git a/tests/monoid_enriched_cat.v b/tests/monoid_enriched_cat.v index 16dc0091b..20e2dd2e3 100644 --- a/tests/monoid_enriched_cat.v +++ b/tests/monoid_enriched_cat.v @@ -23,6 +23,9 @@ Fail HB.structure (* Step 0: define a wrapper predicate in coq-elpi *) +(* 5 lines of documentation + 1 line of elpi code in structure.v + `pred wrapper-mixin o:mixinname, o:gref, o:mixinname` +*) (* Step 1: add a wrapper attribute to declare wrappers, they should index: - the wrapped mixin (`isMon`) From b7f37892933bdc1f959beea4c4b3670875f9025d Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Mon, 19 Jun 2023 16:27:52 +0200 Subject: [PATCH 10/10] Update tests/monoid_enriched_cat.v --- tests/monoid_enriched_cat.v | 3 +++ 1 file changed, 3 insertions(+) diff --git a/tests/monoid_enriched_cat.v b/tests/monoid_enriched_cat.v index 20e2dd2e3..002d1f506 100644 --- a/tests/monoid_enriched_cat.v +++ b/tests/monoid_enriched_cat.v @@ -31,6 +31,9 @@ Fail HB.structure - the wrapped mixin (`isMon`) - the wrapper mixin (`hom_isMon`) - the new subject (`hom`) + This attribute will add an entry in the `wrapper-mixin` database. + As an addition substep, we should check that the wrapper has + exactly one field, which is the wrapped mixin. *) #[wrapper] HB.mixin Record hom_isMon T of Quiver T :=