agda
`Data.List.Base.reverse` is self adjoint wrt `Data.List.Relation.Binary.Subset.Setoid._⊆_`
This is a partial fix to #2353 but organised slightly differently, for consistency with existing uses of reverse⁺ and reverse⁻, via a self-adjointness property of independent interest itself generalising the corresponding self-inverse property for List.reverse.
Not done: extension to Data.List.Relation.Binary.Sublist.Setoid._⊆_ (nor its Heterogeneous generalisation), which seems a lot more fiddly to achieve.
Possible additions? I didn't think to add these earlier, but they are in scope for this PR:
reverse-η : ∀ {xs} → xs ⊆ reverse xs
reverse-η = Membershipₚ.reverse⁺ S
reverse-ε : ∀ {xs} → reverse xs ⊆ xs
reverse-ε = Membershipₚ.reverse⁻ S
with the -η/-ε designations referring to the unit and counit of the self-adjunction...
It almost feels like adding too many synonyms goes overboard? Doesn't pass the Fairbairn test. I'd be tempted to add these as comments in the code.
It almost feels like adding too many synonyms goes overboard? Doesn't pass the Fairbairn test. I'd be tempted to add these as comments in the code.
Fair enough! The alternative would be to take those synonyms out of Membershipₚ (where they've been added as part of this PR from Any) in favour of direct implementation here... but on balance your suggestion re:comment seems a good one.
Is this also true for
Data.List.Relation.Binary.Sublist? In which case we should add it there also, but that can be a separate PR
So that is a good question:
- yes, I think so
- but I found it 'not easy' to prove directly
- and so I'd left it above as a downstream TODO...
Not done: extension to
Data.List.Relation.Binary.Sublist.Setoid._⊆_(nor itsHeterogeneousgeneralisation), which seems a lot more fiddly to achieve.
UPDATED: ... if attempted directly. But the self-adjoint property easily follows (for Setoid and Heterogeneous) from reverse⁺ via reverse-involutive, so it's not clear there's any particular incentive (cf. Fairbairn) to include it directly. Whereas in the special case of Subset considered here, the self-adjoint property does provide a 'fast path' to the desired corollaries...
~~That said, maybe it's not true? Either way, any attempt to prove it by going via a property of reverseAcc seems to get tangled up between any instances of sublist relations of the two arguments to that function...~~
NB the unit/counit laws will not hold in that situation, so there's clearly a bit less going on in that setting than the self-adjunction given here for Subset._⊆_...