[ new ] Interleaving of Lists

src/Data/List/Base.agda

@@ -14,7 +14,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)
@@ -309,8 +309,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/Split.agda

@@ -0,0 +1,109 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- General notion of splitting a list in two in an order-preserving manner
+------------------------------------------------------------------------
+
+module Data.List.Relation.Split where
+
+open import Level
+open import Data.List.Base as List using (List; []; _∷_)
+open import Data.List.Relation.Pointwise using (Pointwise; []; _∷_)
+open import Data.List.Relation.Permutation.Inductive as Perm using (_↭_)
+open import Data.List.Relation.Permutation.Inductive.Properties using (shift)
+open import Data.Product as Prod using (∃; ∃₂; _×_; uncurry; _,_; -,_; proj₂)
+open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
+open import Function
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality as P using (_≡_)
+
+module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c}
+         (L : REL A B l) (R : REL A C r) where
+
+  data Split : List A → REL (List B) (List C) (l ⊔ r) where
+    []   : Split [] [] []
+    _ˡ∷_ : ∀ {a b as l r} → L a b → Split as l r → Split (a ∷ as) (b ∷ l) r
+    _ʳ∷_ : ∀ {a b as l r} → R a b → Split as l r → Split (a ∷ as) l (b ∷ r)
+
+module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c}
+         {L : REL A B l} {R : REL A C r} where
+
+-- injections
+
+  left : ∀ {as bs} → Pointwise L as bs → Split L R as bs []
+  left []       = []
+  left (l ∷ pw) = l ˡ∷ left pw
+
+  right : ∀ {as bs} → Pointwise R as bs → Split L R as [] bs
+  right []       = []
+  right (r ∷ pw) = r ʳ∷ right pw
+
+-- swap
+
+  swap : ∀ {as l r} → Split L R as l r → Split R L as r l
+  swap []        = []
+  swap (l ˡ∷ sp) = l ʳ∷ swap sp
+  swap (r ʳ∷ sp) = r ˡ∷ swap sp
+
+-- extract the "proper" equality split from the pointwise relations
+
+  break : ∀ {as l r} → Split L R as l r → ∃ $ uncurry $ λ asl asr →
+          Split _≡_ _≡_ as asl asr × Pointwise L asl l × Pointwise R asr r
+  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 B l} {R : REL A C r} {P : REL A B p} {Q : REL A C q} where
+
+  map : ∀ {as l r} → L ⇒ P → R ⇒ Q → Split L R as l r → Split P Q as l r
+  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 B l} {R : REL A C r} where
+
+  map₁ : ∀ {P : REL A B p} {as l r} → L ⇒ P → Split L R as l r → Split P R as l r
+  map₁ L⇒P = map L⇒P id
+
+  map₂ : ∀ {P : REL A C p} {as l r} → R ⇒ P → Split L R as l r → Split L P as l r
+  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 →
+          ∃ (uncurry $ Split L R as)
+  split []            = -, []
+  split (inj₁ l ∷ pw) = Prod.map _ (l ˡ∷_) (split pw)
+  split (inj₂ r ∷ pw) = Prod.map _ (r ʳ∷_) (split pw)
+
+  unsplit : ∀ {as l r} → Split L R as l r → ∃ (Pointwise (λ a b → L a b ⊎ R a b) as)
+  unsplit []        = -, []
+  unsplit (l ˡ∷ sp) = Prod.map _ (inj₁ l ∷_) (unsplit sp)
+  unsplit (r ʳ∷ sp) = Prod.map _ (inj₂ r ∷_) (unsplit sp)
+
+------------------------------------------------------------------------
+-- Special case: all the lists have the same type
+
+module _ {a} {A : Set a} where
+
+-- An equality split induces a permutation:
+
+  toPermutation : {as l r : List A} → Split _≡_ _≡_ as l r → as ↭ l List.++ r
+  toPermutation []             = Perm.refl
+  toPermutation (P.refl ˡ∷ sp) = Perm.prep _ (toPermutation sp)
+  toPermutation {a ∷ as} {l} {r ∷ rs} (P.refl ʳ∷ sp) = begin
+    a ∷ as           ↭⟨ Perm.prep a (toPermutation sp) ⟩
+    a ∷ l List.++ rs ↭⟨ Perm.↭-sym (shift a l rs) ⟩
+    l List.++ a ∷ rs ∎ where open Perm.PermutationReasoning

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

