[ refactor ] Reconcile left/right congruence statements and proofs

[jamesmckinna]

Have now added revised types for the new lemmas, and note the following:

• ++⁺ʳ now has a type corresponding to the explicitly quantified version of Algebra.Definitions.LeftCongruent
• ++⁺ˡ now has a type corresponding to the explicitly quantified version of Algebra.Definitions.RightCongruent
  (and explicit because "_++_ can't infer its arguments"... at least in the first case)

Which nomenclature/notation should be taken as canon? (Potential issue: I think that the use(s) of left/right superscript annotations in the Data.List.Relation* hierarchy are opposite to those of the Algebra.* congruence properties... sigh)

Barring the resolution of this question, I think this is (should be! ;-)) good to go now.

Originally posted by @jamesmckinna in #2426 (comment)

cf. #1436

Design decisions to be made:

• It's very unfortunate (ahem) that I seem to be the one who introduced the left/right inversion relative to the existing conventions in Relation.Binary.Definitions and Algebra.Definitions, so I'll try to remedy that with a v3.0 PR, and I'm inclined to decide in favour of the Algebra.Definitions left/right convention, unless anyone strongly objects. NB this goes against @MatthewDaggitt 's original comments on Add left- and right- Pointwise congruence for _++_ on List #2426 ...
• A separate issue is one regarding implicit/explicit quantification in the definition of Left/RightCongruent: when considering prefixing xs ++_ as a Pointwise-respecting (or any other Data.List.Relation.Binary.*), most, if not all of the uses of such properties do not require xs to be given explicitly (and as a suffixing operation, seemingly never, thanks to unification), and only a handful (typically those under Data.List.Relation.Unary.Any.Properties) actually do induction on xs to prove the relevant property, but again, never seem to use it in anger when applying those proofs. So I'm strongly tempted not to change the quantifiers in Algebra.Definitions, again unless anyone strongly objects, and to modify the quantification in Data.List.Relation.*.Properties. This goes slightly against the design advocated in Standardise implicit arguments of cancellation properties. #1436 and elsewhere (eg Associativity... which similarly almost never needs its arguments supplied explicitly), but is conformant with the abstract use of -congˡ and -congʳ derived forms in Algebra.Structures.IsMagma.

(Similar remarks apply to the corresponding lemmas under Data.Vec.Relation.* in the usual way)

Ahead of any review discussion (and consequent potential waste of bandwidth/effort) on a candidate PR, it would be useful to poll opinion on the wisdom of such choices, or otherwise!

[JacquesCarette]

Could you phrase your "decisions to be made" crisply? I feel like I can't give any opinion right now, as I'm not quite sure what I have to give an opinion on! Maybe split things into 1) crisp problem statement, and 2) discussion of the problem ?

[jamesmckinna]

Ouch! Will attempt to do so...

[jamesmckinna]

Here goes (but given I never seem to be able to meet @JacquesCarette 's standards of crispness/non-verbosity, I'm not confident): there are 2 mismatches at issue, as I see things:

• between the abstract (Algebra) and concrete (List/Vec) versions of left/right congruence
• between implicit quantification (in Algebra.Definitions.*Congruent, in particular) and explicit quantification (style-guide recommendations regarding when arguments in Algebra.Definitions.* should be given explicitly in general)

As to discussion of the above, I've probably written a lot/too much already, but I'll return to this provided the above meets the required crispness threshhold.

[JacquesCarette]

Those are quite crisp, thank you.

• I do think we should have a simple interpretation of what left/right means, and be able to clearly articulate it. And that this is absolutely worth fixing.
• I also agree that guidelines for what should be explicit / implicit are worthwhile. Here we will have to settle for guidelines as I think there will always be exceptions. So the guidelines should probably include 'rules' for how to justify exceptions!

Those should likely be two issues, as they are not related to each other. Given the title of this issue, let's keep this one for left/right.

So 'left' (in the context of an obvious binary operator or relation) can mean either

1. works on the left, acts on the left, operates on the left,
2. keeps the left constant

Personally, I think my brain definitely goes to the first interpretation. [And I would not be surprised at all if there were left / right in agda-categories that worked in the opposite way!]

