Stream: Hierarchy Builder devs & users

Topic: parameter illtyped error


view this post on Zulip 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;
}.

view this post on Zulip Enrico Tassi (Jul 12 2021 at 15:35):

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.

view this post on Zulip Enrico Tassi (Jul 12 2021 at 15:36):

or use of IsMonoid A & IsSemigroup A, which is like using the class, but more verbose

view this post on Zulip Enrico Tassi (Jul 12 2021 at 15:37):

we will eventually fix this annoyance

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip Enrico Tassi (Jul 12 2021 at 15:38):

Hum, ok, then please post your file so that I can try it myself.

view this post on Zulip 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 }.

view this post on Zulip Ben Siraphob (Jul 12 2021 at 15:39):

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

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Jul 12 2021 at 15:41):

addrC : forall x y : A, add x y = add y x;

view this post on Zulip Ben Siraphob (Jul 12 2021 at 15:41):

Ah that works, thanks! How can I see the generated code by HB?

view this post on Zulip Enrico Tassi (Jul 12 2021 at 15:42):

You can prefix any HB command with #[log] or, if you are really brave, #[log(raw)].

view this post on Zulip Enrico Tassi (Jul 12 2021 at 15:42):

But fasten you seat belt ;-)

view this post on Zulip Enrico Tassi (Jul 12 2021 at 15:43):

You can also use #[verbose] to get a more gentle listing of what is going on

view this post on Zulip Ben Siraphob (Jul 12 2021 at 15:43):

Spotted some minor typos in Ch 8, PR coming :)

view this post on Zulip Enrico Tassi (Jul 12 2021 at 15:43):

Thanks!

view this post on Zulip Ben Siraphob (Jul 12 2021 at 15:43):

Error: Attribute log is not supported

view this post on Zulip Ben Siraphob (Jul 12 2021 at 15:44):

I tried #[log] HB.structure Definition Group := { A of IsGroup A }.

view this post on Zulip Enrico Tassi (Jul 12 2021 at 15:44):

Hum, it was added in version 1.1.0

view this post on Zulip Enrico Tassi (Jul 12 2021 at 15:44):

which version are you on?

view this post on Zulip Ben Siraphob (Jul 12 2021 at 15:44):

Ah 1.0.0 that's in Nixpkgs

view this post on Zulip Enrico Tassi (Jul 12 2021 at 15:44):

You can Print Module Group, but it does not print a lot of stuff

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Jul 12 2021 at 15:45):

Like canonical structures etc

view this post on Zulip Ben Siraphob (Jul 12 2021 at 15:45):

Ah 1.1.0 seems to cause a build failure in mathcomp-analysis

view this post on Zulip Ben Siraphob (Jul 12 2021 at 15:45):

I see, this module looks identical to the one one would handwrite

view this post on Zulip 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.

view this post on Zulip Ben Siraphob (Jul 12 2021 at 15:47):

Yeah it's version 0.3.6 on Nixpkgs instead of 0.3.9

view this post on Zulip Ben Siraphob (Jul 12 2021 at 15:48):

Are there limitations on what kinds of inheritance hierarchies that can be formulated in HB?

view this post on Zulip Enrico Tassi (Jul 12 2021 at 15:54):

We are aware of that, and MC analysis dev as well.

view this post on Zulip Enrico Tassi (Jul 12 2021 at 15:54):

What do you mean exactly?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Ben Siraphob (Jul 12 2021 at 15:56):

So it sounds tedious to join increasingly distinct structures

view this post on Zulip Enrico Tassi (Jul 12 2021 at 15:56):

MC was ported to HB, but not released yet

view this post on Zulip 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]

view this post on Zulip Enrico Tassi (Jul 12 2021 at 15:59):

This is related to the third entry in the wiki

view this post on Zulip 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

view this post on Zulip 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;
}.

view this post on Zulip Enrico Tassi (Aug 01 2021 at 19:56):

I think this is an instance of https://github.com/math-comp/hierarchy-builder/issues/258

view this post on Zulip Enrico Tassi (Aug 01 2021 at 19:57):

Oh, did you try to write Monoid A already?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Aug 02 2021 at 11:05):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Ben Siraphob (Aug 02 2021 at 12:19):

HB 1.1.0

view this post on Zulip Enrico Tassi (Aug 02 2021 at 14:45):

Hum, it works here (I'm on HB master, but it should make no difference). :-/

view this post on Zulip Ben Siraphob (Aug 03 2021 at 17:04):

Hm, strange. I will override the Nixpkgs version and see

view this post on Zulip Ben Siraphob (Aug 12 2021 at 11:43):

I can replicate this on master

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Aug 12 2021 at 14:53):

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?

view this post on Zulip Ben Siraphob (Aug 14 2021 at 02:40):

It fails using ssreflect's rewrite and Coq's rewrite.

view this post on Zulip Cyril Cohen (Aug 14 2021 at 13:25):

For me it works with ssreflect (and indeed not with vanilla Coq)

view this post on Zulip 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: Jan 29 2023 at 15:02 UTC