[ new ] Interleaving of Lists

CHANGELOG.md

@@ -249,6 +249,11 @@ Other major changes
   generalization of the notion of "first element in the list to satisfy a
   predicate".
 
+* Added new modules `Data.List.Relation.Prefix.Heterogeneous(.Properties)`
+
+* Added new modules `Data.List.Relation.Interleaving(.Setoid/Propositional)`
+  and `Data.List.Relation.Interleaving(.Setoid/Propositional).Properties`.
+
 * Added new module `Data.Vec.Any.Properties`
 
 * Added new modules `Relation.Binary.Construct.NaturalOrder.(Left/Right)`
@@ -486,6 +491,8 @@ Other minor additions
   _[_]%=_ : (xs : List A) → Fin (length xs) → (A → A) → List A
   _[_]∷=_ : (xs : List A) → Fin (length xs) → A → List A
   _─_     : (xs : List A) → Fin (length xs) → List A
+
+  reverseAcc : List A → List A → List A
   ```
 
 * Added new proofs to `Data.List.All.Properties`:
@@ -658,9 +665,10 @@ Other minor additions
   wlog : Total _R_ → Symmetric Q → (∀ a b → a R b → Q a b) → ∀ a b → Q a b
   ```
 
-* Added new definition to `Relation.Binary.Core`:
+* Added new definitions to `Relation.Binary.Core`:
   ```agda
   Antisym R S E = ∀ {i j} → R i j → S j i → E i j
+  Conn P Q = ∀ x y → P x y ⊎ Q y x
   ```
 
 * Added new proofs to `Relation.Binary.Lattice`:

src/Data/List/Base.agda

@@ -16,7 +16,7 @@ open import Data.Bool.Base as Bool
 open import Data.Maybe.Base as Maybe using (Maybe; nothing; just)
 open import Data.Product as Prod using (_×_; _,_)
 open import Data.These as These using (These; this; that; these)
-open import Function using (id; _∘_ ; _∘′_; const)
+open import Function using (id; _∘_ ; _∘′_; const; flip)
 
 open import Relation.Nullary using (yes; no)
 open import Relation.Unary using (Pred; Decidable)
@@ -324,8 +324,13 @@ module _ {a} {A : Set a} where
 ------------------------------------------------------------------------
 -- Operations for reversing lists
 
-reverse : ∀ {a} {A : Set a} → List A → List A
-reverse = foldl (λ rev x → x ∷ rev) []
+module _ {a} {A : Set a} where
+
+  reverseAcc : List A → List A → List A
+  reverseAcc = foldl (flip _∷_)
+
+  reverse : List A → List A
+  reverse = reverseAcc []
 
 -- Snoc.
 

src/Data/List/Relation/Interleaving.agda

@@ -0,0 +1,103 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Generalised notion of interleaving two lists into one in an
+-- order-preserving manner
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.List.Relation.Interleaving where
+
+open import Level
+open import Data.List.Base as List using (List; []; _∷_; _++_)
+open import Data.List.Relation.Pointwise using (Pointwise; []; _∷_)
+open import Data.Product as Prod using (∃; ∃₂; _×_; uncurry; _,_; -,_; proj₂)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Function
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality as P using (_≡_)
+
+------------------------------------------------------------------------
+-- Definition
+
+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
+
+  data Interleaving : List A → List B → List C → Set (a ⊔ b ⊔ c ⊔ l ⊔ r) where
+    []   : Interleaving [] [] []
+    _∷ˡ_ : ∀ {a c l r cs} → L a c → Interleaving l r cs → Interleaving (a ∷ l) r (c ∷ cs)
+    _∷ʳ_ : ∀ {b c l r cs} → R b c → Interleaving l r cs → Interleaving l (b ∷ r) (c ∷ cs)
+
+------------------------------------------------------------------------
+-- Operations
+
+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
+
+-- injections
+
+  left : ∀ {as cs} → Pointwise L as cs → Interleaving L R as [] cs
+  left []       = []
+  left (l ∷ pw) = l ∷ˡ left pw
+
+  right : ∀ {bs cs} → Pointwise R bs cs → Interleaving L R [] bs cs
+  right []       = []
+  right (r ∷ pw) = r ∷ʳ right pw
+
+-- swap
+
+  swap : ∀ {cs l r} → Interleaving L R l r cs → Interleaving R L r l cs
+  swap []        = []
+  swap (l ∷ˡ sp) = l ∷ʳ swap sp
+  swap (r ∷ʳ sp) = r ∷ˡ swap sp
+
+-- extract the "proper" equality split from the pointwise relations
+
+  break : ∀ {cs l r} → Interleaving L R l r cs → ∃ $ uncurry $ λ csl csr →
+          Interleaving _≡_ _≡_ csl csr cs × Pointwise L l csl × Pointwise R r csr
+  break []        = -, [] , [] , []
+  break (l ∷ˡ sp) = let (_ , eq , pwl , pwr) = break sp in
+                    -, P.refl ∷ˡ eq , l ∷ pwl , pwr
+  break (r ∷ʳ sp) = let (_ , eq , pwl , pwr) = break sp in
+                    -, P.refl ∷ʳ eq , pwl , r ∷ pwr
+
+-- map
+
+module _ {a b c l r p q} {A : Set a} {B : Set b} {C : Set c}
+         {L : REL A C l} {R : REL B C r} {P : REL A C p} {Q : REL B C q} where
+
+  map : ∀ {cs l r} → L ⇒ P → R ⇒ Q → Interleaving L R l r cs → Interleaving P Q l r cs
+  map L⇒P R⇒Q []        = []
+  map L⇒P R⇒Q (l ∷ˡ sp) = L⇒P l ∷ˡ map L⇒P R⇒Q sp
+  map L⇒P R⇒Q (r ∷ʳ sp) = R⇒Q r ∷ʳ map L⇒P R⇒Q sp
+
+module _ {a b c l r p} {A : Set a} {B : Set b} {C : Set c}
+         {L : REL A C l} {R : REL B C r} where
+
+  map₁ : ∀ {P : REL A C p} {as l r} → L ⇒ P →
+         Interleaving L R l r as → Interleaving P R l r as
+  map₁ L⇒P = map L⇒P id
+
+  map₂ : ∀ {P : REL B C p} {as l r} → R ⇒ P →
+         Interleaving L R l r as → Interleaving L P l r as
+  map₂ = map id
+
+------------------------------------------------------------------------
+-- Special case: The second and third list have the same type
+
+module _ {a b l r} {A : Set a} {B : Set b} {L : REL A B l} {R : REL A B r} where
+
+-- converting back and forth with pointwise
+
+  split : ∀ {as bs} → Pointwise (λ a b → L a b ⊎ R a b) as bs →
+          ∃₂ λ asr asl → Interleaving L R asl asr bs
+  split []            = [] , [] , []
+  split (inj₁ l ∷ pw) = Prod.map _ (Prod.map _ (l ∷ˡ_)) (split pw)
+  split (inj₂ r ∷ pw) = Prod.map _ (Prod.map _ (r ∷ʳ_)) (split pw)
+
+  unsplit : ∀ {l r as} → Interleaving L R l r as →
+            ∃ λ bs → Pointwise (λ a b → L a b ⊎ R a b) bs as
+  unsplit []        = -, []
+  unsplit (l ∷ˡ sp) = Prod.map _ (inj₁ l ∷_) (unsplit sp)
+  unsplit (r ∷ʳ sp) = Prod.map _ (inj₂ r ∷_) (unsplit sp)

