{-# OPTIONS --cubical-compatible --safe #-}
module Data.List.Relation.Ternary.Appending {a b c} {A : Set a} {B : Set b} {C : Set c} where
open import Level using (Level; _⊔_)
open import Data.List.Base as List using (List; []; _∷_)
open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_)
open import Data.Product.Base using (∃₂; _×_; _,_; -,_)
open import Relation.Binary.Core using (REL)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
private
variable
l r : Level
L : REL A C l
R : REL B C r
as : List A
bs : List B
cs : List C
module _ (L : REL A C l) (R : REL B C r) where
infixr 5 _∷_ []++_
data Appending : List A → List B → List C → Set (a ⊔ b ⊔ c ⊔ l ⊔ r) where
[]++_ : ∀ {bs cs} → Pointwise R bs cs → Appending [] bs cs
_∷_ : ∀ {a as bs c cs} → L a c → Appending as bs cs → Appending (a ∷ as) bs (c ∷ cs)
infixr 5 _++_
_++_ : ∀ {cs₁ cs₂ : List C} → Pointwise L as cs₁ → Pointwise R bs cs₂ →
Appending L R as bs (cs₁ List.++ cs₂)
[] ++ rs = []++ rs
(l ∷ ls) ++ rs = l ∷ (ls ++ rs)
break : Appending L R as bs cs → ∃₂ λ cs₁ cs₂ →
cs₁ List.++ cs₂ ≡ cs × Pointwise L as cs₁ × Pointwise R bs cs₂
break ([]++ rs) = -, -, (refl , [] , rs)
break (l ∷ lrs) =
let (_ , _ , eq , ls , rs) = break lrs in
-, -, (cong (_ ∷_) eq , l ∷ ls , rs)