Optimising `Setoid`s/reasoning by 'rewriting' otherwise higher-dimensional equalities

[jamesmckinna]

For Relation.Binary.PropositionalEquality, we have (at least) the following definitional equalities

• sym refl = refl
• trans refl = id (but trans p refl is only propositionally equal to p...)
• resp P refl = id
• cong f refl = refl
• etc.

whereas for Setoids, we can form the same LHS combinations (or their mutatis mutandis variants, modulo suitable assumptions about respectfulness etc.), but for which we do not even necessarily have the above equalities even as provable equalities between proofs ... never mind any higher-dimensional coherent iterations of such ideas a la HoTT.

But there are various places where it might indeed be useful/more efficient (eg in proofs of divisibility in Algebra) to optimise such combinations, as if those equations did hold, moreover definitionally, and without regard to the definitional biases in trans etc. Example: in Algebra.Properties.Magma.Divisibility we see

xy≈z⇒y∣z : ∀ x y {z} → x ∙ y ≈ z → y ∣ z
xy≈z⇒y∣z x y xy≈z = ∣-respʳ-≈ xy≈z (x∣yx y x)

Now, inlining the definitions yields xy≈z⇒y∣z x y xy≈z = x , trans refl xy≈z which we may then, by fiat, rewrite as

xy≈z⇒y∣z x _ xy≈z = x , xy≈z

being a RHS with the correct type, moreover one which has better reduction behaviour now that we have removed the blocking non-redex trans refl etc.
(Similar examples are available for all the various combinations of left/right respects, left/right transitivity etc.)

Proposal: to go through the library in search of such 'locally optimisable' RHS of definitions in terms of Setoid combinators, and suitably 'optimise' them. Cf. @JacquesCarette 's #2288

[JacquesCarette]

While I'm generally in favour, I'd also like to know: what function is responsible for introducing the trans refl? It feels like it's the "guilty party" here and should be fixed. Without knowing that, I'd have a hard time searching through the library for such potential optimisations!

[jamesmckinna]

While I'm generally in favour, I'd also like to know: what function is responsible for introducing the trans refl? It feels like it's the "guilty party" here and should be fixed. Without knowing that, I'd have a hard time searching through the library for such potential optimisations!

Indeed. I stumbled on this only when I started to look moderately in earnest at trying to tackle #2115 when I saw this particular example of the phenomenon, until I realised that everytime we build up long non-reducing chains of equations, there's always a possibility that they will be deployed in a setting where something might cause them to 'reduce'...

The 'guilty party' x∣yx is easy to fix, as it's even local to the module. Maybe it is in fact the only instance, but ... hard to believe? As for 'searching', yes that was magical thinking, more a case of 'be aware that this might be happening' (eg by using C-c C-n periodically on proof terms to see if they do, indeed, have simpler forms?).

[JacquesCarette]

I agree that this is likely not the only instance (there are tons of similar things in agda-categories but their 'source' is more complex due to "bad" definitions in category theory that are strictly correct but wildly inefficient). So yes, I think actually looking at proof terms is probably the only way to spot these.

Maybe some kind of feature is needed in Agda, like the warnings for operators with no precedence? i.e. dump the normalized form of things of proof type?

[jamesmckinna]

Maybe everything needs to be run through a Solver/some other Reflection-based machinery... such as the example I give on #2631 of trans (comm y x) (trans (comm x y) eq) which (morally!) should reduce to eq...

[JacquesCarette]

As a sanity check, sure. As a way to build the library via meta-programming? Maybe. As a way to build the library? Definitely not!

[jamesmckinna]

Another guilty party: \qed/_∎ itself! (Reflecting on #2677 ...)

After a chain of reasoning (chaining via trans), the end point of such reasoning will be some proof p followed by refl from the end marker. Ie.
trans q (... (trans p refl))...)

Is it OK to have all our Reasoning proofs like this?

Not sure how/if we could re-engineer the combinators to optimise away this last step? Other than, perhaps to make begin_ not be a no-op, and somehow make _∎ return 'the foregoing proof'...

That has/would have the flavour of a foldr vs. foldl associativity property wrt trans...? Or even cons/snoc list fusion #2684 etc.

That is: a chain of reasoning steps could/should remain as a list/chain in a (reflexive)transitive closure (in a proof-relevant bicategory/groupoid! cf. #2249 ), which only gets reified as an actual proof of an equation when reaching _∎...

... might make a fun student project!?

[MatthewDaggitt]

That is: a chain of reasoning steps could/should remain as a list/chain in a (reflexive)transitive closure (in a proof-relevant bicategory/groupoid! cf. #2249 ), which only gets reified as an actual proof of an equation when reaching _∎...

That does indeed sound like the principled approach

[JacquesCarette]

Right, if our combinators built up a list of steps, and then either begin_ or _∎ turned that into an actual proof, we could optimize. I can see if one of my students could do that (either Jacques, who is with me to June, or Sarra, who starts in July). So I'll assign this to myself, as a way to remember this.

[jamesmckinna]

Thanks @MatthewDaggitt for the endorsement.

Thanks @JacquesCarette for perhaps helping take this off me.

Two closing thoughts (which have been fermenting behind the scenes of the above discussion):

• as a meta-programming task (;-)), should this happen at the Tactic/Reflection/meta level, or can it be handled as a normalisation(-by-evaluation!) object-level function, cf. Beylin/Dybjer coherence for bicategories/monoidal categories via NbE for monoids...? UPDATED I can't find PS/PDF for it, but this style of 'internalised tactic' was already present in the archeology, in: https://www.lfcs.inf.ed.ac.uk/reports/89/ECS-LFCS-89-70/ see also https://dl.acm.org/doi/pdf/10.1007/BF01245632
• what about the UX/interactivity aspects? The above seems fine for completed chains of reasoning, but what are the ergonomics of interactive development of equational proofs? It's already the case that the Reasoning syntax/combinators can sometimes leave the proof state ... more obscure than a refl, sym, trans proof (IIRC, trying to replay some of the PLFA equational proofs can 'go wrong' interactively (?))

Regarding the second, and also thinking about the differences between HOL and Isabelle/HOL, the tension between writing a tactic which returns a complete proof, and one which incrementally builds one, seems to require a lot more proof-state management, so the 'nice' student problem might end up being... quite challenging! I look forward to seeing the results!

[jamesmckinna]

Separate, but related: is it time to revisit/overhaul Relation.Binary.Construct.Closure.ReflexiveTransitive and friends? I'm struck by the conspicuous avoidance of any name overlap with List wrt constructors, but some 'emulation' wrt map, fold*, concat (rather than trans, except when defining the Preorder structure... etc.). No real need to, but my DRY spidey-sense has been ... stimulated by looking again at these things in the context of the above...