@@ -0,0 +1,89 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of list-splitting
+------------------------------------------------------------------------
+
+module Data.List.Relation.Split.Properties where
+
+open import Data.Nat
+open import Data.Nat.Properties using (+-suc)
+open import Data.List.Base as List using (List; []; _∷_)
+open import Data.List.Properties using (reverse-involutive)
+open import Data.List.Relation.Split
+open import Function
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality as P using (_≡_)
+
+
+module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c}
+         {L : REL A B l} {R : REL A C r} where
+
+  length : ∀ {as l r} → Split L R as l r →
+           List.length as ≡ List.length l + List.length r
+  length []        = P.refl
+  length (l ˡ∷ sp) = P.cong suc (length sp)
+  length {as} {l} {r ∷ rs} (_ ʳ∷ sp) = begin
+    List.length as                       ≡⟨ P.cong suc (length sp) ⟩
+    suc (List.length l + List.length rs) ≡⟨ P.sym $ +-suc _ _ ⟩
+    List.length l + List.length (r ∷ rs) ∎ where open P.≡-Reasoning
+
+------------------------------------------------------------------------
+-- Split is stable under some List functions
+
+-- (++)
+
+  ++⁺ : ∀ {as₁ as₂ l₁ l₂ r₁ r₂} → Split L R as₁ l₁ r₁ → Split L R as₂ l₂ r₂ →
+        Split L R (as₁ List.++ as₂) (l₁ List.++ l₂) (r₁ List.++ r₂)
+  ++⁺ []         sp₂ = sp₂
+  ++⁺ (l ˡ∷ sp₁) sp₂ = l ˡ∷ (++⁺ sp₁ sp₂)
+  ++⁺ (r ʳ∷ sp₁) sp₂ = r ʳ∷ (++⁺ sp₁ sp₂)
+
+  disjoint : ∀ {as₁ as₂ l₁ r₂} → Split L R as₁ l₁ [] → Split L R as₂ [] r₂ →
+             Split L R (as₁ List.++ as₂) l₁ r₂
+  disjoint []         sp₂ = sp₂
+  disjoint (l ˡ∷ sp₁) sp₂ = l ˡ∷ disjoint sp₁ sp₂
+
+-- map
+
+  map⁺ : ∀ {d e f} {D : Set d} {E : Set e} {F : Set f} {as l r}
+         (f : D → A) (g : E → B) (h : F → C) →
+         Split (λ a b → L (f a) (g b)) (λ a c → R (f a) (h c)) as l r →
+         Split L R (List.map f as) (List.map g l) (List.map h r)
+  map⁺ f g h []        = []
+  map⁺ f g h (l ˡ∷ sp) = l ˡ∷ map⁺ f g h sp
+  map⁺ f g h (r ʳ∷ sp) = r ʳ∷ map⁺ f g h sp
+
+  map⁻ : ∀ {d e f} {D : Set d} {E : Set e} {F : Set f} {as l r}
+         (f : D → A) (g : E → B) (h : F → C) →
+         Split L R (List.map f as) (List.map g l) (List.map h r) →
+         Split (λ a b → L (f a) (g b)) (λ a c → R (f a) (h c)) as l r
+  map⁻ {as = []}    {[]}    {[]}    f g h []        = []
+  map⁻ {as = _ ∷ _} {[]}    {_ ∷ _} f g h (r ʳ∷ sp) = r ʳ∷ map⁻ f g h sp
+  map⁻ {as = _ ∷ _} {_ ∷ _} {[]}    f g h (l ˡ∷ sp) = l ˡ∷ map⁻ f g h sp
+  map⁻ {as = _ ∷ _} {_ ∷ _} {_ ∷ _} f g h (l ˡ∷ sp) = l ˡ∷ map⁻ f g h sp
+  map⁻ {as = _ ∷ _} {_ ∷ _} {_ ∷ _} f g h (r ʳ∷ sp) = r ʳ∷ map⁻ f g h sp
+  -- impossible cases needed until 2.6.0
+  map⁻ {as = []} {_} {_ ∷ _} f g h ()
+  map⁻ {as = []} {_ ∷ _} {_} f g h ()
+  map⁻ {as = _ ∷ _} {[]} {[]} f g h ()
+
+-- reverse
+
+  reverseAcc⁺ : ∀ {as₁ as₂ l₁ l₂ r₁ r₂} → Split L R as₁ l₁ r₁ → Split L R as₂ l₂ r₂ →
+    Split L R (List.reverseAcc as₁ as₂) (List.reverseAcc l₁ l₂) (List.reverseAcc r₁ r₂)
+  reverseAcc⁺ sp₁ []         = sp₁
+  reverseAcc⁺ sp₁ (l ˡ∷ sp₂) = reverseAcc⁺ (l ˡ∷ sp₁) sp₂
+  reverseAcc⁺ sp₁ (r ʳ∷ sp₂) = reverseAcc⁺ (r ʳ∷ sp₁) sp₂
+
+  reverse⁺ : ∀ {as l r} → Split L R as l r →
+            Split L R (List.reverse as) (List.reverse l) (List.reverse r)
+  reverse⁺ = reverseAcc⁺ []
+
+  reverse⁻ : ∀ {as l r} → Split L R (List.reverse as) (List.reverse l) (List.reverse r) →
+             Split L R as l r
+  reverse⁻ {as} {l} {r} sp with reverse⁺ sp
+  ... | sp′ rewrite reverse-involutive as
+                  | reverse-involutive l
+                  | reverse-involutive r = sp′
+

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

@@ -0,0 +1,24 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- List-splitting using a setoid
+------------------------------------------------------------------------
+
+open import Relation.Binary using (Setoid)
+
+module Data.List.Relation.Split.Setoid {c ℓ} (S : Setoid c ℓ) where
+
+open import Data.List.Base as List using (List; []; _∷_)
+open import Data.List.Relation.Pointwise as Pw
+open import Data.List.Relation.Split.Properties
+private module S = Setoid S renaming (Carrier to A); open S
+
+-- re-exporting the basic combinators
+open import Data.List.Relation.Split as Split hiding (Split) public
+
+-- defining a specialised version of the datatype
+Split : List A → List A → List A → Set ℓ
+Split = Split.Split _≈_ _≈_
+
+_++_ : (xs ys : List A) → Split (xs List.++ ys) xs ys
+xs ++ ys = disjoint (Split.left (Pw.refl S.refl)) (Split.right (Pw.refl S.refl))