Look for cases where `wlog` can simplify proofs.

[MatthewDaggitt]

e.g. *-distribˡ-∣-∣

[MatthewDaggitt]

@gallais I had a go with this and can't seem to make it work for *-distribˡ-∣-∣. Care to have a go? Otherwise I suggest we probably close this as it's not exactly crucial.

[gallais]

We had the proof in the original PR thread: #450

[jamesmckinna]

So... five years later, what do we want to do about this?

[jamesmckinna]

Thanks @gallais for responding with #2577 !
Do you think that closes the issue, or would you want to keep it open after that gets merged?

[gallais]

I'm happy for it to be closed but there may still be further instances.

[jamesmckinna]

Indeed, tempting to think that the whole of Data.Integer.Properties might usefully be reviewed in this light, and Data.Nat.Properties (albeit to a lesser extent?). But maybe better to pick these things off piece by piece?

[jamesmckinna]

And... wlog really only operates on the symmetry induced by flip on operations/relations.
What about other symmetries? cf. Läuchli (maybe this is/was (implicit?) in the original issue discussion/PR?), and Tarski's characterisation of elementary equivalence as 'parametricity' for first-order models.

UPDATED: thinking about this a bit more, I've come to the conclusion that the argument order of Relation.Binary.Consequences.wlog is the wrong way round (and not simply because that would yield an easy eta-contraction in the definition of Algebra.Consequences.Setoid.wlog:

------------------------------------------------------------------------
-- Without Loss of Generality

module _  {_R_ : Rel A ℓ₁} {Q : Rel A ℓ₂} where

  wlog : Total _R_ → Symmetric Q →
         (∀ a b → a R b → Q a b) →
         ∀ a b → Q a b
  wlog r-total q-sym prf a b with r-total a b
  ... | inj₁ aRb = prf a b aRb
  ... | inj₂ bRa = q-sym (prf b a bRa)

This (current) version takes R as conceptually prior, and uses the hypotheses of Symmetric Q and ∀ a b → a R b → Q a b to provide an 'elimination principle' for establishing instances of Q. Cf. Relation.Binary.Construct.Interior.Symmetric.unfold

But I think it is better understood (more or less) as:

• Symmetric Q arises because Q is invariant under flip, so we are working relative to 'Sets with a flip-action'
• Total R is then the statement that R is in fact a 'relation' on such a Set-with-a-flip action
• moreover, compatible with Q via ∀ a b → a R b → Q a b
  ie
  this is a 'lifting property' from Sets (downstairs) to flip-Sets (upstairs) wrt the forgetful functor throwing away the flip action.

TL;DR: Symmetric Q is conceptually prior, restricting the universe of discourse to 'Sets with a flip-action', so should come first in the argument order, by considering possible generalisations to 'Sets with a G-action' for some group G?

[jamesmckinna]

It would be great if wlog could also be applied to the symmetry-heavy analyses in Data.Nat.GCD, but there the nature of 'wlog' cashes out as Trichotomy, with easy 'base' case when the two arguments are equal, and symmetry between the _<_ and _>_ cases... so not obviously applicable, sadly?

[jamesmckinna]

See also #2626 for more opportunities to use wlog... by making its type less constrained ;-)

[jamesmckinna]

My experience with trying to use wlog in #2971 suggests that we still don't really have the ergonomics of this combinator sorted out properly, when direct proof is so much less clunky...