diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda index 6e60adda3e..de10d27432 100644 --- a/src/Data/List/Relation/Unary/All/Properties.agda +++ b/src/Data/List/Relation/Unary/All/Properties.agda @@ -77,6 +77,12 @@ null⇒Null : T (null xs) → Null xs null⇒Null {xs = [] } _ = [] null⇒Null {xs = _ ∷ _} () +nullxs→xs≡[] : Null xs → xs ≡ [] +nullxs→xs≡[] [] = refl + +xs≡[]→nullxs : xs ≡ [] → Null xs +xs≡[]→nullxs xs≡[] rewrite xs≡[] = [] + ------------------------------------------------------------------------ -- Properties of the "points-to" relation _[_]=_ diff --git a/src/Data/Queue.agda b/src/Data/Queue.agda new file mode 100644 index 0000000000..cd50200bbc --- /dev/null +++ b/src/Data/Queue.agda @@ -0,0 +1,11 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Queues +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Data.Queue where + +open import Data.Queue.TwoList.Base public diff --git a/src/Data/Queue/QueueSpec.agda b/src/Data/Queue/QueueSpec.agda new file mode 100644 index 0000000000..abbbec8e1d --- /dev/null +++ b/src/Data/Queue/QueueSpec.agda @@ -0,0 +1,82 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Queue specification +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Data.Queue.QueueSpec where + +open import Data.Bool.Base using (Bool) +open import Data.List.Base as List using (List; []; length; _∷_) +open import Data.List.Relation.Unary.All using (Null) +open import Data.Maybe.Base using (Maybe; nothing; just) +open import Data.Nat.Base using (ℕ) +open import Data.Product.Base using (_×_; proj₁; proj₂) +open import Function.Base using (_∘_) +open import Level +open import Relation.Binary.Core using (Rel; _=[_]⇒_) +open import Relation.Binary.Definitions using (_Respects_) +open import Relation.Binary.Structures using (IsEquivalence) +open import Relation.Binary.PropositionalEquality.Core using (_≡_) +open import Relation.Nullary.Decidable.Core using (yes; no; isYes; False; does) +open import Relation.Unary using (Pred; Decidable) + +private + variable + a b : Level + A : Set a + B : Set b + +-- RawQueue defines the 'computations' available on Queues +-- without any of the associated proofs that determine its +-- correctness. +record RawQueue (Q : Set a → Set a) : Set (suc a) where + + field + _≈_ : ∀ {A : Set a} → Rel (Q A) a + Empty : ∀ {A : Set a} → Pred (Q A) a + empty? : Decidable (Empty {A = A}) + fromList : List A → Q A + toList : Q A → List A + enqueue : A → Q A → Q A + dequeue : (q : Q A) → .{{False (empty? q)}} → Q A × A + size : Q A → ℕ + + empty : Q A + empty = fromList [] + + pure : A → Q A + pure = fromList ∘ List.[_] + + to𝔹 : Q A → Bool + to𝔹 = isYes ∘ empty? + + dequeue′ : Q A → Maybe (Q A × A) + dequeue′ q with empty? q in eq + ... | yes _ = nothing + ... | no _ = just (dequeue q) + where instance + _ : False (empty? q) + _ rewrite eq = _ + +-- IsQueue bundles RawQueue with proofs of a Queues correctness, +-- such as enqueue adding 1 to the Queue's size +-- NOTE: not finished adding everything! +record IsQueue {Q : Set a → Set a} (rawQ : RawQueue Q) : Set (suc a) where + + open RawQueue rawQ + + field + isEquivalence : IsEquivalence (_≈_ {A = A}) + ≈-resp-Empty : Empty Respects (_≈_ {A = A}) + ≈-=[toList]⇒-≡ : (_≈_ {A = A}) =[ toList ]⇒ _≡_ + empty-toList : ∀ {q : Q A} → Empty q → Null (toList q) + empty-fromList : ∀ {xs : List A} → Null {A = A} xs → Empty (fromList xs) + toList-fromList : ∀ {q : Q A} {xs : List A} → q ≈ fromList xs → toList q ≡ xs + fromList-toList : ∀ {q : Q A} {xs : List A} → xs ≡ toList q → fromList xs ≈ q + toList-enqueue : ∀ {q : Q A} {x : A} → toList (enqueue x q) ≡ x ∷ toList q + -- for some reason, let x , r = ... doesn't bind x and r?? + toList-dequeue : ∀ {q : Q A} → .{{i : False (empty? q)}} → + let xr = dequeue q {{i}} in toList q ≡ toList (proj₁ xr) List.∷ʳ proj₂ xr diff --git a/src/Data/Queue/TwoList/Base.agda b/src/Data/Queue/TwoList/Base.agda new file mode 100644 index 0000000000..35d8ff6bf9 --- /dev/null +++ b/src/Data/Queue/TwoList/Base.agda @@ -0,0 +1,129 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Queues, basic types and operations +------------------------------------------------------------------------ +{-# OPTIONS --without-K --safe #-} + +-- Queues implemented with the two-list method described in +-- "Purely Functional Data Structures", Chris Okasaki, 1996 +-- +-- Note that the weaker invariant is used here that only guarantees +-- amortized O(1) when the structure is used non-persistently. + +module Data.Queue.TwoList.Base where + +open import Level using (Level) +open import Data.Bool.Base using (Bool; true; false) +open import Data.List.Base as List using (List; []; _∷_; reverse; _++_; length; null) +open import Data.List.Relation.Unary.All using (Null; []; _∷_) +open import Data.List.Relation.Unary.All.Properties using (null⇒Null; Null⇒null) +open import Data.Maybe.Base using (Maybe; nothing; just) +open import Data.Nat.Base using (ℕ; zero; suc; _+_) +open import Data.Product using (_×_; _,_; proj₂) +open import Data.Queue.QueueSpec using (RawQueue; IsQueue) +open import Data.SnocList.Base as SnocList using (List<; toList>; fromList>; []; _<:_; _<><_) +open import Data.SnocList.Relation.Unary.All +open import Data.SnocList.Relation.Unary.All.Properties using (¬null-<:; null-<:→nullxs) +open import Data.Unit.Base using (⊤) +open import Function.Base using (id; const; _∘_) +open import Relation.Binary.PropositionalEquality.Core using (_≡_) +open import Relation.Binary.Core using (Rel) +open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (contradiction) +open import Relation.Nullary.Decidable.Core using (yes; no; isYes; False) +open import Relation.Nullary.Reflects using (ofʸ; ofⁿ) +open import Relation.Unary using (Pred; Decidable) + +private + variable + a b : Level + A : Set a + B : Set b + +-- A Queue consists of a front (dequeue) and back (enqueue) list +-- When enqueing (unless it is the first element), elements are cons'd +-- to the enqueue list. +-- +-- When dequeuing, elements are taken from the head of the dequeue +-- list. If this is empty, the enqueue list is reversed and swapped +-- with the dequeue list. +-- +-- The dequeue-list should be empty iff the whole queue is empty. + +record Queue (A : Set a) : Set a where + constructor mkQ + field + front : List< A + back : List A + inv : Null< front → Null back + +------------------------------------------------------------------------ +--- Basic Functions/Relations/Operators + +Empty : ∀ {A : Set a} → Pred (Queue A) a +Empty {a} {A} q = Null< (Queue.front q) + +empty? : Decidable (Empty {A = A}) +empty? (mkQ front back inv) .Relation.Nullary.does = SnocList.null front +empty? (mkQ [] back inv) .Relation.Nullary.proof = ofʸ [] +empty? (mkQ (xs <: x) back inv) .Relation.Nullary.proof = ofⁿ λ null< → contradiction null< ¬null-<: + +isEmpty : Queue A → Bool +isEmpty q = SnocList.null (Queue.front q) + +------------------------------------------------------------------------ +--- Smart Constructor + +queue : List< A → List A → Queue A +queue [] ys = mkQ ([] <>< ys) [] (const []) +queue xs@(_ <: _) ys = mkQ xs ys null-<:→nullxs + +------------------------------------------------------------------------ +--- Conversion to/from List + +-- Create a List from a Queue, such that the last that would be dequeued +-- becomes the head of the list +toList : Queue A → List A +toList q = (Queue.back q) ++ (toList> (Queue.front q)) + +-- Create a Queue from a List, such that the elements +-- of the list would be dequeued starting from its last element +fromList : List A → Queue A +fromList xs = queue [] xs + +------------------------------------------------------------------------ +-- Construction & Destruction + +empty : Queue A +empty = fromList [] + +enqueue : A → Queue A → Queue A +enqueue x q with bs ← Queue.back q | Queue.front q +... | [] = queue ([] <: x) [] +... | front@(_ <: _) = queue front (x ∷ bs) + +dequeue : ∀ (q : Queue A) .{{_ : False (empty? q)}} → Queue A × A +dequeue (mkQ (xs <: x) back _) = queue xs back , x + +-- Create a queue with a single element +singleton : A → Queue A +singleton = fromList ∘ List.[_] + +-- map : (A → B) → Queue A → Queue B +-- map f empty = empty +-- map f (queue x xs ys) = queue (f x) (List.map f xs) (List.map f ys) + +------------------------------------------------------------------------ +-- Relations + +-- Under the property that toList returns a list in +-- the order of dequeue +_≈_ : ∀ {A : Set a} → Rel (Queue A) a +q ≈ q' = (toList q) ≡ (toList q') + +------------------------------------------------------------------------ +-- Size + +size : Queue A → ℕ +size = length ∘ toList diff --git a/src/Data/Queue/TwoList/Instances.agda b/src/Data/Queue/TwoList/Instances.agda new file mode 100644 index 0000000000..df3ae94af7 --- /dev/null +++ b/src/Data/Queue/TwoList/Instances.agda @@ -0,0 +1,56 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Instances of TwoLisQueue +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Data.Queue.TwoList.Instances where + +open import Data.Queue.TwoList.Base +open import Data.Queue.TwoList.Properties +open import Data.Queue.QueueSpec using (RawQueue; IsQueue) +open import Level using (Level) + +private + variable + a b : Level + A : Set a + B : Set b + +------------------------------------------------------------------------ +--- TwoList Queue is a Raw Queue + +instance + TwoList-RawQueue : RawQueue {a} Queue + TwoList-RawQueue = record + { _≈_ = _≈_ + ; Empty = Empty + ; empty? = empty? + ; fromList = fromList + ; toList = toList + ; enqueue = enqueue + ; dequeue = dequeue + ; size = size + } + +------------------------------------------------------------------------ +-- TwoList Queue is a Queue! + +-- for some reason, unless manually passing some implicits, other implicits remain +-- unsolved? This is also means that you can't assign fields with record syntax and +-- have to use co-pattern matching. My knowledge of implicits isn't good enough to know +-- why or if this indicates 'bad ergonomics' + +instance + TwoList-IsQueue : IsQueue {a} TwoList-RawQueue + TwoList-IsQueue .IsQueue.isEquivalence = ≈-isEquivalence + TwoList-IsQueue .IsQueue.≈-resp-Empty {x = x} {y} = ≈-resp-Empty {x = x} {y = y} + TwoList-IsQueue .IsQueue.≈-=[toList]⇒-≡ {x = x} {y} = ≈-=[toList]⇒-≡ {x = x} {y = y} + TwoList-IsQueue .IsQueue.empty-toList {q = q} = empty-toList {q = q} + TwoList-IsQueue .IsQueue.empty-fromList = empty-fromList + TwoList-IsQueue .IsQueue.toList-fromList {q = q} = toList-fromList {q = q} + TwoList-IsQueue .IsQueue.fromList-toList {q = q} = fromList-toList {q = q} + TwoList-IsQueue .IsQueue.toList-enqueue {q = q} = toList-enqueue {q = q} + TwoList-IsQueue .IsQueue.toList-dequeue {q = q} = toList-dequeue {q = q} diff --git a/src/Data/Queue/TwoList/Properties.agda b/src/Data/Queue/TwoList/Properties.agda new file mode 100644 index 0000000000..9899858090 --- /dev/null +++ b/src/Data/Queue/TwoList/Properties.agda @@ -0,0 +1,212 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Queue-related properties +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Data.Queue.TwoList.Properties where + +open import Level using (Level) +open import Data.List.Base using (List; _∷_; _∷ʳ_; _++_; length) +open import Data.List.Properties using (++-identityʳ; length-++; length-reverse; ++-assoc) +open import Data.List.Relation.Unary.All using (All; Null; []) +open import Data.List.Relation.Unary.All.Properties using (++⁺; nullxs→xs≡[]) +open import Data.Nat.Base using (suc; _+_) +open import Data.Nat.Properties using (+-comm; +-suc; +-assoc) +open import Data.Product.Base using (_×_; proj₁; proj₂) +open import Data.Queue.QueueSpec using (RawQueue; IsQueue) +open import Data.Queue.TwoList.Base +open import Data.SnocList.Base as SnocList using (List<; []; _<:_; toList>; fromList>; _<><_; _<>>_) + renaming (_++_ to _++<_) +open import Data.SnocList.Properties + renaming (++-identityʳ to ++<-identityʳ; ++-identityˡ to ++<-identityˡ; ++-identity to ++<-identity) + hiding (length-++) +open import Data.SnocList.Relation.Unary.All using (All<; Null<; []; _<:_) +open import Data.SnocList.Relation.Unary.All.Properties using (all<>>; all<>) +open import Function.Base using (_∘_) +open import Relation.Binary.Core using (_=[_]⇒_) +open import Relation.Binary.PropositionalEquality.Core as ≡ +open import Relation.Binary.PropositionalEquality.Properties as ≡ +open import Relation.Binary.Definitions using (Reflexive; _Respects_) +open import Relation.Binary.Structures using (IsEquivalence) +open import Relation.Nullary using (¬_; False; contradiction) +open import Relation.Unary using (Pred) +open import Tactic.Cong using (cong!) + +open ≡-Reasoning + +private + variable + a b : Level + A : Set a + B : Set b + + ¬Null : {x : A} {xs : List A} → ¬ Null (x ∷ xs) + ¬Null (() Data.List.Relation.Unary.All.∷ n) + + queue-back[] : ∀ {xs : List< A} → (Queue.back (queue xs [])) ≡ [] + queue-back[] {xs = []} = refl + queue-back[] {xs = xs <: x} = refl + + queue[]xs→back≡[] : ∀ {xs : List A} → (Queue.back (queue [] xs)) ≡ [] + queue[]xs→back≡[] = refl + + queue-front : ∀ {xs : List< A} → (Queue.front (queue xs [])) ≡ xs + queue-front {xs = []} = refl + queue-front {xs = xs <: x} = refl + + queue[]xs→ xs) + queue[]xs→>[]≡[] xs≡[] + +toList≡[]→empty : ∀ {xs : Queue A} → toList xs ≡ [] → Empty xs +toList≡[]→empty {xs = xs} xs≡[] rewrite (toList≡[]→front≡[] {xs = xs} xs≡[]) = [] + +toList-fromList : ∀ {q : Queue A} {xs : List A} → q ≈ fromList xs → toList q ≡ xs +toList-fromList {q = q} {xs = xs} q≈xs = begin + toList q ≡⟨ q≈xs ⟩ + toList (fromList xs) ≡⟨ toList-fromList' xs ⟩ + xs ∎ + where + toList-fromList' : ∀ (xs : List A) → toList (fromList xs) ≡ xs + toList-fromList' xs = begin + toList (fromList xs) ≡⟨⟩ + toList (queue [] xs) ≡⟨ cong₂ _++_ (queue[]xs→back≡[] {xs = xs}) refl ⟩ + [] ++ (toList> (Queue.front (queue [] xs))) ≡⟨⟩ + toList> (Queue.front (queue [] xs)) ≡⟨⟩ + toList> (fromList> xs) ≡⟨ toList>-fromList> xs ⟩ + xs ∎ + +fromList-toList : ∀ {q : Queue A} {xs : List A} → xs ≡ toList q → fromList xs ≈ q +fromList-toList {q = q} {xs} xs≈q = begin + ([] <>< xs) <>> [] ≡⟨ []<>>[]≡xs {xs = xs} ⟩ + xs ≡⟨ xs≈q ⟩ + Queue.back q ++ Queue.front q <>> [] ∎ + +empty-toList : ∀ {q : Queue A} → Empty q → Null (toList q) +empty-toList {q = mkQ front back inv} emptyq = ++⁺ {xs = back} (inv emptyq) (all<> emptyq) + +empty-fromList : ∀ {xs : List A} → Null xs → Empty (fromList xs) +empty-fromList {xs = []} nullxs = [] +empty-fromList {xs = x ∷ xs} nullxs = contradiction nullxs ¬Null + +toList-enqueue : ∀ {q : Queue A} {x : A} → toList (enqueue x q) ≡ x ∷ toList q +toList-enqueue {q = mkQ [] back inv} {x} = begin + x ∷ [] ≡⟨⟩ + x ∷ [] ++ [] ≡⟨ sym (cong! (nullxs→xs≡[] (inv []))) ⟩ + x ∷ back ++ [] ∎ +toList-enqueue {q = mkQ (front <: x) back inv} = refl + +toList-dequeue : ∀ {q : Queue A} → .{{i : False (empty? q)}} → + let xr = dequeue q {{i}} in toList q ≡ toList (proj₁ xr) ∷ʳ proj₂ xr +toList-dequeue {q = mkQ (xs <: x) [] inv} = begin + xs <>> (x ∷ []) ≡⟨ cong! (sym (++<-identityˡ xs)) ⟩ + ([] ++< xs) <>> (x ∷ []) ≡⟨ <>>-toList>++ {xs = ([] ++< xs)} ⟩ + (toList> ([] ++< xs)) ++ (x ∷ []) ≡⟨ cong! (toList>-distrib-++ {xs = []} {ys = xs}) ⟩ + ([] ++ (toList> xs)) ++ (x ∷ []) ≡⟨ cong! (sym (queue-back[] {xs = xs})) ⟩ + ((Queue.back (queue xs [])) ++ (toList> xs)) ++ (x ∷ []) ≡⟨⟩ + ((Queue.back (queue xs [])) ++ (xs <>> [])) ++ (x ∷ []) ≡⟨ cong! (sym (queue-front {xs = xs})) ⟩ + ((Queue.back (queue xs [])) ++ (Queue.front (queue xs []) <>> [])) ++ (x ∷ []) ∎ + +-- either xs empty, so Queue.back ≡ [], or xs is not, so Queue.back ≡ y ∷ ys +toList-dequeue {q = mkQ ([] <: x) (y ∷ ys) inv} = sym (begin + (([] <: y) <>< ys) <>> [] ++ x ∷ [] ≡⟨ cong (λ z → z ++ x ∷ []) (fish-and-chips ys ([] <: y) []) ⟩ + ([] <: y) <>> ([] <>< ys) <>> [] ++ x ∷ [] ≡⟨⟩ + [] <>> (y ∷ (([] <>< ys) <>> [] ++ x ∷ [])) ≡⟨⟩ + (y ∷ (([] <>< ys) <>> [] ++ x ∷ [])) ≡⟨ cong! ([]<>>[]≡xs {xs = ys}) ⟩ + y ∷ ys ++ x ∷ [] ∎ + ) + +toList-dequeue {q = mkQ ((xs <: z) <: x) (y ∷ ys) inv} = begin + y ∷ ys ++ xs <>> (z ∷ x ∷ []) ≡⟨⟩ + y ∷ (ys ++ xs <>> (z ∷ x ∷ [])) ≡⟨ cong! (sym (++-identityʳ (xs <>> (z ∷ x ∷ [])))) ⟩ + y ∷ (ys ++ xs <>> (z ∷ x ∷ []) ++ []) ≡⟨ cong (λ w → y ∷ (ys ++ w)) (++<>> {xs = xs} {ys = []})⟩ + y ∷ (ys ++ xs <>> (z ∷ []) ++ (x ∷ [])) ≡⟨ cong (λ w → y ∷ w) (sym (Data.List.Properties.++-assoc ys (xs <>> (z ∷ [])) (x ∷ []))) ⟩ + y ∷ (ys ++ xs <>> (z ∷ [])) ++ x ∷ [] ∎ + + where + ++<>> : ∀ {x y} {xs : List< A} {ys : List A} → xs <>> (x ∷ y ∷ []) ++ ys ≡ (xs <>> (x ∷ [])) ++ (y ∷ ys) + ++<>> {x = x} {y} {xs} {ys} = begin + xs <>> (x ∷ y ∷ []) ++ ys ≡⟨⟩ + xs <>> ((x ∷ []) ++ (y ∷ [])) ++ ys ≡⟨ sym (<>>++∷ {xs = xs} {ys = (x ∷ [])}) ⟩ + xs <>> (x ∷ []) ++ y ∷ ys ∎ + +------------------------------------------------------------------------ +-- Properties relating to size + +-- enqueue increases size by 1 +-- rewrite could make it cleaner, but are we trying to use that less? +size-enqueue : (x : A) (q : Queue A) → size (enqueue {a} x q) ≡ suc (size q) +size-enqueue {a = a} {A = A} x q@(mkQ [] back inv) = begin + size (queue ([] <: x) []) ≡⟨⟩ + length (x ∷ []) ≡⟨⟩ + suc 0 ≡⟨ cong suc (sym sizeq) ⟩ + suc (size q) ∎ + where + null→≡[] : Null back → back ≡ [] + null→≡[] [] = refl + + back[] : back ≡ [] + back[] = null→≡[] (inv []) + + -- why does length need {a} and {A} after back ↦ []? + sizeq : size q ≡ 0 + sizeq = begin + size q ≡⟨⟩ + length (toList q) ≡⟨⟩ + length (back ++ []) ≡⟨ cong length (++-identityʳ back) ⟩ + length back ≡⟨ cong length back[] ⟩ + length {a} {A} [] ≡⟨⟩ + 0 ∎ + +size-enqueue {A = A} x q@(mkQ front@(_ <: _) back inv) = begin + size (queue front (x ∷ back)) ≡⟨⟩ + length (x ∷ back ++ toList> front) ≡⟨ length-++ (x ∷ back) ⟩ + length (x ∷ back) + length (toList> front) ≡⟨⟩ + suc (length back) + length (toList> front) ≡⟨ +-comm (suc (length back)) (length (toList> front)) ⟩ + length (toList> front) + suc (length back) ≡⟨ +-suc (length (toList> front)) (length back)⟩ + suc (length (toList> front) + length back) ≡⟨ cong suc (+-comm (length (toList> front)) (length back)) ⟩ + suc (length back + length (toList> front)) ≡⟨ cong suc (sym (length-++ back {toList> front})) ⟩ + suc (length (back ++ (toList> front))) ≡⟨⟩ + suc (length (toList q)) ≡⟨⟩ + suc (size q) ∎ + +-- trivial, but ensures empty works correctly +size-empty : size (empty {a} {A}) ≡ 0 +size-empty = refl + +------------------------------------------------------------------------ +-- Properties of _≈_ + +-- it becomes propositional equality on lists, so easy! +≈-isEquivalence : IsEquivalence (_≈_ {A = A}) +≈-isEquivalence = record + { refl = refl + ; sym = sym + ; trans = trans + } + +≈-resp-Empty : Empty Respects (_≈_ {A = A}) +≈-resp-Empty {x = x} {y = y} x≈y empty-x = toList≡[]→empty {xs = y} (begin + toList y ≡⟨ sym x≈y ⟩ + toList x ≡⟨ empty→toList≡[] {x = x} empty-x ⟩ + [] ∎ + ) + +-- _≈_ on TwoList is defined exactly as such +≈-=[toList]⇒-≡ : (_≈_ {A = A}) =[ toList ]⇒ _≡_ +≈-=[toList]⇒-≡ x≈y = x≈y diff --git a/src/Data/SnocList/Properties.agda b/src/Data/SnocList/Properties.agda new file mode 100644 index 0000000000..bf6a760544 --- /dev/null +++ b/src/Data/SnocList/Properties.agda @@ -0,0 +1,125 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- SnocList properties +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Data.SnocList.Properties where + +open import Algebra.Definitions as AlgebraicDefinitions using () +open import Data.Empty using (⊥-elim) +open import Data.List.Base using () renaming (_++_ to _++>_) +open import Data.List.Properties using () renaming (++-assoc to ++>-assoc; ++-identityʳ to ++>-identityʳ) +open import Data.Nat.Base using (suc; _+_) +open import Data.Product.Base using (_,_) +open import Data.SnocList.Base +open import Level using (Level) +open import Relation.Binary.PropositionalEquality.Core as ≡ +open import Relation.Binary.PropositionalEquality.Properties as ≡ +open import Tactic.Cong using (cong!) + +open ≡-Reasoning + +private + variable + a b : Level + A : Set a + B : Set b + +-- Yummy! Best gotten from Penarth Pier :-) +fish-and-chips : ∀ (xs : List> A) (sx : List< A) (ys : List> A) → + (sx <>< xs) <>> ys ≡ sx <>> ( ([] <>< xs) <>> ys ) +fish-and-chips [] sx ys = refl +fish-and-chips xs'@(x :> xs) sx ys = begin + (sx <>< (x :> xs)) <>> ys ≡⟨⟩ + ((sx <: x) <>< xs) <>> ys ≡⟨ fish-and-chips xs (sx <: x) ys ⟩ + (sx <: x) <>> (([] <>< xs) <>> ys) ≡⟨⟩ + sx <>> (x :> (([] <>< xs) <>> ys)) ≡⟨⟩ + sx <>> (([] <: x) <>> (([] <>< xs) <>> ys)) ≡⟨ sym (cong (λ hole → sx <>> hole) (fish-and-chips xs ([] <: x) ys)) ⟩ + sx <>> ((([] <: x) <>< xs) <>> ys) ≡⟨⟩ + sx <>> (([] <>< (x :> xs)) <>> ys) ∎ + +toList>-fromList> : ∀ (xs : List> A) → toList> (fromList> xs) ≡ xs +toList>-fromList> [] = refl +toList>-fromList> (x :> xs) = begin + toList> (fromList> (x :> xs)) ≡⟨⟩ + (([] <: x) <>< xs) <>> [] ≡⟨ fish-and-chips xs ([] <: x) [] ⟩ + ([] <: x) <>> (([] <>< xs) <>> []) ≡⟨⟩ + [] <>> (x :> (([] <>< xs) <>> [])) ≡⟨⟩ + [] <>> (x :> toList> (fromList> xs)) ≡⟨ cong! (toList>-fromList> xs) ⟩ + [] <>> (x :> xs) ≡⟨⟩ + x :> xs ∎ + +¬xs<>>ys≡[] : ∀ {x} {xs : List< A} {ys : List> A} → xs <>> (x :> ys) ≢ [] +¬xs<>>ys≡[] {xs = []} () +¬xs<>>ys≡[] {xs = xs <: x} wrong = ¬xs<>>ys≡[] {xs = xs} wrong + +xs<>>[]≡[] : ∀ {xs : List< A} → xs <>> [] ≡ [] → xs ≡ [] +xs<>>[]≡[] {xs = []} xs<>>[]≡[] = refl +xs<>>[]≡[] {xs = (xs <: x)} xs<>>[]≡[] = ⊥-elim (¬xs<>>ys≡[] {xs = xs} {ys = []} xs<>>[]≡[]) + +[]<>>[]≡xs : ∀ {xs : List> A} → ([] <>< xs) <>> [] ≡ xs +[]<>>[]≡xs {xs = []} = refl +[]<>>[]≡xs {xs = x :> xs} = begin + ([] <: x <>< xs) <>> [] ≡⟨ aux {y = x} {ys = xs} ⟩ + x :> (([] <>< xs) <>> []) ≡⟨ cong (_:>_ x) ([]<>>[]≡xs {xs = xs}) ⟩ + x :> xs ∎ + where + aux : ∀ {y} {ys : List> A} → ([] <: y <>< ys) <>> [] ≡ y :> (([] <>< ys) <>> []) + aux {y = y} {ys = ys} = begin + ([] <: y <>< ys) <>> [] ≡⟨ fish-and-chips ys ([] <: y) [] ⟩ + ([] <: y) <>> (([] <>< ys) <>> []) ≡⟨⟩ + [] <>> (y :> (([] <>< ys) <>> [])) ≡⟨⟩ + y :> (([] <>< ys) <>> []) ∎ + +------------------------------------------------------------------------ +-- Properties of ++ + +length-++ : ∀ (xs : List< A) {ys} → + length (ys ++ xs) ≡ length xs + length ys +length-++ [] = refl +length-++ (xs <: x) = cong suc (length-++ xs) + +module _ {A : Set a} where + + open AlgebraicDefinitions {A = List< A} _≡_ + + ++-identityˡ : LeftIdentity [] _++_ + ++-identityˡ [] = refl + ++-identityˡ (xs <: x) = cong (_<: x) (++-identityˡ xs) + + ++-identityʳ : RightIdentity [] _++_ + ++-identityʳ xs = refl + + ++-identity : Identity [] _++_ + ++-identity = ++-identityˡ , ++-identityʳ + +<>>++∷ : ∀ {z} {xs : List< A} {ys zs : List> A} → (xs <>> ys) ++> (z :> zs) ≡ (xs <>> (ys ++> (z :> []))) ++> zs +<>>++∷ {z = z} {xs = []} {ys = ys} {zs = zs} = begin + ys ++> (z :> zs) ≡⟨⟩ + ys ++> ((z :> []) ++> zs) ≡⟨ sym (++>-assoc ys (z :> []) zs) ⟩ + (ys ++> (z :> [])) ++> zs ∎ +<>>++∷ {z = z} {xs = xs <: x} {ys = ys} {zs = zs} = <>>++∷ {z = z} {xs = xs} {ys = (x :> ys)} {zs = zs} + +<>>-toList>++ : ∀ {xs : List< A} {ys : List> A} → xs <>> ys ≡ (toList> xs) ++> ys +<>>-toList>++ {xs = []} = refl +<>>-toList>++ {xs = xs <: x} {ys} = begin + (xs <: x) <>> ys ≡⟨⟩ + xs <>> (x :> ys) ≡⟨ <>>-toList>++ {xs = xs} ⟩ + (toList> xs) ++> (x :> ys) ≡⟨ <>>++∷ {xs = xs} ⟩ + (xs <>> (x :> [])) ++> ys ∎ + +-- toList> distributes over _++_ (with a change in direction of ++) +-- is it really distributive if it's with two different ++? +toList>-distrib-++ : ∀ {xs ys : List< A} → toList> (xs ++ ys) ≡ (toList> xs) ++> (toList> ys) +toList>-distrib-++ {xs = xs} {ys = []} = begin + xs <>> [] ≡⟨ sym (++>-identityʳ (xs <>> [])) ⟩ + xs <>> [] ++> [] ∎ +toList>-distrib-++ {xs = xs} {ys = ys <: y} = begin + (xs ++ ys) <>> (y :> []) ≡⟨ <>>-toList>++ {xs = (xs ++ ys)} ⟩ + (toList> (xs ++ ys)) ++> (y :> []) ≡⟨ cong! (toList>-distrib-++ {xs = xs} {ys = ys}) ⟩ + (toList> xs ++> toList> ys) ++> (y :> []) ≡⟨ Data.List.Properties.++-assoc (toList> xs) (toList> ys) (y :> []) ⟩ + toList> xs ++> toList> ys ++> (y :> []) ≡⟨ cong! (sym (<>>-toList>++ {xs = ys})) ⟩ + toList> xs ++> ys <>> (y :> []) ∎ diff --git a/src/Data/SnocList/Relation/Unary/All.agda b/src/Data/SnocList/Relation/Unary/All.agda new file mode 100644 index 0000000000..7f36e3a3cd --- /dev/null +++ b/src/Data/SnocList/Relation/Unary/All.agda @@ -0,0 +1,39 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- SnocLists where all elements satisfy a given property +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Data.SnocList.Relation.Unary.All where + +open import Data.SnocList.Base +open import Relation.Unary using (Pred; ∅) +open import Level using (Level; suc; _⊔_) + +private + variable + a b p q r ℓ : Level + A : Set a + B : Set b + P Q R : Pred A p + x : A + xs : List< A + +------------------------------------------------------------------------ +-- Definitions + +-- Given a predicate P, then All P xs means that every element in xs +-- satisfies P. See `Relation.Unary` for an explanation of predicates. +-- +-- Equivalent to the definition on List>, but now for List< + +infixr 5 _<:_ + +data All< {A : Set a} (P : Pred A p) : Pred (List< A) (a ⊔ p) where + [] : All< P [] + _<:_ : ∀ {x xs} (px : P x) (pxs : All< P xs) → All< P (xs <: x) + +Null< : Pred (List< A) _ +Null< = All< ∅ diff --git a/src/Data/SnocList/Relation/Unary/All/Properties.agda b/src/Data/SnocList/Relation/Unary/All/Properties.agda new file mode 100644 index 0000000000..2fd6d38db7 --- /dev/null +++ b/src/Data/SnocList/Relation/Unary/All/Properties.agda @@ -0,0 +1,43 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of All< +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Data.SnocList.Relation.Unary.All.Properties where + +open import Data.List.Relation.Unary.All using (All; Null; []) +open import Data.SnocList.Base using (_<>>_; List<; List>; _:>_; _<:_; toList>; []) +open import Data.SnocList.Relation.Unary.All using (All<; _<:_; Null<) +open import Function.Base using (const) +open import Level using (Level) +open import Relation.Nullary using (¬_; contradiction) +open import Relation.Unary using (Pred) + +private + variable + a b : Level + A : Set a + B : Set b + +------------------------------------------------------------------------ +-- Properites of All< + +all<>> : ∀ {x} {xs : List< A} {ys : List> A} {p : Pred A a} → All p ys → All< p xs → p x → All p (xs <>> (x :> ys)) +all<>> {xs = []} allys allxs px = px All.∷ allys +all<>> {x = a} {xs = xs <: x} {ys = ys} allys (px <: allxs) pa = all<>> (pa All.∷ allys) allxs px + +all<> : ∀ {xs : List< A} {p : Pred A a} → All< p xs → All p (toList> xs) +all<> {xs = []} all< = [] +all<> {xs = xs <: x} (px <: all<) = all<>> [] all< px + +------------------------------------------------------------------------ +-- Properites of Null< + +¬null-<: : {a : A} {as : List< A} → ¬ (Null< (as <: a)) +¬null-<: (() <: n) + +null-<:→nullxs : ∀ {x} {xs : List< A} {ys : List> A} → Null< (xs <: x) → Null ys +null-<:→nullxs null-<: = contradiction null-<: ¬null-<: