Ben Siraphob (Jul 12 2021 at 15:28): Ben Siraphob (Jul 12 2021 at 15:28):Trying out a simple chain of structures seems to fail with a strange error message:
Error:
parameter illtyped: In environment
A : indexed Type
The term "id_phant" has type
"phantom (indexed Type) A -> phantom (indexed Type) A"
while it is expected to have type
"unify (indexed Type) Type A ?t
(Some ("is not canonically a", Semigroup.type))".
How can I reorganize the Semigroup <: Monoid <: Group hierarchy for this to work?
From HB Require Import structures.
From Coq Require Import ssreflect ZArith.
HB.mixin Record IsSemigroup A := {
add : A -> A -> A;
addrA : forall x y z, add x (add y z) = add (add x y) z;
}.
HB.structure Definition Semigroup := { A of IsSemigroup A }.
HB.mixin Record IsMonoid A of IsSemigroup A := {
zero : A;
add0r : forall x, add zero x = x;
}.
HB.structure Definition Monoid := { A of IsMonoid A }.
Notation "0" := zero.
Infix "+" := add.
Check forall (M : Monoid.type) (x : M), x + x = 0.
HB.mixin Record IsGroup A of IsMonoid A := {
opp : A -> A;
addNr : forall x, opp x + x = 0;
}.
It seems the same "bug" of https://github.com/math-comp/hierarchy-builder/issues/258.
The work around is to use of Monoid A instead of of IsMonoid A since the class (Monoid) is closed transitively, but the mixin (IsMonoid) is not, and you need all the dependency of IsMonoid to state you axiom (you need + which is in the semigroup.
Enrico Tassi (Jul 12 2021 at 15:36):or use of IsMonoid A & IsSemigroup A, which is like using the class, but more verbose
Enrico Tassi (Jul 12 2021 at 15:37):we will eventually fix this annoyance
Ben Siraphob (Jul 12 2021 at 15:37):Enrico Tassi said:
or use
of IsMonoid A & IsSemigroup A, which is like using the class, but more verbose
Ah I tried this but I get the same error
Ben Siraphob (Jul 12 2021 at 15:38):using of Monoid A works, thanks, but I run into an error when I try to add commutativity into the mix:
Enrico Tassi (Jul 12 2021 at 15:38):Hum, ok, then please post your file so that I can try it myself.
Ben Siraphob (Jul 12 2021 at 15:39):Neither IsGroup A or Group A fixes the declaration of IsComGroup
From HB Require Import structures.
From Coq Require Import ssreflect ZArith.
HB.mixin Record IsSemigroup A := {
add : A -> A -> A;
addrA : forall x y z, add x (add y z) = add (add x y) z;
}.
HB.structure Definition Semigroup := { A of IsSemigroup A }.
HB.mixin Record IsMonoid A of IsSemigroup A := {
zero : A;
add0r : forall x, add zero x = x;
}.
HB.structure Definition Monoid := { A of IsMonoid A }.
Notation "0" := zero.
Infix "+" := add.
Check forall (M : Monoid.type) (x : M), x + x = 0.
HB.mixin Record IsGroup A of Monoid A := {
opp : A -> A;
addNr : forall x, opp x + x = 0;
}.
HB.structure Definition Group := { A of IsGroup A }.
Notation "- x" := (opp x).
HB.mixin Record IsComGroup A of IsGroup A := {
addrC : forall x y, add x y = add y x;
}.
HB.structure Definition ComGroup := { A of IsComGroup A }.
as a side note I was reading chapter 8 of MCB and I can see why HB is a big improvement for the user :joy:, remembering OOP-style boilerplate is difficult
Enrico Tassi (Jul 12 2021 at 15:40):This is another problem, your axiom does not put x nor y in A. If you add a type annotation it works.
Enrico Tassi (Jul 12 2021 at 15:41):addrC : forall x y : A, add x y = add y x;
Ah that works, thanks! How can I see the generated code by HB?
Enrico Tassi (Jul 12 2021 at 15:42):You can prefix any HB command with #[log] or, if you are really brave, #[log(raw)].
Enrico Tassi (Jul 12 2021 at 15:42):But fasten you seat belt ;-)
Enrico Tassi (Jul 12 2021 at 15:43):You can also use #[verbose] to get a more gentle listing of what is going on
Ben Siraphob (Jul 12 2021 at 15:43):Spotted some minor typos in Ch 8, PR coming :)
Enrico Tassi (Jul 12 2021 at 15:43):Thanks!
Ben Siraphob (Jul 12 2021 at 15:43):Error: Attribute log is not supported
Ben Siraphob (Jul 12 2021 at 15:44):I tried #[log] HB.structure Definition Group := { A of IsGroup A }.
Enrico Tassi (Jul 12 2021 at 15:44):Hum, it was added in version 1.1.0
Enrico Tassi (Jul 12 2021 at 15:44):which version are you on?
Ben Siraphob (Jul 12 2021 at 15:44):Ah 1.0.0 that's in Nixpkgs
Enrico Tassi (Jul 12 2021 at 15:44):You can Print Module Group, but it does not print a lot of stuff
Ben Siraphob (Jul 12 2021 at 15:44):I have a PR bumping the version, hopefully @Cyril Cohen or @Vincent Laporte can review https://github.com/NixOS/nixpkgs/pull/130023
Enrico Tassi (Jul 12 2021 at 15:45):Like canonical structures etc
Ben Siraphob (Jul 12 2021 at 15:45):Ah 1.1.0 seems to cause a build failure in mathcomp-analysis
Ben Siraphob (Jul 12 2021 at 15:45):I see, this module looks identical to the one one would handwrite
Ben Siraphob (Jul 12 2021 at 15:46):Maybe mathcomp-analysis needs to be bumped also in Nixpkgs
File "./theories/measure.v", line 152, characters 0-276:
Warning: elpi: Using coq.env.add-const for declaring axioms or section
variables is deprecated. Use coq.env.add-axiom or
coq.env.add-section-variable instead
[elpi.add-const-for-axiom-or-sectionvar,deprecated]
File "./theories/measure.v", line 160, characters 0-40:
Warning: elpi: Using coq.env.add-const for declaring axioms or section
variables is deprecated. Use coq.env.add-axiom or
coq.env.add-section-variable instead
[elpi.add-const-for-axiom-or-sectionvar,deprecated]
File "./theories/measure.v", line 160, characters 0-40:
Warning: elpi: Using coq.env.add-const for declaring axioms or section
variables is deprecated. Use coq.env.add-axiom or
coq.env.add-section-variable instead
[elpi.add-const-for-axiom-or-sectionvar,deprecated]
File "./theories/measure.v", line 172, characters 0-29:
Warning:
The syntax "HB.instance Key FactoryInstance" is deprecated, use "HB.instance Definition" instead
[lib,elpi]
File "./theories/measure.v", line 180, characters 0-29:
Warning:
The syntax "HB.instance Key FactoryInstance" is deprecated, use "HB.instance Definition" instead
[lib,elpi]
File "./theories/measure.v", line 212, characters 6-17:
Error: measurableT already exists.
Yeah it's version 0.3.6 on Nixpkgs instead of 0.3.9
Ben Siraphob (Jul 12 2021 at 15:48):Are there limitations on what kinds of inheritance hierarchies that can be formulated in HB?
Enrico Tassi (Jul 12 2021 at 15:54):We are aware of that, and MC analysis dev as well.
Enrico Tassi (Jul 12 2021 at 15:54):What do you mean exactly?
Enrico Tassi (Jul 12 2021 at 15:55):There are some hierarchies which are broken by design, see https://github.com/math-comp/hierarchy-builder/wiki , and HB complains about them
Ben Siraphob (Jul 12 2021 at 15:56):I guess when creating structures that are joins, to quote from MCB,
If a new structure S extends structures that are further apart in the hierarchy more than one such additional link may be needed: precisely one for each pair of structures whose join is S. For example, unitRingType requires three such links, while finFieldType in library finalg requires 11. It is highly advisable to map out the hierarchy when simultaneously extending multiple structures.
Ben Siraphob (Jul 12 2021 at 15:56):So it sounds tedious to join increasingly distinct structures
Enrico Tassi (Jul 12 2021 at 15:56):MC was ported to HB, but not released yet
Enrico Tassi (Jul 12 2021 at 15:57):We could generate automatically join-structures. Currently we don't. But all the nasty machinery to make a join work is done for you. [the main problem is that we would pick a silly name, and at the same time doing the join is typically one line]
Enrico Tassi (Jul 12 2021 at 15:59):This is related to the third entry in the wiki
Ben Siraphob (Aug 01 2021 at 15:59):I have a variation of the same issue again, this time annotating the types or augmenting the constraints of IsComMonoid doesn't seem to help
Ben Siraphob (Aug 01 2021 at 15:59):From HB Require Import structures.
From Coq Require Import ssreflect.
HB.mixin Record IsSemigroup A := {
add : A -> A -> A;
addrA : forall (x y z : A), add x (add y z) = add (add x y) z;
}.
HB.structure Definition Semigroup := { A of IsSemigroup A }.
Infix "+" := add.
HB.mixin Record IsMonoid A of IsSemigroup A := {
zero : A;
add0r : forall (x : A), zero + x = x;
}.
HB.structure Definition Monoid := { A of IsMonoid A }.
Notation "0" := zero.
Fail HB.mixin Record IsComMonoid A of IsMonoid A := {
addrC : forall (x y : A), x + y = y + x;
}.
I think this is an instance of https://github.com/math-comp/hierarchy-builder/issues/258
Enrico Tassi (Aug 01 2021 at 19:57):Oh, did you try to write Monoid A already?
Ben Siraphob (Aug 02 2021 at 07:37):Ah, this works
HB.mixin Record IsComMonoid A of Monoid A := {
addrC : forall (x y : A), x + y = y + x;
}.
but I'm not sure what the difference is now between IsMonoid A and Monoid A
Ben Siraphob (Aug 02 2021 at 07:53):Now I can define the hierarchy but the proof doesn't go through.
From HB Require Import structures.
From Coq Require Import ssreflect.
HB.mixin Record IsSemigroup A := {
add : A -> A -> A;
addrA : forall (x y z : A), add x (add y z) = add (add x y) z;
}.
HB.structure Definition Semigroup := { A of IsSemigroup A }.
Infix "+" := add.
HB.mixin Record IsMonoid A of Semigroup A := {
zero : A;
add0r : forall (x : A), zero + x = x;
}.
HB.structure Definition Monoid := { A of IsMonoid A }.
Notation "0" := zero.
HB.mixin Record IsComMonoid A of Monoid A := {
addrC : forall (x y : A), x + y = y + x;
}.
HB.structure Definition ComMonoid := { A of IsComMonoid A }.
HB.mixin Record IsGroup A of Monoid A := {
opp : A -> A;
addNr : forall x, opp x + x = 0;
}.
HB.structure Definition Group := { A of IsGroup A }.
Print Module Group.
Notation "- x" := (opp x).
HB.mixin Record IsComGroup A of Group A & ComMonoid A := { }.
HB.structure Definition ComGroup := { A of IsComGroup A }.
Lemma example (G : ComGroup.type) (a b : G) : (- b + (b + a)) + (- a) = 0.
Proof. rewrite addrC (addrA (opp b)) addNr add0r addNr. Qed.
IsMonoid is just a piece of interface, a mixin. Monoid.type is a structure and Monoid is its class, which the set of mixins (transitively closed) which compose the interface of the structure. So Monoid = IsMonoid + IsSemigroup
Enrico Tassi (Aug 02 2021 at 12:11):The proof works, there is only one goal left which is 0 = 0. You can prefix the line with by which will close it. Did you copy this line from somewhere? It is probably a typo.
Ben Siraphob (Aug 02 2021 at 12:18):I wrote it myself, and if it went through, by would close indeed but one of the rewrites fails:
Error: The LHS of addNr
(- _ + _)
does not match any subterm of the goal
HB 1.1.0
Enrico Tassi (Aug 02 2021 at 14:45):Hum, it works here (I'm on HB master, but it should make no difference). :-/
Ben Siraphob (Aug 03 2021 at 17:04):Hm, strange. I will override the Nixpkgs version and see
Ben Siraphob (Aug 12 2021 at 11:43):I can replicate this on master
Ben Siraphob (Aug 12 2021 at 11:44):Here is the file, for completeness:
From HB Require Import structures.
HB.mixin Record IsSemigroup A := {
add : A -> A -> A;
addrA : forall (x y z : A), add x (add y z) = add (add x y) z;
}.
HB.structure Definition Semigroup := { A of IsSemigroup A }.
Infix "+" := add.
HB.mixin Record IsMonoid A of Semigroup A := {
zero : A;
add0r : forall (x : A), zero + x = x;
}.
HB.structure Definition Monoid := { A of IsMonoid A }.
Notation "0" := zero.
HB.mixin Record IsComMonoid A of Monoid A := {
addrC : forall (x y : A), x + y = y + x;
}.
HB.structure Definition ComMonoid := { A of IsComMonoid A }.
HB.mixin Record IsGroup A of Monoid A := {
opp : A -> A;
addNr : forall x, opp x + x = 0;
}.
HB.structure Definition Group := { A of IsGroup A }.
Print Module Group.
Notation "- x" := (opp x).
HB.mixin Record IsComGroup A of Group A & ComMonoid A := { }.
HB.structure Definition ComGroup := { A of IsComGroup A }.
Lemma example (G : ComGroup.type) (a b : G) : (- b + (b + a)) + (- a) = 0.
Proof. Fail rewrite addrC, (addrA (opp b)), addNr, add0r, addNr. Admitted.
I've to rush now, but it seems you are using Coq's vanilla rewrite, which is picky about implicit arguments (sometimes you have to unfold things your don't see). If you use the ssreflect one, does it still fail?
Ben Siraphob (Aug 14 2021 at 02:40):It fails using ssreflect's rewrite and Coq's rewrite.
Cyril Cohen (Aug 14 2021 at 13:25):For me it works with ssreflect (and indeed not with vanilla Coq)
Cyril Cohen (Aug 14 2021 at 13:25):Require Import ssreflect ssrfun ssrbool.
From HB Require Import structures.
HB.mixin Record IsSemigroup A := {
add : A -> A -> A;
addrA : forall (x y z : A), add x (add y z) = add (add x y) z;
}.
HB.structure Definition Semigroup := { A of IsSemigroup A }.
Infix "+" := add.
HB.mixin Record IsMonoid A of Semigroup A := {
zero : A;
add0r : forall (x : A), zero + x = x;
}.
HB.structure Definition Monoid := { A of IsMonoid A }.
Notation "0" := zero.
HB.mixin Record IsComMonoid A of Monoid A := {
addrC : forall (x y : A), x + y = y + x;
}.
HB.structure Definition ComMonoid := { A of IsComMonoid A }.
HB.mixin Record IsGroup A of Monoid A := {
opp : A -> A;
addNr : forall x, opp x + x = 0;
}.
HB.structure Definition Group := { A of IsGroup A }.
Print Module Group.
Notation "- x" := (opp x).
HB.mixin Record IsComGroup A of Group A & ComMonoid A := { }.
HB.structure Definition ComGroup := { A of IsComGroup A }.
Lemma example (G : ComGroup.type) (a b : G) : (- b + (b + a)) + (- a) = 0.
Proof. by rewrite addrC (addrA (opp b)) addNr add0r addNr. Qed.
Last updated: Dec 07 2023 at 07:39 UTC