[Add] Consequences of associativity for Semigroups

[jmougeot]

Introduce a new module for equational reasoning in semigroups, providing utilities for associativity reasoning and operations.

[JacquesCarette]

For others: the names are taken from the combinators in agda-categories. Those were inherited from older versions of that library. I do not like them! So please do suggest better ones.

[jamesmckinna]

Introduce a new module for equational reasoning in semigroups, providing utilities for associativity reasoning and operations.

With an explicit callback/reference to #2288 ? This PR alone doesn't 'fix' that issue, but contributes a piece of the jigsaw to such a 'fix'.

[jamesmckinna]

Lots of comments, I'm requesting changes based on a single one, but can be summarised as:

• please give lemmas names that can be remembered without needing a lookup table or other instruction manual to explain what they are/how they behave!
• no need for a new module, we already have the Algebra.Properties.* sub-hierarchy...

[jamesmckinna]

OK... thanks for the recent commits, but I'm going to carry on nitpicking:

• the Assoc4 proofs miss lots of symmetry, with 5 'independent' lemmas each with their symmetric counterpart, and since Reasoning.Setoid does have the syntax for applying the symmetric equivalent of an equation, we maybe don't even need the 5 equivalents...
  • u∙[[v∙w]∙x]≈[[u∙v]∙w]∙x = sym [[u∙v]∙w]∙x≈u∙[[v∙w]∙x]
  • u∙[v∙[w∙x]]≈[[u∙v]∙w]∙x = sym [[u∙v]∙w]∙x≈u∙[v∙[w∙x]]
  • [u∙v]∙[w∙x]≈[u∙[v∙w]]∙x = sym [u∙[v∙w]]∙x≈[u∙v]∙[w∙x]
  • u∙[v∙[w∙x]]≈[u∙[v∙w]]∙x = sym [u∙[v∙w]]∙x≈u∙[v∙[w∙x]]
  • u∙[v∙w]]∙x]≈[u∙v]∙[w∙x] = sym [u∙v]∙[w∙x]≈u∙[[v∙w]]∙x]
    where this last one, [u∙v]∙[w∙x]≈u∙[[v∙w]]∙x] is defined as a step-by-step proof, rather than the others, just defined in terms of trans, so could instead consider
  • [u∙v]∙[w∙x]≈u∙[[v∙w]]∙x] = trans (assoc u v (w ∙ x)) (sym (∙-congˡ (assoc v w x)))
• similarly, while the Pushes are symmetric equivalents of something in Pulls, not all the Pulls have their counterparts... but as above, maybe (probably) we don't even need the Pushes at all...
• the square brackets do improve things, I think, but you've overdone them, as there's no need to have each innermost group neither bracketed, nor mention the operation explicitly, cf. x∙yz≈xy∙z, so I should apologise for not expressing my suggestion clearly enough (or else falling into the same trap myself!), so eg. [[u∙v]∙w]∙x≈u∙[[v∙w]∙x] could be simplified to [uv∙w]∙x≈u∙[vw∙x] and that would be, I think, much more readable (with less ink!). Or even [[uv]w]x≈u[[vw]x] but that exchanges one character for two, so is perhaps suboptimal. Etc.

[jamesmckinna]

Also:

Introduce a new module for equational reasoning in semigroups, providing utilities for associativity reasoning and operations.

As with previous comments, we don't need a new module (even if it's moved location), these could all go in Algebra.Properties.Semigroup, and should, I think (another instance of Occam's Eraser: don't multiply modules unnecessarily)

[JacquesCarette]

As I've indicated, I'm not a big fan of push/pull because they are not very mnemomic; the superscripts don't help either. Indeed, if one looks at

module Pulls (x∙y≈z : x ∙ y ≈ z) where
  x∙y≈z⇒[w∙x]∙y≈w∙z : (w ∙ x) ∙ y ≈ w ∙ z

what it really does is

1. refocus on the right
2. apply an equality there.

