From 4527250aee1d1d4655e84f0583d04410b7c53642 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Mon, 22 Jan 2024 11:51:56 +0000 Subject: Advent of proof submissions. Completed all problems save 12, where I had to postulate two lemma. --- src/Problem1.agda | 87 ++++++++++ src/Problem10.agda | 89 +++++++++++ src/Problem11.agda | 69 ++++++++ src/Problem12.agda | 459 +++++++++++++++++++++++++++++++++++++++++++++++++++++ src/Problem13.agda | 93 +++++++++++ src/Problem14.agda | 123 ++++++++++++++ src/Problem15.agda | 154 ++++++++++++++++++ src/Problem16.agda | 46 ++++++ src/Problem17.agda | 116 ++++++++++++++ src/Problem18.agda | 113 +++++++++++++ src/Problem19.agda | 159 +++++++++++++++++++ src/Problem2.agda | 55 +++++++ src/Problem20.agda | 105 ++++++++++++ src/Problem21.agda | 80 ++++++++++ src/Problem22.agda | 87 ++++++++++ src/Problem23.agda | 136 ++++++++++++++++ src/Problem24.agda | 155 ++++++++++++++++++ src/Problem3.agda | 56 +++++++ src/Problem4.agda | 97 +++++++++++ src/Problem5.agda | 44 +++++ src/Problem6.agda | 239 ++++++++++++++++++++++++++++ src/Problem7.agda | 54 +++++++ src/Problem8.agda | 109 +++++++++++++ src/Problem9.agda | 102 ++++++++++++ 24 files changed, 2827 insertions(+) create mode 100644 src/Problem1.agda create mode 100644 src/Problem10.agda create mode 100644 src/Problem11.agda create mode 100644 src/Problem12.agda create mode 100644 src/Problem13.agda create mode 100644 src/Problem14.agda create mode 100644 src/Problem15.agda create mode 100644 src/Problem16.agda create mode 100644 src/Problem17.agda create mode 100644 src/Problem18.agda create mode 100644 src/Problem19.agda create mode 100644 src/Problem2.agda create mode 100644 src/Problem20.agda create mode 100644 src/Problem21.agda create mode 100644 src/Problem22.agda create mode 100644 src/Problem23.agda create mode 100644 src/Problem24.agda create mode 100644 src/Problem3.agda create mode 100644 src/Problem4.agda create mode 100644 src/Problem5.agda create mode 100644 src/Problem6.agda create mode 100644 src/Problem7.agda create mode 100644 src/Problem8.agda create mode 100644 src/Problem9.agda (limited to 'src') diff --git a/src/Problem1.agda b/src/Problem1.agda new file mode 100644 index 0000000..3aab789 --- /dev/null +++ b/src/Problem1.agda @@ -0,0 +1,87 @@ +{-# OPTIONS --safe #-} + +module Problem1 where + +open import Data.Nat +open import Relation.Binary.PropositionalEquality + +open ≡-Reasoning + +data 𝔹 : Set where + T F : 𝔹 + +iterate : (n : ℕ) (f : 𝔹 → 𝔹) (x : 𝔹) → 𝔹 +iterate zero f x = x +iterate (suc n) f x = f (iterate n f x) + +twice = iterate (suc (suc zero)) + +-- There are exactly four functions 𝔹 → 𝔹: the two constant functions, the +-- identiy and the inversion. +-- +-- We can decide (extensionally) which function we have. + +data OneOf (f : 𝔹 → 𝔹) : Set where + is-const : (∀ x y → f x ≡ f y) → OneOf f + is-id : (∀ x → f x ≡ x) → OneOf f + is-not : f T ≡ F → f F ≡ T → OneOf f + +which-one? : (f : 𝔹 → 𝔹) → OneOf f +which-one? f with f T in prfT | f F in prfF +... | T | T = is-const λ + { T T → refl + ; T F → begin + f T ≡⟨ prfT ⟩ + T ≡⟨ sym prfF ⟩ + f F ∎ + ; F T → begin + f F ≡⟨ prfF ⟩ + T ≡⟨ sym prfT ⟩ + f T ∎ + ; F F → refl + } +... | T | F = is-id λ { T → prfT ; F → prfF } +... | F | T = is-not prfT prfF +... | F | F = is-const λ + { T T → refl + ; T F → begin + f T ≡⟨ prfT ⟩ + F ≡⟨ sym prfF ⟩ + f F ∎ + ; F T → begin + f F ≡⟨ prfF ⟩ + F ≡⟨ sym prfT ⟩ + f T ∎ + ; F F → refl + } + +-- First, we show that applying a function thrice is equal to a single +-- application. We do this by splitting on the exact function. + +thrice-is-once : (f : 𝔹 → 𝔹) → iterate 3 f ≗ f +thrice-is-once f with which-one? f +... | is-const prf = λ b → prf (f (f b)) b +... | is-id prf = λ b → + begin + f (f (f b)) ≡⟨ prf (f (f b)) ⟩ + f (f b) ≡⟨ prf (f b) ⟩ + f b ∎ +... | is-not prfT prfF = λ + { T → begin + f (f (f T)) ≡⟨ cong (twice f) prfT ⟩ + f (f F) ≡⟨ cong f prfF ⟩ + f T ∎ + ; F → begin + f (f (f F)) ≡⟨ cong (twice f) prfF ⟩ + f (f T) ≡⟨ cong f prfT ⟩ + f F ∎ + } + +-- We prove the theorem by induction on n. + +goal : ∀ (f : 𝔹 → 𝔹) (b : 𝔹) (n : ℕ) → iterate n (twice f) (f b) ≡ f b +goal f b zero = refl +goal f b (suc n) = begin + f (f (iterate n (twice f) (f b))) ≡⟨ cong (twice f) (goal f b n) ⟩ + f (f (f b)) ≡⟨ thrice-is-once f b ⟩ + f b ∎ diff --git a/src/Problem10.agda b/src/Problem10.agda new file mode 100644 index 0000000..0e465d6 --- /dev/null +++ b/src/Problem10.agda @@ -0,0 +1,89 @@ +module Problem10 where + +open import Relation.Binary.PropositionalEquality + +open ≡-Reasoning + +infixl 15 _⋆_ + +postulate + C : Set + _⋆_ : C → C → C + _ᵒ : C → C + assoc : ∀ a b c → (a ⋆ b) ⋆ c ≡ a ⋆ (b ⋆ c) + ᵒ-prop : ∀ a → a ⋆ a ᵒ ⋆ a ≡ a + +_ᶜ : C → C +x ᶜ = x ᵒ ⋆ x ⋆ x ᵒ + +prop₁ : ∀ a → a ⋆ a ᶜ ⋆ a ≡ a +prop₁ a = begin + a ⋆ (a ᵒ ⋆ a ⋆ a ᵒ) ⋆ a ≡˘⟨ cong (_⋆ a) (assoc a (a ᵒ ⋆ a) (a ᵒ)) ⟩ + a ⋆ (a ᵒ ⋆ a) ⋆ a ᵒ ⋆ a ≡˘⟨ cong (λ - → - ⋆ a ᵒ ⋆ a) (assoc a (a ᵒ) a) ⟩ + a ⋆ a ᵒ ⋆ a ⋆ a ᵒ ⋆ a ≡⟨ cong (λ - → - ⋆ a ᵒ ⋆ a) (ᵒ-prop a) ⟩ + a ⋆ a ᵒ ⋆ a ≡⟨ ᵒ-prop a ⟩ + a ∎ +prop₂ : ∀ a → a ᶜ ⋆ a ⋆ a ᶜ ≡ a ᶜ +prop₂ a = begin + a ᵒ ⋆ a ⋆ a ᵒ ⋆ a ⋆ (a ᵒ ⋆ a ⋆ a ᵒ) ≡˘⟨ assoc (a ᵒ ⋆ a ⋆ a ᵒ ⋆ a) (a ᵒ ⋆ a) (a ᵒ) ⟩ + a ᵒ ⋆ a ⋆ a ᵒ ⋆ a ⋆ (a ᵒ ⋆ a) ⋆ a ᵒ ≡˘⟨ cong (_⋆ a ᵒ) (assoc (a ᵒ ⋆ a ⋆ a ᵒ ⋆ a) (a ᵒ) a) ⟩ + a ᵒ ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ ≡⟨ cong (λ - → - ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ) (assoc (a ᵒ) a (a ᵒ)) ⟩ + a ᵒ ⋆ (a ⋆ a ᵒ) ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ ≡⟨ cong (λ - → - ⋆ a ᵒ ⋆ a ⋆ a ᵒ) (assoc (a ᵒ) (a ⋆ a ᵒ) a) ⟩ + a ᵒ ⋆ (a ⋆ a ᵒ ⋆ a) ⋆ a ᵒ ⋆ a ⋆ a ᵒ ≡⟨ cong (λ - → a ᵒ ⋆ - ⋆ a ᵒ ⋆ a ⋆ a ᵒ) (ᵒ-prop a) ⟩ + a ᵒ ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ ≡⟨ cong (λ - → - ⋆ a ⋆ a ᵒ) (assoc (a ᵒ) a (a ᵒ)) ⟩ + a ᵒ ⋆ (a ⋆ a ᵒ) ⋆ a ⋆ a ᵒ ≡⟨ cong (_⋆ (a ᵒ)) (assoc (a ᵒ) (a ⋆ a ᵒ) a) ⟩ + a ᵒ ⋆ (a ⋆ a ᵒ ⋆ a) ⋆ a ᵒ ≡⟨ cong (λ - → a ᵒ ⋆ - ⋆ a ᵒ) (ᵒ-prop a) ⟩ + a ᵒ ⋆ a ⋆ a ᵒ ∎ + +postulate + commute : ∀ a b → a ⋆ a ≡ a → b ⋆ b ≡ b → a ⋆ b ≡ b ⋆ a + +uniqueness : ∀ a z → a ⋆ z ⋆ a ≡ a + → z ⋆ a ⋆ z ≡ z + → z ≡ a ᶜ +uniqueness a z aza≡a zaz≡z = begin + z ≡˘⟨ zaz≡z ⟩ + z ⋆ a ⋆ z ≡˘⟨ cong (λ - → z ⋆ - ⋆ z) (ᵒ-prop a) ⟩ + z ⋆ (a ⋆ a ᵒ ⋆ a) ⋆ z ≡˘⟨ cong (_⋆ z) (assoc z (a ⋆ a ᵒ) a) ⟩ + z ⋆ (a ⋆ a ᵒ) ⋆ a ⋆ z ≡⟨ assoc (z ⋆ (a ⋆ a ᵒ)) a z ⟩ + z ⋆ (a ⋆ a ᵒ) ⋆ (a ⋆ z) ≡⟨ assoc z (a ⋆ a ᵒ) (a ⋆ z) ⟩ + z ⋆ ((a ⋆ a ᵒ) ⋆ (a ⋆ z)) ≡⟨ cong (z ⋆_) (commute (a ⋆ a ᵒ) (a ⋆ z) aaᵒaaᵒ≡aaᵒ azaz≡az) ⟩ + z ⋆ ((a ⋆ z) ⋆ (a ⋆ a ᵒ)) ≡˘⟨ assoc z (a ⋆ z) (a ⋆ a ᵒ) ⟩ + z ⋆ (a ⋆ z) ⋆ (a ⋆ a ᵒ) ≡˘⟨ cong (_⋆ (a ⋆ a ᵒ)) (assoc z a z) ⟩ + z ⋆ a ⋆ z ⋆ (a ⋆ a ᵒ) ≡⟨ cong (_⋆ (a ⋆ a ᵒ)) zaz≡z ⟩ + z ⋆ (a ⋆ a ᵒ) ≡˘⟨ assoc z a (a ᵒ) ⟩ + z ⋆ a ⋆ a ᵒ ≡˘⟨ cong (λ - → z ⋆ - ⋆ (a ᵒ)) (ᵒ-prop a) ⟩ + z ⋆ (a ⋆ a ᵒ ⋆ a) ⋆ a ᵒ ≡˘⟨ cong (_⋆ a ᵒ) (assoc z (a ⋆ a ᵒ) a) ⟩ + z ⋆ (a ⋆ a ᵒ) ⋆ a ⋆ a ᵒ ≡˘⟨ cong (λ - → - ⋆ a ⋆ a ᵒ) (assoc z a (a ᵒ)) ⟩ + z ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ ≡⟨ cong (_⋆ a ᵒ) (assoc (z ⋆ a) (a ᵒ) a) ⟩ + z ⋆ a ⋆ (a ᵒ ⋆ a) ⋆ a ᵒ ≡⟨ cong (_⋆ a ᵒ) (commute (z ⋆ a) (a ᵒ ⋆ a) zaza≡za aᵒaaᵒa≡aᵒa) ⟩ + a ᵒ ⋆ a ⋆ (z ⋆ a) ⋆ a ᵒ ≡˘⟨ cong (_⋆ a ᵒ) (assoc (a ᵒ ⋆ a) z a) ⟩ + a ᵒ ⋆ a ⋆ z ⋆ a ⋆ a ᵒ ≡⟨ cong (λ - → - ⋆ a ⋆ a ᵒ) (assoc (a ᵒ) a z) ⟩ + a ᵒ ⋆ (a ⋆ z) ⋆ a ⋆ a ᵒ ≡⟨ cong (_⋆ a ᵒ) (assoc (a ᵒ) (a ⋆ z) a) ⟩ + a ᵒ ⋆ (a ⋆ z ⋆ a) ⋆ a ᵒ ≡⟨ cong (λ - → a ᵒ ⋆ - ⋆ a ᵒ) aza≡a ⟩ + a ᵒ ⋆ a ⋆ a ᵒ ∎ + where + zaza≡za : z ⋆ a ⋆ (z ⋆ a) ≡ z ⋆ a + zaza≡za = begin + z ⋆ a ⋆ (z ⋆ a) ≡˘⟨ assoc (z ⋆ a) z a ⟩ + z ⋆ a ⋆ z ⋆ a ≡⟨ cong (_⋆ a) zaz≡z ⟩ + z ⋆ a ∎ + + azaz≡az : a ⋆ z ⋆ (a ⋆ z) ≡ a ⋆ z + azaz≡az = begin + a ⋆ z ⋆ (a ⋆ z) ≡˘⟨ assoc (a ⋆ z) a z ⟩ + a ⋆ z ⋆ a ⋆ z ≡⟨ cong (_⋆ z) aza≡a ⟩ + a ⋆ z ∎ + + aᵒaaᵒa≡aᵒa : a ᵒ ⋆ a ⋆ (a ᵒ ⋆ a) ≡ a ᵒ ⋆ a + aᵒaaᵒa≡aᵒa = begin + a ᵒ ⋆ a ⋆ (a ᵒ ⋆ a) ≡⟨ assoc (a ᵒ) a (a ᵒ ⋆ a) ⟩ + a ᵒ ⋆ (a ⋆ (a ᵒ ⋆ a)) ≡˘⟨ cong (a ᵒ ⋆_) (assoc a (a ᵒ) a) ⟩ + a ᵒ ⋆ (a ⋆ a ᵒ ⋆ a) ≡⟨ cong (a ᵒ ⋆_) (ᵒ-prop a) ⟩ + a ᵒ ⋆ a ∎ + + aaᵒaaᵒ≡aaᵒ : a ⋆ a ᵒ ⋆ (a ⋆ a ᵒ) ≡ a ⋆ a ᵒ + aaᵒaaᵒ≡aaᵒ = begin + a ⋆ a ᵒ ⋆ (a ⋆ a ᵒ) ≡˘⟨ assoc (a ⋆ a ᵒ) a (a ᵒ) ⟩ + a ⋆ a ᵒ ⋆ a ⋆ a ᵒ ≡⟨ cong (_⋆ a ᵒ) (ᵒ-prop a) ⟩ + a ⋆ a ᵒ ∎ diff --git a/src/Problem11.agda b/src/Problem11.agda new file mode 100644 index 0000000..686f645 --- /dev/null +++ b/src/Problem11.agda @@ -0,0 +1,69 @@ +{-# OPTIONS --safe #-} + +module Problem11 where + +data Term : Set where + Ref : Term + Sop : Term + Kop : Term + App : Term → Term → Term + +variable M N P M₁ M₂ M₃ N₁ N₂ : Term + +data _↦_ : Term → Term → Set where + red-S : (App (App (App Sop M) N) P) ↦ (App (App M P) (App N P)) + red-K : (App (App Kop M) N) ↦ M + red-left : M₁ ↦ M₂ → App M₁ N ↦ App M₂ N + red-right : N₁ ↦ N₂ → App M N₁ ↦ App M N₂ + red-trans : M ↦ N → N ↦ P → M ↦ P + +open import Relation.Binary.Reasoning.Base.Partial _↦_ red-trans + +ident : Term +ident = App (App Sop Kop) Kop + +ident-red : App ident M ↦ M +ident-red {M} = begin + App (App (App Sop Kop) Kop) M ∼⟨ red-S ⟩ + App (App Kop M) (App Kop M) ∼⟨ red-K ⟩ + M ∎ + +const-sop : Term +const-sop = App Kop Sop + +const-sop-red : App const-sop M ↦ Sop +const-sop-red = red-K + +const-kop : Term +const-kop = App Kop Kop + +const-kop-red : App const-kop M ↦ Kop +const-kop-red = red-K + +app-app : Term → Term → Term +app-app M N = App (App Sop M) N + +app-app-red : App (app-app M₁ M₂) M₃ ↦ App (App M₁ M₃) (App M₂ M₃) +app-app-red = red-S + +lambda : Term → Term +lambda Ref = ident +lambda Sop = App Kop Sop +lambda Kop = App Kop Kop +lambda (App M N) = app-app (lambda M) (lambda N) + +substitution : Term → Term → Term +substitution Ref N = N +substitution Sop N = Sop +substitution Kop N = Kop +substitution (App M₁ M₂) N = App (substitution M₁ N) (substitution M₂ N) + +beta : ∀ M N → (App (lambda M) N) ↦ (substitution M N) +beta Ref N = ident-red +beta Sop N = const-sop-red +beta Kop N = const-kop-red +beta (App M₁ M₂) N = begin + App (app-app (lambda M₁) (lambda M₂)) N ∼⟨ app-app-red ⟩ + App (App (lambda M₁) N) (App (lambda M₂) N) ∼⟨ red-left (beta M₁ N) ⟩ + App (substitution M₁ N) (App (lambda M₂) N) ∼⟨ red-right (beta M₂ N) ⟩ + App (substitution M₁ N) (substitution M₂ N) ∎ diff --git a/src/Problem12.agda b/src/Problem12.agda new file mode 100644 index 0000000..5c147a2 --- /dev/null +++ b/src/Problem12.agda @@ -0,0 +1,459 @@ +module Problem12 where + +open import Axiom.UniquenessOfIdentityProofs using (UIP; module Decidable⇒UIP) +open import Data.Bool hiding (_≟_) +open import Data.Empty using (⊥-elim) +open import Data.Fin hiding (_+_) +import Data.Fin.Properties as Fin +open import Data.List +open import Data.List.Membership.Propositional +open import Data.List.Membership.Propositional.Properties +open import Data.List.Properties +open import Data.List.Relation.Unary.Any using (here; there; satisfied) +open import Data.Nat using (ℕ;zero;suc;_*_; _+_) +open import Data.Nat.Properties hiding (_≟_) +open import Data.Product hiding (map) +open import Data.Sum hiding (map) +open import Function.Base using (_∘′_) +open import Function.Bundles using (Injection; _↣_; _↔_; mk↣; mk↔′) +open import Relation.Binary.PropositionalEquality +open import Relation.Nullary + +-- copied in here because latest stable stdlib doesn't have it?? +_⊎-dec_ : ∀{A B : Set} → Dec A → Dec B → Dec (A ⊎ B) +does (a? ⊎-dec b?) = does a? ∨ does b? +proof (a? ⊎-dec b?) with proof a? +... | ofʸ p = ofʸ (inj₁ p) +... | ofⁿ ¬p with proof b? +... | ofʸ p = ofʸ (inj₂ p) +... | ofⁿ ¬p₁ = ofⁿ (λ { (inj₁ q) → ¬p q; (inj₂ q) → ¬p₁ q }) + +sum-0 : ∀ n → sum (tabulate {n = n} (λ _ → 0)) ≡ 0 +sum-0 zero = refl +sum-0 (suc n) = sum-0 n + +record DisjointPair (A : Set) : Set where + field + from : A + to : A + diff : from ≢ to + +record MultiGraph : Set where + field + #V : ℕ + Vertex = Fin #V + Edge = DisjointPair Vertex + field + E : List Edge + + V : List (Vertex) + V = allFin #V + + VertexUIP : UIP Vertex + VertexUIP = Decidable⇒UIP.≡-irrelevant _≟_ + + Connects : Vertex → Edge → Set + Connects v e = DisjointPair.from e ≡ v ⊎ DisjointPair.to e ≡ v + + connects : (v : Vertex) → (e : Edge) → Dec (Connects v e) + connects v e = (DisjointPair.from e ≟ v) ⊎-dec (DisjointPair.to e ≟ v) + + connects′ : (e : Edge) → (v : Vertex) → Dec (Connects v e) + connects′ e v = connects v e + + degree′ : (E : List Edge) → Vertex → ℕ + degree′ E v = length (filter (connects v) E) + + degree = degree′ E + + open ≡-Reasoning + + degree-split′ : + (e : Edge) (E : List Edge) (v : Vertex) → + degree′ (e ∷ E) v ≡ degree′ (e ∷ []) v + degree′ E v + degree-split′ e E v with does (connects v e) + ... | false = refl + ... | true = refl + + degree-split : + (e : Edge) (E : List Edge) (V : List Vertex) → + sum (map (degree′ (e ∷ E)) V) ≡ sum (map (degree′ (e ∷ [])) V) + sum (map (degree′ E) V) + degree-split e E [] = refl + degree-split e E (v ∷ V) = begin + degree′ (e ∷ E) v + sum (map (degree′ (e ∷ E)) V) ≡⟨ cong₂ _+_ {x = degree′ (e ∷ E) v} {y = degree′ (e ∷ []) v + degree′ E v} (degree-split′ e E v) (degree-split e E V) ⟩ + (degree′ (e ∷ []) v + degree′ E v) + (sum (map (degree′ (e ∷ [])) V) + sum (map (degree′ E) V)) ≡˘⟨ +-assoc (degree′ (e ∷ []) v + degree′ E v) (sum (map (degree′ (e ∷ [])) V)) (sum (map (degree′ E) V)) ⟩ + degree′ (e ∷ []) v + degree′ E v + sum (map (degree′ (e ∷ [])) V) + sum (map (degree′ E) V) ≡⟨ cong (_+ sum (map (degree′ E) V)) (+-assoc (degree′ (e ∷ []) v) (degree′ E v) (sum (map (degree′ (e ∷ [])) V))) ⟩ + degree′ (e ∷ []) v + (degree′ E v + sum (map (degree′ (e ∷ [])) V)) + sum (map (degree′ E) V) ≡⟨ cong (λ ◌ → degree′ (e ∷ []) v + ◌ + sum (map (degree′ E) V)) (+-comm (degree′ E v) (sum (map (degree′ (e ∷ [])) V))) ⟩ + degree′ (e ∷ []) v + (sum (map (degree′ (e ∷ [])) V) + degree′ E v) + sum (map (degree′ E) V) ≡˘⟨ cong (_+ sum (map (degree′ E) V)) (+-assoc (degree′ (e ∷ []) v) (sum (map (degree′ (e ∷ [])) V)) (degree′ E v)) ⟩ + degree′ (e ∷ []) v + sum (map (degree′ (e ∷ [])) V) + degree′ E v + sum (map (degree′ E) V) ≡⟨ +-assoc (degree′ (e ∷ []) v + sum (map (degree′ (e ∷ [])) V)) (degree′ E v) (sum (map (degree′ E) V)) ⟩ + (degree′ (e ∷ []) v + sum (map (degree′ (e ∷ [])) V)) + (degree′ E v + sum (map (degree′ E) V)) ∎ + + + degree-flip : (e : Edge) (V : List Vertex) → sum (map (degree′ (e ∷ [])) V) ≡ length (filter (connects′ e) V) + degree-flip e [] = refl + degree-flip e (v ∷ V) with does (connects v e) + ... | false = degree-flip e V + ... | true = cong suc (degree-flip e V) + + module _ where + degree-[_]′ : (e : Edge) → (∃[ k ] k ∈ filter (connects′ e) V) ↔ Fin 2 + degree-[ e ]′ = mk↔′ from to from-to to-from + where + from : ∃[ k ] k ∈ filter (connects′ e) V → Fin 2 + from (k , prf) with does (DisjointPair.from e ≟ k) + ... | true = zero + ... | false = suc zero + + to : Fin 2 → ∃[ k ] k ∈ filter (connects′ e) V + to zero = DisjointPair.from e , ∈-filter⁺ (connects′ e) (∈-allFin _) (inj₁ refl) + to (suc zero) = DisjointPair.to e , ∈-filter⁺ (connects′ e) (∈-allFin _) (inj₂ refl) + + from-to : (x : Fin 2) → from (to x) ≡ x + from-to zero with DisjointPair.from e ≟ DisjointPair.from e + ... | yes _ = refl + ... | no x≢x = ⊥-elim (x≢x refl) + from-to (suc zero) with DisjointPair.from e ≟ DisjointPair.to e + ... | yes x≡y = ⊥-elim (DisjointPair.diff e x≡y) + ... | no _ = refl + + open Injection using (injective) renaming (f to _⟨$⟩_) + + -- The only use of axiom K + ∈-tabulate-unique : + {n : ℕ} {A : Set} (uip : UIP A) (f : Fin n ↣ A) {x : A} (p q : x ∈ tabulate (f ⟨$⟩_)) → p ≡ q + ∈-tabulate-unique {suc n} uip f (here p) (here q) = cong here (uip p q) + ∈-tabulate-unique {suc n} uip f (here refl) (there q) = ⊥-elim (0≢1+n (cong toℕ (injective f (proj₂ (∈-tabulate⁻ q))))) + ∈-tabulate-unique {suc n} uip f (there p) (here refl) = ⊥-elim (0≢1+n (cong toℕ (injective f (proj₂ (∈-tabulate⁻ p))))) + ∈-tabulate-unique {suc n} uip f (there p) (there q) = cong there (∈-tabulate-unique uip (mk↣ (Fin.suc-injective ∘′ injective f)) p q) + + postulate + filter⁺-filter⁻ : + {A : Set} {P : A → Set} (P? : ∀ x → Dec (P x)) → + {v : A} (xs : List A) (i : v ∈ filter P? xs) → + uncurry (∈-filter⁺ P? {xs = xs}) (∈-filter⁻ P? i) ≡ i + + to-from : (x : ∃[ k ] k ∈ filter (connects′ e) V) → to (from x) ≡ x + to-from (k , prf) with DisjointPair.from e ≟ k + to-from (k , prf) | yes refl with ∈-filter⁻ (connects′ e) {xs = V} prf in filter⁻-eq + ... | k∈allFin , inj₁ p = cong (_ ,_) (begin + ∈-filter⁺ (connects′ e) (∈-allFin _) (inj₁ refl) ≡⟨ cong (λ ◌ → ∈-filter⁺ (connects′ e) ◌ (inj₁ refl)) (∈-tabulate-unique VertexUIP (mk↣ (λ eq → eq)) _ _) ⟩ + ∈-filter⁺ (connects′ e) k∈allFin (inj₁ refl) ≡⟨ cong (∈-filter⁺ (connects′ e) k∈allFin ∘′ inj₁) (VertexUIP refl p) ⟩ + ∈-filter⁺ (connects′ e) k∈allFin (inj₁ p) ≡˘⟨ cong (uncurry (∈-filter⁺ (connects′ e))) filter⁻-eq ⟩ + uncurry (∈-filter⁺ (connects′ e) {xs = V}) (∈-filter⁻ (connects′ e) prf) ≡⟨ filter⁺-filter⁻ (connects′ e) V prf ⟩ + prf ∎) + ... | k∈allFin , inj₂ k≡to = ⊥-elim (DisjointPair.diff e (sym k≡to)) + to-from (k , prf) | no k≢from with ∈-filter⁻ (connects′ e) {xs = V} prf in filter⁻-eq + ... | k∈allFin , inj₁ k≡from = ⊥-elim (k≢from k≡from) + ... | k∈allFin , inj₂ refl = cong (_ ,_) (begin + ∈-filter⁺ (connects′ e) (∈-allFin _) (inj₂ refl) ≡⟨ cong (λ ◌ → ∈-filter⁺ (connects′ e) ◌ (inj₂ refl)) (∈-tabulate-unique VertexUIP (mk↣ (λ eq → eq)) _ _) ⟩ + ∈-filter⁺ (connects′ e) k∈allFin (inj₂ refl) ≡˘⟨ cong (uncurry (∈-filter⁺ (connects′ e))) filter⁻-eq ⟩ + uncurry (∈-filter⁺ (connects′ e) {xs = V}) (∈-filter⁻ (connects′ e) prf) ≡⟨ filter⁺-filter⁻ (connects′ e) V prf ⟩ + prf ∎) + + postulate + degree-[_] : (e : Edge) → sum (map (degree′ (e ∷ [])) V) ≡ 2 + + handshaking′ : (E : List Edge) → sum (map (degree′ E) V) ≡ 2 * length E + handshaking′ [] = begin + sum (map (λ i → 0) V) ≡⟨ cong sum (map-tabulate {n = #V} (λ i → i) (λ _ → 0)) ⟩ + sum (tabulate {n = #V} (λ i → 0)) ≡⟨ sum-0 #V ⟩ + 0 ∎ + handshaking′ (e ∷ E) = begin + sum (map (degree′ (e ∷ E)) V) ≡⟨ degree-split e E V ⟩ + sum (map (degree′ (e ∷ [])) V) + sum (map (degree′ E) V) ≡⟨ cong₂ _+_ degree-[ e ] (handshaking′ E) ⟩ + 2 + 2 * length E ≡˘⟨ *-distribˡ-+ 2 1 (length E) ⟩ + 2 * (1 + length E) ∎ + + handshaking : sum (map degree V) ≡ 2 * length E + handshaking = handshaking′ E + +-- open import Data.Bool using (_∨_) +-- open import Data.Empty using (⊥-elim) +-- open import Data.Fin as Fin hiding (_+_) +-- import Data.Fin.Properties as Fin +-- open import Data.List as List hiding (map) +-- open import Data.List.Properties +-- open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise; []; _∷_) +-- import Data.List.Relation.Binary.Permutation.Setoid as Permutation +-- import Data.List.Relation.Binary.Permutation.Setoid.Properties as Permutation′ +-- open import Data.Nat using (ℕ; zero; suc; s≤s; _*_; _+_) +-- open import Data.Nat.Properties hiding (_≟_) +-- open import Data.Product hiding (map) +-- open import Data.Sum hiding (map) +-- open import Data.Vec as Vec using (Vec; []; _∷_) + +-- open import Function.Base using (_∘′_; _|>_) +-- open import Function.Bundles using (Injection; _↣_; mk↣) + +-- -- open import Relation.Binary.Consequences u +-- open import Relation.Binary.Bundles using (Setoid) +-- open import Relation.Binary.Definitions using (Irreflexive; Trichotomous; tri<; tri≈; tri>) +-- open import Relation.Binary.PropositionalEquality +-- open import Relation.Nullary + +-- -- copied in here because latest stable stdlib doesn't have it?? +-- _⊎-dec_ : ∀{A B : Set} → Dec A → Dec B → Dec (A ⊎ B) +-- does (a? ⊎-dec b?) = does a? ∨ does b? +-- proof (a? ⊎-dec b?) with proof a? +-- ... | ofʸ p = ofʸ (inj₁ p) +-- ... | ofⁿ ¬p with proof b? +-- ... | ofʸ p = ofʸ (inj₂ p) +-- ... | ofⁿ ¬p₁ = ofⁿ (λ { (inj₁ q) → ¬p q; (inj₂ q) → ¬p₁ q }) + +-- infix 6 _⨾_⨾_ + +-- record DisjointPair (A : Set) : Set where +-- constructor _⨾_⨾_ +-- field +-- from : A +-- to : A +-- diff : from ≢ to + +-- data _≐_ {A : Set} : DisjointPair A → DisjointPair A → Set where +-- refl : ∀ {x y diff diff′} → (x ⨾ y ⨾ diff) ≐ (x ⨾ y ⨾ diff′) +-- transpose : ∀ {x y diff diff′} → (x ⨾ y ⨾ diff) ≐ (y ⨾ x ⨾ diff′) + +-- ≐-setoid : (A : Set) → Setoid _ _ +-- ≐-setoid A = record +-- { Carrier = DisjointPair A +-- ; _≈_ = _≐_ +-- ; isEquivalence = record +-- { refl = refl +-- ; sym = (λ { refl → refl ; transpose → transpose }) +-- ; trans = λ +-- { refl refl → refl +-- ; refl transpose → transpose +-- ; transpose refl → transpose +-- ; transpose transpose → refl +-- } +-- } +-- } + +-- -- Variant of DisjointPair for forcing an order + +-- record OrderedPair (A : Set) (_<_ : A → A → Set) : Set where +-- constructor _⨾_⨾_ +-- field +-- from : A +-- to : A +-- ord : from < to + +-- module Pair where +-- open DisjointPair +-- open Injection renaming (f to _⟨$⟩_) + +-- map : {A B : Set} → A ↣ B → DisjointPair A → DisjointPair B +-- map f p .from = f ⟨$⟩ p .from +-- map f p .to = f ⟨$⟩ p .to +-- map f p .diff = p .diff ∘′ injective f + +-- order : +-- {A : Set} {_<_ : A → A → Set} → +-- Trichotomous _≡_ _<_ → DisjointPair A → OrderedPair A _<_ +-- order compare (from ⨾ to ⨾ diff) with compare from to +-- ... | tri< f _ _ f>t = to ⨾ from ⨾ f>t + +-- forget : +-- {A : Set} {_<_ : A → A → Set} → +-- Irreflexive _≡_ _<_ → OrderedPair A _<_ → DisjointPair A +-- forget irrefl (from ⨾ to ⨾ ord) = from ⨾ to ⨾ λ eq → irrefl eq ord + +-- forget∘order : +-- {A : Set} {_<_ : A → A → Set} → +-- (cmp : Trichotomous _≡_ _<_) (irrefl : Irreflexive _≡_ _<_) (p : DisjointPair A) → +-- forget irrefl (order cmp p) ≐ p +-- forget∘order cmp irrefl (from ⨾ to ⨾ diff) with cmp from to +-- ... | tri< f _ _ f>t = transpose + +-- -- Multigraphs built inductively + +-- private +-- variable n : ℕ + +-- Vertex : ℕ → Set +-- Vertex = Fin + +-- Edge : ℕ → Set +-- Edge n = DisjointPair (Vertex n) + +-- OEdge : ℕ → Set +-- OEdge n = OrderedPair (Vertex n) _<_ + +-- open module ↭′ n = Permutation (≐-setoid (Vertex n)) using () renaming (_↭_ to [_]_↭_) +-- open module ↭′′ {n} = Permutation (≐-setoid (Vertex n)) hiding (_↭_) +-- module ↭ {n} = Permutation′ (≐-setoid (Vertex n)) + +-- module Graph where +-- data Graph : ℕ → Set where +-- [] : Graph 0 +-- _∷_ : Vec ℕ n → Graph n → Graph (suc n) + +-- -- Empty graph +-- empty : (n : ℕ) → Graph n +-- empty zero = [] +-- empty (suc n) = Vec.replicate 0 ∷ empty n + +-- -- Obtain list of edges + +-- edges′′ : ∀ {k} → Vec ℕ n → Vec (Vertex k) n → List (Edge (suc k)) +-- edges′′ es is = +-- Vec.zipWith (λ n i → replicate n (zero ⨾ suc i ⨾ λ ())) es is |> +-- Vec.toList |> +-- concat + +-- edges′ : Vec ℕ n → List (Edge (suc n)) +-- edges′ es = edges′′ es (Vec.allFin _) + +-- step-edges : List (Edge n) → List (Edge (suc n)) +-- step-edges = List.map (Pair.map (mk↣ Fin.suc-injective)) + +-- edges : Graph n → List (Edge n) +-- edges [] = [] +-- edges (es ∷ g) = edges′ es ++ step-edges (edges g) + +-- -- Degree of a node + +-- degree : Graph n → Vertex n → ℕ +-- degree (es ∷ g) zero = Vec.sum es +-- degree (es ∷ g) (suc i) = Vec.lookup es i + degree g i + +-- -- Easy version of handshaking + +-- Handshake : Graph n → Set +-- Handshake {n} g = sum (List.map (degree g) (allFin n)) ≡ 2 * length (edges g) + +-- handshaking-empty : (n : ℕ) → Handshake (empty n) +-- handshaking-empty zero = refl +-- handshaking-empty (suc n) = {!begin +-- Vec.sum ? + sum (List.map (degree (Vec.replicate 0))) ≡⟨ ? ⟩ +-- ? ∎!} +-- where open ≡-Reasoning +-- -- handshaking : (g : Graph n) → sum (List.map (degree g) (allFin n)) ≡ 2 * length (edges g) +-- -- handshaking [] = refl +-- -- handshaking (es ∷ g) = {!begin +-- -- Vec.sum es + sum (List.map (degree (es ∷ g) ))!} +-- -- where open ≡-Reasoning + +-- -- Add an edge to a graph + +-- infixr 5 _∷ᵉ_ + +-- _∷ᵉ_ : OEdge n → Graph n → Graph n +-- (zero ⨾ suc to ⨾ ord) ∷ᵉ (xs ∷ g) = xs Vec.[ to ]%= suc ∷ g +-- (suc from ⨾ suc to ⨾ s≤s ord) ∷ᵉ (xs ∷ g) = xs ∷ (from ⨾ to ⨾ ord ∷ᵉ g) + +-- -- Construction from edges + +-- private +-- order′ : Edge n → OEdge n +-- order′ = Pair.order Fin.<-cmp + +-- forget′ : OEdge n → Edge n +-- forget′ = Pair.forget Fin.<-irrefl + +-- forget′∘order′ : (e : Edge n) → forget′ (order′ e) ≐ e +-- forget′∘order′ = Pair.forget∘order Fin.<-cmp Fin.<-irrefl + +-- fromEdges : List (Edge n) → Graph n +-- fromEdges es = foldr (λ e g → order′ e ∷ᵉ g) (empty _) es + +-- step-edges-↭ : +-- {es es′ : List (Edge n)} → +-- [ n ] es ↭ es′ → [ suc n ] step-edges es ↭ step-edges es′ +-- step-edges-↭ es↭es′ = +-- ↭.map⁺ (≐-setoid (Vertex (suc _))) (λ { refl → refl ; transpose → transpose }) es↭es′ + +-- edges′′⁻¹-[] : ∀ {k n} (is : Vec (Vertex n) k) → edges′′ (Vec.replicate 0) is ≡ [] +-- edges′′⁻¹-[] [] = refl +-- edges′′⁻¹-[] (i ∷ is) = edges′′⁻¹-[] is + +-- edges′′⁻¹-∷ : ∀ {k n} (es : Vec ℕ k) (is : Vec (Vertex n) k) (j : Fin k) → +-- [ suc n ] +-- edges′′ (es Vec.[ j ]%= suc) is +-- ↭ +-- (zero ⨾ suc (Vec.lookup is j) ⨾ λ ()) ∷ edges′′ es is +-- edges′′⁻¹-∷ (e ∷ es) (i ∷ is) zero = ↭-refl +-- edges′′⁻¹-∷ (e ∷ es) (i ∷ is) (suc j) = begin +-- edges′′ (e ∷ es Vec.[ j ]%= suc) (i ∷ is) ≡⟨⟩ +-- replicate e (zero ⨾ suc i ⨾ λ ()) ++ edges′′ (es Vec.[ j ]%= suc) is ↭⟨ ↭.++⁺ˡ (replicate e (zero ⨾ suc i ⨾ λ ())) (edges′′⁻¹-∷ es is j) ⟩ +-- replicate e (zero ⨾ suc i ⨾ λ ()) ++ (zero ⨾ suc k ⨾ λ ()) ∷ edges′′ es is ↭⟨ ↭.↭-shift (replicate e (zero ⨾ suc i ⨾ λ ())) (edges′′ es is) ⟩ +-- (zero ⨾ suc k ⨾ λ ()) ∷ replicate e (zero ⨾ suc i ⨾ λ ()) ++ edges′′ es is ≡⟨⟩ +-- (zero ⨾ suc k ⨾ λ ()) ∷ edges′′ (e ∷ es) (i ∷ is) ∎ +-- where +-- open PermutationReasoning +-- k = Vec.lookup is j + +-- edges′⁻¹-[] : (n : ℕ) → edges′ {n} (Vec.replicate 0) ≡ [] +-- edges′⁻¹-[] n = edges′′⁻¹-[] (Vec.allFin n) + +-- edges′⁻¹-∷ : +-- (es : Vec ℕ n) (to : Vertex n) → +-- [ suc n ] edges′ (es Vec.[ to ]%= suc) ↭ (zero ⨾ suc to ⨾ λ ()) ∷ edges′ es +-- edges′⁻¹-∷ es to = begin +-- edges′ (es Vec.[ to ]%= suc) ↭⟨ edges′′⁻¹-∷ es (Vec.allFin _) to ⟩ +-- (zero ⨾ suc (Vec.lookup (Vec.allFin _) to) ⨾ λ ()) ∷ edges′ es ≡⟨ cong (λ ◌ → (zero ⨾ suc ◌ ⨾ (λ ())) ∷ edges′ es) (Vec-lookup-tabulate (λ i → i) to) ⟩ +-- (zero ⨾ suc to ⨾ λ ()) ∷ edges′ es ∎ +-- where +-- open PermutationReasoning +-- Vec-lookup-tabulate : +-- {A : Set} (f : Fin n → A) (i : Fin n) → Vec.lookup (Vec.tabulate f) i ≡ f i +-- Vec-lookup-tabulate f zero = refl +-- Vec-lookup-tabulate f (suc i) = Vec-lookup-tabulate (f ∘′ suc) i + +-- edges⁻¹-[] : (n : ℕ) → edges (empty n) ≡ [] +-- edges⁻¹-[] zero = refl +-- edges⁻¹-[] (suc n) = cong₂ (λ ◌ᵃ ◌ᵇ → ◌ᵃ ++ step-edges ◌ᵇ) (edges′⁻¹-[] n) (edges⁻¹-[] n) + +-- edges⁻¹-∷ : (e : OEdge n) (g : Graph n) → [ n ] edges (e ∷ᵉ g) ↭ forget′ e ∷ edges g +-- edges⁻¹-∷ (zero ⨾ suc to ⨾ ord) (xs ∷ g) = ↭.++⁺ʳ (step-edges (edges g)) (begin +-- edges′ (xs Vec.[ to ]%= suc) ↭⟨ edges′⁻¹-∷ xs to ⟩ +-- (zero ⨾ suc to ⨾ _ ∷ edges′ xs) ≋⟨ refl ∷ Pointwise.refl refl ⟩ +-- zero ⨾ suc to ⨾ _ ∷ edges′ xs ∎) +-- where open PermutationReasoning +-- edges⁻¹-∷ (suc from ⨾ suc to ⨾ s≤s ord) (xs ∷ g) = begin +-- edges′ xs ++ step-edges (edges (from ⨾ to ⨾ ord ∷ᵉ g)) ↭⟨ ↭.++⁺ˡ (edges′ xs) (step-edges-↭ (edges⁻¹-∷ (from ⨾ to ⨾ ord) g)) ⟩ +-- edges′ xs ++ step-edges (from ⨾ to ⨾ diff ∷ edges g) ≡⟨⟩ +-- edges′ xs ++ (suc from ⨾ suc to ⨾ _) ∷ step-edges (edges g) ↭⟨ ↭.↭-shift (edges′ xs) (step-edges (edges g)) ⟩ +-- (suc from ⨾ suc to ⨾ _ ∷ edges′ xs ++ step-edges (edges g)) ≋⟨ refl ∷ Pointwise.refl refl ⟩ +-- suc from ⨾ suc to ⨾ _ ∷ edges′ xs ++ step-edges (edges g) ∎ +-- where +-- open PermutationReasoning +-- diff = λ eq → Fin.<-irrefl eq ord + +-- edges⁻¹ : (es : List (Edge n)) → [ n ] edges (fromEdges es) ↭ es +-- edges⁻¹ [] = ↭-reflexive (edges⁻¹-[] _) +-- edges⁻¹ (e ∷ es) = begin +-- edges (order′ e ∷ᵉ fromEdges es) ↭⟨ edges⁻¹-∷ (order′ e) (fromEdges es) ⟩ +-- (forget′ (order′ e) ∷ edges (fromEdges es)) ≋⟨ forget′∘order′ e ∷ Pointwise.refl refl ⟩ +-- e ∷ edges (fromEdges es) <⟨ edges⁻¹ es ⟩ +-- e ∷ es ∎ +-- where open PermutationReasoning + +-- -- Multigraphs as defined by the problem +-- -- I've rearranged the definitions to make things easier to prove + +-- Connects : Vertex n → Edge n → Set +-- Connects v e = DisjointPair.from e ≡ v ⊎ DisjointPair.to e ≡ v + +-- connects : (v : Vertex n) → (e : Edge n) → Dec (Connects v e) +-- connects v e = (DisjointPair.from e ≟ v) ⊎-dec (DisjointPair.to e ≟ v) + +-- degree′ : (E : List (Edge n)) → Vertex n → ℕ +-- degree′ E v = length (filter (connects v) E) + +-- record MultiGraph : Set where +-- field +-- #V : ℕ +-- E : List (Edge #V) + +-- V : List (Vertex #V) +-- V = allFin #V + +-- degree = degree′ E + +-- handshaking : sum (List.map degree V) ≡ 2 * length E +-- handshaking = {!!} diff --git a/src/Problem13.agda b/src/Problem13.agda new file mode 100644 index 0000000..53cc178 --- /dev/null +++ b/src/Problem13.agda @@ -0,0 +1,93 @@ +{-# OPTIONS --safe #-} + +module Problem13 where + +open import Data.Empty using (⊥-elim) +open import Data.Fin hiding (_≟_; _+_; _<_; _>_; _≤_) +open import Data.Fin.Properties hiding (_≟_; ≤-trans) +open import Data.Nat +open import Data.Nat.DivMod +open import Data.Nat.Properties +open import Data.Product +open import Data.Unit using (tt) +open import Data.Vec +open import Function.Base using (_$′_) +open import Relation.Nullary.Decidable +open import Relation.Binary.PropositionalEquality + +open ≤-Reasoning renaming (begin_ to begin-≤_) + +okToDivide : ∀ n → n > 1 → False (n ≟ 0) +okToDivide (suc n) p = tt + +toRadix : (n : ℕ)(nz : n > 1) → (f : ℕ) → ℕ → Vec (Fin n) f +toRadix n nz zero k = [] +toRadix n nz (suc f) k with (k divMod n) {okToDivide _ nz} +... | result q r prf₂ = r ∷ toRadix n nz f q + +fromRadix : (n : ℕ) {f : ℕ} → Vec (Fin n) f → ℕ +fromRadix n [] = 0 +fromRadix n (x ∷ xs) = toℕ x + n * fromRadix n xs + +goal₁ : (n : ℕ)(nz : n > 1){f : ℕ}(num : Vec (Fin n) f) + → toRadix n nz f (fromRadix n num) ≡ num +goal₁ n nz [] = refl +goal₁ n nz (x ∷ xs) with ((toℕ x + n * fromRadix n xs) divMod n) {okToDivide _ nz} +... | result q r prf = + let (prf₁ , prf₂) = invertProof x r (fromRadix n xs) q prf in + cong₂ _∷_ (sym prf₁) (trans (sym (cong (toRadix n nz _) prf₂)) (goal₁ n nz xs)) + where + invertProof : (x y : Fin n) (p q : ℕ) → toℕ x + n * p ≡ toℕ y + q * n → x ≡ y × p ≡ q + invertProof x y zero zero prf .proj₁ = + toℕ-injective $′ +-cancelʳ-≡ (toℕ x) (toℕ y) $′ begin-equality + toℕ x + n * zero ≡⟨ prf ⟩ + toℕ y + zero ≡˘⟨ cong (toℕ y +_) (*-zeroʳ n) ⟩ + toℕ y + n * zero ∎ + invertProof x y zero zero prf .proj₂ = refl + invertProof x y zero (suc q) prf = + ⊥-elim $′ <⇒≱ (toℕ 1)(f : ℕ)(k : ℕ)(p : k < n ^ f) + → fromRadix n (toRadix n nz f k) ≡ k +goal₂ n nz zero k k>=_; map) +open import Function +open import Relation.Binary.PropositionalEquality + +open ≡-Reasoning + +data Expr (V : Set) : Set where + λ′_ : Expr (Maybe V) → Expr V + _·_ : Expr V → Expr V → Expr V + var : V → Expr V + +variable V A B C D : Set + +map : (A → B) → Expr A → Expr B +map f (λ′ e) = λ′ map (Maybe.map f) e +map f (e · a) = map f e · map f a +map f (var x) = var (f x) + +_>>=_ : Expr A → (A → Expr B) → Expr B +(λ′ e) >>= f = λ′ (e >>= maybe (map just ∘ f) (var nothing)) +(e · e₁) >>= f = (e >>= f) · (e₁ >>= f) +var x >>= f = f x + +-- Lean users have the advantage of functional extensionality, but Agda users don't +-- So I have provided these congruence lemmas so that Agda users are at no axiomatic disadvantage. + +map-cong : ∀{f g : A → B}(ma : Expr A) → (∀ x → f x ≡ g x) → map f ma ≡ map g ma +map-cong (λ′ ma) eq = cong λ′_ (map-cong ma λ { nothing → refl ; (just x) → cong just (eq x) }) +map-cong (ma · ma₁) eq = cong₂ _·_ (map-cong ma eq) (map-cong ma₁ eq) +map-cong (var x) eq = cong var (eq x) + +>>=-cong : ∀{f g : A → Expr B}(ma : Expr A) → (∀ x → f x ≡ g x) → ma >>= f ≡ ma >>= g +>>=-cong (λ′ ma) eq = cong λ′_ (>>=-cong ma λ { nothing → refl ; (just x) → cong (map just) (eq x) }) +>>=-cong (ma · ma₁) eq = cong₂ _·_ (>>=-cong ma eq) (>>=-cong ma₁ eq) +>>=-cong (var x) eq = eq x + +-- Functor Laws + +map-id : (ma : Expr A) → map id ma ≡ ma +map-id (λ′ ma) = cong λ′_ (begin + map (Maybe.map id) ma ≡⟨ map-cong ma (λ { (just a) → refl ; nothing → refl }) ⟩ + map id ma ≡⟨ map-id ma ⟩ + ma ∎) +map-id (ma · ma₁) = cong₂ _·_ (map-id ma) (map-id ma₁) +map-id (var x) = refl + +map-homo : (f : B → C) (g : A → B) (ma : Expr A) → map f (map g ma) ≡ map (f ∘ g) ma +map-homo f g (λ′ ma) = cong λ′_ (begin + map (Maybe.map f) (map (Maybe.map g) ma) ≡⟨ map-homo (Maybe.map f) (Maybe.map g) ma ⟩ + map (Maybe.map f ∘ Maybe.map g) ma ≡⟨ map-cong ma (λ { (just a) → refl ; nothing → refl }) ⟩ + map (Maybe.map (f ∘ g)) ma ∎) +map-homo f g (ma · ma₁) = cong₂ _·_ (map-homo f g ma) (map-homo f g ma₁) +map-homo f g (var x) = refl + +-- Bind-var is map + +>>=-var : (f : A → B) (ma : Expr A) → ma >>= (var ∘ f) ≡ map f ma +>>=-var f (λ′ ma) = cong λ′_ (begin + ma >>= maybe (var ∘ just ∘ f) (var nothing) ≡⟨ >>=-cong ma (λ { (just a) → refl ; nothing → refl }) ⟩ + ma >>= (var ∘ Maybe.map f) ≡⟨ >>=-var (Maybe.map f) ma ⟩ + map (Maybe.map f) ma ∎) +>>=-var f (ma · ma₁) = cong₂ _·_ (>>=-var f ma) (>>=-var f ma₁) +>>=-var f (var x) = refl + +>>=-assoc : (g : B → C) (f : A → Expr B) (ma : Expr A) → map g (ma >>= f) ≡ ma >>= (map g ∘ f) +>>=-assoc g f (λ′ ma) = cong λ′_ (begin + map (Maybe.map g) (ma >>= maybe (map just ∘ f) (var nothing)) ≡⟨ >>=-assoc (Maybe.map g) (maybe (map just ∘ f) (var nothing)) ma ⟩ + ma >>= (map (Maybe.map g) ∘ maybe (map just ∘ f) (var nothing)) ≡⟨ >>=-cong ma (λ { (just a) → map-homo (Maybe.map g) just (f a) ; nothing → refl }) ⟩ + ma >>= maybe (map (Maybe.map g ∘ just) ∘ f) (var nothing) ≡˘⟨ >>=-cong ma (λ { (just a) → map-homo just g (f a) ; nothing → refl }) ⟩ + ma >>= maybe (map just ∘ map g ∘ f) (var nothing) ∎) +>>=-assoc g f (ma · ma₁) = cong₂ _·_ (>>=-assoc g f ma) (>>=-assoc g f ma₁) +>>=-assoc g f (var x) = refl + +>>=-lift : (f : A → B) (g : B → Expr C) (h : A → Expr C) → g ∘ f ≗ h → (ma : Expr A) → map f ma >>= g ≡ ma >>= h +>>=-lift f g h gf≗h (λ′ ma) = cong λ′_ (>>=-lift _ _ _ (λ { (just a) → cong (map just) (gf≗h a) ; nothing → refl }) ma) +>>=-lift f g h gf≗h (ma · ma₁) = cong₂ _·_ (>>=-lift f g h gf≗h ma) (>>=-lift f g h gf≗h ma₁) +>>=-lift f g h gf≗h (var x) = gf≗h x + +assoc : ∀(g : A → Expr B)(h : B → Expr C)(a : Expr A) + → a >>= (λ a′ → g a′ >>= h) ≡ (a >>= g) >>= h +assoc g h (λ′ ma) = cong λ′_ (begin + ma >>= maybe (λ a → map just (g a >>= h)) (var nothing) ≡⟨ >>=-cong ma (λ { (just a) → lemma a ; nothing → refl }) ⟩ + (ma >>= (λ a → maybe (map just ∘ g) (var nothing) a >>= maybe (map just ∘ h) (var nothing))) ≡⟨ assoc (maybe (map just ∘ g) (var nothing)) (maybe (map just ∘ h) (var nothing)) ma ⟩ + (ma >>= maybe (map just ∘ g) (var nothing)) >>= maybe (map just ∘ h) (var nothing) ∎) + where + lemma : (a : _) → map just (g a >>= h) ≡ map just (g a) >>= maybe (map just ∘ h) (var nothing) + lemma a = begin + map just (g a >>= h) ≡⟨ >>=-assoc just h (g a) ⟩ + g a >>= (map just ∘ h) ≡˘⟨ >>=-lift just (maybe (map just ∘ h) (var nothing)) (map just ∘ h) (λ _ → refl) (g a) ⟩ + map just (g a) >>= maybe (map just ∘ h) (var nothing) ∎ +assoc g h (ma · ma₁) = cong₂ _·_ (assoc g h ma) (assoc g h ma₁) +assoc g h (var x) = refl + +identₗ : ∀(f : A → Expr B)(x : A) → var x >>= f ≡ f x +identₗ _ _ = refl + +identᵣ : ∀(e : Expr A) → e >>= var ≡ e +identᵣ e = begin + e >>= var ≡⟨ >>=-var id e ⟩ + map id e ≡⟨ map-id e ⟩ + e ∎ diff --git a/src/Problem21.agda b/src/Problem21.agda new file mode 100644 index 0000000..e5d27e2 --- /dev/null +++ b/src/Problem21.agda @@ -0,0 +1,80 @@ +{-# OPTIONS --safe #-} + +module Problem21 (Atom : Set) where + +open import Data.List +open import Relation.Binary.PropositionalEquality hiding ([_]) +open import Data.Empty +open import Data.Nat +open import Data.Fin +open import Data.Fin.Patterns +open import Data.Product + +data L : Set where + ⟨_⟩ : Atom → L + ⟨_⟩ᶜ : Atom → L + _⊗_ : L → L → L + _⅋_ : L → L → L + ⊥' : L + 𝟙 : L + +variable A B C : L +variable Δ Γ : List L +variable α β η : Atom + +_ᶜ : L → L +⟨ A ⟩ ᶜ = ⟨ A ⟩ᶜ +⟨ A ⟩ᶜ ᶜ = ⟨ A ⟩ +(A ⊗ B) ᶜ = (A ᶜ) ⅋ (B ᶜ) +(A ⅋ B) ᶜ = (A ᶜ) ⊗ (B ᶜ) +𝟙 ᶜ = ⊥' +⊥' ᶜ = 𝟙 + +_⊸_ : L → L → L +A ⊸ B = (A ᶜ) ⅋ B + +infixl 2 ⊢_ +data ⊢_ : List L → Set where + one : ⊢ [ 𝟙 ] + identity : ⊢ ⟨ α ⟩ ∷ ⟨ α ⟩ᶜ ∷ [] + exch : (n : Fin (length Δ)) + → ⊢ lookup Δ n ∷ (Δ ─ n) + → ⊢ Δ + times : (n : ℕ) + → ⊢ A ∷ take n Δ + → ⊢ B ∷ drop n Δ + → ⊢ A ⊗ B ∷ Δ + par : ⊢ A ∷ B ∷ Δ + → ⊢ A ⅋ B ∷ Δ + bottom : ⊢ Δ + → ⊢ ⊥' ∷ Δ + + cut : ⊢ A ∷ Δ + → ⊢ A ᶜ ∷ Γ + → ⊢ Δ ++ Γ + +id : {A : L} → ⊢ A ∷ A ᶜ ∷ [] +id {⟨ x ⟩} = identity +id {⟨ x ⟩ᶜ} = exch 1F identity +id {A ⊗ B} = exch 1F (par (exch 2F (times 1 (id {A}) (id {B})))) +id {A ⅋ B} = par (exch 2F (times 1 (exch 1F (id {A})) (exch 1F (id {B})))) +id {⊥'} = bottom one +id {𝟙} = exch 1F (bottom one) + +id′ : {A : L} → ⊢ A ᶜ ∷ A ∷ [] +id′ = exch 1F id + +_≈_ : L → L → Set +A ≈ B = (⊢ [ A ] → ⊢ [ B ]) × (⊢ [ B ] → ⊢ [ A ]) + +lem₁ : ((A ⊗ B) ⊸ C) ≈ (A ⊸ (B ⊸ C)) +lem₁ .proj₁ prf = cut prf (exch 1F (par (exch 1F (par (exch 2F (exch 3F (times 2 (times 1 id′ id′) id′))))))) +lem₁ .proj₂ prf = cut prf (exch 1F (par (par (exch 3F (times 1 id′ (times 1 id′ id′)))))) + +lem₂ : (A ⊸ (B ⅋ C)) ≈ ((A ⊸ B) ⅋ C) +lem₂ .proj₁ prf = cut prf (exch 1F (par (par (exch 3F (times 1 id′ (times 1 id′ id′)))))) +lem₂ .proj₂ prf = cut prf (exch 1F (par (exch 1F (par (exch 2F (exch 3F (times 2 (times 1 id′ id′) id′))))))) + +lem₃ : (A ⊸ B) ≈ ((B ᶜ) ⊸ (A ᶜ)) +lem₃ .proj₁ prf = cut prf (exch 1F (par (exch 1F (exch 2F (times 1 id′ id))))) +lem₃ .proj₂ prf = cut prf (exch 1F (par (exch 1F (exch 2F (times 1 (exch 1F (cut id′ id)) id′))))) diff --git a/src/Problem22.agda b/src/Problem22.agda new file mode 100644 index 0000000..a4befd8 --- /dev/null +++ b/src/Problem22.agda @@ -0,0 +1,87 @@ +{-# OPTIONS --safe #-} + +module Problem22 + (Act : Set) + (State : Set) + (_─⟨_⟩→_ : State → Act → State → Set) where + +open import Data.Empty +open import Data.Product +open import Data.Unit +open import Function.Base using (_∘′_) +open import Level +open import Relation.Binary.PropositionalEquality + +variable ℓ : Level +variable α β γ : Act +variable x x′ y y′ z : State + +record Bisimulation(R : State → State → Set ℓ) : Set ℓ where + constructor B + field + left : R x y → x ─⟨ α ⟩→ x′ → ∃[ y′ ] (y ─⟨ α ⟩→ y′ × R x′ y′) + right : R x y → y ─⟨ α ⟩→ y′ → ∃[ x′ ] (x ─⟨ α ⟩→ x′ × R x′ y′) + +open Bisimulation + +_≈_ : State → State → Set₁ +x ≈ y = ∃[ R ] (Bisimulation R × R x y) + +reflexive : x ≈ x +reflexive .proj₁ = _≡_ +reflexive .proj₂ .proj₁ .left refl step = _ , step , refl +reflexive .proj₂ .proj₁ .right refl step = _ , step , refl +reflexive .proj₂ .proj₂ = refl + +symmetric : x ≈ y → y ≈ x +symmetric x≈y .proj₁ x y = x≈y .proj₁ y x +symmetric x≈y .proj₂ .proj₁ .left = x≈y .proj₂ .proj₁ .right +symmetric x≈y .proj₂ .proj₁ .right = x≈y .proj₂ .proj₁ .left +symmetric x≈y .proj₂ .proj₂ = x≈y .proj₂ .proj₂ + +transitive : x ≈ y → y ≈ z → x ≈ z +transitive x≈y y≈z .proj₁ x z = ∃[ y ] x≈y .proj₁ x y × y≈z .proj₁ y z +transitive x≈y y≈z .proj₂ .proj₁ .left (_ , rel₁ , rel₂) stepˡ = + let _ , stepᵐ , rel₁′ = x≈y .proj₂ .proj₁ .left rel₁ stepˡ in + let _ , stepʳ , rel₂′ = y≈z .proj₂ .proj₁ .left rel₂ stepᵐ in + _ , stepʳ , _ , rel₁′ , rel₂′ +transitive x≈y y≈z .proj₂ .proj₁ .right (_ , rel₁ , rel₂) stepʳ = + let _ , stepᵐ , rel₂′ = y≈z .proj₂ .proj₁ .right rel₂ stepʳ in + let _ , stepˡ , rel₁′ = x≈y .proj₂ .proj₁ .right rel₁ stepᵐ in + _ , stepˡ , _ , rel₁′ , rel₂′ +transitive x≈y y≈z .proj₂ .proj₂ = _ , x≈y .proj₂ .proj₂ , y≈z .proj₂ .proj₂ + +bisim-is-bisim : Bisimulation _≈_ +bisim-is-bisim .left (R , bisim , x≈y) stepˡ = + let (y′ , stepʳ , x′≈y′) = bisim .left x≈y stepˡ in + y′ , stepʳ , R , bisim , x′≈y′ +bisim-is-bisim .right (R , bisim , x≈y) stepʳ = + let (x′ , stepˡ , x′≈y′) = bisim .right x≈y stepʳ in + x′ , stepˡ , R , bisim , x′≈y′ + +data HML : Set where + ⟪_⟫_ : Act → HML → HML + ⟦_⟧_ : Act → HML → HML + _∧_ : HML → HML → HML + ⊤′ : HML + ¬′_ : HML → HML + +variable ϕ ψ : HML +infixl 10 _⊧_ +_⊧_ : State → HML → Set +σ ⊧ ⊤′ = ⊤ +σ ⊧ ¬′ ϕ = σ ⊧ ϕ → ⊥ +σ ⊧ ϕ ∧ ψ = (σ ⊧ ϕ) × (σ ⊧ ψ) +σ ⊧ ⟪ α ⟫ ϕ = ∃[ σ′ ] σ ─⟨ α ⟩→ σ′ × σ′ ⊧ ϕ +σ ⊧ ⟦ α ⟧ ϕ = ∀ σ′ → σ ─⟨ α ⟩→ σ′ → σ′ ⊧ ϕ + +hml-bisim : ∀ ϕ → x ≈ y → x ⊧ ϕ → y ⊧ ϕ +hml-bisim ⊤′ (R , bisim , x≈y) prf = prf +hml-bisim (¬′ ϕ) (R , bisim , x≈y) prf = prf ∘′ hml-bisim ϕ (symmetric (R , bisim , x≈y)) +hml-bisim (ϕ ∧ ψ) (R , bisim , x≈y) (prf , prf₁) = hml-bisim ϕ (R , bisim , x≈y) prf , hml-bisim ψ (R , bisim , x≈y) prf₁ +hml-bisim (⟪ a ⟫ ϕ) (R , bisim , x≈y) (x′ , stepˡ , prf) = + let (y′ , stepʳ , x′≈y′) = bisim .left x≈y stepˡ in + y′ , stepʳ , hml-bisim ϕ (R , bisim , x′≈y′) prf +hml-bisim (⟦ a ⟧ ϕ) (R , bisim , x≈y) prf y′ stepʳ = + let (x′ , stepˡ , x′≈y′) = bisim .right x≈y stepʳ in + hml-bisim ϕ (R , bisim , x′≈y′) (prf x′ stepˡ) diff --git a/src/Problem23.agda b/src/Problem23.agda new file mode 100644 index 0000000..6ee5faf --- /dev/null +++ b/src/Problem23.agda @@ -0,0 +1,136 @@ +{-# OPTIONS --safe #-} + +module Problem23 where + +open import Data.List +open import Data.List.Properties +open import Data.Fin using (fromℕ<) +open import Data.Fin.Properties using (fromℕ<-cong) +open import Data.Empty +open import Data.Nat +open import Data.Nat.Properties +open import Data.Product +open import Function +open import Relation.Binary.PropositionalEquality +open import Relation.Nullary +open import Relation.Nullary.Negation + +open ≡-Reasoning + + +variable State : Set +variable f : State → State + +Assertion : Set → Set₁ +Assertion State = State → Set +variable ϕ ϕ′ ψ ψ′ π g : Assertion State + +_∧_ : Assertion State → Assertion State → Assertion State +ϕ ∧ ψ = λ σ → ϕ σ × ψ σ + +¬'_ : Assertion State → Assertion State +¬' ϕ = λ σ → (ϕ σ → ⊥) + +_⇒_ : Assertion State → Assertion State → Set +ϕ ⇒ ψ = ∀ σ → ϕ σ → ψ σ + +data Program (State : Set) : Set₁ where + SKIP : Program State + IF_THEN_ELSE_FI : Assertion State → Program State → Program State → Program State + WHILE_DO_OD : Assertion State → Program State → Program State + _∶_ : Program State → Program State → Program State + UPD : (State → State) → Program State + +infixl 5 _∶_ + +variable P Q : Program State + +data ⟨_⟩_⟨_⟩ {State : Set} : Assertion State → Program State → Assertion State → Set₁ where + skipₕ : ⟨ ϕ ⟩ SKIP ⟨ ϕ ⟩ + ifₕ : ⟨ ϕ ∧ g ⟩ P ⟨ ψ ⟩ → ⟨ ϕ ∧ (¬' g) ⟩ Q ⟨ ψ ⟩ → ⟨ ϕ ⟩ IF g THEN P ELSE Q FI ⟨ ψ ⟩ + whileₕ : ⟨ ϕ ∧ g ⟩ P ⟨ ϕ ⟩ → ⟨ ϕ ⟩ WHILE g DO P OD ⟨ ϕ ∧ (¬' g) ⟩ + seqₕ : ⟨ ϕ ⟩ P ⟨ π ⟩ → ⟨ π ⟩ Q ⟨ ψ ⟩ → ⟨ ϕ ⟩ P ∶ Q ⟨ ψ ⟩ + updₕ : ⟨ ϕ ∘ f ⟩ UPD f ⟨ ϕ ⟩ + conseqₕ : ϕ ⇒ ϕ′ → ⟨ ϕ′ ⟩ P ⟨ ψ′ ⟩ → ψ′ ⇒ ψ → ⟨ ϕ ⟩ P ⟨ ψ ⟩ + + +record ListSum : Set where + field + A : List ℕ + s : ℕ + i : ℕ + +lookup' : List ℕ → ℕ → ℕ +lookup' V n with n : ∀ {n} (xs : CompressedString (suc n)) → cons-c (head-c xs) (tail-c xs) ≡ xs +cons-c∘ (one x zero) = refl +cons-c∘ (one x (suc n)) with x ≟ x +... | yes _ = refl +... | no x≢x = ⊥-elim (x≢x refl) +cons-c∘ (cons zero xs) = cons-c-¬head xs +cons-c∘ (cons (suc n) xs) with not (head-c xs) ≟ not (head-c xs) +... | yes _ = refl +... | no x≢x = ⊥-elim (x≢x refl) + +-- Beta equalities + +head-c∘cons-c : ∀ {n} x (xs : CompressedString n) → head-c (cons-c x xs) ≡ x +head-c∘cons-c x empty = refl +head-c∘cons-c x (one y n) with x ≟ y +... | yes x≡y = sym x≡y +... | no x≢y = sym (¬-not x≢y) +head-c∘cons-c x (cons n xs) with x ≟ not (head-c xs) +... | yes x≡¬y = sym x≡¬y +... | no x≢¬y = sym (¬-not x≢¬y) + +tail-c∘cons-c : ∀ {n} x (xs : CompressedString n) → tail-c (cons-c x xs) ≡ xs +tail-c∘cons-c x empty = refl +tail-c∘cons-c x (one y n) with x ≟ y +... | yes _ = refl +... | no _ = refl +tail-c∘cons-c x (cons n xs) with x ≟ not (head-c xs) +... | yes _ = refl +... | no _ = refl + +-- Goals + +prf₁ : ∀{n} (xs : CompressedString n) → compress (decompress xs) ≡ xs +prf₁ {zero} empty = refl +prf₁ {suc n} xs = begin + cons-c (head-c xs) (compress (decompress (tail-c xs))) ≡⟨ cong (cons-c (head-c xs)) (prf₁ (tail-c xs)) ⟩ + cons-c (head-c xs) (tail-c xs) ≡⟨ cons-c∘ xs ⟩ + xs ∎ + +prf₂ : ∀{n} (xs : Vec Bool n) → decompress (compress xs) ≡ xs +prf₂ [] = refl +prf₂ (x ∷ xs) = + cong₂ _∷_ + (head-c∘cons-c x (compress xs)) + (begin + decompress (tail-c (cons-c x (compress xs))) ≡⟨ cong decompress (tail-c∘cons-c x (compress xs)) ⟩ + decompress (compress xs) ≡⟨ prf₂ xs ⟩ + xs ∎) 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 ∷ [] ∎ -- cgit v1.2.3