From 4905cc6e1bf5c14192c4dd44d0f59a7d0fe82515 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Mon, 20 Jul 2026 17:01:27 -0400 Subject: [PATCH 01/53] Add definition of Queue and basic operations --- src/Data/Queue/Base.agda | 73 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 73 insertions(+) create mode 100644 src/Data/Queue/Base.agda diff --git a/src/Data/Queue/Base.agda b/src/Data/Queue/Base.agda new file mode 100644 index 0000000000..8aa4f13ad3 --- /dev/null +++ b/src/Data/Queue/Base.agda @@ -0,0 +1,73 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Queues, basic types and operations +------------------------------------------------------------------------ +{-# OPTIONS --without-K --safe #-} + +-- Queues implemented with the usual two-list method + +module Data.Queue.Base where + +open import Agda.Builtin.Equality +open import Level using (Level) +open import Data.Bool +open import Data.List.Base as List using (List; []; _∷_; reverse; _++_) +open import Data.Maybe.Base using (Maybe; nothing; just) +open import Data.Nat.Base using (ℕ; zero; suc; _+_) +open import Data.Product using (_×_; _,_) +open import Function + +private + variable + l : Level + A B : Set l + +-- A Queue consists of a dequeue and 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. +-- To enforce this, the head of the dequeue list is taken +-- seperately and a constructor for an empty queue is given. + +data Queue (A : Set l) : Set l where + empty : Queue A + + -- dequeue-head → dequeue-list → enqueue-list + queue : A → List A → List A → Queue A + +------------------------------------------------------------------------ +-- Construction & Destruction + +enqueue : Queue A → A → Queue A +enqueue empty a = queue a [] [] +enqueue (queue dq-hd dq-tail eq) a = queue dq-hd dq-tail (a ∷ eq) + +dequeue : Queue A → Maybe (A × Queue A) +dequeue empty = nothing +dequeue (queue dq-hd [] eq) with reverse eq +... | [] = just (dq-hd , empty) +... | x ∷ req = just (dq-hd , queue x req []) +dequeue (queue dq-hd (x ∷ xs) eq) = just (dq-hd , (queue x xs eq)) + +------------------------------------------------------------------------ +--- Conversion to/from List + +-- Create a List from a Queue, such that the first that would be dequeued +-- becomes the head of the list (i.e. the first element of the queue +-- becomes the last element of the list) +toList : Queue A → List A +toList empty = [] +toList (queue dq-hd dq-tail eq) = dq-hd ∷ (dq-tail ++ (reverse eq)) + +-- Create a Queue from a List, such that the elements +-- of the list would be dequeued starting from its first element +-- (i.e. the first element of the list becomes the last element of the queue) +fromList : List A → Queue A +fromList [] = empty +fromList (x ∷ xs) = queue x xs [] From 4125b12710b3c87dfafad9124e659ee2af6e3a37 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Mon, 20 Jul 2026 17:01:40 -0400 Subject: [PATCH 02/53] Add top-level Queue module --- src/Data/Queue.agda | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 src/Data/Queue.agda diff --git a/src/Data/Queue.agda b/src/Data/Queue.agda new file mode 100644 index 0000000000..24bb668186 --- /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.Base public From bf7790b4010f2aef861a1aecc7eaa37e665646ff Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Mon, 20 Jul 2026 17:06:06 -0400 Subject: [PATCH 03/53] Add some basic functions --- src/Data/Queue/Base.agda | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/src/Data/Queue/Base.agda b/src/Data/Queue/Base.agda index 8aa4f13ad3..3770dc5a01 100644 --- a/src/Data/Queue/Base.agda +++ b/src/Data/Queue/Base.agda @@ -12,7 +12,7 @@ module Data.Queue.Base where open import Agda.Builtin.Equality open import Level using (Level) open import Data.Bool -open import Data.List.Base as List using (List; []; _∷_; reverse; _++_) +open import Data.List.Base as List using (List; []; _∷_; reverse; _++_; length) open import Data.Maybe.Base using (Maybe; nothing; just) open import Data.Nat.Base using (ℕ; zero; suc; _+_) open import Data.Product using (_×_; _,_) @@ -55,6 +55,21 @@ dequeue (queue dq-hd [] eq) with reverse eq ... | x ∷ req = just (dq-hd , queue x req []) dequeue (queue dq-hd (x ∷ xs) eq) = just (dq-hd , (queue x xs eq)) +------------------------------------------------------------------------ +--- Basic Functions + +isEmpty : Queue A → Bool +isEmpty empty = true +isEmpty _ = false + +size : Queue A → ℕ +size empty = 0 +size (queue x xs ys) = 1 + length xs + length ys + +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) + ------------------------------------------------------------------------ --- Conversion to/from List From d26d47cbbeaddacdd609209cf56152d9c1517842 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Mon, 20 Jul 2026 17:18:03 -0400 Subject: [PATCH 04/53] Add singleton function --- src/Data/Queue/Base.agda | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Data/Queue/Base.agda b/src/Data/Queue/Base.agda index 3770dc5a01..84277fca60 100644 --- a/src/Data/Queue/Base.agda +++ b/src/Data/Queue/Base.agda @@ -48,6 +48,10 @@ enqueue : Queue A → A → Queue A enqueue empty a = queue a [] [] enqueue (queue dq-hd dq-tail eq) a = queue dq-hd dq-tail (a ∷ eq) +-- Create a queue with a single element +singleton : A → Queue A +singleton = enqueue empty + dequeue : Queue A → Maybe (A × Queue A) dequeue empty = nothing dequeue (queue dq-hd [] eq) with reverse eq From 6a8bf86dede32cd1093d6878841b42c7a2da8772 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Tue, 21 Jul 2026 10:09:23 -0400 Subject: [PATCH 05/53] Fix imports --- src/Data/Queue/Base.agda | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/Data/Queue/Base.agda b/src/Data/Queue/Base.agda index 3770dc5a01..1a93fb5985 100644 --- a/src/Data/Queue/Base.agda +++ b/src/Data/Queue/Base.agda @@ -9,14 +9,12 @@ module Data.Queue.Base where -open import Agda.Builtin.Equality open import Level using (Level) -open import Data.Bool +open import Data.Bool.Base using (Bool; true; false) open import Data.List.Base as List using (List; []; _∷_; reverse; _++_; length) open import Data.Maybe.Base using (Maybe; nothing; just) open import Data.Nat.Base using (ℕ; zero; suc; _+_) open import Data.Product using (_×_; _,_) -open import Function private variable @@ -37,7 +35,7 @@ private data Queue (A : Set l) : Set l where empty : Queue A - + -- dequeue-head → dequeue-list → enqueue-list queue : A → List A → List A → Queue A @@ -45,7 +43,7 @@ data Queue (A : Set l) : Set l where -- Construction & Destruction enqueue : Queue A → A → Queue A -enqueue empty a = queue a [] [] +enqueue empty a = queue a [] [] enqueue (queue dq-hd dq-tail eq) a = queue dq-hd dq-tail (a ∷ eq) dequeue : Queue A → Maybe (A × Queue A) From 9056b9503719bb24610eb9739a8e472c731609a6 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Tue, 21 Jul 2026 10:09:58 -0400 Subject: [PATCH 06/53] Rename l : Level -> a : Level --- src/Data/Queue/Base.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/Queue/Base.agda b/src/Data/Queue/Base.agda index 1a93fb5985..3eadba80a5 100644 --- a/src/Data/Queue/Base.agda +++ b/src/Data/Queue/Base.agda @@ -18,8 +18,8 @@ open import Data.Product using (_×_; _,_) private variable - l : Level - A B : Set l + a : Level + A B : Set a -- A Queue consists of a dequeue and enqueue list -- When enqueing (unless it is the first element), elements are cons'd @@ -33,7 +33,7 @@ private -- To enforce this, the head of the dequeue list is taken -- seperately and a constructor for an empty queue is given. -data Queue (A : Set l) : Set l where +data Queue (A : Set a) : Set a where empty : Queue A -- dequeue-head → dequeue-list → enqueue-list From 85e54c5e24781d58fb75465414b3028b77ed2c24 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Tue, 21 Jul 2026 10:10:36 -0400 Subject: [PATCH 07/53] Use two levels instead of one --- src/Data/Queue/Base.agda | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Data/Queue/Base.agda b/src/Data/Queue/Base.agda index 3eadba80a5..f45eaaa8a7 100644 --- a/src/Data/Queue/Base.agda +++ b/src/Data/Queue/Base.agda @@ -19,7 +19,9 @@ open import Data.Product using (_×_; _,_) private variable a : Level - A B : Set a + b : Level + A : Set a + B : Set b -- A Queue consists of a dequeue and enqueue list -- When enqueing (unless it is the first element), elements are cons'd From 95be562c1e58f04c762b8314906b7e86a2d54082 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Tue, 21 Jul 2026 11:17:17 -0400 Subject: [PATCH 08/53] Refactor Queue to use record definition --- src/Data/Queue/Base.agda | 64 ++++++++++++++++++++++++---------------- 1 file changed, 39 insertions(+), 25 deletions(-) diff --git a/src/Data/Queue/Base.agda b/src/Data/Queue/Base.agda index f45eaaa8a7..0f5f4eb01c 100644 --- a/src/Data/Queue/Base.agda +++ b/src/Data/Queue/Base.agda @@ -11,10 +11,14 @@ module Data.Queue.Base where open import Level using (Level) open import Data.Bool.Base using (Bool; true; false) +open import Data.Empty using (⊥-elim) open import Data.List.Base as List using (List; []; _∷_; reverse; _++_; 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 (ℕ; zero; suc; _+_) open import Data.Product using (_×_; _,_) +open import Function.Base using (id) +open import Relation.Nullary using (¬_) private variable @@ -23,7 +27,7 @@ private A : Set a B : Set b --- A Queue consists of a dequeue and enqueue list +-- A Queue consists of a fron (dequeue) and back (enqueue) list -- When enqueing (unless it is the first element), elements are cons'd -- to the enqueue list. -- @@ -32,43 +36,55 @@ private -- with the dequeue list. -- -- The dequeue-list should be empty iff the whole queue is empty. --- To enforce this, the head of the dequeue list is taken --- seperately and a constructor for an empty queue is given. -data Queue (A : Set a) : Set a where - empty : Queue A - - -- dequeue-head → dequeue-list → enqueue-list - queue : A → List A → List A → Queue A +record Queue (A : Set a) : Set a where + constructor mkQ + field + front : List A + back : List A + inv : Null front → Null back ------------------------------------------------------------------------ -- Construction & Destruction +-- TODO: use record syntax instead of constructor in enqueue and dequeue? + +empty : Queue A +empty = mkQ [] [] id + +-- NOTE: might not be needed. Could be inlined? Existing lemmas exist? +private + ¬Null : {a : A} {as : List A} → ¬ (Null (a ∷ as)) + ¬Null (() Data.List.Relation.Unary.All.∷ n) + + cons-Null : {a : A} {as bs : List A} → (Null (a ∷ as) → Null bs) → Null as → Null bs + cons-Null hyp [] = {!!} + +-- proofs seem somewhat ugly... +-- TODO: cleanup (before pushing!) enqueue : Queue A → A → Queue A -enqueue empty a = queue a [] [] -enqueue (queue dq-hd dq-tail eq) a = queue dq-hd dq-tail (a ∷ eq) +enqueue (mkQ [] back inv) x = mkQ (x ∷ []) back λ _ → inv [] +enqueue (mkQ (dq-hd ∷ dq-tl) back inv) x = mkQ (dq-hd ∷ dq-tl) (x ∷ back) λ n → ⊥-elim (¬Null n) dequeue : Queue A → Maybe (A × Queue A) -dequeue empty = nothing -dequeue (queue dq-hd [] eq) with reverse eq -... | [] = just (dq-hd , empty) -... | x ∷ req = just (dq-hd , queue x req []) -dequeue (queue dq-hd (x ∷ xs) eq) = just (dq-hd , (queue x xs eq)) +dequeue (mkQ [] [] inv) = nothing +dequeue (mkQ [] (x ∷ back) inv) = {!!} +dequeue (mkQ (x ∷ []) back inv) = just (x , mkQ (reverse back) [] λ _ → []) +dequeue (mkQ (x ∷ y ∷ front) back inv) = just (x , mkQ (y ∷ front) back (λ n → ⊥-elim (¬Null n))) ------------------------------------------------------------------------ --- Basic Functions isEmpty : Queue A → Bool -isEmpty empty = true +isEmpty (mkQ [] [] inv) = true isEmpty _ = false size : Queue A → ℕ -size empty = 0 -size (queue x xs ys) = 1 + length xs + length ys +size (mkQ front back inv) = (length front) + (length back) -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) +-- 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) ------------------------------------------------------------------------ --- Conversion to/from List @@ -77,12 +93,10 @@ map f (queue x xs ys) = queue (f x) (List.map f xs) (List.map f ys) -- becomes the head of the list (i.e. the first element of the queue -- becomes the last element of the list) toList : Queue A → List A -toList empty = [] -toList (queue dq-hd dq-tail eq) = dq-hd ∷ (dq-tail ++ (reverse eq)) +toList (mkQ front back inv) = front ++ (reverse back) -- Create a Queue from a List, such that the elements -- of the list would be dequeued starting from its first element -- (i.e. the first element of the list becomes the last element of the queue) fromList : List A → Queue A -fromList [] = empty -fromList (x ∷ xs) = queue x xs [] +fromList list = mkQ list [] (λ _ → []) From bebe5a2d99d28e54453eee2dc50d298b28385efc Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Tue, 21 Jul 2026 12:32:48 -0400 Subject: [PATCH 09/53] Refactor Queue to use record definition --- src/Data/Queue/Base.agda | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/Data/Queue/Base.agda b/src/Data/Queue/Base.agda index 0f5f4eb01c..daa93c6b81 100644 --- a/src/Data/Queue/Base.agda +++ b/src/Data/Queue/Base.agda @@ -57,9 +57,6 @@ private ¬Null : {a : A} {as : List A} → ¬ (Null (a ∷ as)) ¬Null (() Data.List.Relation.Unary.All.∷ n) - cons-Null : {a : A} {as bs : List A} → (Null (a ∷ as) → Null bs) → Null as → Null bs - cons-Null hyp [] = {!!} - -- proofs seem somewhat ugly... -- TODO: cleanup (before pushing!) enqueue : Queue A → A → Queue A @@ -68,7 +65,8 @@ enqueue (mkQ (dq-hd ∷ dq-tl) back inv) x = mkQ (dq-hd ∷ dq-tl) (x ∷ back) dequeue : Queue A → Maybe (A × Queue A) dequeue (mkQ [] [] inv) = nothing -dequeue (mkQ [] (x ∷ back) inv) = {!!} +-- shouldn't be possible? +dequeue (mkQ [] (x ∷ back) inv) = nothing dequeue (mkQ (x ∷ []) back inv) = just (x , mkQ (reverse back) [] λ _ → []) dequeue (mkQ (x ∷ y ∷ front) back inv) = just (x , mkQ (y ∷ front) back (λ n → ⊥-elim (¬Null n))) From 9ef66fbc9464f057f4b615b7f9063cc6cda2c1cf Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Tue, 21 Jul 2026 12:34:49 -0400 Subject: [PATCH 10/53] Cleanup --- src/Data/Queue/Base.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Data/Queue/Base.agda b/src/Data/Queue/Base.agda index daa93c6b81..26d31bb502 100644 --- a/src/Data/Queue/Base.agda +++ b/src/Data/Queue/Base.agda @@ -22,8 +22,7 @@ open import Relation.Nullary using (¬_) private variable - a : Level - b : Level + a b : Level A : Set a B : Set b From a0b0353601216b72cbd3c88e7837a4c545ea4762 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Tue, 21 Jul 2026 13:03:54 -0400 Subject: [PATCH 11/53] Add properties file --- src/Data/Queue/Properties.agda | 48 ++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) create mode 100644 src/Data/Queue/Properties.agda diff --git a/src/Data/Queue/Properties.agda b/src/Data/Queue/Properties.agda new file mode 100644 index 0000000000..61e1a62296 --- /dev/null +++ b/src/Data/Queue/Properties.agda @@ -0,0 +1,48 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Queue-related properties +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Data.Queue.Properties where + +open import Level using (Level) +open import Data.List.Base +open import Data.List.Properties using (++-identityʳ) +open import Data.List.Relation.Unary.All using (Null; []) +open import Data.Queue.Base using (toList; fromList; empty; mkQ) +open import Relation.Binary.PropositionalEquality.Core as ≡ +open import Relation.Binary.PropositionalEquality.Properties as ≡ + +open ≡-Reasoning + +private + variable + a b : Level + A : Set a + B : Set b + +toList-fromList : {xs : List A} → toList (fromList xs) ≡ xs +toList-fromList {a} {A} {[]} = + begin + toList (fromList []) + ≡⟨⟩ + toList (empty) + ≡⟨⟩ + [] + ∎ + +toList-fromList {a} {A} {x ∷ xs} = + begin + toList (fromList (x ∷ xs)) + ≡⟨⟩ + toList (mkQ (x ∷ xs) [] (λ _ → [])) + ≡⟨⟩ + (x ∷ xs) ++ (reverse []) + ≡⟨⟩ + (x ∷ xs) ++ [] + ≡⟨ ++-identityʳ (x ∷ xs) ⟩ + (x ∷ xs) + ∎ From 253edac288dc343d63e51a3db7f6c525dbd742c4 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Tue, 21 Jul 2026 15:13:19 -0400 Subject: [PATCH 12/53] Use record syntax in dequeue and enqueue --- src/Data/Queue/Base.agda | 39 ++++++++++++++++++++++++++++----------- 1 file changed, 28 insertions(+), 11 deletions(-) diff --git a/src/Data/Queue/Base.agda b/src/Data/Queue/Base.agda index 26d31bb502..185f77c47c 100644 --- a/src/Data/Queue/Base.agda +++ b/src/Data/Queue/Base.agda @@ -5,7 +5,11 @@ ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} --- Queues implemented with the usual two-list method +-- 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 +-- ammortized O(1) when the structure is used non-persistently. module Data.Queue.Base where @@ -17,6 +21,7 @@ open import Data.List.Relation.Unary.All using (Null; []) open import Data.Maybe.Base using (Maybe; nothing; just) open import Data.Nat.Base using (ℕ; zero; suc; _+_) open import Data.Product using (_×_; _,_) +open import Data.SnocList.Base using (List<; toList>) open import Function.Base using (id) open import Relation.Nullary using (¬_) @@ -46,8 +51,6 @@ record Queue (A : Set a) : Set a where ------------------------------------------------------------------------ -- Construction & Destruction --- TODO: use record syntax instead of constructor in enqueue and dequeue? - empty : Queue A empty = mkQ [] [] id @@ -56,18 +59,32 @@ private ¬Null : {a : A} {as : List A} → ¬ (Null (a ∷ as)) ¬Null (() Data.List.Relation.Unary.All.∷ n) --- proofs seem somewhat ugly... --- TODO: cleanup (before pushing!) enqueue : Queue A → A → Queue A -enqueue (mkQ [] back inv) x = mkQ (x ∷ []) back λ _ → inv [] -enqueue (mkQ (dq-hd ∷ dq-tl) back inv) x = mkQ (dq-hd ∷ dq-tl) (x ∷ back) λ n → ⊥-elim (¬Null n) +enqueue (mkQ [] back inv) x = record + { front = (x ∷ []) + ; back = back + ; inv = (λ _ → inv []) + } +enqueue (mkQ (dq-hd ∷ dq-tl) back inv) x = record + { front = (dq-hd ∷ dq-tl) + ; back = (x ∷ back) + ; inv = λ n → ⊥-elim (¬Null n) + } dequeue : Queue A → Maybe (A × Queue A) dequeue (mkQ [] [] inv) = nothing -- shouldn't be possible? dequeue (mkQ [] (x ∷ back) inv) = nothing -dequeue (mkQ (x ∷ []) back inv) = just (x , mkQ (reverse back) [] λ _ → []) -dequeue (mkQ (x ∷ y ∷ front) back inv) = just (x , mkQ (y ∷ front) back (λ n → ⊥-elim (¬Null n))) +dequeue (mkQ (x ∷ []) back inv) = just (x , record + { front = reverse back + ; back = [] + ; inv = λ _ → [] + }) +dequeue (mkQ (x ∷ y ∷ front) back inv) = just (x , record + { front = y ∷ front + ; back = back + ; inv = λ n → ⊥-elim (¬Null n) + }) ------------------------------------------------------------------------ --- Basic Functions @@ -77,7 +94,7 @@ isEmpty (mkQ [] [] inv) = true isEmpty _ = false size : Queue A → ℕ -size (mkQ front back inv) = (length front) + (length back) +size q = (length (Queue.front q)) + (length (Queue.back q)) -- map : (A → B) → Queue A → Queue B -- map f empty = empty @@ -90,7 +107,7 @@ size (mkQ front back inv) = (length front) + (length back) -- becomes the head of the list (i.e. the first element of the queue -- becomes the last element of the list) toList : Queue A → List A -toList (mkQ front back inv) = front ++ (reverse back) +toList q = Queue.front q ++ (reverse (Queue.back q)) -- Create a Queue from a List, such that the elements -- of the list would be dequeued starting from its first element From 100d5db579f008d31557797704d20801708185dc Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Tue, 21 Jul 2026 15:14:46 -0400 Subject: [PATCH 13/53] Fix comment --- src/Data/Queue/Base.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Queue/Base.agda b/src/Data/Queue/Base.agda index 185f77c47c..291658ef6c 100644 --- a/src/Data/Queue/Base.agda +++ b/src/Data/Queue/Base.agda @@ -31,7 +31,7 @@ private A : Set a B : Set b --- A Queue consists of a fron (dequeue) and back (enqueue) list +-- 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. -- From e3f88727484da1a035ac85de7c23f339f8a57178 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams <58709355+silas-hw@users.noreply.github.com> Date: Wed, 22 Jul 2026 11:18:02 -0400 Subject: [PATCH 14/53] Fix typo in 'amortized' Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- src/Data/Queue/Base.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Queue/Base.agda b/src/Data/Queue/Base.agda index 291658ef6c..22ecd1ae74 100644 --- a/src/Data/Queue/Base.agda +++ b/src/Data/Queue/Base.agda @@ -9,7 +9,7 @@ -- "Purely Functional Data Structures", Chris Okasaki, 1996 -- -- Note that the weaker invariant is used here that only guarantees --- ammortized O(1) when the structure is used non-persistently. +-- amortized O(1) when the structure is used non-persistently. module Data.Queue.Base where From 48b6afd047c82ede31e1a7ffb6792a68a1dc4cd9 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams <58709355+silas-hw@users.noreply.github.com> Date: Wed, 22 Jul 2026 11:23:07 -0400 Subject: [PATCH 15/53] Use as-pattern in enqueue Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- src/Data/Queue/Base.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Queue/Base.agda b/src/Data/Queue/Base.agda index 22ecd1ae74..b0afe3420b 100644 --- a/src/Data/Queue/Base.agda +++ b/src/Data/Queue/Base.agda @@ -65,8 +65,8 @@ enqueue (mkQ [] back inv) x = record ; back = back ; inv = (λ _ → inv []) } -enqueue (mkQ (dq-hd ∷ dq-tl) back inv) x = record - { front = (dq-hd ∷ dq-tl) +enqueue (mkQ front@(_ ∷ _) back _) x = record + { front = front ; back = (x ∷ back) ; inv = λ n → ⊥-elim (¬Null n) } From 0bf49e7723289f307992b0170660763aedfa3abd Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Wed, 22 Jul 2026 11:30:46 -0400 Subject: [PATCH 16/53] =?UTF-8?q?Use=20=E2=8A=A5-elim=20on=20impossible=20?= =?UTF-8?q?dequeue=20case?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Queue/Base.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Data/Queue/Base.agda b/src/Data/Queue/Base.agda index 17019ac629..790fb80e35 100644 --- a/src/Data/Queue/Base.agda +++ b/src/Data/Queue/Base.agda @@ -77,8 +77,7 @@ singleton = enqueue empty dequeue : Queue A → Maybe (A × Queue A) dequeue (mkQ [] [] inv) = nothing --- shouldn't be possible? -dequeue (mkQ [] (x ∷ back) inv) = nothing +dequeue (mkQ [] (x ∷ back) inv) = ⊥-elim (¬Null (inv [])) dequeue (mkQ (x ∷ []) back inv) = just (x , record { front = reverse back ; back = [] From 0561f1000ab55dd3ad7806099a66e7a4037e277c Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Wed, 22 Jul 2026 11:37:40 -0400 Subject: [PATCH 17/53] Update argument order for enqueue --- src/Data/Queue/Base.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Data/Queue/Base.agda b/src/Data/Queue/Base.agda index 790fb80e35..c071ff7e38 100644 --- a/src/Data/Queue/Base.agda +++ b/src/Data/Queue/Base.agda @@ -59,13 +59,13 @@ private ¬Null : {a : A} {as : List A} → ¬ (Null (a ∷ as)) ¬Null (() Data.List.Relation.Unary.All.∷ n) -enqueue : Queue A → A → Queue A -enqueue (mkQ [] back inv) x = record +enqueue : A → Queue A → Queue A +enqueue x (mkQ [] back inv) = record { front = (x ∷ []) ; back = back ; inv = (λ _ → inv []) } -enqueue (mkQ front@(_ ∷ _) back _) x = record +enqueue x (mkQ front@(_ ∷ _) back _) = record { front = front ; back = (x ∷ back) ; inv = λ n → ⊥-elim (¬Null n) @@ -73,7 +73,7 @@ enqueue (mkQ front@(_ ∷ _) back _) x = record -- Create a queue with a single element singleton : A → Queue A -singleton = enqueue empty +singleton x = enqueue x empty dequeue : Queue A → Maybe (A × Queue A) dequeue (mkQ [] [] inv) = nothing From 1c1d2c6b220eb7c0f885613f2a1f67ce62679cae Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Wed, 22 Jul 2026 12:03:10 -0400 Subject: [PATCH 18/53] Add proof that enqueue increases size by 1 --- src/Data/Queue/Properties.agda | 27 ++++++++++++++++++++++++++- 1 file changed, 26 insertions(+), 1 deletion(-) diff --git a/src/Data/Queue/Properties.agda b/src/Data/Queue/Properties.agda index 61e1a62296..5ae4b9a8a5 100644 --- a/src/Data/Queue/Properties.agda +++ b/src/Data/Queue/Properties.agda @@ -9,12 +9,17 @@ module Data.Queue.Properties where open import Level using (Level) +open import Data.Empty using (⊥-elim) open import Data.List.Base open import Data.List.Properties using (++-identityʳ) open import Data.List.Relation.Unary.All using (Null; []) -open import Data.Queue.Base using (toList; fromList; empty; mkQ) +open import Data.Nat.Base using (suc; _+_) +open import Data.Nat.Properties using (+-comm; +-suc) +open import Data.Queue.Base open import Relation.Binary.PropositionalEquality.Core as ≡ open import Relation.Binary.PropositionalEquality.Properties as ≡ +open import Relation.Nullary using (¬_) + open ≡-Reasoning @@ -24,6 +29,10 @@ private A : Set a B : Set b + ¬Null : {a : A} {as : List A} → ¬ (Null (a ∷ as)) + ¬Null (() Data.List.Relation.Unary.All.∷ n) + + toList-fromList : {xs : List A} → toList (fromList xs) ≡ xs toList-fromList {a} {A} {[]} = begin @@ -46,3 +55,19 @@ toList-fromList {a} {A} {x ∷ xs} = ≡⟨ ++-identityʳ (x ∷ xs) ⟩ (x ∷ xs) ∎ + +-- enqueue increases size by 1 +enqueueSuc : (a : A) (q : Queue A) → (size (enqueue a q)) ≡ (suc (size q)) +enqueueSuc a (mkQ [] back inv) = refl +enqueueSuc a (mkQ (x ∷ front) back inv) = + begin + size (enqueue a (mkQ (x ∷ front) back inv)) + ≡⟨⟩ + size (mkQ (x ∷ front) (a ∷ back) (λ n → ⊥-elim (¬Null n))) + ≡⟨⟩ + length (x ∷ front) + length (a ∷ back) + ≡⟨⟩ + length (x ∷ front) + suc (length back) + ≡⟨ +-suc (length (x ∷ front)) (length back)⟩ + suc (length (x ∷ front) + length back) + ∎ From 55792de66b0569d1c6a0539c12c836d1caacb1fc Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Wed, 22 Jul 2026 12:19:03 -0400 Subject: [PATCH 19/53] Fix whitespaace --- src/Data/Queue/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Queue/Properties.agda b/src/Data/Queue/Properties.agda index 5ae4b9a8a5..fcf7d3fd90 100644 --- a/src/Data/Queue/Properties.agda +++ b/src/Data/Queue/Properties.agda @@ -68,6 +68,6 @@ enqueueSuc a (mkQ (x ∷ front) back inv) = length (x ∷ front) + length (a ∷ back) ≡⟨⟩ length (x ∷ front) + suc (length back) - ≡⟨ +-suc (length (x ∷ front)) (length back)⟩ + ≡⟨ +-suc (length (x ∷ front)) (length back) ⟩ suc (length (x ∷ front) + length back) ∎ From 7e7edabea4f0bc15cde44c96d3d91022c3ae20c5 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Wed, 22 Jul 2026 13:57:35 -0400 Subject: [PATCH 20/53] Fix whitespace --- src/Data/Queue/Properties.agda | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/Data/Queue/Properties.agda b/src/Data/Queue/Properties.agda index fcf7d3fd90..aa5a98d9f2 100644 --- a/src/Data/Queue/Properties.agda +++ b/src/Data/Queue/Properties.agda @@ -20,7 +20,6 @@ open import Relation.Binary.PropositionalEquality.Core as ≡ open import Relation.Binary.PropositionalEquality.Properties as ≡ open import Relation.Nullary using (¬_) - open ≡-Reasoning private @@ -32,7 +31,6 @@ private ¬Null : {a : A} {as : List A} → ¬ (Null (a ∷ as)) ¬Null (() Data.List.Relation.Unary.All.∷ n) - toList-fromList : {xs : List A} → toList (fromList xs) ≡ xs toList-fromList {a} {A} {[]} = begin @@ -55,7 +53,7 @@ toList-fromList {a} {A} {x ∷ xs} = ≡⟨ ++-identityʳ (x ∷ xs) ⟩ (x ∷ xs) ∎ - + -- enqueue increases size by 1 enqueueSuc : (a : A) (q : Queue A) → (size (enqueue a q)) ≡ (suc (size q)) enqueueSuc a (mkQ [] back inv) = refl From 98104281e44c34c7c91983657d7835594177d548 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Wed, 22 Jul 2026 15:40:36 -0400 Subject: [PATCH 21/53] Reformat equaltiy proofs to abide by style guide --- src/Data/Queue/Properties.agda | 50 ++++++++++++---------------------- 1 file changed, 17 insertions(+), 33 deletions(-) diff --git a/src/Data/Queue/Properties.agda b/src/Data/Queue/Properties.agda index aa5a98d9f2..7aba275c8a 100644 --- a/src/Data/Queue/Properties.agda +++ b/src/Data/Queue/Properties.agda @@ -32,40 +32,24 @@ private ¬Null (() Data.List.Relation.Unary.All.∷ n) toList-fromList : {xs : List A} → toList (fromList xs) ≡ xs -toList-fromList {a} {A} {[]} = - begin - toList (fromList []) - ≡⟨⟩ - toList (empty) - ≡⟨⟩ - [] - ∎ - -toList-fromList {a} {A} {x ∷ xs} = - begin - toList (fromList (x ∷ xs)) - ≡⟨⟩ - toList (mkQ (x ∷ xs) [] (λ _ → [])) - ≡⟨⟩ - (x ∷ xs) ++ (reverse []) - ≡⟨⟩ - (x ∷ xs) ++ [] - ≡⟨ ++-identityʳ (x ∷ xs) ⟩ - (x ∷ xs) - ∎ +toList-fromList {a} {A} {[]} = begin + toList (fromList []) ≡⟨⟩ + toList (empty) ≡⟨⟩ + [] ∎ + +toList-fromList {a} {A} {x ∷ xs} = begin + toList (fromList (x ∷ xs)) ≡⟨⟩ + toList (mkQ (x ∷ xs) [] (λ _ → [])) ≡⟨⟩ + (x ∷ xs) ++ (reverse []) ≡⟨⟩ + (x ∷ xs) ++ [] ≡⟨ ++-identityʳ (x ∷ xs) ⟩ + (x ∷ xs) ∎ -- enqueue increases size by 1 enqueueSuc : (a : A) (q : Queue A) → (size (enqueue a q)) ≡ (suc (size q)) enqueueSuc a (mkQ [] back inv) = refl -enqueueSuc a (mkQ (x ∷ front) back inv) = - begin - size (enqueue a (mkQ (x ∷ front) back inv)) - ≡⟨⟩ - size (mkQ (x ∷ front) (a ∷ back) (λ n → ⊥-elim (¬Null n))) - ≡⟨⟩ - length (x ∷ front) + length (a ∷ back) - ≡⟨⟩ - length (x ∷ front) + suc (length back) - ≡⟨ +-suc (length (x ∷ front)) (length back) ⟩ - suc (length (x ∷ front) + length back) - ∎ +enqueueSuc a (mkQ (x ∷ front) back inv) = begin + size (enqueue a (mkQ (x ∷ front) back inv)) ≡⟨⟩ + size (mkQ (x ∷ front) (a ∷ back) (λ n → ⊥-elim (¬Null n))) ≡⟨⟩ + length (x ∷ front) + length (a ∷ back) ≡⟨⟩ + length (x ∷ front) + suc (length back) ≡⟨ +-suc (length (x ∷ front)) (length back) ⟩ + suc (length (x ∷ front) + length back) ∎ From bedd0dffd7e27a895c4f09e24ff24ee0c9c5ffb8 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Thu, 23 Jul 2026 11:03:40 -0400 Subject: [PATCH 22/53] Move TwoList Queue into its own module to allow for different implementations --- src/Data/Queue.agda | 2 +- src/Data/Queue/{ => TwoList}/Base.agda | 2 +- src/Data/Queue/{ => TwoList}/Properties.agda | 6 +++--- 3 files changed, 5 insertions(+), 5 deletions(-) rename src/Data/Queue/{ => TwoList}/Base.agda (99%) rename src/Data/Queue/{ => TwoList}/Properties.agda (96%) diff --git a/src/Data/Queue.agda b/src/Data/Queue.agda index 24bb668186..cd50200bbc 100644 --- a/src/Data/Queue.agda +++ b/src/Data/Queue.agda @@ -8,4 +8,4 @@ module Data.Queue where -open import Data.Queue.Base public +open import Data.Queue.TwoList.Base public diff --git a/src/Data/Queue/Base.agda b/src/Data/Queue/TwoList/Base.agda similarity index 99% rename from src/Data/Queue/Base.agda rename to src/Data/Queue/TwoList/Base.agda index c071ff7e38..e2425632ca 100644 --- a/src/Data/Queue/Base.agda +++ b/src/Data/Queue/TwoList/Base.agda @@ -11,7 +11,7 @@ -- Note that the weaker invariant is used here that only guarantees -- amortized O(1) when the structure is used non-persistently. -module Data.Queue.Base where +module Data.Queue.TwoList.Base where open import Level using (Level) open import Data.Bool.Base using (Bool; true; false) diff --git a/src/Data/Queue/Properties.agda b/src/Data/Queue/TwoList/Properties.agda similarity index 96% rename from src/Data/Queue/Properties.agda rename to src/Data/Queue/TwoList/Properties.agda index 7aba275c8a..7e1d6b4b1c 100644 --- a/src/Data/Queue/Properties.agda +++ b/src/Data/Queue/TwoList/Properties.agda @@ -6,7 +6,7 @@ {-# OPTIONS --without-K --safe #-} -module Data.Queue.Properties where +module Data.Queue.TwoList.Properties where open import Level using (Level) open import Data.Empty using (⊥-elim) @@ -15,7 +15,7 @@ open import Data.List.Properties using (++-identityʳ) open import Data.List.Relation.Unary.All using (Null; []) open import Data.Nat.Base using (suc; _+_) open import Data.Nat.Properties using (+-comm; +-suc) -open import Data.Queue.Base +open import Data.Queue.TwoList.Base open import Relation.Binary.PropositionalEquality.Core as ≡ open import Relation.Binary.PropositionalEquality.Properties as ≡ open import Relation.Nullary using (¬_) @@ -43,7 +43,7 @@ toList-fromList {a} {A} {x ∷ xs} = begin (x ∷ xs) ++ (reverse []) ≡⟨⟩ (x ∷ xs) ++ [] ≡⟨ ++-identityʳ (x ∷ xs) ⟩ (x ∷ xs) ∎ - + -- enqueue increases size by 1 enqueueSuc : (a : A) (q : Queue A) → (size (enqueue a q)) ≡ (suc (size q)) enqueueSuc a (mkQ [] back inv) = refl From 79b5d6c4d9bda65ebb5208528ae3456325181cc7 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Thu, 23 Jul 2026 11:05:18 -0400 Subject: [PATCH 23/53] Remove unneeded parens --- src/Data/Queue/TwoList/Base.agda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Data/Queue/TwoList/Base.agda b/src/Data/Queue/TwoList/Base.agda index e2425632ca..1ed1d2e074 100644 --- a/src/Data/Queue/TwoList/Base.agda +++ b/src/Data/Queue/TwoList/Base.agda @@ -61,13 +61,13 @@ private enqueue : A → Queue A → Queue A enqueue x (mkQ [] back inv) = record - { front = (x ∷ []) + { front = x ∷ [] ; back = back - ; inv = (λ _ → inv []) + ; inv = λ _ → inv [] } enqueue x (mkQ front@(_ ∷ _) back _) = record { front = front - ; back = (x ∷ back) + ; back = x ∷ back ; inv = λ n → ⊥-elim (¬Null n) } @@ -97,7 +97,7 @@ isEmpty (mkQ [] [] inv) = true isEmpty _ = false size : Queue A → ℕ -size q = (length (Queue.front q)) + (length (Queue.back q)) +size q = length (Queue.front q) + length (Queue.back q) -- map : (A → B) → Queue A → Queue B -- map f empty = empty @@ -116,4 +116,4 @@ toList q = Queue.front q ++ (reverse (Queue.back q)) -- of the list would be dequeued starting from its first element -- (i.e. the first element of the list becomes the last element of the queue) fromList : List A → Queue A -fromList list = mkQ list [] (λ _ → []) +fromList list = mkQ list [] λ _ → [] From 5b36b007654654668303c11fbb5c4f1f18c74e94 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Thu, 23 Jul 2026 11:06:40 -0400 Subject: [PATCH 24/53] Cleanup isEmpty --- src/Data/Queue/TwoList/Base.agda | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Data/Queue/TwoList/Base.agda b/src/Data/Queue/TwoList/Base.agda index 1ed1d2e074..531376b586 100644 --- a/src/Data/Queue/TwoList/Base.agda +++ b/src/Data/Queue/TwoList/Base.agda @@ -16,7 +16,7 @@ module Data.Queue.TwoList.Base where open import Level using (Level) open import Data.Bool.Base using (Bool; true; false) open import Data.Empty using (⊥-elim) -open import Data.List.Base as List using (List; []; _∷_; reverse; _++_; length) +open import Data.List.Base as List using (List; []; _∷_; reverse; _++_; length; null) open import Data.List.Relation.Unary.All using (Null; []) open import Data.Maybe.Base using (Maybe; nothing; just) open import Data.Nat.Base using (ℕ; zero; suc; _+_) @@ -93,8 +93,7 @@ dequeue (mkQ (x ∷ y ∷ front) back inv) = just (x , record --- Basic Functions isEmpty : Queue A → Bool -isEmpty (mkQ [] [] inv) = true -isEmpty _ = false +isEmpty (mkQ front back inv) = null front size : Queue A → ℕ size q = length (Queue.front q) + length (Queue.back q) From 7de85c2bbbf3b7c6e303beaec54a79a972ddc6b7 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Thu, 23 Jul 2026 11:07:51 -0400 Subject: [PATCH 25/53] Rename 'list' to 'xs' in fromList --- src/Data/Queue/TwoList/Base.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Queue/TwoList/Base.agda b/src/Data/Queue/TwoList/Base.agda index 531376b586..9a38dfa70e 100644 --- a/src/Data/Queue/TwoList/Base.agda +++ b/src/Data/Queue/TwoList/Base.agda @@ -115,4 +115,4 @@ toList q = Queue.front q ++ (reverse (Queue.back q)) -- of the list would be dequeued starting from its first element -- (i.e. the first element of the list becomes the last element of the queue) fromList : List A → Queue A -fromList list = mkQ list [] λ _ → [] +fromList xs = mkQ xs [] λ _ → [] From 1c56ada0b153aa1576bdd4f13df60a651a5dbe09 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Thu, 23 Jul 2026 11:09:17 -0400 Subject: [PATCH 26/53] Make xs explicit in toList-fromList --- src/Data/Queue/TwoList/Properties.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/Queue/TwoList/Properties.agda b/src/Data/Queue/TwoList/Properties.agda index 7e1d6b4b1c..db338fbbd8 100644 --- a/src/Data/Queue/TwoList/Properties.agda +++ b/src/Data/Queue/TwoList/Properties.agda @@ -31,13 +31,13 @@ private ¬Null : {a : A} {as : List A} → ¬ (Null (a ∷ as)) ¬Null (() Data.List.Relation.Unary.All.∷ n) -toList-fromList : {xs : List A} → toList (fromList xs) ≡ xs -toList-fromList {a} {A} {[]} = begin +toList-fromList : (xs : List A) → toList (fromList xs) ≡ xs +toList-fromList [] = begin toList (fromList []) ≡⟨⟩ toList (empty) ≡⟨⟩ [] ∎ -toList-fromList {a} {A} {x ∷ xs} = begin +toList-fromList (x ∷ xs) = begin toList (fromList (x ∷ xs)) ≡⟨⟩ toList (mkQ (x ∷ xs) [] (λ _ → [])) ≡⟨⟩ (x ∷ xs) ++ (reverse []) ≡⟨⟩ From 5cacded75cc4f9fade081f2a8e3b7e99f4c7a3a0 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Thu, 23 Jul 2026 11:13:04 -0400 Subject: [PATCH 27/53] Use As-pattern in toList-fromList --- src/Data/Queue/TwoList/Properties.agda | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Data/Queue/TwoList/Properties.agda b/src/Data/Queue/TwoList/Properties.agda index db338fbbd8..dff5821875 100644 --- a/src/Data/Queue/TwoList/Properties.agda +++ b/src/Data/Queue/TwoList/Properties.agda @@ -37,12 +37,12 @@ toList-fromList [] = begin toList (empty) ≡⟨⟩ [] ∎ -toList-fromList (x ∷ xs) = begin - toList (fromList (x ∷ xs)) ≡⟨⟩ - toList (mkQ (x ∷ xs) [] (λ _ → [])) ≡⟨⟩ - (x ∷ xs) ++ (reverse []) ≡⟨⟩ - (x ∷ xs) ++ [] ≡⟨ ++-identityʳ (x ∷ xs) ⟩ - (x ∷ xs) ∎ +toList-fromList xs@(_ ∷ _) = begin + toList (fromList xs) ≡⟨⟩ + toList (mkQ xs [] (λ _ → [])) ≡⟨⟩ + xs ++ (reverse []) ≡⟨⟩ + xs ++ [] ≡⟨ ++-identityʳ xs ⟩ + xs ∎ -- enqueue increases size by 1 enqueueSuc : (a : A) (q : Queue A) → (size (enqueue a q)) ≡ (suc (size q)) From a3c6edac5609b1ba22d4de214fe477090ef055be Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Thu, 23 Jul 2026 11:13:52 -0400 Subject: [PATCH 28/53] Rename enqueueSuc to size-enqueue --- src/Data/Queue/TwoList/Properties.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/Queue/TwoList/Properties.agda b/src/Data/Queue/TwoList/Properties.agda index dff5821875..558f96c2e1 100644 --- a/src/Data/Queue/TwoList/Properties.agda +++ b/src/Data/Queue/TwoList/Properties.agda @@ -45,9 +45,9 @@ toList-fromList xs@(_ ∷ _) = begin xs ∎ -- enqueue increases size by 1 -enqueueSuc : (a : A) (q : Queue A) → (size (enqueue a q)) ≡ (suc (size q)) -enqueueSuc a (mkQ [] back inv) = refl -enqueueSuc a (mkQ (x ∷ front) back inv) = begin +size-enqueue : (a : A) (q : Queue A) → (size (enqueue a q)) ≡ (suc (size q)) +size-enqueue a (mkQ [] back inv) = refl +size-enqueue a (mkQ (x ∷ front) back inv) = begin size (enqueue a (mkQ (x ∷ front) back inv)) ≡⟨⟩ size (mkQ (x ∷ front) (a ∷ back) (λ n → ⊥-elim (¬Null n))) ≡⟨⟩ length (x ∷ front) + length (a ∷ back) ≡⟨⟩ From c3b93fb5c7f018c33349e3da2219fba3a57593ec Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Thu, 23 Jul 2026 12:25:17 -0400 Subject: [PATCH 29/53] Add start of QueueSpec --- src/Data/Queue/QueueSpec.agda | 33 ++++++++++++++++++++++++++++++++ src/Data/Queue/TwoList/Base.agda | 15 +++++++++++++++ 2 files changed, 48 insertions(+) create mode 100644 src/Data/Queue/QueueSpec.agda diff --git a/src/Data/Queue/QueueSpec.agda b/src/Data/Queue/QueueSpec.agda new file mode 100644 index 0000000000..e1957cc16f --- /dev/null +++ b/src/Data/Queue/QueueSpec.agda @@ -0,0 +1,33 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Queue specification +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Data.Queue.QueueSpec where + +open import Data.List.Base using (List) +open import Data.Maybe.Base using (Maybe; nothing; just) +open import Data.Nat.Base using (ℕ) +open import Data.Product using (_×_; _,_) +open import Level using (Level) + +private + variable + a b : Level + A : Set a + B : Set b + +-- Along these lines? +record IsQueue (Queue : (Set a) → (Set a)) : (Set (Level.suc a)) where + field + enqueue : A → Queue A → Queue A + dequeue : Queue A → Maybe (A × Queue A) + + empty : Queue A + size : Queue A → ℕ + + toList : Queue A → List A + fromList : List A → Queue A diff --git a/src/Data/Queue/TwoList/Base.agda b/src/Data/Queue/TwoList/Base.agda index 9a38dfa70e..b34bf076db 100644 --- a/src/Data/Queue/TwoList/Base.agda +++ b/src/Data/Queue/TwoList/Base.agda @@ -21,6 +21,7 @@ open import Data.List.Relation.Unary.All using (Null; []) open import Data.Maybe.Base using (Maybe; nothing; just) open import Data.Nat.Base using (ℕ; zero; suc; _+_) open import Data.Product using (_×_; _,_) +open import Data.Queue.QueueSpec using (IsQueue) open import Data.SnocList.Base using (List<; toList>) open import Function.Base using (id) open import Relation.Nullary using (¬_) @@ -116,3 +117,17 @@ toList q = Queue.front q ++ (reverse (Queue.back q)) -- (i.e. the first element of the list becomes the last element of the queue) fromList : List A → Queue A fromList xs = mkQ xs [] λ _ → [] + +------------------------------------------------------------------------ +--- TwoList Queue is a Queue + +instance + TwoListQueueIsQueue : IsQueue {a} Queue + TwoListQueueIsQueue = record + { enqueue = enqueue + ; dequeue = dequeue + ; empty = empty + ; size = size + ; toList = toList + ; fromList = fromList + } From 3c614005338911cd6ccf1493f27862c3e6747d66 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Fri, 24 Jul 2026 10:23:40 -0400 Subject: [PATCH 30/53] Add size-empty lemma --- src/Data/Queue/TwoList/Properties.agda | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/Data/Queue/TwoList/Properties.agda b/src/Data/Queue/TwoList/Properties.agda index 558f96c2e1..abdf0d268c 100644 --- a/src/Data/Queue/TwoList/Properties.agda +++ b/src/Data/Queue/TwoList/Properties.agda @@ -52,4 +52,9 @@ size-enqueue a (mkQ (x ∷ front) back inv) = begin size (mkQ (x ∷ front) (a ∷ back) (λ n → ⊥-elim (¬Null n))) ≡⟨⟩ length (x ∷ front) + length (a ∷ back) ≡⟨⟩ length (x ∷ front) + suc (length back) ≡⟨ +-suc (length (x ∷ front)) (length back) ⟩ - suc (length (x ∷ front) + length back) ∎ + suc (length (x ∷ front) + length back) ∎ + +-- trivial, but ensures empty works correctly +size-empty : size (empty {a} {A}) ≡ 0 +size-empty = refl + From a2d5854387678793f60cf4025d9369a9650f5d9d Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Fri, 24 Jul 2026 11:13:02 -0400 Subject: [PATCH 31/53] Add smart constructor --- src/Data/Queue/TwoList/Base.agda | 59 ++++++++++++-------------- src/Data/Queue/TwoList/Properties.agda | 26 +++++++++++- 2 files changed, 50 insertions(+), 35 deletions(-) diff --git a/src/Data/Queue/TwoList/Base.agda b/src/Data/Queue/TwoList/Base.agda index b34bf076db..e538a3c85f 100644 --- a/src/Data/Queue/TwoList/Base.agda +++ b/src/Data/Queue/TwoList/Base.agda @@ -23,7 +23,7 @@ open import Data.Nat.Base using (ℕ; zero; suc; _+_) open import Data.Product using (_×_; _,_) open import Data.Queue.QueueSpec using (IsQueue) open import Data.SnocList.Base using (List<; toList>) -open import Function.Base using (id) +open import Function.Base using (id; const) open import Relation.Nullary using (¬_) private @@ -32,6 +32,16 @@ private A : Set a B : Set b + ¬Null : {a : A} {as : List A} → ¬ (Null (a ∷ as)) + ¬Null (() Data.List.Relation.Unary.All.∷ n) + + null-[] : ∀ {xs : List A} → Null xs → Null {A = A} [] + null-[] = const [] + + -- mckinna seems to have a better idea but currently doesnt type check + null-∷ : ∀ {x} {xs ys : List A} → Null (x ∷ xs) → Null ys + null-∷ = λ x₁ → ⊥-elim (¬Null x₁) + -- 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. @@ -52,49 +62,32 @@ record Queue (A : Set a) : Set a where ------------------------------------------------------------------------ -- Construction & Destruction -empty : Queue A -empty = mkQ [] [] id +queue : List A → List A → Queue A +queue [] ys = mkQ (reverse ys) [] null-[] +queue xs@(_ ∷ _) ys = mkQ xs ys null-∷ --- NOTE: might not be needed. Could be inlined? Existing lemmas exist? -private - ¬Null : {a : A} {as : List A} → ¬ (Null (a ∷ as)) - ¬Null (() Data.List.Relation.Unary.All.∷ n) +empty : Queue A +empty = queue [] [] enqueue : A → Queue A → Queue A -enqueue x (mkQ [] back inv) = record - { front = x ∷ [] - ; back = back - ; inv = λ _ → inv [] - } -enqueue x (mkQ front@(_ ∷ _) back _) = record - { front = front - ; back = x ∷ back - ; inv = λ n → ⊥-elim (¬Null n) - } +enqueue x q with bs ← Queue.back q | Queue.front q +... | [] = queue (x ∷ []) [] +... | front@(_ ∷ _) = queue front (x ∷ bs) + +dequeue : Queue A → Maybe (A × Queue A) +dequeue q with Queue.front q +... | [] = nothing +... | x ∷ xs = just (x , queue xs (Queue.back q)) -- Create a queue with a single element singleton : A → Queue A singleton x = enqueue x empty -dequeue : Queue A → Maybe (A × Queue A) -dequeue (mkQ [] [] inv) = nothing -dequeue (mkQ [] (x ∷ back) inv) = ⊥-elim (¬Null (inv [])) -dequeue (mkQ (x ∷ []) back inv) = just (x , record - { front = reverse back - ; back = [] - ; inv = λ _ → [] - }) -dequeue (mkQ (x ∷ y ∷ front) back inv) = just (x , record - { front = y ∷ front - ; back = back - ; inv = λ n → ⊥-elim (¬Null n) - }) - ------------------------------------------------------------------------ --- Basic Functions isEmpty : Queue A → Bool -isEmpty (mkQ front back inv) = null front +isEmpty q = null (Queue.front q) size : Queue A → ℕ size q = length (Queue.front q) + length (Queue.back q) @@ -116,7 +109,7 @@ toList q = Queue.front q ++ (reverse (Queue.back q)) -- of the list would be dequeued starting from its first element -- (i.e. the first element of the list becomes the last element of the queue) fromList : List A → Queue A -fromList xs = mkQ xs [] λ _ → [] +fromList xs = queue xs [] ------------------------------------------------------------------------ --- TwoList Queue is a Queue diff --git a/src/Data/Queue/TwoList/Properties.agda b/src/Data/Queue/TwoList/Properties.agda index abdf0d268c..3a363f17f3 100644 --- a/src/Data/Queue/TwoList/Properties.agda +++ b/src/Data/Queue/TwoList/Properties.agda @@ -45,8 +45,30 @@ toList-fromList xs@(_ ∷ _) = begin xs ∎ -- enqueue increases size by 1 -size-enqueue : (a : A) (q : Queue A) → (size (enqueue a q)) ≡ (suc (size q)) -size-enqueue a (mkQ [] back inv) = refl +-- feels uneccesarily complex for the empty front case? +-- rewrite could make it cleaner, but are we trying to use that less? +size-enqueue : (x : A) (q : Queue A) → (size (enqueue x q)) ≡ (suc (size q)) +size-enqueue {A = A} x q@(mkQ [] back inv) = begin + size (enqueue x (mkQ [] back inv)) ≡⟨⟩ + size (queue (x ∷ []) []) ≡⟨⟩ + suc 0 ≡⟨ cong suc (sym sizeq) ⟩ + suc (size q) ∎ + where + null[] : Null back → back ≡ [] + null[] [] = refl + + back[] : back ≡ [] + back[] = null[] (inv []) + + sizeq : size q ≡ 0 + sizeq = begin + size q ≡⟨⟩ + length {A = A} [] + length back ≡⟨⟩ + 0 + length back ≡⟨⟩ + length back ≡⟨ cong length back[] ⟩ + length {A = A} [] ≡⟨⟩ + 0 ∎ + size-enqueue a (mkQ (x ∷ front) back inv) = begin size (enqueue a (mkQ (x ∷ front) back inv)) ≡⟨⟩ size (mkQ (x ∷ front) (a ∷ back) (λ n → ⊥-elim (¬Null n))) ≡⟨⟩ From 4ae85fc59144e88001125cdddcdcc5960b8cdbe4 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 26 Jul 2026 12:36:28 +0100 Subject: [PATCH 32/53] fix: `whitespace` for `Data.Queue.TwoList.Properties` --- src/Data/Queue/TwoList/Properties.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Queue/TwoList/Properties.agda b/src/Data/Queue/TwoList/Properties.agda index 3a363f17f3..01d4e7403e 100644 --- a/src/Data/Queue/TwoList/Properties.agda +++ b/src/Data/Queue/TwoList/Properties.agda @@ -56,7 +56,7 @@ size-enqueue {A = A} x q@(mkQ [] back inv) = begin where null[] : Null back → back ≡ [] null[] [] = refl - + back[] : back ≡ [] back[] = null[] (inv []) @@ -68,7 +68,7 @@ size-enqueue {A = A} x q@(mkQ [] back inv) = begin length back ≡⟨ cong length back[] ⟩ length {A = A} [] ≡⟨⟩ 0 ∎ - + size-enqueue a (mkQ (x ∷ front) back inv) = begin size (enqueue a (mkQ (x ∷ front) back inv)) ≡⟨⟩ size (mkQ (x ∷ front) (a ∷ back) (λ n → ⊥-elim (¬Null n))) ≡⟨⟩ From 257a08b068d194d24c351e70885c2887b785c909 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams <58709355+silas-hw@users.noreply.github.com> Date: Mon, 27 Jul 2026 13:05:15 -0400 Subject: [PATCH 33/53] Update src/Data/Queue/QueueSpec.agda Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- src/Data/Queue/QueueSpec.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Queue/QueueSpec.agda b/src/Data/Queue/QueueSpec.agda index e1957cc16f..eb57936072 100644 --- a/src/Data/Queue/QueueSpec.agda +++ b/src/Data/Queue/QueueSpec.agda @@ -21,7 +21,7 @@ private B : Set b -- Along these lines? -record IsQueue (Queue : (Set a) → (Set a)) : (Set (Level.suc a)) where +record IsQueue (Queue : Set a → Set a) : Set (suc a) where field enqueue : A → Queue A → Queue A dequeue : Queue A → Maybe (A × Queue A) From 612c74389f4f1c2f496a07f0a1d350c600722ed2 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams <58709355+silas-hw@users.noreply.github.com> Date: Mon, 27 Jul 2026 13:05:55 -0400 Subject: [PATCH 34/53] Update src/Data/Queue/QueueSpec.agda Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- src/Data/Queue/QueueSpec.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Queue/QueueSpec.agda b/src/Data/Queue/QueueSpec.agda index eb57936072..931237593c 100644 --- a/src/Data/Queue/QueueSpec.agda +++ b/src/Data/Queue/QueueSpec.agda @@ -12,7 +12,7 @@ open import Data.List.Base using (List) open import Data.Maybe.Base using (Maybe; nothing; just) open import Data.Nat.Base using (ℕ) open import Data.Product using (_×_; _,_) -open import Level using (Level) +open import Level using (Level; suc) private variable From e0b83ddd7e9c5ff9c2cf8d3dbee75f2704990c6b Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Mon, 27 Jul 2026 13:15:32 -0400 Subject: [PATCH 35/53] Improve null-:: --- src/Data/Queue/TwoList/Base.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/Queue/TwoList/Base.agda b/src/Data/Queue/TwoList/Base.agda index e538a3c85f..ec1d22a42e 100644 --- a/src/Data/Queue/TwoList/Base.agda +++ b/src/Data/Queue/TwoList/Base.agda @@ -17,7 +17,7 @@ open import Level using (Level) open import Data.Bool.Base using (Bool; true; false) open import Data.Empty using (⊥-elim) 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 using (Null; []; _∷_) open import Data.Maybe.Base using (Maybe; nothing; just) open import Data.Nat.Base using (ℕ; zero; suc; _+_) open import Data.Product using (_×_; _,_) @@ -38,9 +38,8 @@ private null-[] : ∀ {xs : List A} → Null xs → Null {A = A} [] null-[] = const [] - -- mckinna seems to have a better idea but currently doesnt type check null-∷ : ∀ {x} {xs ys : List A} → Null (x ∷ xs) → Null ys - null-∷ = λ x₁ → ⊥-elim (¬Null x₁) + null-∷ (()∷ _) -- A Queue consists of a front (dequeue) and back (enqueue) list -- When enqueing (unless it is the first element), elements are cons'd @@ -86,6 +85,7 @@ singleton x = enqueue x empty ------------------------------------------------------------------------ --- Basic Functions +-- empty? : Dec (Null f isEmpty : Queue A → Bool isEmpty q = null (Queue.front q) From a071100e0f44588214b74a0f0fd70e093b4b4a0b Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Mon, 27 Jul 2026 16:55:19 -0400 Subject: [PATCH 36/53] Add RawQueue interface and bundle into IsQueue --- src/Data/Queue/QueueSpec.agda | 60 ++++++++++++++++++++++++++------ src/Data/Queue/TwoList/Base.agda | 60 +++++++++++++++++++------------- 2 files changed, 84 insertions(+), 36 deletions(-) diff --git a/src/Data/Queue/QueueSpec.agda b/src/Data/Queue/QueueSpec.agda index 931237593c..0e03bb050b 100644 --- a/src/Data/Queue/QueueSpec.agda +++ b/src/Data/Queue/QueueSpec.agda @@ -8,11 +8,17 @@ module Data.Queue.QueueSpec where -open import Data.List.Base using (List) +open import Data.Bool.Base using (Bool) +open import Data.List.Base as List using (List; []; length) open import Data.Maybe.Base using (Maybe; nothing; just) open import Data.Nat.Base using (ℕ) -open import Data.Product using (_×_; _,_) -open import Level using (Level; suc) +open import Data.Product.Base using (_×_) +open import Function.Base using (_∘_) +open import Level +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.PropositionalEquality.Core using (_≡_) +open import Relation.Nullary.Decidable.Core using (yes; no; isYes; False) +open import Relation.Unary using (Pred; Decidable) private variable @@ -20,14 +26,46 @@ private A : Set a B : Set b --- Along these lines? -record IsQueue (Queue : Set a → Set a) : Set (suc a) where +-- 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 - enqueue : A → Queue A → Queue A - dequeue : Queue A → Maybe (A × Queue A) + _≈_ : ∀ {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)}} → A × Q A + + empty : Q A + empty = fromList [] + + pure : A → Q A + pure = fromList ∘ List.[_] + + toℕ : Q A → ℕ + toℕ = length ∘ toList + + to𝔹 : Q A → Bool + to𝔹 = isYes ∘ empty? - empty : Queue A - size : Queue A → ℕ + dequeue′ : Q A → Maybe (A × Q A) + dequeue′ q with empty? q in eq + ... | yes _ = nothing + ... | no _ = just (dequeue q) + where instance + _ : False (empty? q) + _ rewrite eq = _ - toList : Queue A → List A - fromList : List A → Queue A +-- IsQueue bundles RawQueue with proofs of a Queues correctness, +-- such as enqueue adding 1 to the Queue's size +record IsQueue {Q : Set a → Set a} (rawQ : RawQueue Q) : Set (suc a) where + + open RawQueue rawQ + + field + empty-toList : toList (empty {A = A}) ≡ [] + fromList-empty : empty {A = A} ≈ fromList [] diff --git a/src/Data/Queue/TwoList/Base.agda b/src/Data/Queue/TwoList/Base.agda index ec1d22a42e..fc18b60755 100644 --- a/src/Data/Queue/TwoList/Base.agda +++ b/src/Data/Queue/TwoList/Base.agda @@ -18,13 +18,17 @@ open import Data.Bool.Base using (Bool; true; false) open import Data.Empty using (⊥-elim) 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 (_×_; _,_) -open import Data.Queue.QueueSpec using (IsQueue) +open import Data.Queue.QueueSpec using (RawQueue; IsQueue) open import Data.SnocList.Base using (List<; toList>) open import Function.Base using (id; const) open import Relation.Nullary using (¬_) +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 @@ -58,6 +62,23 @@ record Queue (A : Set a) : Set a where back : List A inv : Null front → Null back +------------------------------------------------------------------------ +--- Basic Functions + +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 = null front +empty? (mkQ [] back inv) .Relation.Nullary.proof = ofʸ [] +empty? (mkQ (x ∷ xs) back inv) .Relation.Nullary.proof = ofⁿ λ empty → ⊥-elim (¬Null empty) + +isEmpty : Queue A → Bool +isEmpty q = null (Queue.front q) + +size : Queue A → ℕ +size q = length (Queue.front q) + length (Queue.back q) + ------------------------------------------------------------------------ -- Construction & Destruction @@ -73,25 +94,14 @@ enqueue x q with bs ← Queue.back q | Queue.front q ... | [] = queue (x ∷ []) [] ... | front@(_ ∷ _) = queue front (x ∷ bs) -dequeue : Queue A → Maybe (A × Queue A) -dequeue q with Queue.front q -... | [] = nothing -... | x ∷ xs = just (x , queue xs (Queue.back q)) +dequeue : ∀ (q : Queue A) .{{_ : False (empty? q)}} → A × Queue A +-- dequeue q with (x ∷ xs) ← (Queue.front q) = x , queue xs (Queue.back q) +dequeue (mkQ (x ∷ xs) back inv) = x , (queue xs back) -- Create a queue with a single element singleton : A → Queue A singleton x = enqueue x empty ------------------------------------------------------------------------- ---- Basic Functions - --- empty? : Dec (Null f -isEmpty : Queue A → Bool -isEmpty q = null (Queue.front q) - -size : Queue A → ℕ -size q = length (Queue.front q) + length (Queue.back q) - -- 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) @@ -114,13 +124,13 @@ fromList xs = queue xs [] ------------------------------------------------------------------------ --- TwoList Queue is a Queue -instance - TwoListQueueIsQueue : IsQueue {a} Queue - TwoListQueueIsQueue = record - { enqueue = enqueue - ; dequeue = dequeue - ; empty = empty - ; size = size - ; toList = toList - ; fromList = fromList - } +TwoList-RawQueue : RawQueue {a} Queue +TwoList-RawQueue = record + { _≈_ = {!!} + ; Empty = Empty + ; empty? = empty? + ; fromList = fromList + ; toList = toList + ; enqueue = enqueue + ; dequeue = dequeue + } From 379375ae205f493f4858e977aac09555f8943a0a Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Mon, 27 Jul 2026 17:05:35 -0400 Subject: [PATCH 37/53] Cleanup code --- src/Data/Queue/TwoList/Base.agda | 41 ++++++++++++++++++-------------- 1 file changed, 23 insertions(+), 18 deletions(-) diff --git a/src/Data/Queue/TwoList/Base.agda b/src/Data/Queue/TwoList/Base.agda index fc18b60755..66beddfa87 100644 --- a/src/Data/Queue/TwoList/Base.agda +++ b/src/Data/Queue/TwoList/Base.agda @@ -24,7 +24,7 @@ open import Data.Nat.Base using (ℕ; zero; suc; _+_) open import Data.Product using (_×_; _,_) open import Data.Queue.QueueSpec using (RawQueue; IsQueue) open import Data.SnocList.Base using (List<; toList>) -open import Function.Base using (id; const) +open import Function.Base using (id; const; _∘_) open import Relation.Nullary using (¬_) open import Relation.Nullary.Decidable.Core using (yes; no; isYes; False) open import Relation.Nullary.Reflects using (ofʸ; ofⁿ) @@ -80,14 +80,33 @@ size : Queue A → ℕ size q = length (Queue.front q) + length (Queue.back q) ------------------------------------------------------------------------ --- Construction & Destruction +--- Smart Constructor queue : List A → List A → Queue A queue [] ys = mkQ (reverse ys) [] null-[] queue xs@(_ ∷ _) ys = mkQ xs ys null-∷ +------------------------------------------------------------------------ +--- Conversion to/from List + +-- Create a List from a Queue, such that the first that would be dequeued +-- becomes the head of the list (i.e. the first element of the queue +-- becomes the last element of the list) +toList : Queue A → List A +toList q = Queue.front q ++ (reverse (Queue.back q)) + +-- Create a Queue from a List, such that the elements +-- of the list would be dequeued starting from its first element +-- (i.e. the first element of the list becomes the last element of the queue) +fromList : List A → Queue A +fromList xs = queue xs [] + + +------------------------------------------------------------------------ +-- Construction & Destruction + empty : Queue A -empty = queue [] [] +empty = fromList [] enqueue : A → Queue A → Queue A enqueue x q with bs ← Queue.back q | Queue.front q @@ -100,26 +119,12 @@ dequeue (mkQ (x ∷ xs) back inv) = x , (queue xs back) -- Create a queue with a single element singleton : A → Queue A -singleton x = enqueue x empty +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) ------------------------------------------------------------------------- ---- Conversion to/from List - --- Create a List from a Queue, such that the first that would be dequeued --- becomes the head of the list (i.e. the first element of the queue --- becomes the last element of the list) -toList : Queue A → List A -toList q = Queue.front q ++ (reverse (Queue.back q)) - --- Create a Queue from a List, such that the elements --- of the list would be dequeued starting from its first element --- (i.e. the first element of the list becomes the last element of the queue) -fromList : List A → Queue A -fromList xs = queue xs [] ------------------------------------------------------------------------ --- TwoList Queue is a Queue From d724dfb7d34cb22db23160dbff88d514b367a2f3 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Mon, 27 Jul 2026 18:05:59 -0400 Subject: [PATCH 38/53] Define equality relation on TwoList queues --- src/Data/Queue/QueueSpec.agda | 6 +++--- src/Data/Queue/TwoList/Base.agda | 24 +++++++++++++++++------- 2 files changed, 20 insertions(+), 10 deletions(-) diff --git a/src/Data/Queue/QueueSpec.agda b/src/Data/Queue/QueueSpec.agda index 0e03bb050b..696d100656 100644 --- a/src/Data/Queue/QueueSpec.agda +++ b/src/Data/Queue/QueueSpec.agda @@ -17,7 +17,7 @@ open import Function.Base using (_∘_) open import Level open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality.Core using (_≡_) -open import Relation.Nullary.Decidable.Core using (yes; no; isYes; False) +open import Relation.Nullary.Decidable.Core using (yes; no; isYes; False; does) open import Relation.Unary using (Pred; Decidable) private @@ -32,14 +32,14 @@ private record RawQueue (Q : Set a → Set a) : Set (suc a) where field - _≈_ : ∀ {A : Set a} → Rel (Q A) a + _≈_ : ∀ {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)}} → A × Q A - + empty : Q A empty = fromList [] diff --git a/src/Data/Queue/TwoList/Base.agda b/src/Data/Queue/TwoList/Base.agda index 66beddfa87..46d8f7d0a7 100644 --- a/src/Data/Queue/TwoList/Base.agda +++ b/src/Data/Queue/TwoList/Base.agda @@ -21,10 +21,12 @@ 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 (_×_; _,_) +open import Data.Product using (_×_; _,_; proj₂) open import Data.Queue.QueueSpec using (RawQueue; IsQueue) open import Data.SnocList.Base using (List<; toList>) +open import Data.Unit.Base using (⊤) open import Function.Base using (id; const; _∘_) +open import Relation.Binary.Core using (Rel) open import Relation.Nullary using (¬_) open import Relation.Nullary.Decidable.Core using (yes; no; isYes; False) open import Relation.Nullary.Reflects using (ofʸ; ofⁿ) @@ -63,7 +65,7 @@ record Queue (A : Set a) : Set a where inv : Null front → Null back ------------------------------------------------------------------------ ---- Basic Functions +--- Basic Functions/Relations/Operators Empty : ∀ {A : Set a} → Pred (Queue A) a Empty {a} {A} q = Null (Queue.front q) @@ -76,9 +78,6 @@ empty? (mkQ (x ∷ xs) back inv) .Relation.Nullary.proof = ofⁿ λ empty → isEmpty : Queue A → Bool isEmpty q = null (Queue.front q) -size : Queue A → ℕ -size q = length (Queue.front q) + length (Queue.back q) - ------------------------------------------------------------------------ --- Smart Constructor @@ -101,7 +100,6 @@ toList q = Queue.front q ++ (reverse (Queue.back q)) fromList : List A → Queue A fromList xs = queue xs [] - ------------------------------------------------------------------------ -- Construction & Destruction @@ -125,13 +123,25 @@ singleton = fromList ∘ List.[_] -- map f empty = empty -- map f (queue x xs ys) = queue (f x) (List.map f xs) (List.map f ys) +------------------------------------------------------------------------ +--- Relations + +-- NOTE: experimental. Still not entirely sure the best way to define this +data _≈_ {A : Set a} : Queue A → Queue A → Set a where + empty-equal : ∀ {q q' : Queue A} → Empty q → Empty q' → q ≈ q' + enqueue-equal : ∀ {q q' : Queue A} {x : A} → q ≈ q' → (enqueue x q) ≈ (enqueue x q') + dequeue-equal : ∀ {q q' : Queue A} → + .{{_ : False (empty? q)}} → + .{{_ : False (empty? q')}} → + q ≈ q' → + (proj₂ (dequeue q)) ≈ (proj₂ (dequeue q')) ------------------------------------------------------------------------ --- TwoList Queue is a Queue TwoList-RawQueue : RawQueue {a} Queue TwoList-RawQueue = record - { _≈_ = {!!} + { _≈_ = _≈_ ; Empty = Empty ; empty? = empty? ; fromList = fromList From 41e76dd840d0663c35405867961be7274a26a3c8 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Mon, 27 Jul 2026 19:01:14 -0400 Subject: [PATCH 39/53] Add approx relation --- src/Data/Queue/Properties.agda | 28 ++++++++++++++++++++++++++++ src/Data/Queue/QueueSpec.agda | 2 +- src/Data/Queue/TwoList/Base.agda | 20 ++++++++------------ 3 files changed, 37 insertions(+), 13 deletions(-) create mode 100644 src/Data/Queue/Properties.agda diff --git a/src/Data/Queue/Properties.agda b/src/Data/Queue/Properties.agda new file mode 100644 index 0000000000..dc0d85a4f4 --- /dev/null +++ b/src/Data/Queue/Properties.agda @@ -0,0 +1,28 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of Queues, regardless of implementation +------------------------------------------------------------------------ + +module Data.Queue.Properties where + +open import Data.Queue.QueueSpec using (RawQueue) +open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong) +open import Relation.Binary.Structures using (IsEquivalence) +open import Level using (Level; suc) + +open RawQueue + +private + variable + a b : Level + A : Set a + B : Set b + +≈-refl : ∀ {Q : Set a → Set a} {RQ : RawQueue Q} {q : Q A} → (RQ ≈ q) q +≈-refl {_} {A} {Q} {RQ} {q} = {!q!} + + + + + diff --git a/src/Data/Queue/QueueSpec.agda b/src/Data/Queue/QueueSpec.agda index 696d100656..70270e3f2b 100644 --- a/src/Data/Queue/QueueSpec.agda +++ b/src/Data/Queue/QueueSpec.agda @@ -32,7 +32,7 @@ private record RawQueue (Q : Set a → Set a) : Set (suc a) where field - _≈_ : ∀ {A : Set a} → Rel (Q A) a + _≈_ : ∀ {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 diff --git a/src/Data/Queue/TwoList/Base.agda b/src/Data/Queue/TwoList/Base.agda index 46d8f7d0a7..41c9de481f 100644 --- a/src/Data/Queue/TwoList/Base.agda +++ b/src/Data/Queue/TwoList/Base.agda @@ -26,6 +26,7 @@ open import Data.Queue.QueueSpec using (RawQueue; IsQueue) open import Data.SnocList.Base using (List<; toList>) 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.Decidable.Core using (yes; no; isYes; False) @@ -124,24 +125,19 @@ singleton = fromList ∘ List.[_] -- map f (queue x xs ys) = queue (f x) (List.map f xs) (List.map f ys) ------------------------------------------------------------------------ ---- Relations - --- NOTE: experimental. Still not entirely sure the best way to define this -data _≈_ {A : Set a} : Queue A → Queue A → Set a where - empty-equal : ∀ {q q' : Queue A} → Empty q → Empty q' → q ≈ q' - enqueue-equal : ∀ {q q' : Queue A} {x : A} → q ≈ q' → (enqueue x q) ≈ (enqueue x q') - dequeue-equal : ∀ {q q' : Queue A} → - .{{_ : False (empty? q)}} → - .{{_ : False (empty? q')}} → - q ≈ q' → - (proj₂ (dequeue q)) ≈ (proj₂ (dequeue q')) +-- 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') ------------------------------------------------------------------------ --- TwoList Queue is a Queue TwoList-RawQueue : RawQueue {a} Queue TwoList-RawQueue = record - { _≈_ = _≈_ + { _≈_ = _≈_ ; Empty = Empty ; empty? = empty? ; fromList = fromList From c2246b4b6c42b4bf39a390f6b8c67ce36288fa1f Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Mon, 27 Jul 2026 19:02:00 -0400 Subject: [PATCH 40/53] Remove stale file --- src/Data/Queue/Properties.agda | 28 ---------------------------- 1 file changed, 28 deletions(-) delete mode 100644 src/Data/Queue/Properties.agda diff --git a/src/Data/Queue/Properties.agda b/src/Data/Queue/Properties.agda deleted file mode 100644 index dc0d85a4f4..0000000000 --- a/src/Data/Queue/Properties.agda +++ /dev/null @@ -1,28 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- Properties of Queues, regardless of implementation ------------------------------------------------------------------------- - -module Data.Queue.Properties where - -open import Data.Queue.QueueSpec using (RawQueue) -open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong) -open import Relation.Binary.Structures using (IsEquivalence) -open import Level using (Level; suc) - -open RawQueue - -private - variable - a b : Level - A : Set a - B : Set b - -≈-refl : ∀ {Q : Set a → Set a} {RQ : RawQueue Q} {q : Q A} → (RQ ≈ q) q -≈-refl {_} {A} {Q} {RQ} {q} = {!q!} - - - - - From e8ff3b821848a8921f17dbb5da4f62b6ee72ac47 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Mon, 27 Jul 2026 19:03:40 -0400 Subject: [PATCH 41/53] Fix whitespace --- src/Data/Queue/QueueSpec.agda | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Data/Queue/QueueSpec.agda b/src/Data/Queue/QueueSpec.agda index 70270e3f2b..86c371e46c 100644 --- a/src/Data/Queue/QueueSpec.agda +++ b/src/Data/Queue/QueueSpec.agda @@ -62,6 +62,7 @@ record RawQueue (Q : Set a → Set a) : Set (suc a) where -- 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 From e2cc2c8a716556d21b5f7883afa94278dd0b0f54 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams <58709355+silas-hw@users.noreply.github.com> Date: Tue, 28 Jul 2026 09:27:32 -0400 Subject: [PATCH 42/53] Cleanup dequeue on TwoList Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- src/Data/Queue/TwoList/Base.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Queue/TwoList/Base.agda b/src/Data/Queue/TwoList/Base.agda index 41c9de481f..bc42dbf81f 100644 --- a/src/Data/Queue/TwoList/Base.agda +++ b/src/Data/Queue/TwoList/Base.agda @@ -114,7 +114,7 @@ enqueue x q with bs ← Queue.back q | Queue.front q dequeue : ∀ (q : Queue A) .{{_ : False (empty? q)}} → A × Queue A -- dequeue q with (x ∷ xs) ← (Queue.front q) = x , queue xs (Queue.back q) -dequeue (mkQ (x ∷ xs) back inv) = x , (queue xs back) +dequeue (mkQ (x ∷ xs) back _) = x , queue xs back -- Create a queue with a single element singleton : A → Queue A From e7901933fab475c39961dc26cbe447102f096db7 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Tue, 28 Jul 2026 10:04:38 -0400 Subject: [PATCH 43/53] Add properties to IsQueue --- src/Data/Queue/QueueSpec.agda | 22 +++++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/src/Data/Queue/QueueSpec.agda b/src/Data/Queue/QueueSpec.agda index 86c371e46c..6b67f82e46 100644 --- a/src/Data/Queue/QueueSpec.agda +++ b/src/Data/Queue/QueueSpec.agda @@ -9,13 +9,16 @@ 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.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 (_×_) +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.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) @@ -68,5 +71,14 @@ record IsQueue {Q : Set a → Set a} (rawQ : RawQueue Q) : Set (suc a) where open RawQueue rawQ field - empty-toList : toList (empty {A = A}) ≡ [] - fromList-empty : empty {A = A} ≈ fromList [] + 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) ≡ toList q List.∷ʳ x + -- 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) ≡ (proj₁ xr) ∷ (toList (proj₂ xr)) From 6a717da91a60a05af010616f1bbd51551ff6db77 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Tue, 28 Jul 2026 13:05:50 -0400 Subject: [PATCH 44/53] Fix Properties to use new definitions in QueueSpec --- src/Data/Queue/QueueSpec.agda | 4 +- src/Data/Queue/TwoList/Base.agda | 21 ++++++----- src/Data/Queue/TwoList/Properties.agda | 51 +++++++++++++++----------- 3 files changed, 43 insertions(+), 33 deletions(-) diff --git a/src/Data/Queue/QueueSpec.agda b/src/Data/Queue/QueueSpec.agda index 6b67f82e46..2c403a6f8b 100644 --- a/src/Data/Queue/QueueSpec.agda +++ b/src/Data/Queue/QueueSpec.agda @@ -49,8 +49,8 @@ record RawQueue (Q : Set a → Set a) : Set (suc a) where pure : A → Q A pure = fromList ∘ List.[_] - toℕ : Q A → ℕ - toℕ = length ∘ toList + size : Q A → ℕ + size = length ∘ toList to𝔹 : Q A → Bool to𝔹 = isYes ∘ empty? diff --git a/src/Data/Queue/TwoList/Base.agda b/src/Data/Queue/TwoList/Base.agda index bc42dbf81f..0061b35dd4 100644 --- a/src/Data/Queue/TwoList/Base.agda +++ b/src/Data/Queue/TwoList/Base.agda @@ -135,13 +135,14 @@ q ≈ q' = (toList q) ≡ (toList q') ------------------------------------------------------------------------ --- TwoList Queue is a Queue -TwoList-RawQueue : RawQueue {a} Queue -TwoList-RawQueue = record - { _≈_ = _≈_ - ; Empty = Empty - ; empty? = empty? - ; fromList = fromList - ; toList = toList - ; enqueue = enqueue - ; dequeue = dequeue - } +instance + TwoList-RawQueue : RawQueue {a} Queue + TwoList-RawQueue = record + { _≈_ = _≈_ + ; Empty = Empty + ; empty? = empty? + ; fromList = fromList + ; toList = toList + ; enqueue = enqueue + ; dequeue = dequeue + } diff --git a/src/Data/Queue/TwoList/Properties.agda b/src/Data/Queue/TwoList/Properties.agda index 01d4e7403e..82532cff04 100644 --- a/src/Data/Queue/TwoList/Properties.agda +++ b/src/Data/Queue/TwoList/Properties.agda @@ -11,16 +11,19 @@ module Data.Queue.TwoList.Properties where open import Level using (Level) open import Data.Empty using (⊥-elim) open import Data.List.Base -open import Data.List.Properties using (++-identityʳ) +open import Data.List.Properties using (++-identityʳ; length-++; length-reverse) open import Data.List.Relation.Unary.All using (Null; []) open import Data.Nat.Base using (suc; _+_) open import Data.Nat.Properties using (+-comm; +-suc) +open import Data.Queue.QueueSpec using (RawQueue; IsQueue) open import Data.Queue.TwoList.Base +open import Function.Base using (_∘_) open import Relation.Binary.PropositionalEquality.Core as ≡ open import Relation.Binary.PropositionalEquality.Properties as ≡ open import Relation.Nullary using (¬_) open ≡-Reasoning +open RawQueue {{...}} using (size) private variable @@ -45,14 +48,13 @@ toList-fromList xs@(_ ∷ _) = begin xs ∎ -- enqueue increases size by 1 --- feels uneccesarily complex for the empty front case? -- rewrite could make it cleaner, but are we trying to use that less? -size-enqueue : (x : A) (q : Queue A) → (size (enqueue x q)) ≡ (suc (size q)) -size-enqueue {A = A} x q@(mkQ [] back inv) = begin - size (enqueue x (mkQ [] back inv)) ≡⟨⟩ - size (queue (x ∷ []) []) ≡⟨⟩ - suc 0 ≡⟨ cong suc (sym sizeq) ⟩ - suc (size q) ∎ +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 @@ -60,21 +62,28 @@ size-enqueue {A = A} x q@(mkQ [] back inv) = begin back[] : back ≡ [] back[] = null[] (inv []) + -- why does length need {a} and {A} after reverse back ↦ reverse []? sizeq : size q ≡ 0 sizeq = begin - size q ≡⟨⟩ - length {A = A} [] + length back ≡⟨⟩ - 0 + length back ≡⟨⟩ - length back ≡⟨ cong length back[] ⟩ - length {A = A} [] ≡⟨⟩ - 0 ∎ - -size-enqueue a (mkQ (x ∷ front) back inv) = begin - size (enqueue a (mkQ (x ∷ front) back inv)) ≡⟨⟩ - size (mkQ (x ∷ front) (a ∷ back) (λ n → ⊥-elim (¬Null n))) ≡⟨⟩ - length (x ∷ front) + length (a ∷ back) ≡⟨⟩ - length (x ∷ front) + suc (length back) ≡⟨ +-suc (length (x ∷ front)) (length back) ⟩ - suc (length (x ∷ front) + length back) ∎ + size q ≡⟨⟩ + length (toList q) ≡⟨⟩ + length ([] ++ (reverse back)) ≡⟨⟩ + length (reverse back) ≡⟨ cong (length ∘ reverse) back[] ⟩ + length {a} {A} (reverse []) ≡⟨⟩ + length {a} {A} [] ≡⟨⟩ + 0 ∎ + +size-enqueue {A = A} x q@(mkQ front@(_ ∷ _) back inv) = begin + size (queue front (x ∷ back)) ≡⟨⟩ + length (front ++ (reverse ( x ∷ back))) ≡⟨ length-++ front ⟩ + length front + length (reverse (x ∷ back)) ≡⟨ cong (_+_ (length front)) (length-reverse (x ∷ back)) ⟩ + length front + length (x ∷ back) ≡⟨⟩ + length front + suc (length back) ≡⟨ cong ((_+_ (length front)) ∘ suc) (sym (length-reverse back)) ⟩ + length front + suc (length (reverse back)) ≡⟨ +-suc (length front) (length (reverse back)) ⟩ + suc (length front + length (reverse back)) ≡⟨ cong suc (sym (length-++ front {reverse (back)})) ⟩ + suc (length (front ++ (reverse back))) ≡⟨⟩ + suc (length (toList q)) ≡⟨⟩ + suc (size q) ∎ -- trivial, but ensures empty works correctly size-empty : size (empty {a} {A}) ≡ 0 From d1a9ea91e7a0624094df4e39c84d7b53e35f10fb Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Tue, 28 Jul 2026 16:40:37 -0400 Subject: [PATCH 45/53] =?UTF-8?q?Prove=20IsEquivalence=20of=20=E2=89=88?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Queue/TwoList/Properties.agda | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/Data/Queue/TwoList/Properties.agda b/src/Data/Queue/TwoList/Properties.agda index 82532cff04..79f598bb98 100644 --- a/src/Data/Queue/TwoList/Properties.agda +++ b/src/Data/Queue/TwoList/Properties.agda @@ -20,6 +20,8 @@ open import Data.Queue.TwoList.Base open import Function.Base using (_∘_) open import Relation.Binary.PropositionalEquality.Core as ≡ open import Relation.Binary.PropositionalEquality.Properties as ≡ +open import Relation.Binary.Definitions using (Reflexive) +open import Relation.Binary.Structures using (IsEquivalence) open import Relation.Nullary using (¬_) open ≡-Reasoning @@ -89,3 +91,13 @@ size-enqueue {A = A} x q@(mkQ front@(_ ∷ _) back inv) = begin 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 + } From 2ec3eaa976739a549dc14a2321b24835b6cc62eb Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 29 Jul 2026 10:19:35 +0100 Subject: [PATCH 46/53] fix: `whitespace` --- src/Data/Queue/TwoList/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Queue/TwoList/Properties.agda b/src/Data/Queue/TwoList/Properties.agda index 79f598bb98..2318eb43f1 100644 --- a/src/Data/Queue/TwoList/Properties.agda +++ b/src/Data/Queue/TwoList/Properties.agda @@ -74,7 +74,7 @@ size-enqueue {a = a} {A = A} x q@(mkQ [] back inv) = begin length {a} {A} (reverse []) ≡⟨⟩ length {a} {A} [] ≡⟨⟩ 0 ∎ - + size-enqueue {A = A} x q@(mkQ front@(_ ∷ _) back inv) = begin size (queue front (x ∷ back)) ≡⟨⟩ length (front ++ (reverse ( x ∷ back))) ≡⟨ length-++ front ⟩ From 99fc8f1846c9de262cf1e035dfdaba07b843bc6f Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Wed, 29 Jul 2026 09:40:32 -0400 Subject: [PATCH 47/53] Cleanup code --- src/Data/Queue/QueueSpec.agda | 2 +- src/Data/Queue/TwoList/Base.agda | 3 +-- src/Data/Queue/TwoList/Properties.agda | 18 +++++++++--------- 3 files changed, 11 insertions(+), 12 deletions(-) diff --git a/src/Data/Queue/QueueSpec.agda b/src/Data/Queue/QueueSpec.agda index 2c403a6f8b..507c1ce28b 100644 --- a/src/Data/Queue/QueueSpec.agda +++ b/src/Data/Queue/QueueSpec.agda @@ -81,4 +81,4 @@ record IsQueue {Q : Set a → Set a} (rawQ : RawQueue Q) : Set (suc a) where toList-enqueue : ∀ {q : Q A} {x : A} → toList (enqueue x q) ≡ toList q List.∷ʳ x -- 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) ≡ (proj₁ xr) ∷ (toList (proj₂ xr)) + let xr = dequeue q {{i}} in toList q ≡ proj₁ xr ∷ toList (proj₂ xr) diff --git a/src/Data/Queue/TwoList/Base.agda b/src/Data/Queue/TwoList/Base.agda index 0061b35dd4..a2caf3e978 100644 --- a/src/Data/Queue/TwoList/Base.agda +++ b/src/Data/Queue/TwoList/Base.agda @@ -93,7 +93,7 @@ queue xs@(_ ∷ _) ys = mkQ xs ys null-∷ -- becomes the head of the list (i.e. the first element of the queue -- becomes the last element of the list) toList : Queue A → List A -toList q = Queue.front q ++ (reverse (Queue.back q)) +toList q = Queue.front q ++ reverse (Queue.back q) -- Create a Queue from a List, such that the elements -- of the list would be dequeued starting from its first element @@ -113,7 +113,6 @@ enqueue x q with bs ← Queue.back q | Queue.front q ... | front@(_ ∷ _) = queue front (x ∷ bs) dequeue : ∀ (q : Queue A) .{{_ : False (empty? q)}} → A × Queue A --- dequeue q with (x ∷ xs) ← (Queue.front q) = x , queue xs (Queue.back q) dequeue (mkQ (x ∷ xs) back _) = x , queue xs back -- Create a queue with a single element diff --git a/src/Data/Queue/TwoList/Properties.agda b/src/Data/Queue/TwoList/Properties.agda index 2318eb43f1..65b7b5b183 100644 --- a/src/Data/Queue/TwoList/Properties.agda +++ b/src/Data/Queue/TwoList/Properties.agda @@ -33,10 +33,10 @@ private A : Set a B : Set b - ¬Null : {a : A} {as : List A} → ¬ (Null (a ∷ as)) + ¬Null : {a : A} {as : List A} → ¬ Null (a ∷ as) ¬Null (() Data.List.Relation.Unary.All.∷ n) -toList-fromList : (xs : List A) → toList (fromList xs) ≡ xs +toList-fromList : (xs : List A) → toList (fromList xs) ≡ xs toList-fromList [] = begin toList (fromList []) ≡⟨⟩ toList (empty) ≡⟨⟩ @@ -45,7 +45,7 @@ toList-fromList [] = begin toList-fromList xs@(_ ∷ _) = begin toList (fromList xs) ≡⟨⟩ toList (mkQ xs [] (λ _ → [])) ≡⟨⟩ - xs ++ (reverse []) ≡⟨⟩ + xs ++ reverse [] ≡⟨⟩ xs ++ [] ≡⟨ ++-identityʳ xs ⟩ xs ∎ @@ -54,9 +54,9 @@ toList-fromList xs@(_ ∷ _) = begin 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) ∎ + length (x ∷ []) ≡⟨⟩ + suc 0 ≡⟨ cong suc (sym sizeq) ⟩ + suc (size q) ∎ where null[] : Null back → back ≡ [] null[] [] = refl @@ -76,13 +76,13 @@ size-enqueue {a = a} {A = A} x q@(mkQ [] back inv) = begin 0 ∎ size-enqueue {A = A} x q@(mkQ front@(_ ∷ _) back inv) = begin - size (queue front (x ∷ back)) ≡⟨⟩ - length (front ++ (reverse ( x ∷ back))) ≡⟨ length-++ front ⟩ + size (queue front (x ∷ back)) ≡⟨⟩ + length (front ++ reverse (x ∷ back)) ≡⟨ length-++ front ⟩ length front + length (reverse (x ∷ back)) ≡⟨ cong (_+_ (length front)) (length-reverse (x ∷ back)) ⟩ length front + length (x ∷ back) ≡⟨⟩ length front + suc (length back) ≡⟨ cong ((_+_ (length front)) ∘ suc) (sym (length-reverse back)) ⟩ length front + suc (length (reverse back)) ≡⟨ +-suc (length front) (length (reverse back)) ⟩ - suc (length front + length (reverse back)) ≡⟨ cong suc (sym (length-++ front {reverse (back)})) ⟩ + suc (length front + length (reverse back)) ≡⟨ cong suc (sym (length-++ front {reverse back})) ⟩ suc (length (front ++ (reverse back))) ≡⟨⟩ suc (length (toList q)) ≡⟨⟩ suc (size q) ∎ From 6fe776f1f323a9ae733010f785151a45460e1cb5 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Wed, 29 Jul 2026 16:14:19 -0400 Subject: [PATCH 48/53] Add All< and Null< --- src/Data/SnocList/Relation/Unary/All.agda | 39 +++++++++++++++++++++++ 1 file changed, 39 insertions(+) create mode 100644 src/Data/SnocList/Relation/Unary/All.agda 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< ∅ From 0512a11c29a535390fe349b3e9372e10f6ffa154 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Wed, 29 Jul 2026 16:14:39 -0400 Subject: [PATCH 49/53] Update TwoList Queue to use SnocList --- src/Data/Queue/TwoList/Base.agda | 52 +++++++++------- src/Data/Queue/TwoList/Properties.agda | 86 +++++++++++++++----------- 2 files changed, 81 insertions(+), 57 deletions(-) diff --git a/src/Data/Queue/TwoList/Base.agda b/src/Data/Queue/TwoList/Base.agda index a2caf3e978..2855e41ee2 100644 --- a/src/Data/Queue/TwoList/Base.agda +++ b/src/Data/Queue/TwoList/Base.agda @@ -23,7 +23,8 @@ 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 using (List<; toList>) +open import Data.SnocList.Base as SnocList using (List<; toList>; fromList>; []; _<:_) +open import Data.SnocList.Relation.Unary.All open import Data.Unit.Base using (⊤) open import Function.Base using (id; const; _∘_) open import Relation.Binary.PropositionalEquality.Core using (_≡_) @@ -39,15 +40,24 @@ private A : Set a B : Set b - ¬Null : {a : A} {as : List A} → ¬ (Null (a ∷ as)) - ¬Null (() Data.List.Relation.Unary.All.∷ n) + ¬null : {a : A} {as : List A} → ¬ (Null (a ∷ as)) + ¬null (() Data.List.Relation.Unary.All.∷ n) + + ¬null< : {a : A} {as : List< A} → ¬ (Null< (as <: a)) + ¬null< (() Data.SnocList.Relation.Unary.All.<: n) null-[] : ∀ {xs : List A} → Null xs → Null {A = A} [] null-[] = const [] + null<-[] : ∀ {xs : List< A} → Null< xs → Null {A = A} [] + null<-[] = const [] + null-∷ : ∀ {x} {xs ys : List A} → Null (x ∷ xs) → Null ys null-∷ (()∷ _) + null-<: : ∀ {x} {xs : List< A} {ys : List A} → Null< (xs <: x) → Null ys + null-<: (()<: _) + -- 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. @@ -61,45 +71,43 @@ private record Queue (A : Set a) : Set a where constructor mkQ field - front : List A + front : List< A back : List A - inv : Null front → Null back + 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 {a} {A} q = Null< (Queue.front q) empty? : Decidable (Empty {A = A}) -empty? (mkQ front back inv) .Relation.Nullary.does = null front +empty? (mkQ front back inv) .Relation.Nullary.does = SnocList.null front empty? (mkQ [] back inv) .Relation.Nullary.proof = ofʸ [] -empty? (mkQ (x ∷ xs) back inv) .Relation.Nullary.proof = ofⁿ λ empty → ⊥-elim (¬Null empty) +empty? (mkQ (xs <: x) back inv) .Relation.Nullary.proof = ofⁿ (λ e → ⊥-elim (¬null< e)) isEmpty : Queue A → Bool -isEmpty q = null (Queue.front q) +isEmpty q = SnocList.null (Queue.front q) ------------------------------------------------------------------------ --- Smart Constructor -queue : List A → List A → Queue A -queue [] ys = mkQ (reverse ys) [] null-[] -queue xs@(_ ∷ _) ys = mkQ xs ys null-∷ +queue : List< A → List A → Queue A +queue [] ys = mkQ (fromList> (reverse ys)) [] null<-[] +queue xs@(_ <: _) ys = mkQ xs ys null-<: ------------------------------------------------------------------------ --- Conversion to/from List --- Create a List from a Queue, such that the first that would be dequeued --- becomes the head of the list (i.e. the first element of the queue --- becomes the last element of the 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.front q ++ reverse (Queue.back q) +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 first element --- (i.e. the first element of the list becomes the last element of the queue) +-- of the list would be dequeued starting from its last element fromList : List A → Queue A -fromList xs = queue xs [] +fromList xs = queue (fromList> xs) [] ------------------------------------------------------------------------ -- Construction & Destruction @@ -109,11 +117,11 @@ 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) +... | [] = queue ([] <: x) [] +... | front@(_ <: _) = queue front (x ∷ bs) dequeue : ∀ (q : Queue A) .{{_ : False (empty? q)}} → A × Queue A -dequeue (mkQ (x ∷ xs) back _) = x , queue xs back +dequeue (mkQ (xs <: x) back _) = x , queue xs back -- Create a queue with a single element singleton : A → Queue A diff --git a/src/Data/Queue/TwoList/Properties.agda b/src/Data/Queue/TwoList/Properties.agda index 65b7b5b183..24743b809e 100644 --- a/src/Data/Queue/TwoList/Properties.agda +++ b/src/Data/Queue/TwoList/Properties.agda @@ -4,7 +4,7 @@ -- Queue-related properties ------------------------------------------------------------------------ -{-# OPTIONS --without-K --safe #-} +-- {-# OPTIONS --without-K --safe #-} module Data.Queue.TwoList.Properties where @@ -14,9 +14,12 @@ open import Data.List.Base open import Data.List.Properties using (++-identityʳ; length-++; length-reverse) open import Data.List.Relation.Unary.All using (Null; []) open import Data.Nat.Base using (suc; _+_) -open import Data.Nat.Properties using (+-comm; +-suc) +open import Data.Nat.Properties using (+-comm; +-suc; +-assoc) 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>) +open import Data.SnocList.Properties using (toList>-fromList>) +open import Data.SnocList.Relation.Unary.All using (All<; Null<; []; _<:_) open import Function.Base using (_∘_) open import Relation.Binary.PropositionalEquality.Core as ≡ open import Relation.Binary.PropositionalEquality.Properties as ≡ @@ -33,30 +36,44 @@ private A : Set a B : Set b - ¬Null : {a : A} {as : List A} → ¬ Null (a ∷ as) + ¬Null : {x : A} {xs : List A} → ¬ Null (x ∷ xs) ¬Null (() Data.List.Relation.Unary.All.∷ n) -toList-fromList : (xs : List A) → toList (fromList xs) ≡ xs -toList-fromList [] = begin - toList (fromList []) ≡⟨⟩ - toList (empty) ≡⟨⟩ - [] ∎ + null-<: : ∀ {x} {xs : List< A} {ys : List A} → Null< (xs <: x) → Null ys + null-<: (()<: _) -toList-fromList xs@(_ ∷ _) = begin - toList (fromList xs) ≡⟨⟩ - toList (mkQ xs [] (λ _ → [])) ≡⟨⟩ - xs ++ reverse [] ≡⟨⟩ - xs ++ [] ≡⟨ ++-identityʳ xs ⟩ - xs ∎ + queue-back[] : ∀ {xs : List< A} → (Queue.back (queue xs [])) ≡ [] + queue-back[] {xs = []} = refl + queue-back[] {xs = xs <: x} = refl + + queue-front : ∀ {xs : List< A} → (Queue.front (queue xs [])) ≡ xs + queue-front {xs = []} = refl + queue-front {xs = xs <: x} = refl + +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} ⟩ + xs ∎ + where + toList-fromList' : ∀ {xs : List A} → toList (fromList xs) ≡ xs + toList-fromList' {xs = xs} = begin + toList (fromList xs) ≡⟨⟩ + toList (queue (fromList> xs) []) ≡⟨⟩ + (Queue.back (queue (fromList> xs) [])) ++ (toList> (Queue.front (queue (fromList> xs) []))) ≡⟨ cong₂ _++_ (queue-back[] {xs = fromList> xs}) refl ⟩ + [] ++ (toList> (Queue.front (queue (fromList> xs) []))) ≡⟨⟩ + (toList> (Queue.front (queue (fromList> xs) []))) ≡⟨ cong toList> (queue-front {xs = fromList> xs}) ⟩ + toList> (fromList> xs) ≡⟨ toList>-fromList> xs ⟩ + xs ∎ -- 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) ∎ + size (queue ([] <: x) []) ≡⟨⟩ + length (x ∷ []) ≡⟨⟩ + suc 0 ≡⟨ cong suc (sym sizeq) ⟩ + suc (size q) ∎ where null[] : Null back → back ≡ [] null[] [] = refl @@ -64,26 +81,25 @@ size-enqueue {a = a} {A = A} x q@(mkQ [] back inv) = begin back[] : back ≡ [] back[] = null[] (inv []) - -- why does length need {a} and {A} after reverse back ↦ reverse []? + -- why does length need {a} and {A} after back ↦ []? sizeq : size q ≡ 0 sizeq = begin - size q ≡⟨⟩ - length (toList q) ≡⟨⟩ - length ([] ++ (reverse back)) ≡⟨⟩ - length (reverse back) ≡⟨ cong (length ∘ reverse) back[] ⟩ - length {a} {A} (reverse []) ≡⟨⟩ - length {a} {A} [] ≡⟨⟩ - 0 ∎ - -size-enqueue {A = A} x q@(mkQ front@(_ ∷ _) back inv) = 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 (front ++ reverse (x ∷ back)) ≡⟨ length-++ front ⟩ - length front + length (reverse (x ∷ back)) ≡⟨ cong (_+_ (length front)) (length-reverse (x ∷ back)) ⟩ - length front + length (x ∷ back) ≡⟨⟩ - length front + suc (length back) ≡⟨ cong ((_+_ (length front)) ∘ suc) (sym (length-reverse back)) ⟩ - length front + suc (length (reverse back)) ≡⟨ +-suc (length front) (length (reverse back)) ⟩ - suc (length front + length (reverse back)) ≡⟨ cong suc (sym (length-++ front {reverse back})) ⟩ - suc (length (front ++ (reverse 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) ∎ From 009697ce3b9e6b89422b1b6fee120302fb6f8582 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Wed, 29 Jul 2026 16:16:09 -0400 Subject: [PATCH 50/53] Fix whitespace --- src/Data/SnocList/Properties.agda | 46 +++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 src/Data/SnocList/Properties.agda diff --git a/src/Data/SnocList/Properties.agda b/src/Data/SnocList/Properties.agda new file mode 100644 index 0000000000..e89db2bb65 --- /dev/null +++ b/src/Data/SnocList/Properties.agda @@ -0,0 +1,46 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- SnocList properties +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Data.SnocList.Properties where + +open import Data.SnocList.Base +open import Relation.Binary.PropositionalEquality.Core as ≡ +open import Relation.Binary.PropositionalEquality.Properties as ≡ +open import Level using (Level) + +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 (λ e → [] <>> (x :> e)) (toList>-fromList> xs) ⟩ + [] <>> (x :> xs) ≡⟨⟩ + x :> xs ∎ From b4e1ec743fe4b5c64fae8e328613884c6fef5950 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Wed, 29 Jul 2026 16:31:25 -0400 Subject: [PATCH 51/53] Cleanup code --- src/Data/Queue/TwoList/Base.agda | 2 +- src/Data/Queue/TwoList/Properties.agda | 26 +++++++++++++------------- 2 files changed, 14 insertions(+), 14 deletions(-) diff --git a/src/Data/Queue/TwoList/Base.agda b/src/Data/Queue/TwoList/Base.agda index 2855e41ee2..e17df82b21 100644 --- a/src/Data/Queue/TwoList/Base.agda +++ b/src/Data/Queue/TwoList/Base.agda @@ -93,7 +93,7 @@ isEmpty q = SnocList.null (Queue.front q) --- Smart Constructor queue : List< A → List A → Queue A -queue [] ys = mkQ (fromList> (reverse ys)) [] null<-[] +queue [] ys = mkQ (fromList> (reverse ys)) [] null<-[] queue xs@(_ <: _) ys = mkQ xs ys null-<: ------------------------------------------------------------------------ diff --git a/src/Data/Queue/TwoList/Properties.agda b/src/Data/Queue/TwoList/Properties.agda index 24743b809e..c60bf0cd97 100644 --- a/src/Data/Queue/TwoList/Properties.agda +++ b/src/Data/Queue/TwoList/Properties.agda @@ -53,22 +53,22 @@ private 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} ⟩ + toList (fromList xs) ≡⟨ toList-fromList' xs ⟩ xs ∎ where - toList-fromList' : ∀ {xs : List A} → toList (fromList xs) ≡ xs - toList-fromList' {xs = xs} = begin - toList (fromList xs) ≡⟨⟩ - toList (queue (fromList> xs) []) ≡⟨⟩ - (Queue.back (queue (fromList> xs) [])) ++ (toList> (Queue.front (queue (fromList> xs) []))) ≡⟨ cong₂ _++_ (queue-back[] {xs = fromList> xs}) refl ⟩ + -- TODO: can probably cleanup a little + toList-fromList' : ∀ (xs : List A) → toList (fromList xs) ≡ xs + toList-fromList' xs = begin + toList (fromList xs) ≡⟨⟩ + toList (queue (fromList> xs) []) ≡⟨ cong₂ _++_ (queue-back[] {xs = fromList> xs}) refl ⟩ [] ++ (toList> (Queue.front (queue (fromList> xs) []))) ≡⟨⟩ - (toList> (Queue.front (queue (fromList> xs) []))) ≡⟨ cong toList> (queue-front {xs = fromList> xs}) ⟩ - toList> (fromList> xs) ≡⟨ toList>-fromList> xs ⟩ - xs ∎ - + toList> (Queue.front (queue (fromList> xs) [])) ≡⟨ cong toList> (queue-front {xs = fromList> xs}) ⟩ + toList> (fromList> xs) ≡⟨ toList>-fromList> xs ⟩ + xs ∎ + -- 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 : (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 ∷ []) ≡⟨⟩ @@ -87,13 +87,13 @@ size-enqueue {a = a} {A = A} x q@(mkQ [] back inv) = begin size q ≡⟨⟩ length (toList q) ≡⟨⟩ length (back ++ []) ≡⟨ cong length (++-identityʳ back) ⟩ - length (back) ≡⟨ cong length 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 ++ 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)⟩ From 07212a41fdab0ea782e755ecb78b81ecffc7627b Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Wed, 29 Jul 2026 18:25:47 -0400 Subject: [PATCH 52/53] Fix whitespace --- src/Data/Queue/TwoList/Properties.agda | 60 +++++++++++++++++++++++--- 1 file changed, 55 insertions(+), 5 deletions(-) diff --git a/src/Data/Queue/TwoList/Properties.agda b/src/Data/Queue/TwoList/Properties.agda index c60bf0cd97..321c7c56e4 100644 --- a/src/Data/Queue/TwoList/Properties.agda +++ b/src/Data/Queue/TwoList/Properties.agda @@ -4,7 +4,7 @@ -- Queue-related properties ------------------------------------------------------------------------ --- {-# OPTIONS --without-K --safe #-} +{-# OPTIONS --without-K --safe #-} module Data.Queue.TwoList.Properties where @@ -23,7 +23,7 @@ open import Data.SnocList.Relation.Unary.All using (All<; Null<; []; _<:_) open import Function.Base using (_∘_) open import Relation.Binary.PropositionalEquality.Core as ≡ open import Relation.Binary.PropositionalEquality.Properties as ≡ -open import Relation.Binary.Definitions using (Reflexive) +open import Relation.Binary.Definitions using (Reflexive; _Respects_) open import Relation.Binary.Structures using (IsEquivalence) open import Relation.Nullary using (¬_) @@ -49,7 +49,7 @@ private queue-front : ∀ {xs : List< A} → (Queue.front (queue xs [])) ≡ xs queue-front {xs = []} = refl queue-front {xs = xs <: x} = refl - + 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 ⟩ @@ -65,7 +65,7 @@ toList-fromList {q = q} {xs = xs} q≈xs = begin toList> (Queue.front (queue (fromList> xs) [])) ≡⟨ cong toList> (queue-front {xs = fromList> xs}) ⟩ toList> (fromList> xs) ≡⟨ toList>-fromList> xs ⟩ xs ∎ - + -- 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) @@ -89,7 +89,7 @@ size-enqueue {a = a} {A = A} x q@(mkQ [] back inv) = begin length (back ++ []) ≡⟨ cong length (++-identityʳ back) ⟩ length back ≡⟨ cong length back[] ⟩ length {a} {A} [] ≡⟨⟩ - 0 ∎ + 0 ∎ size-enqueue {A = A} x q@(mkQ front@(_ <: _) back inv) = begin size (queue front (x ∷ back)) ≡⟨⟩ @@ -117,3 +117,53 @@ size-empty = refl ; sym = sym ; trans = trans } + +toList-Empty : ∀ {x : Queue A} → Empty x → toList x ≡ [] +toList-Empty {x = x@(mkQ [] back inv)} [] = begin + toList (mkQ [] back inv) ≡⟨⟩ + back ++ [] ≡⟨ ++-identityʳ back ⟩ + back ≡⟨ back[] ⟩ + [] ∎ + where + null[] : Null back → back ≡ [] + null[] [] = refl + + back[] : back ≡ [] + back[] = null[] (inv []) + +toList-front : ∀ {xs : Queue A} → toList xs ≡ [] → Queue.front xs ≡ [] +toList-front {xs = xs@(mkQ front back inv)} xs≡[] = begin + {!!} ≡⟨⟩ + {!!} ≡⟨⟩ + {!!} ≡⟨⟩ + {!!} + +null[] : ∀ {xs : List< A} → xs ≡ [] → Null< xs +null[] = {!!} + +empty[] : ∀ {xs : Queue A} → (toList xs) ≡ [] → Empty xs +empty[] {xs = xs} xs≡[] = null[] (toList-front {xs = xs} xs≡[]) + +≈-resp-Empty : Empty Respects (_≈_ {A = A}) +≈-resp-Empty {x = x} {y = y} x≈y empty-x = empty[] {xs = y} (begin + toList y ≡⟨ sym x≈y ⟩ + toList x ≡⟨ toList-Empty {x = x} empty-x ⟩ + [] ∎ + ) + +------------------------------------------------------------------------ +-- TwoList Queue is a Queue! + +instance + TwoList-IsQueue : IsQueue {a} TwoList-RawQueue + TwoList-IsQueue = record + { isEquivalence = ≈-isEquivalence + ; ≈-resp-Empty = {!!} + ; ≈-=[toList]⇒-≡ = {!!} + ; empty-toList = {!!} + ; empty-fromList = {!!} + ; toList-fromList = {!!} + ; fromList-toList = {!!} + ; toList-enqueue = {!!} + ; toList-dequeue = {!!} + } From 84d517b9bf499ddf95204870f99d802037692576 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Wed, 29 Jul 2026 19:21:16 -0400 Subject: [PATCH 53/53] =?UTF-8?q?Prove=20=E2=89=88-resp-Empty=20on=20TwoLi?= =?UTF-8?q?st?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Queue/TwoList/Properties.agda | 89 ++++++++++++++++---------- 1 file changed, 55 insertions(+), 34 deletions(-) diff --git a/src/Data/Queue/TwoList/Properties.agda b/src/Data/Queue/TwoList/Properties.agda index 321c7c56e4..78a2ba6074 100644 --- a/src/Data/Queue/TwoList/Properties.agda +++ b/src/Data/Queue/TwoList/Properties.agda @@ -118,31 +118,45 @@ size-empty = refl ; trans = trans } -toList-Empty : ∀ {x : Queue A} → Empty x → toList x ≡ [] -toList-Empty {x = x@(mkQ [] back inv)} [] = begin - toList (mkQ [] back inv) ≡⟨⟩ - back ++ [] ≡⟨ ++-identityʳ back ⟩ - back ≡⟨ back[] ⟩ - [] ∎ - where - null[] : Null back → back ≡ [] - null[] [] = refl +-- NOTE: *most* of these: +-- A) Can be moved elsewhere (e.g. the null proofs that are repeated in TwoList.Base, etc...) +-- B) Should be renamed +private + toList-Empty : ∀ {x : Queue A} → Empty x → toList x ≡ [] + toList-Empty {x = x@(mkQ [] back inv)} [] = begin + toList (mkQ [] back inv) ≡⟨⟩ + back ++ [] ≡⟨ ++-identityʳ back ⟩ + back ≡⟨ back[] ⟩ + [] ∎ + where + null[] : Null back → back ≡ [] + null[] [] = refl - back[] : back ≡ [] - back[] = null[] (inv []) + back[] : back ≡ [] + back[] = null[] (inv []) -toList-front : ∀ {xs : Queue A} → toList xs ≡ [] → Queue.front xs ≡ [] -toList-front {xs = xs@(mkQ front back inv)} xs≡[] = begin - {!!} ≡⟨⟩ - {!!} ≡⟨⟩ - {!!} ≡⟨⟩ - {!!} + ++-[] : ∀ {xs ys : List A} → (xs ++ ys) ≡ [] → ys ≡ [] + ++-[] {xs = []} {ys = []} xs++ys≡[] = xs++ys≡[] -null[] : ∀ {xs : List< A} → xs ≡ [] → Null< xs -null[] = {!!} + ¬null< : {a : A} {as : List< A} → ¬ (Null< (as <: a)) + ¬null< (() Data.SnocList.Relation.Unary.All.<: n) -empty[] : ∀ {xs : Queue A} → (toList xs) ≡ [] → Empty xs -empty[] {xs = xs} xs≡[] = null[] (toList-front {xs = xs} xs≡[]) + null[] : ∀ {xs : List< A} → xs ≡ [] → Null< xs + null[] xs≡[] rewrite xs≡[] = [] + + ¬<>>[] : ∀ {x} {xs : List< A} {ys : List A} → xs SnocList.<>> (x ∷ ys) ≢ [] + ¬<>>[] {xs = []} () + ¬<>>[] {xs = xs <: x} wrong = ¬<>>[] {xs = xs} wrong + + <>>[] : ∀ {xs : List< A} → xs SnocList.<>> [] ≡ [] → xs ≡ [] + <>>[] {xs = []} xs<>>[]≡[] = refl + <>>[] {xs = (xs <: x)} xs<>>[]≡[] = ⊥-elim (¬<>>[] {x = x} {xs = xs} {ys = []} xs<>>[]≡[]) + + toList-front : ∀ {xs : Queue A} → toList xs ≡ [] → Queue.front xs ≡ [] + toList-front {xs = xs@(mkQ front [] inv)} xs≡[] = <>>[] xs≡[] + + empty[] : ∀ {xs : Queue A} → toList xs ≡ [] → Empty xs + empty[] {xs = xs} xs≡[] = null[] (toList-front {xs = xs} xs≡[]) ≈-resp-Empty : Empty Respects (_≈_ {A = A}) ≈-resp-Empty {x = x} {y = y} x≈y empty-x = empty[] {xs = y} (begin @@ -151,19 +165,26 @@ empty[] {xs = xs} xs≡[] = null[] (toList-front {xs = xs} xs≡[]) [] ∎ ) +-- For some reason, gives unresolved implicits of +-- _x.inv_750 : Null< (Queue.front x) → Null (Queue.back x) +-- _y.inv_753 : Null< (Queue.front y) → Null (Queue.back y) +-- But I'm too tired to trace it through and figure out why for today! +-- ≈-resp-Empty' : Empty Respects (_≈_ {A = A}) +-- ≈-resp-Empty' = ≈-resp-Empty + ------------------------------------------------------------------------ -- TwoList Queue is a Queue! -instance - TwoList-IsQueue : IsQueue {a} TwoList-RawQueue - TwoList-IsQueue = record - { isEquivalence = ≈-isEquivalence - ; ≈-resp-Empty = {!!} - ; ≈-=[toList]⇒-≡ = {!!} - ; empty-toList = {!!} - ; empty-fromList = {!!} - ; toList-fromList = {!!} - ; fromList-toList = {!!} - ; toList-enqueue = {!!} - ; toList-dequeue = {!!} - } +-- instance +-- TwoList-IsQueue : IsQueue {a} TwoList-RawQueue +-- TwoList-IsQueue = record +-- { isEquivalence = ≈-isEquivalence +-- ; ≈-resp-Empty = ≈-resp-Empty +-- ; ≈-=[toList]⇒-≡ = {!!} +-- ; empty-toList = {!!} +-- ; empty-fromList = {!!} +-- ; toList-fromList = {!!} +-- ; fromList-toList = {!!} +-- ; toList-enqueue = {!!} +-- ; toList-dequeue = {!!} +-- }