search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
583 stars 236 forks source link

Add `EquationalReasoning` combinators for `_∼[ set ]_`? #2483

Open jamesmckinna opened 1 month ago

jamesmckinna commented 1 month ago

We have Function.Related.Propositional.EquationalReasoning.↔-syntax for bag equality _∼[ bag ]_, and despite _∼[ set ]_ having formally the same properties (incl. symmetry via SK-sym), we don't seem to have syntax for it (and hence the symmetric combinator syntax ↔⟨ ... ⟨ in order to be able to avoid explicit appeals to SK-sym). And AFAICT, instantiating Function.Related.Propositional.EquationalReasoning at {k = set} does not permit the ↔-syntax to be reused for set equality.

And/But I don't quite understand what needs to be changed/added to be able to fix this.

Taneb commented 1 month ago

I agree that this would be a reasonable addition

MatthewDaggitt commented 1 month ago

So the issue is that by convention we use ∼ for non-symmetric relations and so it has no symmetric counter-part. The best approach I think would be to create new BagReasoning and SetReasoning modules in List.Relation.Binary.BagAndSetEquality where we export proper (meaningfully named!) symmetric combinators...