diff options
Diffstat (limited to 'src/Problem18.agda')
| -rw-r--r-- | src/Problem18.agda | 113 |
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) |