I have a question that is not so much about Hierarchy Builder but more about best practices for developing algebraic hierarchies (nonetheless within the context of using HB).
I am working on my own hobby project of developing some constructive commutative algebra, and I quickly need/want(?) to distinguish between additive and multiplicative monoid, group, etc. structure and combine them, etc. Of course, these satisfy all the same theorems but there are different names and notations associated with them.
I think that in the Lean mathlib, they just literally write all this stuff twice, but it seemed like maybe some members of this community would have a better idea --- or at least, some advice on how I should deal with the proliferation of duplicated concepts that nonetheless have different "attitudes". Thanks for any ideas you can offer! :)
Maybe try with the display
idea experimented for order structures in MathComp https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/order.v That would at least enable different notations on a single theory.
I recently had a chat with @Cyril Cohen on this very topic, but of course I don't remember all the details (in particular at some point one needs to improve HB a little, but anyway...).
One part of the solution I can recall is applied in order.v and consists in a "display" dummy argument, so that the same structure can be displayed with different notations. The documented limitation (of inference disregarding the display argument) is the thing HB does not support, but I don't recall when you need it. I guess Cyril does.
Hi all, thanks! I think I'm trying out something similar to this idea.
In my opinion, how to make additive and multiplicative monoids coexist is one of the most interesting open questions related to packed classes. Since the ring structure inherits from both monoids, I think that a solution with displays is fragile (or Cyril has a great solution that overcomes this issue). I would rather try a solution with copying stuffs.
Hmm, so what I'm finding I want is to be able to have _both_ an additive and multiplicative structure on a given carrier type, but this doesn't seem to work in HB. Here is an example:
From HB Require Import structures.
From Coq Require Import ssreflect ssrfun ZArith.
Inductive pol := Add | Mul.
HB.mixin Record is_semigroup (p : pol) (S : Type) :=
{ op : S -> S -> S;
oprA : associative op }.
HB.structure Definition Semigroup p := {S of is_semigroup p S}.
Infix "+" := (@op Add _).
Infix "×" := (@op Mul _) (at level 100).
Notation addrA := (@oprA Add _).
Notation mulrA := (@oprA Mul _).
HB.instance Definition _ : is_semigroup Add Z :=
is_semigroup.Build Add Z Z.add Z.add_assoc.
HB.instance Definition _ : is_semigroup Mul Z :=
is_semigroup.Build Mul Z Z.mul Z.mul_assoc.
Variable x y : Z.
Fail Check (x × y).
Check (x + y).
Copying is not really a viable approach for me at the moment, since the structure of the library is evolving and thus it would not be OK for me to have to execute every single change twice. (Maybe for a stable library copying would be viable.)
What HB does in this case, on the is_semigroup Mul
instance, is:
[1658825579.262069] HB: skipping already existing semigroup_Semigroup
instance on Z
For me the "copying" problematic is essentially a question of naming the lemmas:
And I think both should coexist within the same hierarchy generation mechanism.
Copying per se is not a problem, we could do it fully automatically, we could also envision a "generic" naming system where you specify how the name of your operator is inserted in the generated lemma names...
Once this (UX problematic) is solved the technical solution is secondary (albeit important to test to see whether it scales), should it be with displays or with separate structures (and the difference between those two solutions is actually not that big...)
As of now, HB does not support "parsing" of displays (i.e. elaboration taking displays into account, as of now it discards them during elaboration, and then rejects if the solution was wrong) hence the failure of your exaxmple @Jonathan Sterling, only printing (i.e. inserting an inferred display). I am of course envisioning extending it so that your example works, but I'm not a 100% sure yet whether that's the way to go.
Thanks for the feedback! Do you have any suggestions on what I should do to proceed today?
I'm surprised the pol
index is not used to discriminate the two structures here, how come?
Matthieu Sozeau said:
I'm surprised the
pol
index is not used to discriminate the two structures here, how come?
No backtracking, the key is S
.
Couldn't you imagine having multiple keys in this case?
Matthieu Sozeau said:
Couldn't you imagine having multiple keys in this case?
Yes we can, but we need to change the design pattern entirely (the good thing is that we can test it on mathcomp to see if it scales!)
I have multiple options for that (namely 3) and we could talk about them if you like.
Jonathan Sterling said:
Thanks for the feedback! Do you have any suggestions on what I should do to proceed today?
Three options, neither of which are really nice, but they could be more natively supported by HB in the long run... (I'm writing them, it can take some time)
From HB Require Import structures.
From Coq Require Import ssreflect ssrfun ZArith.
HB.mixin Record is_semigroup_op (S : Type) (op : S -> S -> S) :=
{ oprA : associative op }.
HB.structure Definition Semigroup S := {op of is_semigroup_op S op}.
HB.instance Definition _ : is_semigroup_op Z Z.add :=
is_semigroup_op.Build Z Z.add Z.add_assoc.
HB.instance Definition _ : is_semigroup_op Z Z.mul :=
is_semigroup_op.Build Z Z.mul Z.mul_assoc.
HB.mixin Record is_semigroup_op (S : Type) (op : S -> S -> S) :=
{ oprA : associative op }.
HB.structure Definition SemigroupOp S := {op of is_semigroup_op S op}.
HB.instance Definition Zadd_sg : is_semigroup_op Z Z.add :=
is_semigroup_op.Build Z Z.add Z.add_assoc.
HB.instance Definition Zmul_sg : is_semigroup_op Z Z.mul :=
is_semigroup_op.Build Z Z.mul Z.mul_assoc.
HB.mixin Record is_add_semigroup (S : Type) :=
{ add : S -> S -> S; add_sg : is_semigroup_op S add }.
HB.structure Definition AddSemigroup := {S of is_add_semigroup S}.
(* could be automated *)
HB.instance Definition _ (S : AddSemigroup.type) := @add_sg S.
(* could be generated with appropriate seeding for name generation *)
Lemma addrA (S : AddSemigroup.type) : associative (@add S).
Proof. exact: oprA. Qed.
HB.mixin Record is_mul_semigroup (S : Type) :=
{ mul : S -> S -> S; mul_sg : is_semigroup_op S mul }.
HB.structure Definition MulSemigroup := {S of is_mul_semigroup S}.
HB.instance Definition _ (S : MulSemigroup.type) := @mul_sg S.
Lemma mulrA (S : MulSemigroup.type) : associative (@mul S).
Proof. exact: oprA. Qed.
Infix "+" := (@add _).
Infix "×" := (@mul _) (at level 100).
(* could be generated too *)
HB.instance Definition _ : is_add_semigroup Z :=
is_add_semigroup.Build Z Z.add Zadd_sg.
HB.instance Definition _ : is_mul_semigroup Z :=
is_mul_semigroup.Build Z Z.mul Zmul_sg.
if you didn't have the theory of individual operators, you also have the variant where you use one for the other.
(I'll be lazy on this one)
Option 3. Use aliases:
From HB Require Import structures.
From Coq Require Import ssreflect ssrfun ZArith.
Inductive pol := Add | Mul.
HB.mixin Record is_semigroup (p : pol) (S : Type) :=
{ op : S -> S -> S;
oprA : associative op }.
HB.structure Definition Semigroup p := {S of is_semigroup p S}.
Infix "+" := (@op Add _).
Infix "×" := (@op Mul _) (at level 100).
Notation addrA := (@oprA Add _).
Notation mulrA := (@oprA Mul _).
HB.instance Definition _ : is_semigroup Add Z :=
is_semigroup.Build Add Z Z.add Z.add_assoc.
Definition Zm := Z.
HB.instance Definition _ : is_semigroup Mul Zm :=
is_semigroup.Build Mul Z Z.mul Z.mul_assoc.
Variable x y : Z.
Check ((x : Zm) × y).
Check (x + y).
As I said, neither of these solutions are satisfactory, but we can discuss on which one elaborate
Wow, thanks for taking the time to write this out! I am leaning toward #2 as the best approach for me, but I will play with it a bit to ensure that I understand it :)
if you didn't have the theory of individual operators, you also have the variant where you use one for the other.
(I'll be lazy on this one)
Then maybe I should expand on this.
Hmm, after playing with it a bit I am not sure I'm as excited about #2 as I was before ;-) I guess the problem for me is basically that it doesn't really seem to reduce the amount of duplication that I am having to deal with. I'll have to think about it some more.
Jonathan Sterling said:
Hmm, after playing with it a bit I am not sure I'm as excited about #2 as I was before ;-) I guess the problem for me is basically that it doesn't really seem to reduce the amount of duplication that I am having to deal with. I'll have to think about it some more.
Sure, I think none of the solutions are good... they are all temporary fixes to me.
Cool :) But your #2 gave me some good ideas that I'm experimenting with now... It might be enough to get me moving forward. Thanks again!
Here's another related problem I'm struggling with:
HB.mixin Record is_monoid_unit S (op : S -> S -> S) (emp : S) : Type := { (* todo *) }.
Fail HB.structure Definition MonoidUnit (S : Type) (op : S -> S -> S) :=
{emp of is_monoid_unit S op emp}.
The code above returns the error message HB: coercion not to Sortclass or Funclass not supported yet.
. Interestingly, if I change emp : S
to something like emp : unit -> S
, it works. Any ideas?
Yes! This is a limitation of Coq : one cannot put a coercion to a variable type. There has to be a constant :grimacing:
Or a sort or a function space
Right now we only support the latter, but we'll extend it. (I'd like to discuss with other people whether it's a good idea to have a default coercion target)
Gotcha, thanks! I think that limitation makes quite a bit of sense. Do you have a suggestion for how I should change this code, however? I'm trying to extend the #2-style semigroup example that you worked out to monoids.
I advise to make the neutral element a parameter of the structure operator (and a field of the monoid)
I see; I guess the thing I'm struggling with here is that this is very different from the way we designed the op
on the semigroup. I wonder why we should not change that one accordingly too? I am a little concerned I'm about to design myself into a hole.
(Btw it's totally ok if the answer to my questions is: "Stop trying to do this until we come up with a global solution" --- every few months I like to check in and see what I can do with HB, and I'm not insisting that it all be workable today.)
@Cyril Cohen isn't #2 something planned already (for the category business)?
Enrico Tassi said:
Cyril Cohen isn't #2 something planned already (for the category business)?
Yes!
But it does not entirely match the purpose it serves for @Jonathan Sterling
Jonathan Sterling said:
(Btw it's totally ok if the answer to my questions is: "Stop trying to do this until we come up with a global solution" --- every few months I like to check in and see what I can do with HB, and I'm not insisting that it all be workable today.)
Yes, it's more or less that. Well more precisely, if you need to do something right now, please proceed with half-baked solutions. Otherwise, please wait a little bit :)
Jonathan Sterling said:
I think that in the Lean mathlib, they just literally write all this stuff twice, but it seemed like maybe some members of this community would have a better idea --- or at least, some advice on how I should deal with the proliferation of duplicated concepts that nonetheless have different "attitudes". Thanks for any ideas you can offer! :)
I realise that I'm very late to this discussion. And I'm very eager to hear of any solutions that HB comes up with.
That being said, in mathlib we don't literally write everything twice. We have a tactic that does that for us. to_additive
will "additivize" both the name + statement + proof. If you don't like the name it generates, then you can pass that as optional argument to the tactic.
So generically the pattern is
@[to_additive]
lemma foo_mul_bar : bla bla :=
my_proof
Johan Commelin said:
Jonathan Sterling said:
I think that in the Lean mathlib, they just literally write all this stuff twice, but it seemed like maybe some members of this community would have a better idea --- or at least, some advice on how I should deal with the proliferation of duplicated concepts that nonetheless have different "attitudes". Thanks for any ideas you can offer! :)
I realise that I'm very late to this discussion. And I'm very eager to hear of any solutions that HB comes up with.
That being said, in mathlib we don't literally write everything twice. We have a tactic that does that for us.
to_additive
will "additivize" both the name + statement + proof. If you don't like the name it generates, then you can pass that as optional argument to the tactic.So generically the pattern is
@[to_additive] lemma foo_mul_bar : bla bla := my_proof
Thanks for clarifying that!
Last updated: Sep 30 2023 at 16:01 UTC