Simple Operational Transformation in Agda

OpTransVec.agda

module OpTransVec where

open import Data.Vec
open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Function using (_∘_)

data Op (A : Set) : ℕ → ℕ → Set where
  ε : Op A 0 0
  retain : ∀ {n m} → Op A n m → Op A (suc n) (suc m)
  delete : ∀ {n m} → Op A n m → Op A (suc n) m
  insert : ∀ {n m} (x : A) → Op A n m → Op A n (suc m)

apply : ∀ {A n m} → Vec A n → Op A n m → Vec A m
apply xs (insert x o) = x ∷ apply xs o
apply (x ∷ xs) (delete o) = apply xs o
apply (x ∷ xs) (retain o) = x ∷ apply xs o
apply [] ε = []

id : ∀ {A n} → Op A n n
id {n = zero} = ε
id {n = suc n} = retain id

apply-id : ∀ {A n} (xs : Vec A n) → apply xs id ≡ xs
apply-id [] = refl
apply-id (x ∷ xs) = cong (_∷_ x) (apply-id xs)

compose : ∀ {A n m o} → Op A n m → Op A m o → Op A n o
compose a (insert x b) = insert x (compose a b)
compose a ε = a
compose (delete a) b = delete (compose a b)
compose (insert x a) (delete b) = compose a b
compose (insert x a) (retain b) = insert x (compose a b)
compose (retain a) (delete b) = delete (compose a b)
compose (retain a) (retain b) = retain (compose a b)

invert : ∀ {A n m} → Vec A n → Op A n m → Op A m n
invert [] ε = ε
invert (x ∷ xs) (retain o) = retain (invert xs o)
invert (x ∷ xs) (delete o) = insert x (invert xs o)
invert xs (insert x o) = delete (invert xs o)

invert-correct : ∀ {A n m} → (xs : Vec A n)(o : Op A n m) → apply (apply xs o) (invert xs o) ≡ xs
invert-correct [] ε = refl
invert-correct (x ∷ xs) (retain o) = cong (_∷_ _) (invert-correct xs o)
invert-correct (x ∷ xs) (delete o) = cong (_∷_ _) (invert-correct xs o)
invert-correct [] (insert x o) = invert-correct [] o
invert-correct (x ∷ xs) (insert y o) = invert-correct (x ∷ xs) o

compose-correct : ∀ {A n m o xs} (a : Op A n m) (b : Op A m o) → apply xs (compose a b) ≡ apply (apply xs a) b
compose-correct {xs = []} ε ε = refl
compose-correct ε (insert x b) = cong (_∷_ x) (compose-correct ε b)
compose-correct {xs = x ∷ xs} (retain a) (retain b) = cong (_∷_ x) (compose-correct a b)
compose-correct {xs = x ∷ xs} (retain a) (delete b) = compose-correct a b
compose-correct (retain a) (insert x b) = cong (_∷_ x) (compose-correct (retain a) b)
compose-correct {xs = x ∷ xs} (delete a) ε = compose-correct a ε
compose-correct {xs = x ∷ xs} (delete a) (retain b) = compose-correct a (retain b)
compose-correct {xs = x ∷ xs} (delete a) (delete b) = compose-correct a (delete b)
compose-correct (delete a) (insert x b) = cong (_∷_ x) (compose-correct (delete a) b)
compose-correct (insert x a) (retain b) = cong (_∷_ x) (compose-correct a b)
compose-correct (insert x a) (delete b) = compose-correct a b
compose-correct (insert x a) (insert y b) = cong (_∷_ y) (compose-correct (insert x a) b)

id-compose : ∀ {A n m} (o : Op A n m) → compose id o ≡ o
id-compose ε = refl
id-compose (retain o) = cong retain (id-compose o)
id-compose (delete o) = cong delete (id-compose o)
id-compose (insert x o) = cong (insert x) (id-compose o)

compose-id : ∀ {A n m} (o : Op A n m) → compose o id ≡ o
compose-id ε = refl
compose-id (retain o) = cong retain (compose-id o)
compose-id {m = zero} (delete o) = refl
compose-id {m = suc n} (delete o) = cong delete (compose-id o)
compose-id (insert x o) = cong (insert x) (compose-id o)

transform : ∀ {A n m₁ m₂} (a : Op A n m₁) (b : Op A n m₂) → ∃ λ o → Op A m₁ o × Op A m₂ o
transform {m₁ = o} a ε = o , id , a
transform {m₂ = o} ε b = o , b , id
transform (retain a) (retain b) with transform a b
transform (retain a) (retain b) | o , a' , b' = suc o , retain a' , retain b'
transform (insert x a) b with transform a b
transform (insert x a) b | o , a' , b' = suc o , retain a' , insert x b'
transform a (insert x b) with transform a b
transform a (insert x b) | o , a' , b' = suc o , insert x a' , retain b'
transform (delete a) (delete b) = transform a b
transform (delete a) (retain b) with transform a b
transform (delete a) (retain b) | o , a' , b' = o , a' , delete b'
transform (retain a) (delete b) with transform a b
transform (retain a) (delete b) | o , a' , b' = o , delete a' , b'

transform-converges : ∀ {A n m₁ m₂} (xs : Vec A n) (a : Op A n m₁) (b : Op A n m₂) → let t = proj₂ (transform a b) in apply (apply xs a) (proj₁ t) ≡ apply (apply xs b) (proj₂ t)
transform-converges [] ε ε = refl
transform-converges [] ε (insert x b) = cong (_∷_ x) (sym (apply-id (apply [] b)))
transform-converges [] (insert x a) ε = cong (_∷_ x) (apply-id (apply [] a))
transform-converges [] (insert x a) (insert y b) = cong (_∷_ x) (transform-converges [] a (insert y b))
transform-converges (x ∷ xs) (retain a) (retain b) = cong (_∷_ x) (transform-converges xs a b)
transform-converges (x ∷ xs) (retain a) (delete b) = transform-converges xs a b
transform-converges (x ∷ xs) (retain a) (insert y b) = cong (_∷_ y) (transform-converges (x ∷ xs) (retain a) b)
transform-converges (x ∷ xs) (delete a) (retain b) = transform-converges xs a b
transform-converges (x ∷ xs) (delete a) (delete b) = transform-converges xs a b
transform-converges (x ∷ xs) (delete a) (insert y b) = cong (_∷_ y) (transform-converges (x ∷ xs) (delete a) b)
transform-converges (x ∷ xs) (insert y a) (retain b) = cong (_∷_ y) (transform-converges (x ∷ xs) a (retain b))
transform-converges (x ∷ xs) (insert y a) (delete b) = cong (_∷_ y) (transform-converges (x ∷ xs) a (delete b))
transform-converges (x ∷ xs) (insert y a) (insert z b) = cong (_∷_ y) (transform-converges (x ∷ xs) a (insert z b))