Easy proofs of the triangle and pentagon laws for list interleaving

Interleaving.agda

module Interleaving where

open import Data.List using (List; []; _∷_)
open import Data.List.Relation.Binary.Pointwise as Pw
open import Data.List.Relation.Ternary.Interleaving.Propositional
open import Data.Product
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
open import Relation.Unary renaming (U to Un)

module _ {a} {A : Set a} where

  infix 40 []∼_ _+_∼_ _≈_ _≈ᴵ_

  []∼_ : List A → Set a
  []∼_ = Pointwise _≡_ []

  _+_∼_ : (xs ys zs : List A) → Set a
  _+_∼_ = Interleaving

  _≈_ : (xs ys : List A) → Set a
  _≈_ = Pointwise _≡_

  ≈⇒≡ = Pointwise-≡⇒≡
  ≡⇒≈ = ≡⇒Pointwise-≡

  ≈-refl : ∀ {xs} → xs ≈ xs
  ≈-refl = Pw.refl ≡.refl
  ≈-trans : ∀ {xs ys zs} → xs ≈ ys → ys ≈ zs → xs ≈ zs
  ≈-trans = Pw.transitive ≡.trans
  ≈-sym : ∀ {xs ys} → xs ≈ ys → ys ≈ xs
  ≈-sym = Pw.symmetric ≡.sym

  +-resp-≈′ : ∀ {xs xs′ ys ys′ zs zs′} →
    xs + ys ∼ zs → xs ≈ xs′ → ys ≈ ys′ → zs′ ≈ zs → xs′ + ys′ ∼ zs′
  +-resp-≈′ [] [] [] [] = []
  +-resp-≈′ (consˡ i) (≡.refl ∷ qxs) qys (≡.refl ∷ qzs) = consˡ (+-resp-≈′ i qxs qys qzs)
  +-resp-≈′ (consʳ i) qxs (≡.refl ∷ qys) (≡.refl ∷ qzs) = consʳ (+-resp-≈′ i qxs qys qzs)

  +-resp-≈ : ∀ {xs xs′ ys ys′ zs zs′} →
    xs ≈ xs′ → ys ≈ ys′ → zs′ ≈ zs →
    xs + ys ∼ zs → xs′ + ys′ ∼ zs′
  +-resp-≈ qxs qys qzs i = +-resp-≈′ i qxs qys qzs

  assoc→ : ∀ {xs ys zs xyzs} →
    ∃⟨ xs + ys ∼_ ∩ _+ zs ∼ xyzs ⟩ →
    ∃⟨ ys + zs ∼_ ∩ xs +_∼ xyzs ⟩
  assoc→ (_ , i , j) = go i j
    where
    go : ∀ {xs ys zs xyzs} →
      ∀ {xys} → xs + ys ∼ xys → xys + zs ∼ xyzs →
      ∃⟨ ys + zs ∼_ ∩ xs +_∼ xyzs ⟩
    go i (consʳ j) with _ , i′ , j′ ← go i j = _ , consʳ i′ , consʳ j′
    go [] [] = _ , [] , []
    go (consˡ i) (consˡ j) with _ , i′ , j′ ← go i j = _ , i′ , consˡ j′
    go (consʳ i) (consˡ j) with _ , i′ , j′ ← go i j = _ , consˡ i′ , consʳ j′

  unright : ∀ {ys zs} → [] + ys ∼ zs → ys ≈ zs
  unright [] = []
  unright (q ∷ʳ i) = q ∷ unright i

  unleft : ∀ {xs zs} → xs + [] ∼ zs → xs ≈ zs
  unleft [] = []
  unleft (q ∷ˡ i) = q ∷ unleft i

  identityˡ→ : ∀ {ys zs} → ∃⟨ []∼_ ∩ _+ ys ∼ zs ⟩ → ys ≈ zs
  identityˡ→ (_ , [] , i) = unright i

  identityʳ→ : ∀ {xs zs} → ∃⟨ []∼_ ∩ xs +_∼ zs ⟩ → xs ≈ zs
  identityʳ→ (_ , [] , i) = unleft i

  data _≈ᴵ_ : ∀ {xs xs′ ys ys′ zs zs′} → xs + ys ∼ zs → xs′ + ys′ ∼ zs′ → Set a where
    []≈ : [] ≈ᴵ []
    consˡ≈ : ∀ {z z′ xs xs′ ys ys′ zs zs′} {q : z ≡ z′}
      {i : xs + ys ∼ zs} {j : xs′ + ys′ ∼ zs′} → i ≈ᴵ j → (q ∷ˡ i) ≈ᴵ (q ∷ˡ j)
    consʳ≈ : ∀ {z z′ xs xs′ ys ys′ zs zs′} {q : z ≡ z′}
      {i : xs + ys ∼ zs} {j : xs′ + ys′ ∼ zs′} → i ≈ᴵ j → (q ∷ʳ i) ≈ᴵ (q ∷ʳ j)

  triangle-left : ∀ {xs zs xyzs} →
    (∃ \ ys → []∼ ys × ∃ \ xys → xs + ys ∼ xys × xys + zs ∼ xyzs) →
    xs + zs ∼ xyzs
  triangle-left {xs} {zs} {xyzs} (_ , n , _ , i , j) =
    +-resp-≈ (≈-sym (identityʳ→ (_ , n , i))) ≈-refl ≈-refl j

  triangle-right : ∀ {xs zs xyzs} →
    (∃ \ ys → []∼ ys × ∃ \ xys → xs + ys ∼ xys × xys + zs ∼ xyzs) →
    xs + zs ∼ xyzs
  triangle-right (_ , n , _ , i , j) with _ , i′ , j′ ← assoc→ (_ , i , j) =
    +-resp-≈ ≈-refl (≈-sym (identityˡ→ (_ , n , i′))) ≈-refl j′

  triangle : ∀ {xs zs xyzs} p →
    triangle-left p ≈ᴵ triangle-right {xs} {zs} {xyzs} p
  triangle (_ , [] , _ , i , consʳ j) = consʳ≈ (triangle (_ , [] , _ , i , j))
  triangle (_ , [] , _ , [] , []) = []≈
  triangle (_ , [] , _ , consˡ i , consˡ j) =
    consˡ≈ (triangle (_ , [] , _ , i , j))

  pentagon-left : ∀ {ws xs ys zs wxyzs} →
    (∃ \ wxs → ws + xs ∼ wxs × ∃ \ wxys → wxs + ys ∼ wxys × wxys + zs ∼ wxyzs) →
    (∃ \ yzs → ys + zs ∼ yzs × ∃ \ xyzs → xs + yzs ∼ xyzs × ws + xyzs ∼ wxyzs)
  pentagon-left (_ , wx , _ , [wx]y , [wxy]z)
    with _ , yz , [wx][yz] ← assoc→ (_ , [wx]y , [wxy]z)
    with _ , x[yz] , w[xyz] ← assoc→ (_ , wx , [wx][yz])
    = _ , yz , _ , x[yz] , w[xyz]

  pentagon-right : ∀ {ws xs ys zs wxyzs} →
    (∃ \ wxs → ws + xs ∼ wxs × ∃ \ wxys → wxs + ys ∼ wxys × wxys + zs ∼ wxyzs) →
    (∃ \ yzs → ys + zs ∼ yzs × ∃ \ xyzs → xs + yzs ∼ xyzs × ws + xyzs ∼ wxyzs)
  pentagon-right (_ , wx , _ , [wx]y , [wxy]z)
    with _ , xy , w[xy] ← assoc→ (_ , wx , [wx]y)
    with _ , [xy]z , w[xyz] ← assoc→ (_ , w[xy] , [wxy]z)
    with _ , yz , x[yz] ← assoc→ (_ , xy , [xy]z)
    = _ , yz , _ , x[yz] , w[xyz]

  pentagon : ∀ {ws xs ys zs wxyzs} p →
    let yzsl , yzl , xyzsl , x[yz]l , w[xyz]l =
         pentagon-left {ws} {xs} {ys} {zs} {wxyzs} p in
    let yzsr , yzr , xyzsr , x[yz]r , w[xyz]r = pentagon-right p in
    yzl ≈ᴵ yzr × x[yz]l ≈ᴵ x[yz]r × w[xyz]l ≈ᴵ w[xyz]r
  pentagon (_ , [] , _ , [] , []) = []≈ , []≈ , []≈
  pentagon (_ , consˡ wx , _ , consˡ [wx]y , consˡ [wxy]z)
    with yzq , x[yz]q , w[xyz]q ← pentagon (_ , wx , _ , [wx]y , [wxy]z)
    = yzq , x[yz]q , consˡ≈ w[xyz]q
  pentagon (_ , consʳ wx , _ , consˡ [wx]y , consˡ [wxy]z)
    with yzq , x[yz]q , w[xyz]q ← pentagon (_ , wx , _ , [wx]y , [wxy]z)
    = yzq , consˡ≈ x[yz]q , consʳ≈ w[xyz]q
  pentagon (_ , wx , _ , consʳ [wx]y , consˡ [wxy]z)
    with yzq , x[yz]q , w[xyz]q ← pentagon (_ , wx , _ , [wx]y , [wxy]z)
    = consˡ≈ yzq , consʳ≈ x[yz]q , consʳ≈ w[xyz]q
  pentagon (_ , wx , _ , [wx]y , consʳ [wxy]z)
    with yzq , x[yz]q , w[xyz]q ← pentagon (_ , wx , _ , [wx]y , [wxy]z)
    = consʳ≈ yzq , consʳ≈ x[yz]q , consʳ≈ w[xyz]q