From d1dfef885fbf3ef0cc8040e2d497ffcbc31175d6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 30 Mar 2021 15:48:52 +0200 Subject: [PATCH 1/2] Update README.md --- README.md | 73 +++++++++++++++++++++++++++++++++---------------------- 1 file changed, 44 insertions(+), 29 deletions(-) diff --git a/README.md b/README.md index ce9a81a0d..16c2f63b3 100644 --- a/README.md +++ b/README.md @@ -3,9 +3,18 @@ # Hierarchy Builder -High level commands to declare and evolve a hierarchy based on packed classes. +Hierarchy Builder (HB) provides high level commands to declare a hierarchy of algebraic structure +(or interfaces if you prefer the glossary of computer science) for the Coq system. -[Presented at FSCD2020, talk available on youtube.](https://www.youtube.com/watch?v=F6iRaTlQrlo) +Given a structure one can develop its theory, and that theory becomes automatically applicable to +all the examples of the structure. One can also declare alternative interfaces, for convenience +or backward compatibility, and provide glue code linking thse interfaces to the structures part of +the hierarchy. + +HB commands compile down to Coq modules, sections, records, coercions, canonical structure instances +and notations following the *packed classes* discipline which is at the core of the [Mathematical +Components](https://github.com/math-comp/math-comp) library. All that complexity is hidden behind +a few concepts and a few declarative Coq commands. ## Example @@ -13,14 +22,15 @@ High level commands to declare and evolve a hierarchy based on packed classes. From HB Require Import structures. From Coq Require Import ssreflect ZArith. -HB.mixin Record AddComoid_of_Type A := { +HB.mixin Record is_AddComoid A := { zero : A; add : A -> A -> A; addrA : forall x y z, add x (add y z) = add (add x y) z; addrC : forall x y, add x y = add y x; add0r : forall x, add zero x = x; }. -HB.structure Definition AddComoid := { A of AddComoid_of_Type A }. + +HB.structure Definition AddComoid := { A of is_AddComoid A }. Notation "0" := zero. Infix "+" := add. @@ -35,17 +45,18 @@ We proceed by declaring how to obtain an Abelian group out of the additive, commutative, monoid. ```coq -HB.mixin Record AbelianGrp_of_AddComoid A of AddComoid A := { +HB.mixin Record is_AbelianGrp A of AddComoid A := { opp : A -> A; addNr : forall x, opp x + x = 0; }. -HB.structure Definition AbelianGrp := { A of AbelianGrp_of_AddComoid A & }. + +HB.structure Definition AbelianGrp := { A of is_AbelianGrp A & is_AddComoid A }. Notation "- x" := (opp x). ``` Abelian groups feature the operations and properties given by the -`AbelianGrp_of_AddComoid` mixin (and its dependency `AddComoid`). +`is_AbelianGrp` mixin (and its dependency `is_AddComoid`). ```coq Lemma example (G : AbelianGrp.type) (x : G) : x + (- x) = - 0. @@ -57,9 +68,10 @@ the lemma just proved on a statement about `Z`. ```coq HB.instance Definition Z_CoMoid := - AddComoid_of_Type.Build Z 0%Z Z.add Z.add_assoc Z.add_comm Z.add_0_l. + is_AddComoid.Build Z 0%Z Z.add Z.add_assoc Z.add_comm Z.add_0_l. + HB.instance Definition Z_AbGrp := - AbelianGrp_of_AddComoid.Build Z Z.opp Z.add_opp_diag_l. + is_AbelianGrp.Build Z Z.opp Z.add_opp_diag_l. Lemma example2 (x : Z) : x + (- x) = - 0. Proof. by rewrite example. Qed. @@ -67,12 +79,8 @@ Proof. by rewrite example. Qed. ## Documentation -### Status - -The software is beta-quality, it works but error messages should be improved. - -This [draft paper](https://hal.inria.fr/hal-02478907) describes the language -in full detail. +This [paper](https://hal.inria.fr/hal-02478907) describes the language +in details, and the corresponding talk [is available on youtube.](https://www.youtube.com/watch?v=F6iRaTlQrlo) ### Installation & availability @@ -87,7 +95,8 @@ opam repo add coq-released https://coq.inria.fr/opam/released opam install coq-hierarchy-builder ``` -- You can use it in nix with the attribute `coqPackages_8_11.hierarchy-builder` e.g. via `nix-shell -p coq_8_11 -p coqPackages_8_11.hierarchy-builder` +- You can use it in nix with the attribute `coqPackages_8_11.hierarchy-builder` e.g. + via `nix-shell -p coq_8_11 -p coqPackages_8_11.hierarchy-builder`

