{-# 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)