Source code on Github
{-# OPTIONS --cubical-compatible --safe #-}
module Data.List.Relation.Ternary.Interleaving.Properties where
open import Data.Nat.Base
open import Data.Nat.Properties using (+-suc)
open import Data.List.Base hiding (_∷ʳ_)
open import Data.List.Properties using (reverse-involutive)
open import Data.List.Relation.Ternary.Interleaving hiding (map)
open import Function
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
using (_≡_; refl; sym; cong; module ≡-Reasoning)
open ≡-Reasoning
module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c}
{L : REL A C l} {R : REL B C r} where
interleave-length : ∀ {as l r} → Interleaving L R l r as →
length as ≡ length l + length r
interleave-length [] = refl
interleave-length (l ∷ˡ sp) = cong suc (interleave-length sp)
interleave-length {as} {l} {r ∷ rs} (_ ∷ʳ sp) = begin
length as ≡⟨ cong suc (interleave-length sp) ⟩
suc (length l + length rs) ≡⟨ sym $ +-suc _ _ ⟩
length l + length (r ∷ rs) ∎
++⁺ : ∀ {as₁ as₂ l₁ l₂ r₁ r₂} →
Interleaving L R as₁ l₁ r₁ →
Interleaving L R as₂ l₂ r₂ →
Interleaving L R (as₁ ++ as₂) (l₁ ++ l₂) (r₁ ++ r₂)
++⁺ [] sp₂ = sp₂
++⁺ (l ∷ˡ sp₁) sp₂ = l ∷ˡ (++⁺ sp₁ sp₂)
++⁺ (r ∷ʳ sp₁) sp₂ = r ∷ʳ (++⁺ sp₁ sp₂)
++-disjoint : ∀ {as₁ as₂ l₁ r₂} →
Interleaving L R l₁ [] as₁ →
Interleaving L R [] r₂ as₂ →
Interleaving L R l₁ r₂ (as₁ ++ as₂)
++-disjoint [] sp₂ = sp₂
++-disjoint (l ∷ˡ sp₁) sp₂ = l ∷ˡ ++-disjoint sp₁ sp₂
module _ {a b c d e f l r}
{A : Set a} {B : Set b} {C : Set c}
{D : Set d} {E : Set e} {F : Set f}
{L : REL A C l} {R : REL B C r}
(f : E → A) (g : F → B) (h : D → C)
where
map⁺ : ∀ {as l r} →
Interleaving (λ x z → L (f x) (h z)) (λ y z → R (g y) (h z)) l r as →
Interleaving L R (map f l) (map g r) (map h as)
map⁺ [] = []
map⁺ (l ∷ˡ sp) = l ∷ˡ map⁺ sp
map⁺ (r ∷ʳ sp) = r ∷ʳ map⁺ sp
map⁻ : ∀ {as l r} →
Interleaving L R (map f l) (map g r) (map h as) →
Interleaving (λ x z → L (f x) (h z)) (λ y z → R (g y) (h z)) l r as
map⁻ {[]} {[]} {[]} [] = []
map⁻ {_ ∷ _} {[]} {_ ∷ _} (r ∷ʳ sp) = r ∷ʳ map⁻ sp
map⁻ {_ ∷ _} {_ ∷ _} {[]} (l ∷ˡ sp) = l ∷ˡ map⁻ sp
map⁻ {_ ∷ _} {_ ∷ _} {_ ∷ _} (l ∷ˡ sp) = l ∷ˡ map⁻ sp
map⁻ {_ ∷ _} {_ ∷ _} {_ ∷ _} (r ∷ʳ sp) = r ∷ʳ map⁻ sp
module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c}
{L : REL A C l} {R : REL B C r}
where
reverseAcc⁺ : ∀ {as₁ as₂ l₁ l₂ r₁ r₂} →
Interleaving L R l₁ r₁ as₁ →
Interleaving L R l₂ r₂ as₂ →
Interleaving L R (reverseAcc l₁ l₂) (reverseAcc r₁ r₂) (reverseAcc as₁ as₂)
reverseAcc⁺ sp₁ [] = sp₁
reverseAcc⁺ sp₁ (l ∷ˡ sp₂) = reverseAcc⁺ (l ∷ˡ sp₁) sp₂
reverseAcc⁺ sp₁ (r ∷ʳ sp₂) = reverseAcc⁺ (r ∷ʳ sp₁) sp₂
ʳ++⁺ : ∀ {as₁ as₂ l₁ l₂ r₁ r₂} →
Interleaving L R l₁ r₁ as₁ →
Interleaving L R l₂ r₂ as₂ →
Interleaving L R (l₁ ʳ++ l₂) (r₁ ʳ++ r₂) (as₁ ʳ++ as₂)
ʳ++⁺ sp₁ sp₂ = reverseAcc⁺ sp₂ sp₁
reverse⁺ : ∀ {as l r} → Interleaving L R l r as →
Interleaving L R (reverse l) (reverse r) (reverse as)
reverse⁺ = reverseAcc⁺ []
reverse⁻ : ∀ {as l r} → Interleaving L R (reverse l) (reverse r) (reverse as) →
Interleaving L R l r as
reverse⁻ {as} {l} {r} sp with reverse⁺ sp
... | sp′ rewrite reverse-involutive as
| reverse-involutive l
| reverse-involutive r = sp′