src/Data/List/Relation/Interleaving/Properties.agda

@@ -0,0 +1,107 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of general interleavings
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.List.Relation.Interleaving.Properties where
+
+open import Data.Nat
+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.Interleaving hiding (map)
+open import Function
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; refl; sym; cong; module ≡-Reasoning)
+open ≡-Reasoning
+
+------------------------------------------------------------------------
+-- length
+
+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₂
+
+------------------------------------------------------------------------
+-- map
+
+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
+  -- impossible cases needed until 2.6.0
+  map⁻ {[]} {_} {_ ∷ _} ()
+  map⁻ {[]} {_ ∷ _} {_} ()
+  map⁻ {_ ∷ _} {[]} {[]} ()
+
+------------------------------------------------------------------------
+-- reverse
+
+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₂
+
+  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′

src/Data/List/Relation/Interleaving/Propositional.agda

@@ -0,0 +1,46 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Interleavings of lists using propositional equality
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (Setoid)
+
+module Data.List.Relation.Interleaving.Propositional {a} {A : Set a} where
+
+open import Level using (_⊔_)
+open import Data.List.Base as List using (List; []; _∷_; _++_)
+open import Data.List.Relation.Pointwise as Pw using ()
+open import Data.List.Relation.Interleaving.Properties
+open import Data.List.Relation.Permutation.Inductive as Perm using (_↭_)
+open import Data.List.Relation.Permutation.Inductive.Properties using (shift)
+import Data.List.Relation.Interleaving.Setoid as General
+open import Relation.Binary.PropositionalEquality using (setoid; refl)
+open Perm.PermutationReasoning
+
+------------------------------------------------------------------------
+-- Re-export the basic combinators
+
+open General hiding (Interleaving) public
+
+------------------------------------------------------------------------
+-- Definition
+
+Interleaving : List A → List A → List A → Set a
+Interleaving = General.Interleaving (setoid A)
+
+pattern consˡ xs = refl ∷ˡ xs
+pattern consʳ xs = refl ∷ʳ xs
+
+------------------------------------------------------------------------
+-- New combinators
+
+toPermutation : ∀ {l r as} → Interleaving l r as → as ↭ l ++ r
+toPermutation []         = Perm.refl
+toPermutation (consˡ sp) = Perm.prep _ (toPermutation sp)
+toPermutation {l} {r ∷ rs} {a ∷ as} (consʳ sp) = begin
+  a ∷ as       ↭⟨ Perm.prep a (toPermutation sp) ⟩
+  a ∷ l ++ rs  ↭⟨ Perm.↭-sym (shift a l rs) ⟩
+  l ++ a ∷ rs  ∎

src/Data/List/Relation/Interleaving/Propositional/Properties.agda

@@ -0,0 +1,18 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of interleaving using propositional equality
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.List.Relation.Interleaving.Propositional.Properties
+  {a} {A : Set a} where
+
+import Data.List.Relation.Interleaving.Setoid.Properties as SetoidProperties
+open import Relation.Binary.PropositionalEquality using (setoid)
+
+------------------------------------------------------------------------
+-- Re-exporting existing properties
+
+open SetoidProperties (setoid A) public

src/Data/List/Relation/Interleaving/Setoid.agda

@@ -0,0 +1,28 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Interleavings of lists using setoid equality
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (Setoid)
+
+module Data.List.Relation.Interleaving.Setoid {c ℓ} (S : Setoid c ℓ) where
+
+open import Level using (_⊔_)
+open import Data.List.Base as List using (List; []; _∷_)
+open import Data.List.Relation.Interleaving.Properties
+import Data.List.Relation.Interleaving as General
+open Setoid S renaming (Carrier to A)
+
+------------------------------------------------------------------------
+-- Definition
+
+Interleaving : List A → List A → List A → Set (c ⊔ ℓ)
+Interleaving = General.Interleaving _≈_ _≈_
+
+------------------------------------------------------------------------
+-- Re-export the basic combinators
+
+open General hiding (Interleaving) public