Redefine Algebra.Consequences.Setoid.wlog

[jamesmckinna]

The trouble with the definition:

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

module _ {p} {P : Pred A p}
         (≈-subst : Substitutive _≈_ p)
         (∙-comm : Commutative _∙_)
         where

  subst∧comm⇒sym : Symmetric (λ a b → P (a ∙ b))
  subst∧comm⇒sym = ≈-subst P (∙-comm _ _)

  wlog : ∀ {r} {_R_ : Rel _ r} → Total _R_ →
         (∀ a b → a R b → P (a ∙ b)) →
         ∀ a b → P (a ∙ b)
  wlog r-total = BinaryConsequences.wlog r-total subst∧comm⇒sym

is twofold:

• the assumption ≈-subst : Substitutive _≈_ p is needlessly restrictive, when ≈-resp : P Respects _≈_ would suffice
• moreover, as even pointed out in Relation.Binary.Definitions, a relation _≈_ only ever satisfies Substitutive _≈_ p when it is PropositionalEquality (or a derivative of it), so the Setoid version of wlog can only ever be deployed in the Propositional case!

Arguably this is bug, so should be fixed as non-backwards-compatible change in v2.3 ;-) but v3.0 is probably more reasonable, or at least, less unreasonable...

Accordingly, propose instead:

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

module _ {p} {P : Pred A p}
         (≈-resp : P Respects _≈_)
         (∙-comm : Commutative _∙_)
         where

  resp∧comm⇒sym : Symmetric (λ a b → P (a ∙ b))
  resp∧comm⇒sym = ≈-resp (∙-comm _ _)

  wlog : ∀ {r} {_R_ : Rel _ r} → Total _R_ →
         (∀ a b → a R b → P (a ∙ b)) →
         ∀ a b → P (a ∙ b)
  wlog r-total = BinaryConsequences.wlog r-total resp∧comm⇒sym

with marginal knock-on consequences for the Propositional case (resp P instead of subst)

[gallais]

I think we should find a use case of this function before refactoring it!

IME it's utterly useless and I always had to resort to the more general Binary.Consequences
definition. That's due to the fact this specialised version captures exactly one use of a ∙ b but
typical Ps have multiple occurences of a and b and require abstracting over more than just
a ∙ b to prove that the predicate is stable.

It's not easy to explain, but people can get a feel for it by taking the wlog proofs I
have pushed and trying to rephrase them in term of this specialisation.

[jamesmckinna]

A-ha!? Oops.

[JacquesCarette]

Doesn't this actually argue for deleting this entirely?

[jamesmckinna]

Doesn't this actually argue for deleting this entirely?

Arguably, yes, I guess so, but in the meantime, it would be interesting to investigate what might work instead, viz. conditions under which (∀ a b → a R b → Q a b (a ∙ b)) → ∀ a b → Q a b (a ∙ b) would provable... presumably some of combination of Q Respects... and ∀ a b → Q a b (a ∙ b) → Q b a (b ∙ a) symmetry?

[JacquesCarette]

Open an issue? Because this one seems to be about something else.

[jamesmckinna]

Open an issue? Because this one seems to be about something else.

Well, maybe you're right, but having opened the original issue (in a simple minded, low energy local fix way ...) Guillaume's comment made me think some more about things, so it seemed 'in scope' for an issue about changing an existing definition...

But it may indeed end up that the 'change' should involve deletion/deprecation. UPDATED: and indeed, as the Algebra.*.wlog is used nowhere in the library, agree in the first instance that deprecation is the way to go until something better can be agreed upon.