{-# OPTIONS --cubical-compatible --safe #-}
open import Equality
module Tree-sort.Examples
{c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where
open Derived-definitions-and-properties eq
open import Prelude
open import Bag-equivalence eq
import Nat eq as Nat
_≤?_ : ℕ → ℕ → Bool
m ≤? n with Nat.total m n
... | inj₁ m≤n = true
... | inj₂ n<m = false
import Tree-sort.Partial eq _≤?_ as P
open import Tree-sort.Full eq Nat._≤_ Nat.total as F using (cons; nil)
orderedP : P.tree-sort (3 ∷ 1 ∷ 2 ∷ []) ≡ 1 ∷ 2 ∷ 3 ∷ []
orderedP = refl _
orderedF : F.tree-sort (3 ∷ 1 ∷ 2 ∷ []) ≡
cons 1 (cons 2 (cons 3 (nil _) _) _) _
orderedF = refl _
a-bag-equivalenceP : 1 ∷ 2 ∷ 3 ∷ [] ≈-bag 3 ∷ 1 ∷ 2 ∷ []
a-bag-equivalenceP = P.tree-sort-permutes (3 ∷ 1 ∷ 2 ∷ [])
a-bag-equivalenceF : 1 ∷ 2 ∷ 3 ∷ [] ≈-bag 3 ∷ 1 ∷ 2 ∷ []
a-bag-equivalenceF = F.tree-sort-permutes (3 ∷ 1 ∷ 2 ∷ [])