So that's what I'd like the naming to reflect. Now, I quite like the 'synonym' _⟩∙⟨_ for ∙-cong (hoping to introduce that synonym too.) So then if we take ⭆ to be refocus (on the right), then the above could be ⭆∙⟨_. We would similarly have a refocus on the left then act on that side as ⭅⟨_∙. I would be fine with putting in a marker for where "nothing happens". So we could have:

• ⭆-I∙⟨_ : refocus right then apply equation there
• ⭅-_⟩∙I : refocus left then apply equation there
• I∙_⟩-⭅ : apply equation on right then refocus left
• _⟩∙I-⭆ : apply equation on left then refocus right

Note that these are meant to have the 3 variables be implicit, on purpose: if they cannot be figured out by Agda, then it's probably better to use the 'long form' of the reasoning (i.e. explicit calls to assoc).

[jamesmckinna]

As I've indicated, I'm not a big fan of push/pull because they are not very mnemomic; the superscripts don't help either. Indeed, if one looks at

module Pulls (x∙y≈z : x ∙ y ≈ z) where
  x∙y≈z⇒[w∙x]∙y≈w∙z : (w ∙ x) ∙ y ≈ w ∙ z

what it really does is

1. refocus on the right

2. apply an equality there.

So that's what I'd like the naming to reflect. Now, I quite like the 'synonym' _⟩∙⟨_ for ∙-cong (hoping to introduce that synonym too.) So then if we take ⭆ to be refocus (on the right), then the above could be ⭆∙⟨_. We would similarly have a refocus on the left then act on that side as ⭅⟨_∙. I would be fine with putting in a marker for where "nothing happens". So we could have:

* `⭆-I∙⟨_` : refocus right then apply equation there

* `⭅-_⟩∙I` : refocus left then apply equation there

* `I∙_⟩-⭅` : apply equation on right then refocus left

* `_⟩∙I-⭆` : apply equation on left then refocus right

Note that these are meant to have the 3 variables be implicit, on purpose: if they cannot be figured out by Agda, then it's probably better to use the 'long form' of the reasoning (i.e. explicit calls to assoc).

OK, I guess it is/was good to see how far apart the various contributors are on how to think about these naming issues, and their intended semantic underpinnings. But I have to say that I find the gap between the symbolic names you propose ((NB in my Firefox font for GitHub, your symbol ⭅ doesn't even display!) and those intended meanings so large that I simply cannot imagine ever using these principles except via uncomprehending cut-and-paste from the module, and with the above explanation by my side as user manual.

In the face of this, I am going to suggest

• either that we roll back to a text-based name, with your clear desire to inject 'refocus' as an idiom as a basis for the name (and I even suggested names based around that above)...
• or that we redraw the 'implicational' forms I suggested to make the x∙y≈z⇒prefix implicit as an infix argument position, with eg.
  • x∙y≈z⇒[w∙x]∙y≈w∙z : (w ∙ x) ∙ y ≈ w ∙ z becoming [wx]y≈[_]wz or [wx]y≈⟨_⟩wz, but again, we have up until now avoided making operators for equational proofs into infixes/mixfixes... except in the 'equation over equation' presentation of equality-modulo-cast in Data.Vec.Relation.Binary.Equality.Cast
• or simply that I withdraw from even expressing a view about this (much less merge the PR), other than to say that adopting such a change as you propose would mark such a meta-level breaking change from existing practice in stdlib that... I am completely lost for words!

Barn-burning.

[JacquesCarette]

My firefox displays them all just fine!

I would be fine with a name that involves refocus instead of symbology. We could use superscripts for indicating left/right refocusing. The one thing I don't know how to make nice: refocus-then-cong vs cong-then-refocus.

Your mixfix suggestion might have legs. In fact, by eliding the common prefix entirely, using it as a purely prefix operation might result in a name that's close to readable.

If my mnemonic symbology is not acceptable, I would think a text-based name based around 'refocus' is probably better than other unicode soup.

[MatthewDaggitt]

Conclusion: accept but note that there should be better solution

[MatthewDaggitt]

@JacquesCarette ?

The changes have actually been made, but James is away and so this is blocking.

[jamesmckinna]

Sorry for not having rescinded the old review! Thanks for merging!