[jamesmckinna]

Thanks @JacquesCarette .

The 'discussion'/issue title unfortunately does/did seem to involve both parts, mostly because of earlier bad decisions by me in #2426 :

• I (somehow!?) got left and right mixed up wrt the 'conventional' usage in Algebra.Definitions (but this is why there is also a call back to Standardise implicit arguments of cancellation properties. #1436 because that seems to suffer from a similar problem, again wrt both parts... getting the quantification right, and getting left-right handedness right
• I chose for explicit quantification following the style guide/discussion of Algebra.Definitions also in Standardise implicit arguments of cancellation properties. #1436 , despite the fact that the *Congruent definitions (and their abstract deployment in Algebra.Structures) use implicit quantification, and seemingly, never seem to need the explicit versions is use, but sometimes when proving them.

HTH.

[jamesmckinna]

... Given the title of this issue, let's keep this one for left/right.

So 'left' (in the context of an obvious binary operator or relation) can mean either

1. works on the left, acts on the left, operates on the left,

2. keeps the left constant

Algebra.Definitions.LeftCongruent and Algebra.Definitions.LeftCancellative favour 2.

Data.List.Relation.Binary.Equality.Setoid.++-cancelˡ similarly.

Data.List.Relation.Binary.Equality.Setoid.++⁺ˡ keeps the right-hand term constant (and vice versa for ++⁺ʳ/left-hand constant), inheriting from Data.List.Relation.Binary.Pointwise.

Personally, I think my brain definitely goes to the first interpretation. [And I would not be surprised at all if there were left / right in agda-categories that worked in the opposite way!]

So it seems that, at least on the examples polled, consistency favours 2, sorry!

[jamesmckinna]

I looked again at the original PR, and it's v2.2, so actually fixing the offending switch in handedness should be a non-breaking change! (and we should do it quickly!)

[jamesmckinna]

Aaargh... further investigation reveals further instances of 'opposite' conventions being employed:

• Data.List.Relation.Binary.Subset.Setoid.Properties with convention 1. above (refactored in Revamp of Data.List.Relation.Binary.Subset #1355 ):

  ++⁺ʳ : ∀ {xs ys} zs → xs ⊆ ys → zs ++ xs ⊆ zs ++ ys
  ++⁺ˡ : ∀ {xs ys} zs → xs ⊆ ys → xs ++ zs ⊆ ys ++ zs

• similarly, Data.List.Relation.Unary.Enumerates.Setoid.Properties, Data.List.Relation.Unary.Any.Properties, ditto. for Vec
• while Data.List.Relation.Binary.Sublist.Setoid.Properties observes convention 2. above, but has lemma statements not as instances of LeftCongruent etc...

Sigh.

[JacquesCarette]

I did rather expect a lot more contradictions would show up.

Not sure I would be convinced by a "majority" argument unless it was > 80% on one side. Certainly a 60/40 split would most definitely not sway me. I think we should 'design' this.

Having said that: "works on the left" and "keeps left constant" are both really simple to explain, so I don't actually care which one is chosen.

[jamesmckinna]

Re: majority arguments. Indeed, I agree (majority should be more decisive)... But in #2426 I even went against what was prevailing in those modules.

For me, the argument is more (now): all such lemmas should be phrased in terms of LeftCongruent and RightCongruent, and then the handedness of those two definitions should determine everything else. Currently, they reflect convention 2. But for v3.0 we should agree to either keep that or make the breaking change to reverse it. And then, consider the knock-ons for Cancellable, Identity, ... etc...

[JacquesCarette]

For #2426 the main reason I'm still hesitating (even though that clearly introduce unnecessary inconsistency): what if we decide that the current handedness of the ones you changed there were actually right? That would introduce unnecessary incompatibilities.

I do agree that we ought to go through LeftCongruent and RightCongruent to lessen the chances of future mistakes.

[jamesmckinna]

As with my comment on #2535 whatever design choice we make will give rise to a breaking (hence: v3.0) change somewhere. But for v2.2, we can restore 'local' consistency/coherence. leaving things as they are seems... 'bad'.