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.
or use of IsMonoid A & IsSemigroup A
, which is like using the class, but more verbose
we will eventually fix this annoyance
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
using of Monoid A
works, thanks, but I run into an error when I try to add commutativity into the mix:
Hum, ok, then please post your file so that I can try it myself.
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
This is another problem, your axiom does not put x
nor y
in A
. If you add a type annotation it works.
addrC : forall x y : A, add x y = add y x;
Ah that works, thanks! How can I see the generated code by HB?
You can prefix any HB command with #[log]
or, if you are really brave, #[log(raw)]
.
But fasten you seat belt ;-)
You can also use #[verbose]
to get a more gentle listing of what is going on
Spotted some minor typos in Ch 8, PR coming :)
Thanks!
Error: Attribute log is not supported
I tried #[log] HB.structure Definition Group := { A of IsGroup A }.
Hum, it was added in version 1.1.0
which version are you on?
Ah 1.0.0 that's in Nixpkgs
You can Print Module Group
, but it does not print a lot of stuff
I have a PR bumping the version, hopefully @Cyril Cohen or @Vincent Laporte can review https://github.com/NixOS/nixpkgs/pull/130023
Like canonical structures etc
Ah 1.1.0 seems to cause a build failure in mathcomp-analysis
I see, this module looks identical to the one one would handwrite
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
Are there limitations on what kinds of inheritance hierarchies that can be formulated in HB?
We are aware of that, and MC analysis dev as well.
What do you mean exactly?
There are some hierarchies which are broken by design, see https://github.com/math-comp/hierarchy-builder/wiki , and HB complains about them
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.
So it sounds tedious to join increasingly distinct structures
MC was ported to HB, but not released yet
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]
This is related to the third entry in the wiki
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
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
Oh, did you try to write Monoid A
already?
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
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
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.
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
Hum, it works here (I'm on HB master, but it should make no difference). :-/
Hm, strange. I will override the Nixpkgs version and see
I can replicate this on master
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?
It fails using ssreflect's rewrite and Coq's rewrite.
For me it works with ssreflect (and indeed not with vanilla Coq)
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