{-# OPTIONS --without-K #-}
module Tree where
open import Bag-equivalence
open import Equality.Propositional
open import Prelude hiding (id)
import Bijection
open Bijection equality-with-J using (_↔_)
import Function-universe
open Function-universe equality-with-J
data Tree (A : Set) : Set where
leaf : Tree A
node : (l : Tree A) (x : A) (r : Tree A) → Tree A
AnyT : ∀ {A} → (A → Set) → (Tree A → Set)
AnyT P leaf = ⊥
AnyT P (node l x r) = AnyT P l ⊎ P x ⊎ AnyT P r
_∈T_ : ∀ {A} → A → Tree A → Set
x ∈T t = AnyT (_≡_ x) t
_≈-bagT_ : ∀ {A} → Tree A → Tree A → Set
t₁ ≈-bagT t₂ = ∀ x → x ∈T t₁ ↔ x ∈T t₂
singleton : {A : Set} → A → Tree A
singleton x = node leaf x leaf
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 : {A : Set} → Tree A → List A
flatten leaf = []
flatten (node l x r) = flatten l ++ x ∷ flatten r
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 □
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
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 □