Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Merge and sorted lists and agda
open import Relation.Binary
open import Relation.Binary.PropositionalEquality renaming (sym to psym ; trans to ptrans)
module SortedList
(A : Set)
(_≤_ : A -> A -> Set)
(isDecTotalOrder : IsDecTotalOrder _≡_ _≤_)
where
open import Data.Nat hiding (_≤_ ; _≤?_)
open import Data.List hiding ([_])
open import Data.Product
open import Data.Sum
open import Data.Empty
open import Data.Nat.Properties as NP
open import Algebra.Structures
open import Relation.Nullary
open import Relation.Unary
open import Function
open IsDecTotalOrder isDecTotalOrder
module TO = IsDecTotalOrder isDecTotalOrder
module NC = IsCommutativeSemiring NP.isCommutativeSemiring
mutual
data SVec :-> Set where
[] : SVec 0
[_] : A -> SVec 1
_∷_Witness_ : {n} -> (x : A) -> (xs : SVec (suc n)) -> (p : x ≤ min xs) -> SVec (suc (suc n))
min : {n} -> SVec (suc n) -> A
min [ x ] = x
min (x ∷ xs Witness _) = x
max : {n} -> SVec (suc n) -> A
max [ x ] = x
max (x ∷ xs Witness _) = max xs
rest : {n} -> SVec (suc n) -> SVec n
rest [ _ ] = []
rest (x ∷ xs Witness p) = xs
min-is-min : {n m : ℕ} (eq : suc n ≡ suc m) (xs : SVec (suc n)) -> min xs ≡ min (subst SVec eq xs)
min-is-min eq xs with eq
min-is-min eq [ y ] | _≡_.refl = _≡_.refl
min-is-min eq (x ∷ xs Witness p) | _≡_.refl = _≡_.refl
data All (P : A -> Set) : {n : ℕ} (xs : SVec n) -> Set where
[]-All : All P []
_:All_∷_ : {n} (xs : SVec (suc n)) -> P (min xs) -> All P (rest xs) -> All P {suc n} xs
map-all : {P Q : A -> Set} {n : ℕ} {xs : SVec n} -> P ⊆ Q -> All P xs -> All Q xs
map-all f []-All = []-All
map-all {xs = xs} f (.xs :All p ∷ ps) = xs :All f p ∷ map-all f ps
min≤rest : {n} (xs : SVec (suc n)) -> All (_≤_ (min xs)) (rest xs)
min≤rest [ x ] = []-All
min≤rest (x ∷ xs Witness p) = xs :All p ∷ map-all (TO.trans p) (min≤rest xs)
lview : {n} -> SVec (suc n) -> A × SVec n
lview [ x ] = x , []
lview (x ∷ xs Witness _) = x , xs
toList : {n} -> SVec n -> List A
toList [] = []
toList [ x ] = x ∷ []
toList (x ∷ xs Witness _) = x ∷ toList xs
≤-sym : {x y : A} -> ¬ (x ≤ y) -> y ≤ x
≤-sym {x} {y} p with total x y
≤-sym p | inj₁ a = ⊥-elim (p a)
≤-sym p | inj₂ b = b
mutual
insert : {n} -> A -> SVec n -> SVec (suc n)
insert x [] = [ x ]
insert x [ y ] with total x y
insert x [ y ] | inj₁ p = x ∷ [ y ] Witness p
insert x [ y ] | inj₂ p = y ∷ [ x ] Witness p
insert x (y ∷ ys Witness p) with total x y
insert x (y ∷ ys Witness p) | inj₁ q = x ∷ y ∷ ys Witness p Witness q
insert x (y ∷ ys Witness p) | inj₂ q = y ∷ insert x ys Witness y≤min-insert y x ys p q
y≤min-insert : {n} -> (v x : A)(ys : SVec (suc n)) -> v ≤ min ys -> v ≤ x -> v ≤ min (insert x ys)
y≤min-insert v x [ y ] s t with total x y
y≤min-insert v x [ y ] s t | inj₁ p = t
y≤min-insert v x [ y ] s t | inj₂ p = s
y≤min-insert v x (y ∷ ys Witness p) s t with total x y
y≤min-insert v x (y ∷ ys Witness p) s t | inj₁ q = t
y≤min-insert v x (y ∷ ys Witness p) s t | inj₂ q = s
fromList : (xs : List A) -> SVec (length xs)
fromList [] = []
fromList (x ∷ xs) = insert x (fromList xs)
mutual
merge : {n} {m} -> SVec n -> SVec m -> SVec (n + m)
merge [] ys = ys
merge {n} xs [] = subst SVec (NC.+-comm 0 n) xs
merge [ x ] ys = insert x ys
merge {n} xs [ y ] = subst SVec (NC.+-comm 1 n) (insert y xs)
merge {suc (suc n)} {suc (suc m)} (x ∷ xs Witness p) (y ∷ ys Witness q)
with total x y | merge xs (y ∷ ys Witness q) | merge ys (x ∷ xs Witness p)
... | inj₁ r | m1 | m2 = x ∷ m1 Witness {!x≤min-merge x y xs ys p q r!}
... | inj₂ r | m1 | m2 = subst SVec (NC.+-comm (2 + m) (2 + n))
(y ∷ m2 Witness {!x≤min-merge y x ys xs q p r!})
x≤min-merge : {n m} -> (x y : A)(xs : SVec (suc n))(ys : SVec (suc m))(p : x ≤ min xs)(q : y ≤ min ys) -> x ≤ y -> x ≤ min (merge xs (y ∷ ys Witness q))
x≤min-merge x y [ a ] ys p q r = y≤min-insert x a (y ∷ ys Witness q) r p
x≤min-merge {suc n} {m} x y (xx ∷ xss Witness pa) ys p q r with total xx y
... | inj₁ s = p
... | inj₂ s = subst (_≤_ x)
(min-is-min (NC.+-comm (2 + m) (2 + n))
(y ∷ merge ys (xx ∷ xss Witness pa) Witness
x≤min-merge y xx ys xss q pa s))
r
{- merge {suc n} {suc m} xs ys with total (min xs) (min ys)
... | inj₁ p = merge-rest xs ys p
... | inj₂ p = subst SVec (NC.+-comm (suc m) (suc n)) (merge-rest ys xs p)-}
{- merge-rest : ∀ {n m} (x : SVec (suc n)) (y : SVec (suc m)) -> min x ≤ min y -> SVec (suc n + suc m)
merge-rest {n} {m} x y p = subst SVec (cong suc (NC.+-comm (suc m) n)) (min x ∷ merge y (rest x) Witness {!!})-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment