------------------------------------------------------------------------
-- Binary trees
------------------------------------------------------------------------

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

module Tree where

open import Bag-equivalence
open import Equality.Propositional
open import Prelude hiding (id)

open import Bijection equality-with-J using (_↔_)
open import Function-universe equality-with-J
open import List equality-with-J

------------------------------------------------------------------------
-- Binary trees

data Tree (A : Set) : Set where
  leaf : Tree A
  node : (l : Tree A) (x : A) (r : Tree A)  Tree A

-- Any.

AnyT :  {A}  (A  Set)  (Tree A  Set)
AnyT P leaf         = 
AnyT P (node l x r) = AnyT P l  P x  AnyT P r

-- Membership.

infix 4 _∈T_

_∈T_ :  {A}  A  Tree A  Set
x ∈T t = AnyT (_≡_ x) t

-- Bag equivalence.

_≈-bagT_ :  {A}  Tree A  Tree A  Set
t₁ ≈-bagT t₂ =  x  x ∈T t₁  x ∈T t₂

------------------------------------------------------------------------
-- Singleton

-- Singleton trees.

singleton : {A : Set}  A  Tree A
singleton x = node leaf x leaf

-- Any lemma for singleton.

Any-singleton :  {A : Set} (P : A  Set) {x} 
                AnyT P (singleton x)  P x
Any-singleton P {x} =
  AnyT P (singleton x)  ↔⟨⟩
    P x             ↔⟨ ⊎-left-identity 
  P x                 ↔⟨ ⊎-right-identity 
  P x                   

------------------------------------------------------------------------
-- Flatten

-- Inorder flattening of a tree.

flatten : {A : Set}  Tree A  List A
flatten leaf         = []
flatten (node l x r) = flatten l ++ x  flatten r

-- Flatten does not add or remove any elements.

flatten-lemma : {A : Set} (t : Tree A)   z  z  flatten t  z ∈T t
flatten-lemma leaf         = λ z   
flatten-lemma (node l x r) = λ z 
  z  flatten l ++ x  flatten r         ↔⟨ Any-++ (_≡_ z) _ _ 
  z  flatten l  z  x  z  flatten r  ↔⟨ flatten-lemma l z ⊎-cong (z  x ) ⊎-cong flatten-lemma r z 
  z ∈T l         z  x  z ∈T r         

------------------------------------------------------------------------
-- Bags can (perhaps) be defined as binary trees quotiented by bag
-- equivalence

-- Agda doesn't support quotients, so the following type is used to
-- state that two quotients are isomorphic.
--
-- Note that this definition may not actually make sense if the
-- relations _≈A_ and _≈B_ are not /proof-irrelevant/ equivalence
-- relations.

record _/_↔_/_ (A : Set) (_≈A_ : A  A  Set)
               (B : Set) (_≈B_ : B  B  Set) : Set where
  field
    to        : A  B
    to-resp   :  x y  x ≈A y  to x ≈B to y
    from      : B  A
    from-resp :  x y  x ≈B y  from x ≈A from y
    to∘from   :  x  to (from x) ≈B x
    from∘to   :  x  from (to x) ≈A x

-- Lists quotiented by bag equivalence are isomorphic to binary trees
-- quotiented by bag equivalence (assuming that one can actually
-- quotient by bag equivalence, and that the definition of _/_↔_/_
-- makes sense in this case).

list-bags↔tree-bags : {A : Set}  List A / _≈-bag_  Tree A / _≈-bagT_
list-bags↔tree-bags {A} = record
  { to        = to-tree
  ; to-resp   = λ xs ys xs≈ys z 
                  z ∈T to-tree xs  ↔⟨ to-tree-lemma xs z 
                  z  xs           ↔⟨ xs≈ys z 
                  z  ys           ↔⟨ inverse $ to-tree-lemma ys z 
                  z ∈T to-tree ys  
  ; from      = flatten
  ; from-resp = λ t₁ t₂ t₁≈t₂ z 
                  z  flatten t₁  ↔⟨ flatten-lemma t₁ z 
                  z ∈T t₁         ↔⟨ t₁≈t₂ z 
                  z ∈T t₂         ↔⟨ inverse $ flatten-lemma t₂ z 
                  z  flatten t₂  
  ; to∘from   = to∘from
  ; from∘to   = from∘to
  }
  where
  to-tree : List A  Tree A
  to-tree = foldr (node leaf) leaf

  to-tree-lemma :  xs z  z ∈T to-tree xs  z  xs
  to-tree-lemma []       = λ z   
  to-tree-lemma (x  xs) = λ z 
      z  x    z ∈T to-tree xs  ↔⟨ id ⊎-cong id ⊎-cong to-tree-lemma xs z 
      z  x    z  xs           ↔⟨ ⊎-assoc 
    (  z  x)  z  xs           ↔⟨ ⊎-left-identity ⊎-cong id 
    z  x        z  xs           

  to-tree-++ :  {P : A  Set} xs {ys} 
               AnyT P (to-tree (xs ++ ys)) 
               AnyT P (to-tree xs)  AnyT P (to-tree ys)
  to-tree-++ {P} [] {ys} =
    AnyT P (to-tree ys)      ↔⟨ inverse ⊎-left-identity 
      AnyT P (to-tree ys)  
  to-tree-++ {P} (x  xs) {ys} =
      P x  AnyT P (to-tree (xs ++ ys))                  ↔⟨ id ⊎-cong id ⊎-cong to-tree-++ xs 
      P x  AnyT P (to-tree xs)  AnyT P (to-tree ys)    ↔⟨ lemma _ _ _ _ 
    (  P x  AnyT P (to-tree xs))  AnyT P (to-tree ys)  
    where
    lemma : (A B C D : Set)  A  B  C  D  (A  B  C)  D
    lemma A B C D =
      A  B  C  D      ↔⟨ ⊎-assoc 
      (A  B)  C  D    ↔⟨ ⊎-assoc 
      ((A  B)  C)  D  ↔⟨ inverse ⊎-assoc ⊎-cong id 
      (A  B  C)  D    

  to∘from :  t  to-tree (flatten t) ≈-bagT t
  to∘from leaf         = λ z   
  to∘from (node l x r) = λ z 
    z ∈T to-tree (flatten l ++ x  flatten r)                        ↔⟨ to-tree-++ (flatten l) 
    z ∈T to-tree (flatten l)    z  x  z ∈T to-tree (flatten r)  ↔⟨ to∘from l z ⊎-cong id ⊎-cong id ⊎-cong to∘from r z 
    z ∈T l                      z  x  z ∈T r                    ↔⟨ id ⊎-cong ⊎-left-identity 
    z ∈T l                        z  x  z ∈T r                    

  from∘to :  xs  flatten (to-tree xs) ≈-bag xs
  from∘to []       = λ z   
  from∘to (x  xs) = λ z 
    z  x  z  flatten (to-tree xs)  ↔⟨ id ⊎-cong from∘to xs z 
    z  x  z  xs