# Bag Equivalence via a Proof-Relevant Membership RelationBag Equivalence via a Proof-Relevant Membership Relation Nils Anders Danielsson Interactive Theorem Proving,
Third International Conference,
ITP 2012.
The original publication is available at www.springerlink.com. [pdf, highlighted code, tarball with code, darcs repository (may include more recent developments)] ## AbstractTwo lists are *bag equivalent* 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. This paper describes how one can define bag equivalence as the presence of bijections between sets of membership proofs. This definition has some desirable properties:
- Many bag equivalences 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 slight variation of the definition one gets set equivalence instead, i.e. equality up to order and multiplicity. Other variations give the subset and subbag preorders.
- The definition works well in mechanised proofs.
## UpdateThe paper states that the new definition of bag equivalence is *equivalent* to a more standard one. In the accompanying code it is proved that, if "bijection" is replaced by the equivalent concept of "weak equivalence" in the general versions of these definitions (those that work for all unary containers), then they are *isomorphic* (assuming extensionality).
Nils Anders Danielsson Disclaimer Last updated Mon May 28 13:10:30 UTC 2012. |