To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

Bag Equivalence via a Pro… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

Bag Equivalence via a Proof-Relevant Membership Relation

Conference paper
Authors Nils Anders Danielsson
Published in Interactive Theorem Proving, Third International Conference, ITP 2012
Volume 7406 (LNCS)
Pages 149-165
ISBN 978-3-642-32347-8
ISSN 0302-9743
Publication year 2012
Published at Department of Computer Science and Engineering (GU)
Pages 149-165
Language en
Subject categories Theoretical computer science


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

Page Manager: Webmaster|Last update: 9/11/2012

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?