------------------------------------------------------------------------ -- Code related to the paper "Bag Equivalence via a Proof-Relevant -- Membership Relation" -- -- Nils Anders Danielsson ------------------------------------------------------------------------ -- Note that the code does not follow the paper exactly. For instance, -- many definitions are universe-polymorphic, and in some cases where -- the paper contains both a specialised and a more general definition -- the code only contains the more general one. -- -- The code has also been changed after the paper was published. For -- instance, "bag equivalence" is now defined using equivalences -- instead of bijections, and some lemmas about how two definitions of -- bag equivalence are logically equivalent have been strengthened to -- equivalences (proved using function extensionality). {-# OPTIONS --cubical-compatible --safe #-} module README.Bag-equivalence where ------------------------------------------------------------------------ -- 2: Brief Introduction to Agda -- The prelude, containing List, ℕ, Fin, ⊥, ⊤, _⊎_ (written as _+_ in -- the paper), ∃, and _×_. import Prelude -- Some list functions: length and index (called lookup in the paper). import List -- Logical equivalences: _⇔_. import Logical-equivalence -- Bijections: _↔_. import Bijection -- Equality: _≡_. import Equality.Propositional -- The K rule, and a proof showing that it implies proof-irrelevance. import Equality -- Bijectional reasoning combinators (more general than those in the -- paper): inverse (written as sym in the paper), _□, and _↔⟨_⟩_. import Function-universe ------------------------------------------------------------------------ -- 3: Bag Equivalence for Lists -- Any, _∈_, and the two definitions of bag equivalence. import Bag-equivalence ------------------------------------------------------------------------ -- 4: Bijectional Reasoning -- Definitions of map, concat and _>>=_ (the latter as part of a monad -- instance). import List -- Algebraic properties of type constructors (like ⊥ ⊎ A ↔ A). import Function-universe import Fin -- All the main lemmas from this section, including -- >>=-left-distributive. import Bag-equivalence ------------------------------------------------------------------------ -- 5: The Definitions Are Equivalent -- The proof showing that the two definitions are logically -- equivalent. import Bag-equivalence -- A proof, not included in the paper, which shows that the -- definitions are equivalent (assuming extensionality). import Container.List -- There are infinitely many proofs of ℕ ≡ ℕ in homotopy type theory. import Univalence-axiom ------------------------------------------------------------------------ -- 6: Bag Equivalence for Arbitrary Containers -- Containers, including Any, _∈_, the two definitions of bag -- equivalence, and a proof showing that the two definitions are -- logically equivalent. -- -- There is also a proof, not included in the paper, which shows that -- the definitions are equivalent (assuming extensionality). import Container import Equivalence -- The List, Stream and Tree containers. It is shown that the general -- definition of bag equivalence for containers, instantiated with the -- List container, is equivalent (in a certain sense) to the list-only -- definition given above. import Container.List import Container.Stream import Container.Tree ------------------------------------------------------------------------ -- 7: More Bijectional Reasoning -- Three implementations of tree sort are provided. -- 1) An implementation of tree sort, formally proved to return a -- permutation of the input. import Tree-sort.Partial import Tree-sort.Examples -- 2) An implementation of tree sort, formally proved to return a -- /sorted/ permutation of the input. import Tree-sort.Full import Tree-sort.Examples -- 3) An implementation of tree sort which uses containers to -- represent trees and lists. -- -- In the module Tree-sort.Full indexed types are used to enforce -- sortedness, but this development uses non-indexed containers, so -- sortedness is not enforced. -- -- The implementation using containers has the advantage of uniform -- definitions of Any/membership/bag equivalence, but the other -- implementations use more direct definitions and are perhaps a -- bit "leaner". import Container.Tree import Container.Tree-sort import Container.Tree-sort.Example ------------------------------------------------------------------------ -- 8: Set Equivalence, Subsets and Subbags -- Injections: _↣_. import Injection -- The general definition of set and bag equivalence and the subset -- and subbag preorders, as well as preservation lemmas such as -- >>=-cong. import Bag-equivalence ------------------------------------------------------------------------ -- 9: Related Work -- One of the definitions of bag equivalence from Coq's standard -- library has been replicated, and shown to be sound with respect to -- the other ones. import Bag-equivalence ------------------------------------------------------------------------ -- 10: Conclusions -- Two proofs showing that cons is left cancellative, using different -- definitions of bag equivalence. import Bag-equivalence