## Calculating Bag EqualitiesCalculating Bag Equalities ## AbstractTwo lists are "bag equal" if they are permutations of each other, i.e. if they contain the same elements, with the same multiplicity, but perhaps not in the same order. I plan to describe how one can define bag equality as the presence of bijections between sets of membership proofs. This definition has some nice properties: - Many bag equalities can be proved using a flexible form of equational reasoning.
- The definition generalises easily to arbitrary unary containers, including types with infinite values, such as streams.
- By using a small variant of the definition one gets set equality instead, i.e. equality where neither multiplicity nor order matters. Similar variations give the subset and subbag preorders.
- The definition works well in mechanised proofs.
Last updated Mon Feb 6 21:20:01 UTC 2012. |