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

{-# OPTIONS --without-K #-}

module README.Bag-equivalence where

------------------------------------------------------------------------
-- 2: Brief Introduction to Agda

-- The prelude, containing List, ℕ, length, Fin, ⊥, ⊤, _⊎_ (written as
-- _+_ in the paper), lookup, ∃, and _×_.

import Prelude

-- Equivalences: _⇔_.

import 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 _>>=_.

import Prelude

-- 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 equivalence proof.

import Bag-equivalence

-- 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
-- equivalent.
--
-- There is also a proof which shows that the definitions are
-- isomorphic (assuming extensionality), if "bijection" is replaced by
-- the equivalent concept of "weak equivalence" in the definitions of
-- bag equivalence.

import Container
import Weak-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

------------------------------------------------------------------------

-- For an overview over the other modules in this development, see the
-- README.

import README