Jonathan Sterling (Jul 26 2022 at 08:00): Jonathan Sterling (Jul 26 2022 at 08:00):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! :)
Pierre Roux (Jul 26 2022 at 08:12):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.
Enrico Tassi (Jul 26 2022 at 08:16):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.
Jonathan Sterling (Jul 26 2022 at 08:34):Hi all, thanks! I think I'm trying out something similar to this idea.
Kazuhiko Sakaguchi (Jul 26 2022 at 08:48):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.
Jonathan Sterling (Jul 26 2022 at 08:49):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.)
Jonathan Sterling (Jul 26 2022 at 08:53):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.
Jonathan Sterling (Jul 26 2022 at 09:04):Thanks for the feedback! Do you have any suggestions on what I should do to proceed today?
Matthieu Sozeau (Jul 26 2022 at 09:04):I'm surprised the pol index is not used to discriminate the two structures here, how come?
Cyril Cohen (Jul 26 2022 at 09:05):Matthieu Sozeau said:
I'm surprised the
polindex is not used to discriminate the two structures here, how come?
No backtracking, the key is S.
Matthieu Sozeau (Jul 26 2022 at 09:07):Couldn't you imagine having multiple keys in this case?
Cyril Cohen (Jul 26 2022 at 09:09):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.
Cyril Cohen (Jul 26 2022 at 09:11):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)
Cyril Cohen (Jul 26 2022 at 09:19):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)
Cyril Cohen (Jul 26 2022 at 09:21):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
Jonathan Sterling (Jul 26 2022 at 09:24):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 :)
Cyril Cohen (Jul 26 2022 at 09:25):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.
Jonathan Sterling (Jul 26 2022 at 09:35):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.
Cyril Cohen (Jul 26 2022 at 09:42):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.
Jonathan Sterling (Jul 26 2022 at 09:43):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!
Jonathan Sterling (Jul 26 2022 at 10:33):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?
Cyril Cohen (Jul 26 2022 at 10:35):Yes! This is a limitation of Coq : one cannot put a coercion to a variable type. There has to be a constant :grimacing:
Cyril Cohen (Jul 26 2022 at 10:35):Or a sort or a function space
Cyril Cohen (Jul 26 2022 at 10:36):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)
Jonathan Sterling (Jul 26 2022 at 10:37):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.
Cyril Cohen (Jul 26 2022 at 10:42):I advise to make the neutral element a parameter of the structure operator (and a field of the monoid)
Jonathan Sterling (Jul 26 2022 at 10:43):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.
Jonathan Sterling (Jul 26 2022 at 10:43):(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.)
Enrico Tassi (Jul 26 2022 at 12:01):@Cyril Cohen isn't #2 something planned already (for the category business)?
Cyril Cohen (Jul 26 2022 at 12:32):Enrico Tassi said:
Cyril Cohen isn't #2 something planned already (for the category business)?
Yes!
Cyril Cohen (Jul 26 2022 at 12:32):But it does not entirely match the purpose it serves for @Jonathan Sterling
Cyril Cohen (Jul 26 2022 at 16:50):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 :)
Johan Commelin (Aug 31 2022 at 14:53):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_additivewill "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: May 28 2023 at 18:29 UTC