Advent of proof submissions.HEADmaster

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

1 files changed, 113 insertions, 0 deletions

diff --git a/src/Problem18.agda b/src/Problem18.agda
new file mode 100644
index 0000000..e71dcb9
--- /dev/null
+++ b/src/Problem18.agda
@@ -0,0 +1,113 @@
+{-# OPTIONS --safe #-}
+
+module Problem18 (Symbol : Set) where
+
+open import Data.Nat
+open import Data.Vec
+open import Relation.Binary.PropositionalEquality
+open import Data.Product
+
+open ≡-Reasoning
+
+variable n m a b c d : ℕ
+
+data Patch : ℕ → ℕ → Set where
+  end : Patch 0 0
+  skp : Patch n m → Patch (suc n) (suc m)
+  del : Patch n m → Patch (suc n) m
+  ins : Symbol → Patch n m → Patch n (suc m)
+
+apply : Patch n m → Vec Symbol n → Vec Symbol m
+apply end  []  = []
+apply (ins x p) xs = x ∷ apply p xs
+apply (skp p) (x ∷ xs) = x ∷ apply p xs
+apply (del p) (x ∷ xs) = apply p xs
+
+infixl 50 _·_
+_·_ : Patch a b → Patch b c → Patch a c
+end      · p₂        = p₂
+skp p₁   · skp p₂    = skp (p₁ · p₂)
+skp p₁   · del p₂    = del (p₁ · p₂)
+skp p₁   · ins x p₂  = ins x (skp p₁ · p₂)
+ins x p₁ · ins x₂ p₂ = ins x₂ (ins x p₁ · p₂)
+del p₁   · ins x₂ p₂ = ins x₂ (del p₁ · p₂)
+del p₁   · p₂        = del (p₁ · p₂)
+ins x p₁ · skp p₂    = ins x (p₁ · p₂)
+ins x p₁ · del p₂    = p₁ · p₂
+
+_≈_ : (x y : Patch a b) → Set
+x ≈ y = ∀ d → apply x d ≡ apply y d
+
+compose-correct : ∀ (p₁ : Patch a b) (p₂ : Patch b c) (d : Vec Symbol a)
+                → apply (p₁ · p₂) d ≡ apply p₂ (apply p₁ d)
+compose-correct end        p₂         []      = refl
+compose-correct (skp p₁)   (skp p₂)   (x ∷ d) = cong (x ∷_) (compose-correct p₁ p₂ d)
+compose-correct (skp p₁)   (del p₂)   (x ∷ d) = compose-correct p₁ p₂ d
+compose-correct (skp p₁)   (ins y p₂) (x ∷ d) = cong (y ∷_) (compose-correct (skp p₁) p₂ (x ∷ d))
+compose-correct (del p₁)   end        (x ∷ d) = compose-correct p₁ end d
+compose-correct (del p₁)   (skp p₂)   (x ∷ d) = compose-correct p₁ (skp p₂) d
+compose-correct (del p₁)   (del p₂)   (x ∷ d) = compose-correct p₁ (del p₂) d
+compose-correct (del p₁)   (ins y p₂) (x ∷ d) = cong (y ∷_) (compose-correct (del p₁) p₂ (x ∷ d))
+compose-correct (ins y p₁) (skp p₂)   d       = cong (y ∷_) (compose-correct p₁ p₂ d)
+compose-correct (ins y p₁) (del p₂)   d       = compose-correct p₁ p₂ d
+compose-correct (ins y p₁) (ins z p₂) d       = cong (z ∷_) (compose-correct (ins y p₁) p₂ d)
+
+compose-assoc : ∀ (p₁ : Patch a b) (p₂ : Patch b c) (p₃ : Patch c d)
+              → (p₁ · p₂) · p₃ ≈ p₁ · (p₂ · p₃)
+compose-assoc p₁ p₂ p₃ d = begin
+  apply (p₁ · p₂ · p₃) d           ≡⟨  compose-correct (p₁ · p₂) p₃ d ⟩
+  apply p₃ (apply (p₁ · p₂) d)     ≡⟨  cong (apply p₃) (compose-correct p₁ p₂ d) ⟩
+  apply p₃ (apply p₂ (apply p₁ d)) ≡˘⟨ compose-correct p₂ p₃ (apply p₁ d) ⟩
+  apply (p₂ · p₃) (apply p₁ d)     ≡˘⟨ compose-correct p₁ (p₂ · p₃) d ⟩
+  apply (p₁ · (p₂ · p₃)) d         ∎
+
+
+record Merge (p₁ : Patch a b)(p₂ : Patch a c) : Set where
+    constructor M
+    field size : ℕ
+    field p₁′ : Patch b size
+    field p₂′ : Patch c size
+
+
+merge : ∀(p₁ : Patch a b)(p₂ : Patch a c) → Merge p₁ p₂
+merge end end = M 0 end end
+merge p₁ (ins x p₂)     = let m = merge p₁ p₂ in M (suc (Merge.size m)) (ins x (Merge.p₁′ m)) (skp (Merge.p₂′ m))
+merge (ins x p₁) p₂     = let m = merge p₁ p₂ in M (suc (Merge.size m)) (skp (Merge.p₁′ m))   (ins x (Merge.p₂′ m))
+merge (del p₁) (skp p₂) = let m = merge p₁ p₂ in M (Merge.size m)       (Merge.p₁′ m)         (del (Merge.p₂′ m))
+merge (skp p₁) (del p₂) = let m = merge p₁ p₂ in M (Merge.size m)       (del (Merge.p₁′ m))   (Merge.p₂′ m)
+merge (del p₁) (del p₂) = let m = merge p₁ p₂ in M (Merge.size m)       (Merge.p₁′ m)         (Merge.p₂′ m)
+merge (skp p₁) (skp p₂) = let m = merge p₁ p₂ in M (suc (Merge.size m)) (skp (Merge.p₁′ m))   (skp (Merge.p₂′ m))
+
+merge-pushout :
+  (p₁ : Patch a b) (p₂ : Patch a c) →
+  p₁ · Merge.p₁′ (merge p₁ p₂) ≈ p₂ · Merge.p₂′ (merge p₁ p₂)
+merge-pushout end        end        d       = refl
+merge-pushout end        (ins z p₂) d       = cong (z ∷_) (merge-pushout end p₂ d)
+merge-pushout (skp p₁)   (skp p₂)   (x ∷ d) = cong (x ∷_) (merge-pushout p₁ p₂ d)
+merge-pushout (skp p₁)   (del p₂)   (x ∷ d) = begin
+  apply (p₁ · Merge.p₁′ (merge p₁ p₂)) d                   ≡⟨  merge-pushout p₁ p₂ d ⟩
+  apply (p₂ · Merge.p₂′ (merge p₁ p₂)) d                   ≡⟨  compose-correct p₂ (Merge.p₂′ (merge p₁ p₂)) d ⟩
+  apply (Merge.p₂′ (merge p₁ p₂)) (apply p₂ d)             ≡⟨⟩
+  apply (Merge.p₂′ (merge p₁ p₂)) (apply (del p₂) (x ∷ d)) ≡˘⟨ compose-correct (del p₂) (Merge.p₂′ (merge p₁ p₂)) (x ∷ d) ⟩
+  apply (del p₂ · Merge.p₂′ (merge p₁ p₂)) (x ∷ d)         ∎
+merge-pushout (skp p₁)   (ins z p₂) d       = cong (z ∷_) (merge-pushout (skp p₁) p₂ d )
+merge-pushout (del p₁)   (skp p₂)   (x ∷ d) = begin
+  apply (del p₁ · Merge.p₁′ (merge p₁ p₂)) (x ∷ d)         ≡⟨  compose-correct (del p₁) (Merge.p₁′ (merge p₁ p₂)) (x ∷ d) ⟩
+  apply (Merge.p₁′ (merge p₁ p₂)) (apply (del p₁) (x ∷ d)) ≡⟨⟩
+  apply (Merge.p₁′ (merge p₁ p₂)) (apply p₁ d)             ≡˘⟨ compose-correct p₁ (Merge.p₁′ (merge p₁ p₂)) d ⟩
+  apply (p₁ · Merge.p₁′ (merge p₁ p₂)) d                   ≡⟨  merge-pushout p₁ p₂ d ⟩
+  apply (p₂ · Merge.p₂′ (merge p₁ p₂)) d                   ∎
+merge-pushout (del p₁)   (del p₂)   (x ∷ d) = begin
+  apply (del p₁ · Merge.p₁′ (merge p₁ p₂)) (x ∷ d)         ≡⟨  compose-correct (del p₁) (Merge.p₁′ (merge p₁ p₂)) (x ∷ d) ⟩
+  apply (Merge.p₁′ (merge p₁ p₂)) (apply (del p₁) (x ∷ d)) ≡⟨⟩
+  apply (Merge.p₁′ (merge p₁ p₂)) (apply p₁ d)             ≡˘⟨ compose-correct p₁ (Merge.p₁′ (merge p₁ p₂)) d ⟩
+  apply (p₁ · Merge.p₁′ (merge p₁ p₂)) d                   ≡⟨  merge-pushout p₁ p₂ d ⟩
+  apply (p₂ · Merge.p₂′ (merge p₁ p₂)) d                   ≡⟨  compose-correct p₂ (Merge.p₂′ (merge p₁ p₂)) d ⟩
+  apply (Merge.p₂′ (merge p₁ p₂)) (apply p₂ d)             ≡⟨⟩
+  apply (Merge.p₂′ (merge p₁ p₂)) (apply (del p₂) (x ∷ d)) ≡˘⟨ compose-correct (del p₂) (Merge.p₂′ (merge p₁ p₂)) (x ∷ d) ⟩
+  apply (del p₂ · Merge.p₂′ (merge p₁ p₂)) (x ∷ d)         ∎
+merge-pushout (del p₁)   (ins z p₂) d       = cong (z ∷_) (merge-pushout (del p₁) p₂ d)
+merge-pushout (ins y p₁) end        d       = cong (y ∷_) (merge-pushout p₁ end d)
+merge-pushout (ins y p₁) (skp p₂)   d       = cong (y ∷_) (merge-pushout p₁ (skp p₂) d)
+merge-pushout (ins y p₁) (del p₂)   d       = cong (y ∷_) (merge-pushout p₁ (del p₂) d)
+merge-pushout (ins y p₁) (ins z p₂) d       = cong (z ∷_) (merge-pushout (ins y p₁) p₂ d)