agda
Add new operations (cf. `RawQuasigroup`) to `IsGroup`
Tackles second item of #2247 .
Issues:
- deprecation of
_-_inIsGroup? - adding operations to
Algebra.Bundles.Raw.RawGroup?
Knock-on changes (potentially):
- Instances of
_-_defined in, and hence would clash with any opening of theRawGroup|IsGroupinstance:
- [ ]
Data.Integer.Base|Properties - [ ]
Data.Rational.Base|Properties - [ ]
Data.Rational.Unnormalised.Base|Properties
- Instances of
_-_not defined in, but would be by opening theRawGroup|IsGroupinstance:
- [ ]
Data.Parity.Base|Properties - [ ]
Data.Sign.Base|Properties
Hmm so a few questions.
- Firstly, I think this definitely falls foul of the Fairbairn threshold? I was going to suggest
_∙⁻¹_should be_∙_⁻¹but then why not just write out the full thing? - Why do you not export them for
AbelianGroup?
Matthew, thanks for the attentive close reading...
1. Firstly, I think this definitely falls foul of the [Fairbairn threshold](https://wiki.haskell.org/Fairbairn_threshold)? I was going to suggest `_∙⁻¹_` should be `_∙_⁻¹` but then why not just write out the full thing?
So, indeed that's a fair question: one reason to introduce a distinct symbol is to avoid ambiguous parsing, which would otherwise definitely occur with your suggestion. Here the situation is slightly different from #2249 (though clearly cognate, and arising from the same root issue #2247), not least because we don't have so much group theory formalised yet to see the recurrence of the pattern... other than as the derived form _-_, but that doesn't belong in Group... on a 'conventional' reading of the symbol
2. Why do you not export them for `AbelianGroup`?
Again, this was a 'design' choice, underlying the whole PR: I don't think _-_ is a sensible choice of operator symbol for Group at all, while it surely is for (our customary informal intuitions/practice around) AbelianGroup; and once you are commutative, then the two otherwise-distinct Group operations become extensionally equal... (the alternative design would be to add that lemma to Algebra.Consequences.Group), so it struck me that the less invasive thing to do was to retain _-_ for AbelianGroup (again: that could be done by renaming the Group operation, but I wasn't sure about the deprecation consequences for trying to shift the operation symbol to the 'right' place), but not pollute its namespace with all the now-equivalent variants.
It does make a lot of sense to seriously consider adding some such symbol - basically because 200 years of Group Theory has continued to do so. So they find it adds something useful to the domain, and we would need a solid reason to decide otherwise. There seems to be a strong usability / readability case to be made.
Having said that, neither _∙⁻¹_ nor _∙_⁻¹ seem to actually achieve that! If we can't use some kind of division-like symbol, then the increase in readability is not enough as the suggested symbols are essentially the same as writing it out in full.
It does make sense to call this _-_ in AbelianGroup.
Thanks for the prompts to rethink, but I would definitely welcome suggestions as to a 'good' notation for these: maybe the Lambek-style left- and right- 'divides' symbols are the way to go? Or does that have the wrong associations wrt Preorder-based symbology?
I think
quasigroupandloopuse \ and // .
yes! It seems as though they could be used, ... in place... if we refactor Algebra.Structures to put IsQuasigroup and IsLoop before IsGroup, and then create+open the relevant instances as manifest fields of IsGroup...
... such a refactoring would, however, perturb the universal-algebra-finitary-signature enumeration currently embodied in that module...
... suggestion(s) welcome as to the 'best'/a 'middle' path to resolving this cleanly.
I don't have a good suggestion, as I don't really know the actual effect the refactoring would have. It might range from harmless to completely unacceptable.
... So maybe the correct thing to do is add them in-place on their own terms, and downstream establish a lemma of the form: IsGroup yields IsQuasigroup/IsLoop...?
Such lemmas would definitely be guaranteed low-disruption. Thus definitely a viable path.
Hopefully the addition of the isQuasigroup and isLoop structural lemmas now gives more 'weight' to this PR.
Outstanding refactoring opportunities, emerging in the course of doing this:
- derived operations in
IsGroup, orRawGroup? cf. #2252 how to get them correctly re-exported toIsGroupif added toRawGroup, and vice versa...? - duplication between proofs of
Cancellativeproperties forAlgebra.Properties.QuasigroupandAlgebra.Properties.Group; UPDATED: refactored to achieve this; - ~~do those proofs belong instead in
Algebra.Consequences.Setoid?~~ UPDATED: for another time - simplify the new proofs added here to exploit the lemmas in
Algebra.Properties.Quasigroup|Loop? UPDATED: refactored to achieve this now.
Plus: adding other derived operations #2268
Only issue outstanding for me: the current design factors between
-
Structures.IsGroupfor the additional derivable operations, and -
Properties.Group, which takes aBundled instance to then expose the underlyingStructure...
Does the operation material belong under Structures or should it all belong in the Bundle (leaving out the question of which bundle, Raw or otherwise... ;-))?
Note on reflexive reasoning (comment also left on #2152 already merged into v2.0):
... I've had to use explicit
x ≈⟨ refl ⟩...steps, because there is no abbreviation≈⟨⟩declared, whereas≡⟨⟩is available as an alternative. Was this what you intended, or should there be a bug-fixing issue/PR raised to add the additional syntax?
Originally posted by @jamesmckinna in https://github.com/agda/agda-stdlib/pull/2152#discussion_r1472742455
On the latest refactorings: they basically consist of moving lemmas from Algebra.Properties.Group to their 'true' homes in Algebra.Properties.Loop/Algebra.Properties.Quasigroup , and publicly (re-)exporting them from ...Group, together with some refactoring to derive existing Group properties from 'simpler' (or: now already proved) lemmas, such as SelfInverse _⁻¹ etc.
But that's it now.