Advent of proof submissions.HEADmaster

Completed all problems save 12, where I had to postulate two lemma.

1 files changed, 102 insertions, 0 deletions

diff --git a/src/Problem9.agda b/src/Problem9.agda
new file mode 100644
index 0000000..9bc5a61
--- /dev/null
+++ b/src/Problem9.agda
@@ -0,0 +1,102 @@
+{-# OPTIONS --safe #-}
+
+module Problem9 where
+
+open import Data.Nat
+open import Relation.Binary.PropositionalEquality
+open import Data.Maybe as Maybe using (Maybe; just; nothing)
+open import Relation.Nullary
+open import Data.List
+open import Data.Nat.Properties using (suc-injective)
+open import Data.List.Properties using (++-identityʳ;length-++; ++-assoc;unfold-reverse; length-reverse)
+
+open ≡-Reasoning
+
+variable A : Set
+
+record Queue A : Set where
+  constructor Q
+  field
+    size-front  : ℕ
+    size-back   : ℕ
+    front : List A
+    back  : List A
+
+    invariant : size-back ≤ size-front
+    size-inv₁ : length front ≡ size-front
+    size-inv₂ : length back ≡ size-back
+open Queue
+
+record CorrectQueue (Q : Set → Set) : Set₁ where
+  field
+    abstraction : Q A → List A
+    enqueue     : A → Q A → Q A
+    dequeue     : Q A → Maybe (Q A)
+    first       : Q A → Maybe A
+    size        : Q A → ℕ
+    empty       : Q A
+
+    emptyᵣ      : abstraction (empty {A}) ≡ []
+    sizeᵣ       : ∀ (q : Q A) → size q ≡ length (abstraction q)
+    firstᵣ      : ∀ (q : Q A) → first q ≡ head (abstraction q)
+    dequeueᵣ    : ∀ (q : Q A) → Maybe.map abstraction (dequeue q) ≡ tail (abstraction q)
+    enqueueᵣ    : ∀ (q : Q A) x → abstraction (enqueue x q) ≡ abstraction q ∷ʳ x
+
+enqueueQ  : A → Queue A → Queue A
+enqueueQ x q with suc (size-back q) ≤? size-front  q
+... | yes p = Q (size-front q) (suc (size-back q)) (front q) (x ∷ back q) p (size-inv₁ q) (cong suc (size-inv₂ q))
+... | no  p = Q (size-front q + suc (size-back q)) 0 (front q ++ reverse (x ∷ back q)) [] z≤n (trans (length-++ (front q)) (cong₂ _+_ (size-inv₁ q) (trans (length-reverse (x ∷ back q) ) (cong suc (size-inv₂ q))))) refl
+
+dequeueQ : Queue A → Maybe (Queue A)
+dequeueQ (Q _ _ [] [] z≤n refl refl) = nothing
+dequeueQ (Q (suc size-front₁) size-back₁ (x ∷ front₁) back₁ invariant₁ size-inv₃ size-inv₄) with size-back₁ ≤? size-front₁
+... | yes p  = just (Q size-front₁ size-back₁ front₁ back₁ p (suc-injective size-inv₃) size-inv₄)
+... | no p   = just (Q (size-front₁ + size-back₁) 0 (front₁ ++ reverse back₁) [] z≤n (trans (length-++ front₁) (cong₂ _+_ (suc-injective size-inv₃) (trans (length-reverse back₁) size-inv₄))) refl)
+
+firstQ : Queue A → Maybe A
+firstQ (Q size-front₁ size-back₁ [] back₁ invariant₁ size-inv₃ size-inv₄) = nothing
+firstQ (Q size-front₁ size-back₁ (x ∷ front₁) back₁ invariant₁ size-inv₃ size-inv₄) = just x
+
+sizeQ : Queue A → ℕ
+sizeQ q = size-front q + size-back q
+
+emptyQ : Queue A
+emptyQ = Q 0 0 [] [] z≤n refl refl
+
+open CorrectQueue
+
+goal : CorrectQueue Queue
+
+-- Data portion of goal
+goal .abstraction q = front q ++ reverse (back q)
+goal .enqueue x q = enqueueQ x q
+goal .dequeue q = dequeueQ q
+goal .first q = firstQ q
+goal .size q = sizeQ q
+goal .empty = emptyQ
+
+-- Correctness portion of goal
+goal .emptyᵣ = refl
+goal .sizeᵣ q = begin
+  sizeQ q                                      ≡⟨⟩
+  size-front q + size-back q                   ≡˘⟨ cong₂ _+_ (size-inv₁ q) (size-inv₂ q) ⟩
+  length (front q) + length (back q)           ≡˘⟨ cong (length (front q) +_) (length-reverse (back q)) ⟩
+  length (front q) + length (reverse (back q)) ≡˘⟨ length-++ (front q) ⟩
+  length (front q ++ reverse (back q))         ∎
+goal .firstᵣ (Q .0 .0 [] [] z≤n refl refl) = refl
+goal .firstᵣ (Q _ _ (x ∷ front₁) back₁ _ _ _) = refl
+goal .dequeueᵣ (Q .0 .0 [] [] z≤n refl refl) = refl
+goal .dequeueᵣ (Q (suc size-front₁) size-back₁ (x ∷ front₁) back₁ invariant₁ size-inv₃ size-inv₄)
+  with size-back₁ ≤? size-front₁
+... | yes p = refl
+... | no p = cong just (++-identityʳ (front₁ ++ reverse back₁))
+goal .enqueueᵣ q x with suc (size-back q) ≤? size-front q
+... | yes p = begin
+  front q ++ reverse (x ∷ back q)         ≡⟨ cong (front q ++_) (unfold-reverse x (back q)) ⟩
+  front q ++ reverse (back q) ++ x ∷ []   ≡˘⟨ ++-assoc (front q) (reverse (back q)) (x ∷ []) ⟩
+  (front q ++ reverse (back q)) ++ x ∷ [] ∎
+... | no p = begin
+  (front q ++ reverse (x ∷ back q)) ++ [] ≡⟨ ++-identityʳ (front q ++ reverse (x ∷ back q)) ⟩
+  front q ++ reverse (x ∷ back q)         ≡⟨ cong (front q ++_) (unfold-reverse x (back q)) ⟩
+  front q ++ reverse (back q) ++ x ∷ []   ≡˘⟨ ++-assoc (front q) (reverse (back q)) (x ∷ []) ⟩
+  (front q ++ reverse (back q)) ++ x ∷ [] ∎