{-# OPTIONS --cubical-compatible --safe #-}
open import Equality
open import Prelude hiding (id; _∘_; lower)
module Tree-sort.Full
{c⁺}
(eq : ∀ {a p} → Equality-with-J a p c⁺)
{A : Type}
(le : A → A → Type)
(total : ∀ x y → le x y ⊎ le y x)
where
open Derived-definitions-and-properties eq
open import Bag-equivalence eq using () renaming (Any to AnyL)
open import Bijection eq using (_↔_)
open import Equivalence eq using (_≃_)
open import Function-universe eq hiding (Kind; module Kind)
open import List eq
data Extended : Type where
min max : Extended
[_] : (x : A) → Extended
infix 4 _≤_
_≤_ : Extended → Extended → Type
min ≤ y = ⊤
[ x ] ≤ [ y ] = le x y
x ≤ max = ⊤
_ ≤ _ = ⊥
infix 4 _,_
record _≤[_]≤_ (l : Extended) (x : A) (u : Extended) : Type where
constructor _,_
field
lower : l ≤ [ x ]
upper : [ x ] ≤ u
data Ordered-list (l u : Extended) : Type where
nil : (l≤u : l ≤ u) → Ordered-list l u
cons : (x : A) (xs : Ordered-list [ x ] u) (l≤x : l ≤ [ x ]) →
Ordered-list l u
to-list : ∀ {l u} → Ordered-list l u → List A
to-list (nil l≤u) = []
to-list (cons x xs l≤x) = x ∷ to-list xs
infix 5 node
syntax node x lx xu = lx -[ x ]- xu
data Search-tree (l u : Extended) : Type where
leaf : (l≤u : l ≤ u) → Search-tree l u
node : (x : A) (lx : Search-tree l [ x ]) (xu : Search-tree [ x ] u) →
Search-tree l u
AnyT : ∀ {l u} → (A → Type) → Search-tree l u → Type
AnyT P (leaf _) = ⊥
AnyT P (node x l r) = AnyT P l ⊎ P x ⊎ AnyT P r
data Kind : Type where
list ordered-list search-tree : Kind
Index : Kind → Type
Index list = ⊤
Index _ = Extended
⟦_⟧ : (k : Kind) → (Index k → Index k → Type)
⟦ list ⟧ _ _ = List A
⟦ ordered-list ⟧ l u = Ordered-list l u
⟦ search-tree ⟧ l u = Search-tree l u
Any : ∀ {k l u} → (A → Type) → (⟦ k ⟧ l u → Type)
Any {k = list} = AnyL
Any {k = ordered-list} = λ P → AnyL P ∘ to-list
Any {k = search-tree} = AnyT
infix 4 _∈_
_∈_ : ∀ {k l u} → A → ⟦ k ⟧ l u → Type
x ∈ xs = Any (λ y → x ≡ y) xs
infix 4 _≈-bag_
_≈-bag_ : ∀ {k₁ k₂ l₁ u₁ l₂ u₂} → ⟦ k₁ ⟧ l₁ u₁ → ⟦ k₂ ⟧ l₂ u₂ → Type
xs ≈-bag ys = ∀ z → (z ∈ xs) ≃ (z ∈ ys)
singleton : ∀ {l u} (x : A) → l ≤[ x ]≤ u → Search-tree l u
singleton x (l≤x , x≤u) = leaf l≤x -[ x ]- leaf x≤u
Any-singleton : ∀ (P : A → Type) {l u x} (l≤x≤u : l ≤[ x ]≤ u) →
Any P (singleton x l≤x≤u) ↔ P x
Any-singleton P {x} l≤x≤u =
Any P (singleton x l≤x≤u) ↔⟨⟩
⊥ ⊎ P x ⊎ ⊥ ↔⟨ ⊎-left-identity ⟩
P x ⊎ ⊥ ↔⟨ ⊎-right-identity ⟩
P x □
insert : ∀ {l u} (x : A) → Search-tree l u → l ≤[ x ]≤ u →
Search-tree l u
insert x (leaf _) l≤x≤u = singleton x l≤x≤u
insert x (ly -[ y ]- yu) (l≤x , x≤u) with total x y
... | inj₁ x≤y = insert x ly (l≤x , x≤y) -[ y ]- yu
... | inj₂ y≤x = ly -[ y ]- insert x yu (y≤x , x≤u)
Any-insert : ∀ (P : A → Type) {l u} x t (l≤x≤u : l ≤[ x ]≤ u) →
Any P (insert x t l≤x≤u) ↔ P x ⊎ Any P t
Any-insert P {l} {u} x (leaf l≤u) l≤x≤u =
Any P (singleton x l≤x≤u) ↔⟨ Any-singleton P l≤x≤u ⟩
P x ↔⟨ inverse ⊎-right-identity ⟩
P x ⊎ ⊥ ↔⟨⟩
P x ⊎ Any P (leaf {l = l} {u = u} l≤u) □
Any-insert P x (ly -[ y ]- yu) (l≤x , x≤u) with total x y
... | inj₁ x≤y =
Any P (insert x ly (l≤x , x≤y)) ⊎ P y ⊎ Any P yu ↔⟨ Any-insert P x ly (l≤x , x≤y) ⊎-cong id ⟩
(P x ⊎ Any P ly) ⊎ P y ⊎ Any P yu ↔⟨ inverse ⊎-assoc ⟩
P x ⊎ Any P ly ⊎ P y ⊎ Any P yu □
... | inj₂ y≤x =
Any P ly ⊎ P y ⊎ Any P (insert x yu (y≤x , x≤u)) ↔⟨ id ⊎-cong id ⊎-cong Any-insert P x yu (y≤x , x≤u) ⟩
Any P ly ⊎ P y ⊎ P x ⊎ Any P yu ↔⟨ lemma _ _ _ _ ⟩
P x ⊎ Any P ly ⊎ P y ⊎ Any P yu □
where
lemma : (A B C D : Type) → A ⊎ B ⊎ C ⊎ D ↔ C ⊎ A ⊎ B ⊎ D
lemma A B C D =
A ⊎ B ⊎ C ⊎ D ↔⟨ id ⊎-cong ⊎-assoc ⟩
A ⊎ (B ⊎ C) ⊎ D ↔⟨ id ⊎-cong ⊎-comm ⊎-cong id ⟩
A ⊎ (C ⊎ B) ⊎ D ↔⟨ ⊎-assoc ⟩
(A ⊎ C ⊎ B) ⊎ D ↔⟨ ⊎-assoc ⊎-cong id ⟩
((A ⊎ C) ⊎ B) ⊎ D ↔⟨ (⊎-comm ⊎-cong id) ⊎-cong id ⟩
((C ⊎ A) ⊎ B) ⊎ D ↔⟨ inverse ⊎-assoc ⊎-cong id ⟩
(C ⊎ A ⊎ B) ⊎ D ↔⟨ inverse ⊎-assoc ⟩
C ⊎ (A ⊎ B) ⊎ D ↔⟨ id ⊎-cong inverse ⊎-assoc ⟩
C ⊎ A ⊎ B ⊎ D □
to-search-tree : List A → Search-tree min max
to-search-tree = foldr (λ x t → insert x t _) (leaf _)
to-search-tree-lemma : ∀ xs → to-search-tree xs ≈-bag xs
to-search-tree-lemma [] = λ z →
z ∈ leaf {l = min} {u = max} _ ↔⟨⟩
z ∈ [] □
to-search-tree-lemma (x ∷ xs) = λ z →
z ∈ insert x (to-search-tree xs) _ ↔⟨ Any-insert (λ x → z ≡ x) _ _ _ ⟩
z ≡ x ⊎ z ∈ to-search-tree xs ↔⟨ id ⊎-cong to-search-tree-lemma xs z ⟩
z ∈ x ∷ xs □
infixr 5 append
syntax append x lx xu = lx -⁅ x ⁆- xu
append : ∀ {l u} (x : A) →
Ordered-list l [ x ] → Ordered-list [ x ] u → Ordered-list l u
nil l≤x -⁅ x ⁆- xu = cons x xu l≤x
cons y yx l≤y -⁅ x ⁆- xu = cons y (yx -⁅ x ⁆- xu) l≤y
Any-append : ∀ (P : A → Type) {l u} x
(lx : Ordered-list l [ x ]) (xu : Ordered-list [ x ] u) →
Any P (lx -⁅ x ⁆- xu) ↔ Any P lx ⊎ P x ⊎ Any P xu
Any-append P x (nil l≤x) xu =
P x ⊎ Any P xu ↔⟨ inverse ⊎-left-identity ⟩
⊥ ⊎ P x ⊎ Any P xu □
Any-append P x (cons y yx l≤y) xu =
P y ⊎ Any P (append x yx xu) ↔⟨ id ⊎-cong Any-append P x yx xu ⟩
P y ⊎ Any P yx ⊎ P x ⊎ Any P xu ↔⟨ ⊎-assoc ⟩
(P y ⊎ Any P yx) ⊎ P x ⊎ Any P xu □
flatten : ∀ {l u} → Search-tree l u → Ordered-list l u
flatten (leaf l≤u) = nil l≤u
flatten (l -[ x ]- r) = flatten l -⁅ x ⁆- flatten r
flatten-lemma : ∀ {l u} (t : Search-tree l u) → flatten t ≈-bag t
flatten-lemma {l} {u} (leaf l≤u) = λ z →
z ∈ nil {l = l} {u = u} l≤u ↔⟨⟩
z ∈ leaf {l = l} {u = u} l≤u □
flatten-lemma (l -[ x ]- r) = λ z →
z ∈ flatten l -⁅ x ⁆- flatten r ↔⟨ Any-append (λ x → z ≡ x) _ _ _ ⟩
z ∈ flatten l ⊎ z ≡ x ⊎ z ∈ flatten r ↔⟨ flatten-lemma l z ⊎-cong id ⊎-cong flatten-lemma r z ⟩
z ∈ l ⊎ z ≡ x ⊎ z ∈ r ↔⟨⟩
z ∈ l -[ x ]- r □
tree-sort : List A → Ordered-list min max
tree-sort = flatten ∘ to-search-tree
tree-sort-permutes : ∀ xs → tree-sort xs ≈-bag xs
tree-sort-permutes xs = λ z →
z ∈ tree-sort xs ↔⟨⟩
z ∈ flatten (to-search-tree xs) ↔⟨ flatten-lemma (to-search-tree xs) _ ⟩
z ∈ to-search-tree xs ↔⟨ to-search-tree-lemma xs _ ⟩
z ∈ xs □