Skip to content

Commit ab43a34

Browse files
gallaisMatthewDaggitt
gallais
authored and
MatthewDaggitt
committed
[ new ] Interleaving of Lists (#529)
1 parent 861b96c commit ab43a34

File tree

9 files changed

+371
-5
lines changed

9 files changed

+371
-5
lines changed

‎CHANGELOG.md

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -256,6 +256,11 @@ Other major changes
256256
generalization of the notion of "first element in the list to satisfy a
257257
predicate".
258258

259+
* Added new modules `Data.List.Relation.Prefix.Heterogeneous(.Properties)`
260+
261+
* Added new modules `Data.List.Relation.Interleaving(.Setoid/Propositional)`
262+
and `Data.List.Relation.Interleaving(.Setoid/Propositional).Properties`.
263+
259264
* Added new module `Data.Vec.Any.Properties`
260265

261266
* Added new modules `Data.Vec.Membership.(Setoid/DecSetoid/DecPropositional)`
@@ -509,6 +514,8 @@ Other minor additions
509514
_[_]%=_ : (xs : List A) → Fin (length xs) → (A → A) → List A
510515
_[_]∷=_ : (xs : List A) → Fin (length xs) → A → List A
511516
_─_ : (xs : List A) → Fin (length xs) → List A
517+
518+
reverseAcc : List A → List A → List A
512519
```
513520

514521
* Added new proofs to `Data.List.All.Properties`:
@@ -693,9 +700,10 @@ Other minor additions
693700
wlog : Total _R_ → Symmetric Q → (∀ a b → a R b → Q a b) → ∀ a b → Q a b
694701
```
695702

696-
* Added new definition to `Relation.Binary.Core`:
703+
* Added new definitions to `Relation.Binary.Core`:
697704
```agda
698705
Antisym R S E = ∀ {i j} → R i j → S j i → E i j
706+
Conn P Q = ∀ x y → P x y ⊎ Q y x
699707
```
700708

701709
* Added new proofs to `Relation.Binary.Lattice`:

‎src/Data/List/Base.agda

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ open import Data.Bool.Base as Bool
1616
open import Data.Maybe.Base as Maybe using (Maybe; nothing; just)
1717
open import Data.Product as Prod using (_×_; _,_)
1818
open import Data.These as These using (These; this; that; these)
19-
open import Function using (id; _∘_ ; _∘′_; const)
19+
open import Function using (id; _∘_ ; _∘′_; const; flip)
2020

2121
open import Relation.Nullary using (yes; no)
2222
open import Relation.Unary using (Pred; Decidable)
@@ -324,8 +324,13 @@ module _ {a} {A : Set a} where
324324
------------------------------------------------------------------------
325325
-- Operations for reversing lists
326326

327-
reverse : ∀ {a} {A : Set a} → List A → List A
328-
reverse = foldl (λ rev x → x ∷ rev) []
327+
module _ {a} {A : Set a} where
328+
329+
reverseAcc : List A → List A → List A
330+
reverseAcc = foldl (flip _∷_)
331+
332+
reverse : List A → List A
333+
reverse = reverseAcc []
329334

330335
-- Snoc.
331336

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

Lines changed: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,103 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Generalised notion of interleaving two lists into one in an
5+
-- order-preserving manner
6+
------------------------------------------------------------------------
7+
8+
{-# OPTIONS --without-K --safe #-}
9+
10+
module Data.List.Relation.Interleaving where
11+
12+
open import Level
13+
open import Data.List.Base as List using (List; []; _∷_; _++_)
14+
open import Data.List.Relation.Pointwise using (Pointwise; []; _∷_)
15+
open import Data.Product as Prod using (∃; ∃₂; _×_; uncurry; _,_; -,_; proj₂)
16+
open import Data.Sum using (_⊎_; inj₁; inj₂)
17+
open import Function
18+
open import Relation.Binary
19+
open import Relation.Binary.PropositionalEquality as P using (_≡_)
20+
21+
------------------------------------------------------------------------
22+
-- Definition
23+
24+
module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c}
25+
(L : REL A C l) (R : REL B C r) where
26+
27+
data Interleaving : List A → List B → List C → Set (a ⊔ b ⊔ c ⊔ l ⊔ r) where
28+
[] : Interleaving [] [] []
29+
_∷ˡ_ : ∀ {a c l r cs} → L a c → Interleaving l r cs → Interleaving (a ∷ l) r (c ∷ cs)
30+
_∷ʳ_ : ∀ {b c l r cs} → R b c → Interleaving l r cs → Interleaving l (b ∷ r) (c ∷ cs)
31+
32+
------------------------------------------------------------------------
33+
-- Operations
34+
35+
module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c}
36+
{L : REL A C l} {R : REL B C r} where
37+
38+
-- injections
39+
40+
left : ∀ {as cs} → Pointwise L as cs → Interleaving L R as [] cs
41+
left [] = []
42+
left (l ∷ pw) = l ∷ˡ left pw
43+
44+
right : ∀ {bs cs} → Pointwise R bs cs → Interleaving L R [] bs cs
45+
right [] = []
46+
right (r ∷ pw) = r ∷ʳ right pw
47+
48+
-- swap
49+
50+
swap : ∀ {cs l r} → Interleaving L R l r cs → Interleaving R L r l cs
51+
swap [] = []
52+
swap (l ∷ˡ sp) = l ∷ʳ swap sp
53+
swap (r ∷ʳ sp) = r ∷ˡ swap sp
54+
55+
-- extract the "proper" equality split from the pointwise relations
56+
57+
break : ∀ {cs l r} → Interleaving L R l r cs → ∃ $ uncurry $ λ csl csr →
58+
Interleaving _≡_ _≡_ csl csr cs × Pointwise L l csl × Pointwise R r csr
59+
break [] = -, [] , [] , []
60+
break (l ∷ˡ sp) = let (_ , eq , pwl , pwr) = break sp in
61+
-, P.refl ∷ˡ eq , l ∷ pwl , pwr
62+
break (r ∷ʳ sp) = let (_ , eq , pwl , pwr) = break sp in
63+
-, P.refl ∷ʳ eq , pwl , r ∷ pwr
64+
65+
-- map
66+
67+
module _ {a b c l r p q} {A : Set a} {B : Set b} {C : Set c}
68+
{L : REL A C l} {R : REL B C r} {P : REL A C p} {Q : REL B C q} where
69+
70+
map : ∀ {cs l r} → L ⇒ P → R ⇒ Q → Interleaving L R l r cs → Interleaving P Q l r cs
71+
map L⇒P R⇒Q [] = []
72+
map L⇒P R⇒Q (l ∷ˡ sp) = L⇒P l ∷ˡ map L⇒P R⇒Q sp
73+
map L⇒P R⇒Q (r ∷ʳ sp) = R⇒Q r ∷ʳ map L⇒P R⇒Q sp
74+
75+
module _ {a b c l r p} {A : Set a} {B : Set b} {C : Set c}
76+
{L : REL A C l} {R : REL B C r} where
77+
78+
map₁ : ∀ {P : REL A C p} {as l r} → L ⇒ P →
79+
Interleaving L R l r as → Interleaving P R l r as
80+
map₁ L⇒P = map L⇒P id
81+
82+
map₂ : ∀ {P : REL B C p} {as l r} → R ⇒ P →
83+
Interleaving L R l r as → Interleaving L P l r as
84+
map₂ = map id
85+
86+
------------------------------------------------------------------------
87+
-- Special case: The second and third list have the same type
88+
89+
module _ {a b l r} {A : Set a} {B : Set b} {L : REL A B l} {R : REL A B r} where
90+
91+
-- converting back and forth with pointwise
92+
93+
split : ∀ {as bs} → Pointwise (λ a b → L a b ⊎ R a b) as bs →
94+
∃₂ λ asr asl → Interleaving L R asl asr bs
95+
split [] = [] , [] , []
96+
split (inj₁ l ∷ pw) = Prod.map _ (Prod.map _ (l ∷ˡ_)) (split pw)
97+
split (inj₂ r ∷ pw) = Prod.map _ (Prod.map _ (r ∷ʳ_)) (split pw)
98+
99+
unsplit : ∀ {l r as} → Interleaving L R l r as →
100+
∃ λ bs → Pointwise (λ a b → L a b ⊎ R a b) bs as
101+
unsplit [] = -, []
102+
unsplit (l ∷ˡ sp) = Prod.map _ (inj₁ l ∷_) (unsplit sp)
103+
unsplit (r ∷ʳ sp) = Prod.map _ (inj₂ r ∷_) (unsplit sp)

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