@@ -115,19 +124,25 @@ opam install coq-hierarchy-builder
(click to expand)

-- `HB.mixin` declares a mixin -- `HB.structure` declares a structure -- `HB.factory` declares a factory -- `HB.builders` and `HB.end` declare a set of builders -- `HB.instance` declares a structure instance -- `HB.export` exports a module and schedules it for re-export -- `HB.reexport` exports all modules scheduled for re-export -- `HB.graph` prints the structure hierarchy to a dot file -- `HB.status` dumps the contents of the hierarchy (debug purposes) - -Their documentation can be found in the comments of [structures.v](structures.v), -search for `Elpi Command` and you will find them. All commands can be -prefixed with the attribute `#[verbose]` to get an idea of what they are doing. +- HB core commands: + - `HB.mixin` declares a mixin + - `HB.structure` declares a structure + - `HB.factory` declares a factory + - `HB.builders` and `HB.end` declare a set of builders + - `HB.instance` declares a structure instance + +- HB support commands: + - `HB.export` exports a module and schedules it for re-export + - `HB.reexport` exports all modules and instances scheduled for re-export + - `HB.graph` prints the structure hierarchy to a dot file + - `HB.status` dumps the contents of the hierarchy (debug purposes) + - `HB.check` is similar to `Check` (test purposes) + +The documentation of all commands can be found in the comments of +[structures.v](structures.v), search for `Elpi Command` and you will +find them. All commands can be prefixed with the attribute `#[verbose]` +to get an idea of what they are doing. + See also the `#[log]` attribute in the "Plan B" section below.

From 592eaeacc14c15fea69ee3ed53d74c01c041bfa4 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 30 Mar 2021 16:32:09 +0200 Subject: [PATCH 2/2] renaming --- README.md | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/README.md b/README.md index 16c2f63b3..14b25366b 100644 --- a/README.md +++ b/README.md @@ -8,7 +8,7 @@ Hierarchy Builder (HB) provides high level commands to declare a hierarchy of al Given a structure one can develop its theory, and that theory becomes automatically applicable to all the examples of the structure. One can also declare alternative interfaces, for convenience -or backward compatibility, and provide glue code linking thse interfaces to the structures part of +or backward compatibility, and provide glue code linking these interfaces to the structures part of the hierarchy. HB commands compile down to Coq modules, sections, records, coercions, canonical structure instances @@ -22,7 +22,7 @@ a few concepts and a few declarative Coq commands. From HB Require Import structures. From Coq Require Import ssreflect ZArith. -HB.mixin Record is_AddComoid A := { +HB.mixin Record IsAddComoid A := { zero : A; add : A -> A -> A; addrA : forall x y z, add x (add y z) = add (add x y) z; @@ -30,7 +30,7 @@ HB.mixin Record is_AddComoid A := { add0r : forall x, add zero x = x; }. -HB.structure Definition AddComoid := { A of is_AddComoid A }. +HB.structure Definition AddComoid := { A of IsAddComoid A }. Notation "0" := zero. Infix "+" := add. @@ -45,18 +45,18 @@ We proceed by declaring how to obtain an Abelian group out of the additive, commutative, monoid. ```coq -HB.mixin Record is_AbelianGrp A of AddComoid A := { +HB.mixin Record AddComoid_IsAbelianGrp A of IsAddComoid A := { opp : A -> A; addNr : forall x, opp x + x = 0; }. -HB.structure Definition AbelianGrp := { A of is_AbelianGrp A & is_AddComoid A }. +HB.structure Definition AbelianGrp := { A of AddComoid_IsAbelianGrp A & IsAddComoid A }. Notation "- x" := (opp x). ``` Abelian groups feature the operations and properties given by the -`is_AbelianGrp` mixin (and its dependency `is_AddComoid`). +`IsAbelianGrp` mixin (and its dependency `IsAddComoid`). ```coq Lemma example (G : AbelianGrp.type) (x : G) : x + (- x) = - 0. @@ -68,10 +68,10 @@ the lemma just proved on a statement about `Z`. ```coq HB.instance Definition Z_CoMoid := - is_AddComoid.Build Z 0%Z Z.add Z.add_assoc Z.add_comm Z.add_0_l. + IsAddComoid.Build Z 0%Z Z.add Z.add_assoc Z.add_comm Z.add_0_l. HB.instance Definition Z_AbGrp := - is_AbelianGrp.Build Z Z.opp Z.add_opp_diag_l. + IsAbelianGrp.Build Z Z.opp Z.add_opp_diag_l. Lemma example2 (x : Z) : x + (- x) = - 0. Proof. by rewrite example. Qed.