Calculating Bag Equalities

Calculating Bag Equalities
Talk given at meeting #68 of IFIP WG2.1, Rome, 2012-02-06. (Slightly edited.) [pdf]

Abstract

Two 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.