Lines changed: 107 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,107 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Properties of general interleavings
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
module Data.List.Relation.Interleaving.Properties where
10+
11+
open import Data.Nat
12+
open import Data.Nat.Properties using (+-suc)
13+
open import Data.List.Base hiding (_∷ʳ_)
14+
open import Data.List.Properties using (reverse-involutive)
15+
open import Data.List.Relation.Interleaving hiding (map)
16+
open import Function
17+
open import Relation.Binary
18+
open import Relation.Binary.PropositionalEquality
19+
using (_≡_; refl; sym; cong; module ≡-Reasoning)
20+
open ≡-Reasoning
21+
22+
------------------------------------------------------------------------
23+
-- length
24+
25+
module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c}
26+
{L : REL A C l} {R : REL B C r} where
27+
28+
interleave-length : ∀ {as l r} → Interleaving L R l r as →
29+
length as ≡ length l + length r
30+
interleave-length [] = refl
31+
interleave-length (l ∷ˡ sp) = cong suc (interleave-length sp)
32+
interleave-length {as} {l} {r ∷ rs} (_ ∷ʳ sp) = begin
33+
length as ≡⟨ cong suc (interleave-length sp) ⟩
34+
suc (length l + length rs) ≡⟨ sym $ +-suc _ _ ⟩
35+
length l + length (r ∷ rs) ∎
36+
37+
------------------------------------------------------------------------
38+
-- _++_
39+
40+
++⁺ : ∀ {as₁ as₂ l₁ l₂ r₁ r₂} →
41+
Interleaving L R as₁ l₁ r₁ → Interleaving L R as₂ l₂ r₂ →
42+
Interleaving L R (as₁ ++ as₂) (l₁ ++ l₂) (r₁ ++ r₂)
43+
++⁺ [] sp₂ = sp₂
44+
++⁺ (l ∷ˡ sp₁) sp₂ = l ∷ˡ (++⁺ sp₁ sp₂)
45+
++⁺ (r ∷ʳ sp₁) sp₂ = r ∷ʳ (++⁺ sp₁ sp₂)
46+
47+
++-disjoint : ∀ {as₁ as₂ l₁ r₂} →
48+
Interleaving L R l₁ [] as₁ → Interleaving L R [] r₂ as₂ →
49+
Interleaving L R l₁ r₂ (as₁ ++ as₂)
50+
++-disjoint [] sp₂ = sp₂
51+
++-disjoint (l ∷ˡ sp₁) sp₂ = l ∷ˡ ++-disjoint sp₁ sp₂
52+
53+
------------------------------------------------------------------------
54+
-- map
55+
56+
module _ {a b c d e f l r}
57+
{A : Set a} {B : Set b} {C : Set c}
58+
{D : Set d} {E : Set e} {F : Set f}
59+
{L : REL A C l} {R : REL B C r}
60+
(f : E → A) (g : F → B) (h : D → C)
61+
where
62+
63+
map⁺ : ∀ {as l r} →
64+
Interleaving (λ x z → L (f x) (h z)) (λ y z → R (g y) (h z)) l r as →
65+
Interleaving L R (map f l) (map g r) (map h as)
66+
map⁺ [] = []
67+
map⁺ (l ∷ˡ sp) = l ∷ˡ map⁺ sp
68+
map⁺ (r ∷ʳ sp) = r ∷ʳ map⁺ sp
69+
70+
map⁻ : ∀ {as l r} →
71+
Interleaving L R (map f l) (map g r) (map h as) →
72+
Interleaving (λ x z → L (f x) (h z)) (λ y z → R (g y) (h z)) l r as
73+
map⁻ {[]} {[]} {[]} [] = []
74+
map⁻ {_ ∷ _} {[]} {_ ∷ _} (r ∷ʳ sp) = r ∷ʳ map⁻ sp
75+
map⁻ {_ ∷ _} {_ ∷ _} {[]} (l ∷ˡ sp) = l ∷ˡ map⁻ sp
76+
map⁻ {_ ∷ _} {_ ∷ _} {_ ∷ _} (l ∷ˡ sp) = l ∷ˡ map⁻ sp
77+
map⁻ {_ ∷ _} {_ ∷ _} {_ ∷ _} (r ∷ʳ sp) = r ∷ʳ map⁻ sp
78+
-- impossible cases needed until 2.6.0
79+
map⁻ {[]} {_} {_ ∷ _} ()
80+
map⁻ {[]} {_ ∷ _} {_} ()
81+
map⁻ {_ ∷ _} {[]} {[]} ()
82+
83+
------------------------------------------------------------------------
84+
-- reverse
85+
86+
module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c}
87+
{L : REL A C l} {R : REL B C r}
88+
where
89+
90+
reverseAcc⁺ : ∀ {as₁ as₂ l₁ l₂ r₁ r₂} →
91+
Interleaving L R l₁ r₁ as₁ →
92+
Interleaving L R l₂ r₂ as₂ →
93+
Interleaving L R (reverseAcc l₁ l₂) (reverseAcc r₁ r₂) (reverseAcc as₁ as₂)
94+
reverseAcc⁺ sp₁ [] = sp₁
95+
reverseAcc⁺ sp₁ (l ∷ˡ sp₂) = reverseAcc⁺ (l ∷ˡ sp₁) sp₂
96+
reverseAcc⁺ sp₁ (r ∷ʳ sp₂) = reverseAcc⁺ (r ∷ʳ sp₁) sp₂
97+
98+
reverse⁺ : ∀ {as l r} → Interleaving L R l r as →
99+
Interleaving L R (reverse l) (reverse r) (reverse as)
100+
reverse⁺ = reverseAcc⁺ []
101+
102+
reverse⁻ : ∀ {as l r} → Interleaving L R (reverse l) (reverse r) (reverse as) →
103+
Interleaving L R l r as
104+
reverse⁻ {as} {l} {r} sp with reverse⁺ sp
105+
... | sp′ rewrite reverse-involutive as
106+
| reverse-involutive l
107+
| reverse-involutive r = sp′

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

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Interleavings of lists using propositional equality
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
open import Relation.Binary using (Setoid)
10+
11+
module Data.List.Relation.Interleaving.Propositional {a} {A : Set a} where
12+
13+
open import Level using (_⊔_)
14+
open import Data.List.Base as List using (List; []; _∷_; _++_)
15+
open import Data.List.Relation.Pointwise as Pw using ()
16+
open import Data.List.Relation.Interleaving.Properties
17+
open import Data.List.Relation.Permutation.Inductive as Perm using (_↭_)
18+
open import Data.List.Relation.Permutation.Inductive.Properties using (shift)
19+
import Data.List.Relation.Interleaving.Setoid as General
20+
open import Relation.Binary.PropositionalEquality using (setoid; refl)
21+
open Perm.PermutationReasoning
22+
23+
------------------------------------------------------------------------
24+
-- Re-export the basic combinators
25+
26+
open General hiding (Interleaving) public
27+
28+
------------------------------------------------------------------------
29+
-- Definition
30+
31+
Interleaving : List A → List A → List A → Set a
32+
Interleaving = General.Interleaving (setoid A)
33+
34+
pattern consˡ xs = refl ∷ˡ xs
35+
pattern consʳ xs = refl ∷ʳ xs
36+
37+
------------------------------------------------------------------------
38+
-- New combinators
39+
40+
toPermutation : ∀ {l r as} → Interleaving l r as → as ↭ l ++ r
41+
toPermutation [] = Perm.refl
42+
toPermutation (consˡ sp) = Perm.prep _ (toPermutation sp)
43+
toPermutation {l} {r ∷ rs} {a ∷ as} (consʳ sp) = begin
44+
a ∷ as ↭⟨ Perm.prep a (toPermutation sp) ⟩
45+
a ∷ l ++ rs ↭⟨ Perm.↭-sym (shift a l rs) ⟩
46+
l ++ a ∷ rs ∎

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

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Properties of interleaving using propositional equality
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
module Data.List.Relation.Interleaving.Propositional.Properties
10+
{a} {A : Set a} where
11+
12+
import Data.List.Relation.Interleaving.Setoid.Properties as SetoidProperties
13+
open import Relation.Binary.PropositionalEquality using (setoid)
14+
15+
------------------------------------------------------------------------
16+
-- Re-exporting existing properties
17+
18+
open SetoidProperties (setoid A) public

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

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Interleavings of lists using setoid equality
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
open import Relation.Binary using (Setoid)
10+
11+
module Data.List.Relation.Interleaving.Setoid {c ℓ} (S : Setoid c ℓ) where
12+
13+
open import Level using (_⊔_)
14+
open import Data.List.Base as List using (List; []; _∷_)
15+
open import Data.List.Relation.Interleaving.Properties
16+
import Data.List.Relation.Interleaving as General
17+
open Setoid S renaming (Carrier to A)
18+
19+
------------------------------------------------------------------------
20+
-- Definition
21+
22+
Interleaving : List A → List A → List A → Set (c ⊔ ℓ)
23+
Interleaving = General.Interleaving _≈_ _≈_
24+
25+
------------------------------------------------------------------------
26+
-- Re-export the basic combinators
27+
28+
open General hiding (Interleaving) public

0 commit comments

Comments
 (0)