diff --git a/master/Data.List.Relation.Binary.Sublist.DecSetoid.html b/master/Data.List.Relation.Binary.Sublist.DecSetoid.html
index 1092a00479..dc7f8e81fa 100644
--- a/master/Data.List.Relation.Binary.Sublist.DecSetoid.html
+++ b/master/Data.List.Relation.Binary.Sublist.DecSetoid.html
@@ -37,7 +37,7 @@
_⊆?_ : Decidable _⊆_
-_⊆?_ = HeterogeneousProperties.sublist? _≟_
+_⊆?_ = HeterogeneousProperties.sublist? _≟_
⊆-isDecPartialOrder : IsDecPartialOrder _≋_ _⊆_
⊆-isDecPartialOrder = record
diff --git a/master/Data.List.Relation.Binary.Sublist.Heterogeneous.Properties.html b/master/Data.List.Relation.Binary.Sublist.Heterogeneous.Properties.html
index a6ea206419..962e2485bd 100644
--- a/master/Data.List.Relation.Binary.Sublist.Heterogeneous.Properties.html
+++ b/master/Data.List.Relation.Binary.Sublist.Heterogeneous.Properties.html
@@ -40,687 +40,703 @@
open import Relation.Binary.Structures
using (IsPreorder; IsPartialOrder; IsDecPartialOrder)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
+import Relation.Binary.Reasoning.Preorder as ≲-Reasoning
+open import Relation.Binary.Reasoning.Syntax
+
+private
+ variable
+ a b c d e p q r s t : Level
+ A : Set a
+ B : Set b
+ C : Set c
+ D : Set d
+ x : A
+ y : B
+ as cs xs : List A
+ bs ds ys : List B
+ ass : List (List A)
+ bss : List (List B)
+ m n : ℕ
+
+
+
+
+module _ {R : REL A B r} where
+
+ ∷-injectiveˡ : {px qx : R x y} {pxs qxs : Sublist R xs ys} →
+ (Sublist R (x ∷ xs) (y ∷ ys) ∋ px ∷ pxs) ≡ (qx ∷ qxs) → px ≡ qx
+ ∷-injectiveˡ ≡.refl = ≡.refl
+
+ ∷-injectiveʳ : {px qx : R x y} {pxs qxs : Sublist R xs ys} →
+ (Sublist R (x ∷ xs) (y ∷ ys) ∋ px ∷ pxs) ≡ (qx ∷ qxs) → pxs ≡ qxs
+ ∷-injectiveʳ ≡.refl = ≡.refl
+
+ ∷ʳ-injective : {pxs qxs : Sublist R xs ys} →
+ (Sublist R xs (y ∷ ys) ∋ y ∷ʳ pxs) ≡ (y ∷ʳ qxs) → pxs ≡ qxs
+ ∷ʳ-injective ≡.refl = ≡.refl
+
+module _ {R : REL A B r} where
+
+ length-mono-≤ : Sublist R as bs → length as ≤ length bs
+ length-mono-≤ [] = z≤n
+ length-mono-≤ (y ∷ʳ rs) = ℕ.m≤n⇒m≤1+n (length-mono-≤ rs)
+ length-mono-≤ (r ∷ rs) = s≤s (length-mono-≤ rs)
+
+
+
+
+ fromPointwise : Pointwise R ⇒ Sublist R
+ fromPointwise [] = []
+ fromPointwise (p ∷ ps) = p ∷ fromPointwise ps
+
+ toPointwise : length as ≡ length bs →
+ Sublist R as bs → Pointwise R as bs
+ toPointwise {bs = []} eq [] = []
+ toPointwise {bs = b ∷ bs} eq (r ∷ rs) = r ∷ toPointwise (ℕ.suc-injective eq) rs
+ toPointwise {bs = b ∷ bs} eq (b ∷ʳ rs) =
+ contradiction (s≤s (length-mono-≤ rs)) (ℕ.<-irrefl eq)
+
+
+
+
+
+
+
+
+
+module _ {R : REL A B r} where
+
+ tail-Sublist : Sublist R as bs →
+ Maybe.All (λ as → Sublist R as bs) (tail as)
+ tail-Sublist [] = nothing
+ tail-Sublist (b ∷ʳ ps) = Maybe.map (b ∷ʳ_) (tail-Sublist ps)
+ tail-Sublist (p ∷ ps) = just (_ ∷ʳ ps)
+
+ take-Sublist : ∀ n → Sublist R as bs → Sublist R (take n as) bs
+ take-Sublist n (y ∷ʳ rs) = y ∷ʳ take-Sublist n rs
+ take-Sublist zero rs = minimum _
+ take-Sublist (suc n) [] = []
+ take-Sublist (suc n) (r ∷ rs) = r ∷ take-Sublist n rs
+
+ drop-Sublist : ∀ n → Sublist R ⇒ (Sublist R ∘′ drop n)
+ drop-Sublist n (y ∷ʳ rs) = y ∷ʳ drop-Sublist n rs
+ drop-Sublist zero rs = rs
+ drop-Sublist (suc n) [] = []
+ drop-Sublist (suc n) (r ∷ rs) = _ ∷ʳ drop-Sublist n rs
+
+module _ {R : REL A B r} {P : Pred A p} (P? : U.Decidable P) where
+
+ takeWhile-Sublist : Sublist R as bs → Sublist R (takeWhile P? as) bs
+ takeWhile-Sublist [] = []
+ takeWhile-Sublist (y ∷ʳ rs) = y ∷ʳ takeWhile-Sublist rs
+ takeWhile-Sublist {a ∷ as} (r ∷ rs) with does (P? a)
+ ... | true = r ∷ takeWhile-Sublist rs
+ ... | false = minimum _
+
+ dropWhile-Sublist : Sublist R as bs → Sublist R (dropWhile P? as) bs
+ dropWhile-Sublist [] = []
+ dropWhile-Sublist (y ∷ʳ rs) = y ∷ʳ dropWhile-Sublist rs
+ dropWhile-Sublist {a ∷ as} (r ∷ rs) with does (P? a)
+ ... | true = _ ∷ʳ dropWhile-Sublist rs
+ ... | false = r ∷ rs
+
+ filter-Sublist : Sublist R as bs → Sublist R (filter P? as) bs
+ filter-Sublist [] = []
+ filter-Sublist (y ∷ʳ rs) = y ∷ʳ filter-Sublist rs
+ filter-Sublist {a ∷ as} (r ∷ rs) with does (P? a)
+ ... | true = r ∷ filter-Sublist rs
+ ... | false = _ ∷ʳ filter-Sublist rs
+
+
+
+
+
+
+
+module _ {R : REL A B r} where
+
+
+
+
+ ∷ˡ⁻ : Sublist R (x ∷ xs) ys → Sublist R xs ys
+ ∷ˡ⁻ (y ∷ʳ rs) = y ∷ʳ ∷ˡ⁻ rs
+ ∷ˡ⁻ (r ∷ rs) = _ ∷ʳ rs
+
+ ∷ʳ⁻ : ¬ R x y → Sublist R (x ∷ xs) (y ∷ ys) →
+ Sublist R (x ∷ xs) ys
+ ∷ʳ⁻ ¬r (y ∷ʳ rs) = rs
+ ∷ʳ⁻ ¬r (r ∷ rs) = contradiction r ¬r
+
+ ∷⁻ : Sublist R (x ∷ xs) (y ∷ ys) → Sublist R xs ys
+ ∷⁻ (y ∷ʳ rs) = ∷ˡ⁻ rs
+ ∷⁻ (x ∷ rs) = rs
+
+module _ {R : REL C D r} where
+
+
+
+
+ map⁺ : (f : A → C) (g : B → D) →
+ Sublist (λ a b → R (f a) (g b)) as bs →
+ Sublist R (List.map f as) (List.map g bs)
+ map⁺ f g [] = []
+ map⁺ f g (y ∷ʳ rs) = g y ∷ʳ map⁺ f g rs
+ map⁺ f g (r ∷ rs) = r ∷ map⁺ f g rs
+
+ map⁻ : (f : A → C) (g : B → D) →
+ Sublist R (List.map f as) (List.map g bs) →
+ Sublist (λ a b → R (f a) (g b)) as bs
+ map⁻ {as = []} {bs} f g rs = minimum _
+ map⁻ {as = a ∷ as} {b ∷ bs} f g (_ ∷ʳ rs) = b ∷ʳ map⁻ f g rs
+ map⁻ {as = a ∷ as} {b ∷ bs} f g (r ∷ rs) = r ∷ map⁻ f g rs
+
+
+module _ {R : REL A B r} where
+
+
+
+
+ ++⁺ : Sublist R as bs → Sublist R cs ds →
+ Sublist R (as ++ cs) (bs ++ ds)
+ ++⁺ [] cds = cds
+ ++⁺ (y ∷ʳ abs) cds = y ∷ʳ ++⁺ abs cds
+ ++⁺ (ab ∷ abs) cds = ab ∷ ++⁺ abs cds
+
+ ++⁻ : length as ≡ length bs →
+ Sublist R (as ++ cs) (bs ++ ds) → Sublist R cs ds
+ ++⁻ {as = []} {[]} eq rs = rs
+ ++⁻ {as = a ∷ as} {b ∷ bs} eq rs = ++⁻ (ℕ.suc-injective eq) (∷⁻ rs)
+
+ ++ˡ : (cs : List B) → Sublist R as bs → Sublist R as (cs ++ bs)
+ ++ˡ zs = ++⁺ (minimum zs)
+
+ ++ʳ : (cs : List B) → Sublist R as bs → Sublist R as (bs ++ cs)
+ ++ʳ cs [] = minimum cs
+ ++ʳ cs (y ∷ʳ rs) = y ∷ʳ ++ʳ cs rs
+ ++ʳ cs (r ∷ rs) = r ∷ ++ʳ cs rs
+
+
+
+
+
+ concat⁺ : Sublist (Sublist R) ass bss →
+ Sublist R (concat ass) (concat bss)
+ concat⁺ [] = []
+ concat⁺ (y ∷ʳ rss) = ++ˡ y (concat⁺ rss)
+ concat⁺ (rs ∷ rss) = ++⁺ rs (concat⁺ rss)
+
+
+
+
+ take⁺ : m ≤ n → Pointwise R as bs →
+ Sublist R (take m as) (take n bs)
+ take⁺ z≤n ps = minimum _
+ take⁺ (s≤s m≤n) [] = []
+ take⁺ (s≤s m≤n) (p ∷ ps) = p ∷ take⁺ m≤n ps
+
+ drop⁺ : m ≥ n → Sublist R as bs →
+ Sublist R (drop m as) (drop n bs)
+ drop⁺ (z≤n {m}) rs = drop-Sublist m rs
+ drop⁺ (s≤s m≥n) [] = []
+ drop⁺ (s≤s m≥n) (y ∷ʳ rs) = drop⁺ (ℕ.m≤n⇒m≤1+n m≥n) rs
+ drop⁺ (s≤s m≥n) (r ∷ rs) = drop⁺ m≥n rs
+
+ drop⁺-≥ : m ≥ n → Pointwise R as bs →
+ Sublist R (drop m as) (drop n bs)
+ drop⁺-≥ m≥n pw = drop⁺ m≥n (fromPointwise pw)
+
+ drop⁺-⊆ : ∀ m → Sublist R as bs →
+ Sublist R (drop m as) (drop m bs)
+ drop⁺-⊆ m = drop⁺ (ℕ.≤-refl {m})
+
+module _ {R : REL A B r} {P : Pred A p} {Q : Pred B q}
+ (P? : U.Decidable P) (Q? : U.Decidable Q) where
+
+ ⊆-takeWhile-Sublist : (∀ {a b} → R a b → P a → Q b) →
+ Pointwise R as bs →
+ Sublist R (takeWhile P? as) (takeWhile Q? bs)
+ ⊆-takeWhile-Sublist rp⇒q [] = []
+ ⊆-takeWhile-Sublist {a ∷ as} {b ∷ bs} rp⇒q (p ∷ ps) with P? a | Q? b
+ ... | false because _ | _ = minimum _
+ ... | true because _ | true because _ = p ∷ ⊆-takeWhile-Sublist rp⇒q ps
+ ... | yes pa | no ¬qb = contradiction (rp⇒q p pa) ¬qb
+
+ ⊇-dropWhile-Sublist : (∀ {a b} → R a b → Q b → P a) →
+ Pointwise R as bs →
+ Sublist R (dropWhile P? as) (dropWhile Q? bs)
+ ⊇-dropWhile-Sublist rq⇒p [] = []
+ ⊇-dropWhile-Sublist {a ∷ as} {b ∷ bs} rq⇒p (p ∷ ps) with P? a | Q? b
+ ... | true because _ | true because _ = ⊇-dropWhile-Sublist rq⇒p ps
+ ... | true because _ | false because _ =
+ b ∷ʳ dropWhile-Sublist P? (fromPointwise ps)
+ ... | false because _ | false because _ = p ∷ fromPointwise ps
+ ... | no ¬pa | yes qb = contradiction (rq⇒p p qb) ¬pa
+
+ ⊆-filter-Sublist : (∀ {a b} → R a b → P a → Q b) →
+ Sublist R as bs → Sublist R (filter P? as) (filter Q? bs)
+ ⊆-filter-Sublist rp⇒q [] = []
+ ⊆-filter-Sublist rp⇒q (y ∷ʳ rs) with does (Q? y)
+ ... | true = y ∷ʳ ⊆-filter-Sublist rp⇒q rs
+ ... | false = ⊆-filter-Sublist rp⇒q rs
+ ⊆-filter-Sublist {a ∷ as} {b ∷ bs} rp⇒q (r ∷ rs) with P? a | Q? b
+ ... | true because _ | true because _ = r ∷ ⊆-filter-Sublist rp⇒q rs
+ ... | false because _ | true because _ = _ ∷ʳ ⊆-filter-Sublist rp⇒q rs
+ ... | false because _ | false because _ = ⊆-filter-Sublist rp⇒q rs
+ ... | yes pa | no ¬qb = contradiction (rp⇒q r pa) ¬qb
+
+module _ {R : Rel A r} {P : Pred A p} (P? : U.Decidable P) where
+
+ takeWhile-filter : Pointwise R as as →
+ Sublist R (takeWhile P? as) (filter P? as)
+ takeWhile-filter [] = []
+ takeWhile-filter {a ∷ as} (p ∷ ps) with does (P? a)
+ ... | true = p ∷ takeWhile-filter ps
+ ... | false = minimum _
+
+ filter-dropWhile : Pointwise R as as →
+ Sublist R (filter P? as) (dropWhile (¬? ∘ P?) as)
+ filter-dropWhile [] = []
+ filter-dropWhile {a ∷ as} (p ∷ ps) with does (P? a)
+ ... | true = p ∷ filter-Sublist P? (fromPointwise ps)
+ ... | false = filter-dropWhile ps
+
+
+
+
+module _ {R : REL A B r} where
+
+ reverseAcc⁺ : Sublist R as bs → Sublist R cs ds →
+ Sublist R (reverseAcc cs as) (reverseAcc ds bs)
+ reverseAcc⁺ [] cds = cds
+ reverseAcc⁺ (y ∷ʳ abs) cds = reverseAcc⁺ abs (y ∷ʳ cds)
+ reverseAcc⁺ (r ∷ abs) cds = reverseAcc⁺ abs (r ∷ cds)
+
+ ʳ++⁺ : Sublist R as bs → Sublist R cs ds →
+ Sublist R (as ʳ++ cs) (bs ʳ++ ds)
+ ʳ++⁺ = reverseAcc⁺
+
+ reverse⁺ : Sublist R as bs → Sublist R (reverse as) (reverse bs)
+ reverse⁺ rs = reverseAcc⁺ rs []
+
+ reverse⁻ : Sublist R (reverse as) (reverse bs) → Sublist R as bs
+ reverse⁻ {as = as} {bs = bs} p = cast (reverse⁺ p) where
+ cast = ≡.subst₂ (Sublist R) (List.reverse-involutive as) (List.reverse-involutive bs)
+
+
+
+
+module _ {R : REL A B r} where
+
+ ∷⁻¹ : R x y → Sublist R xs ys ⇔ Sublist R (x ∷ xs) (y ∷ ys)
+ ∷⁻¹ r = mk⇔ (r ∷_) ∷⁻
+
+ ∷ʳ⁻¹ : ¬ R x y → Sublist R (x ∷ xs) ys ⇔ Sublist R (x ∷ xs) (y ∷ ys)
+ ∷ʳ⁻¹ ¬r = mk⇔ (_ ∷ʳ_) (∷ʳ⁻ ¬r)
+
+
+
+
+module _ {R : REL A B r} where
+
+ Sublist-[]-universal : U.Universal (Sublist R [])
+ Sublist-[]-universal [] = []
+ Sublist-[]-universal (_ ∷ _) = _ ∷ʳ Sublist-[]-universal _
+
+ Sublist-[]-irrelevant : U.Irrelevant (Sublist R [])
+ Sublist-[]-irrelevant [] [] = ≡.refl
+ Sublist-[]-irrelevant (y ∷ʳ p) (.y ∷ʳ q) = ≡.cong (y ∷ʳ_) (Sublist-[]-irrelevant p q)
+
+
+
+
+ toAny-injective :{p q : Sublist R [ x ] xs} → toAny p ≡ toAny q → p ≡ q
+ toAny-injective {p = y ∷ʳ p} {y ∷ʳ q} =
+ ≡.cong (y ∷ʳ_) ∘′ toAny-injective ∘′ there-injective
+ toAny-injective {p = _ ∷ p} {_ ∷ q} =
+ ≡.cong₂ (flip _∷_) (Sublist-[]-irrelevant p q) ∘′ here-injective
+
+ fromAny-injective : {p q : Any (R x) xs} →
+ fromAny {R = R} p ≡ fromAny q → p ≡ q
+ fromAny-injective {p = here px} {here qx} = ≡.cong here ∘′ ∷-injectiveˡ
+ fromAny-injective {p = there p} {there q} =
+ ≡.cong there ∘′ fromAny-injective ∘′ ∷ʳ-injective
+
+ toAny∘fromAny≗id : (p : Any (R x) xs) → toAny (fromAny {R = R} p) ≡ p
+ toAny∘fromAny≗id (here px) = ≡.refl
+ toAny∘fromAny≗id (there p) = ≡.cong there (toAny∘fromAny≗id p)
+
+ Sublist-[x]-bijection : (Sublist R [ x ] xs) ⤖ (Any (R x) xs)
+ Sublist-[x]-bijection = mk⤖ (toAny-injective , strictlySurjective⇒surjective < fromAny , toAny∘fromAny≗id >)
+
+
+
+
+module Reflexivity
+ {R : Rel A r}
+ (R-refl : Reflexive R) where
+
+ reflexive : _≡_ ⇒ Sublist R
+ reflexive ≡.refl = fromPointwise (Pw.refl R-refl)
+
+ refl : Reflexive (Sublist R)
+ refl = reflexive ≡.refl
+
+open Reflexivity public
+
+module Transitivity
+ {R : REL A B r} {S : REL B C s} {T : REL A C t}
+ (rs⇒t : Trans R S T) where
+
+ trans : Trans (Sublist R) (Sublist S) (Sublist T)
+ trans rs (y ∷ʳ ss) = y ∷ʳ trans rs ss
+ trans (y ∷ʳ rs) (s ∷ ss) = _ ∷ʳ trans rs ss
+ trans (r ∷ rs) (s ∷ ss) = rs⇒t r s ∷ trans rs ss
+ trans [] [] = []
+
+open Transitivity public
+
+module Antisymmetry
+ {R : REL A B r} {S : REL B A s} {E : REL A B e}
+ (rs⇒e : Antisym R S E) where
-private
- variable
- a b c d e p q r s t : Level
- A : Set a
- B : Set b
- C : Set c
- D : Set d
- x : A
- y : B
- as cs xs : List A
- bs ds ys : List B
- ass : List (List A)
- bss : List (List B)
- m n : ℕ
-
-
-
-
-module _ {R : REL A B r} where
-
- ∷-injectiveˡ : {px qx : R x y} {pxs qxs : Sublist R xs ys} →
- (Sublist R (x ∷ xs) (y ∷ ys) ∋ px ∷ pxs) ≡ (qx ∷ qxs) → px ≡ qx
- ∷-injectiveˡ ≡.refl = ≡.refl
-
- ∷-injectiveʳ : {px qx : R x y} {pxs qxs : Sublist R xs ys} →
- (Sublist R (x ∷ xs) (y ∷ ys) ∋ px ∷ pxs) ≡ (qx ∷ qxs) → pxs ≡ qxs
- ∷-injectiveʳ ≡.refl = ≡.refl
-
- ∷ʳ-injective : {pxs qxs : Sublist R xs ys} →
- (Sublist R xs (y ∷ ys) ∋ y ∷ʳ pxs) ≡ (y ∷ʳ qxs) → pxs ≡ qxs
- ∷ʳ-injective ≡.refl = ≡.refl
-
-module _ {R : REL A B r} where
-
- length-mono-≤ : Sublist R as bs → length as ≤ length bs
- length-mono-≤ [] = z≤n
- length-mono-≤ (y ∷ʳ rs) = ℕ.m≤n⇒m≤1+n (length-mono-≤ rs)
- length-mono-≤ (r ∷ rs) = s≤s (length-mono-≤ rs)
-
-
-
-
- fromPointwise : Pointwise R ⇒ Sublist R
- fromPointwise [] = []
- fromPointwise (p ∷ ps) = p ∷ fromPointwise ps
-
- toPointwise : length as ≡ length bs →
- Sublist R as bs → Pointwise R as bs
- toPointwise {bs = []} eq [] = []
- toPointwise {bs = b ∷ bs} eq (r ∷ rs) = r ∷ toPointwise (ℕ.suc-injective eq) rs
- toPointwise {bs = b ∷ bs} eq (b ∷ʳ rs) =
- contradiction (s≤s (length-mono-≤ rs)) (ℕ.<-irrefl eq)
-
-
-
-
-
-
-
-
-
-module _ {R : REL A B r} where
-
- tail-Sublist : Sublist R as bs →
- Maybe.All (λ as → Sublist R as bs) (tail as)
- tail-Sublist [] = nothing
- tail-Sublist (b ∷ʳ ps) = Maybe.map (b ∷ʳ_) (tail-Sublist ps)
- tail-Sublist (p ∷ ps) = just (_ ∷ʳ ps)
-
- take-Sublist : ∀ n → Sublist R as bs → Sublist R (take n as) bs
- take-Sublist n (y ∷ʳ rs) = y ∷ʳ take-Sublist n rs
- take-Sublist zero rs = minimum _
- take-Sublist (suc n) [] = []
- take-Sublist (suc n) (r ∷ rs) = r ∷ take-Sublist n rs
-
- drop-Sublist : ∀ n → Sublist R ⇒ (Sublist R ∘′ drop n)
- drop-Sublist n (y ∷ʳ rs) = y ∷ʳ drop-Sublist n rs
- drop-Sublist zero rs = rs
- drop-Sublist (suc n) [] = []
- drop-Sublist (suc n) (r ∷ rs) = _ ∷ʳ drop-Sublist n rs
-
-module _ {R : REL A B r} {P : Pred A p} (P? : U.Decidable P) where
-
- takeWhile-Sublist : Sublist R as bs → Sublist R (takeWhile P? as) bs
- takeWhile-Sublist [] = []
- takeWhile-Sublist (y ∷ʳ rs) = y ∷ʳ takeWhile-Sublist rs
- takeWhile-Sublist {a ∷ as} (r ∷ rs) with does (P? a)
- ... | true = r ∷ takeWhile-Sublist rs
- ... | false = minimum _
-
- dropWhile-Sublist : Sublist R as bs → Sublist R (dropWhile P? as) bs
- dropWhile-Sublist [] = []
- dropWhile-Sublist (y ∷ʳ rs) = y ∷ʳ dropWhile-Sublist rs
- dropWhile-Sublist {a ∷ as} (r ∷ rs) with does (P? a)
- ... | true = _ ∷ʳ dropWhile-Sublist rs
- ... | false = r ∷ rs
-
- filter-Sublist : Sublist R as bs → Sublist R (filter P? as) bs
- filter-Sublist [] = []
- filter-Sublist (y ∷ʳ rs) = y ∷ʳ filter-Sublist rs
- filter-Sublist {a ∷ as} (r ∷ rs) with does (P? a)
- ... | true = r ∷ filter-Sublist rs
- ... | false = _ ∷ʳ filter-Sublist rs
-
-
-
-
-
-
-
-module _ {R : REL A B r} where
-
-
-
-
- ∷ˡ⁻ : Sublist R (x ∷ xs) ys → Sublist R xs ys
- ∷ˡ⁻ (y ∷ʳ rs) = y ∷ʳ ∷ˡ⁻ rs
- ∷ˡ⁻ (r ∷ rs) = _ ∷ʳ rs
-
- ∷ʳ⁻ : ¬ R x y → Sublist R (x ∷ xs) (y ∷ ys) →
- Sublist R (x ∷ xs) ys
- ∷ʳ⁻ ¬r (y ∷ʳ rs) = rs
- ∷ʳ⁻ ¬r (r ∷ rs) = contradiction r ¬r
-
- ∷⁻ : Sublist R (x ∷ xs) (y ∷ ys) → Sublist R xs ys
- ∷⁻ (y ∷ʳ rs) = ∷ˡ⁻ rs
- ∷⁻ (x ∷ rs) = rs
-
-module _ {R : REL C D r} where
-
-
-
-
- map⁺ : (f : A → C) (g : B → D) →
- Sublist (λ a b → R (f a) (g b)) as bs →
- Sublist R (List.map f as) (List.map g bs)
- map⁺ f g [] = []
- map⁺ f g (y ∷ʳ rs) = g y ∷ʳ map⁺ f g rs
- map⁺ f g (r ∷ rs) = r ∷ map⁺ f g rs
-
- map⁻ : (f : A → C) (g : B → D) →
- Sublist R (List.map f as) (List.map g bs) →
- Sublist (λ a b → R (f a) (g b)) as bs
- map⁻ {as = []} {bs} f g rs = minimum _
- map⁻ {as = a ∷ as} {b ∷ bs} f g (_ ∷ʳ rs) = b ∷ʳ map⁻ f g rs
- map⁻ {as = a ∷ as} {b ∷ bs} f g (r ∷ rs) = r ∷ map⁻ f g rs
-
-
-module _ {R : REL A B r} where
-
-
-
-
- ++⁺ : Sublist R as bs → Sublist R cs ds →
- Sublist R (as ++ cs) (bs ++ ds)
- ++⁺ [] cds = cds
- ++⁺ (y ∷ʳ abs) cds = y ∷ʳ ++⁺ abs cds
- ++⁺ (ab ∷ abs) cds = ab ∷ ++⁺ abs cds
-
- ++⁻ : length as ≡ length bs →
- Sublist R (as ++ cs) (bs ++ ds) → Sublist R cs ds
- ++⁻ {as = []} {[]} eq rs = rs
- ++⁻ {as = a ∷ as} {b ∷ bs} eq rs = ++⁻ (ℕ.suc-injective eq) (∷⁻ rs)
-
- ++ˡ : (cs : List B) → Sublist R as bs → Sublist R as (cs ++ bs)
- ++ˡ zs = ++⁺ (minimum zs)
-
- ++ʳ : (cs : List B) → Sublist R as bs → Sublist R as (bs ++ cs)
- ++ʳ cs [] = minimum cs
- ++ʳ cs (y ∷ʳ rs) = y ∷ʳ ++ʳ cs rs
- ++ʳ cs (r ∷ rs) = r ∷ ++ʳ cs rs
-
-
-
-
-
- concat⁺ : Sublist (Sublist R) ass bss →
- Sublist R (concat ass) (concat bss)
- concat⁺ [] = []
- concat⁺ (y ∷ʳ rss) = ++ˡ y (concat⁺ rss)
- concat⁺ (rs ∷ rss) = ++⁺ rs (concat⁺ rss)
-
-
-
-
- take⁺ : m ≤ n → Pointwise R as bs →
- Sublist R (take m as) (take n bs)
- take⁺ z≤n ps = minimum _
- take⁺ (s≤s m≤n) [] = []
- take⁺ (s≤s m≤n) (p ∷ ps) = p ∷ take⁺ m≤n ps
-
- drop⁺ : m ≥ n → Sublist R as bs →
- Sublist R (drop m as) (drop n bs)
- drop⁺ (z≤n {m}) rs = drop-Sublist m rs
- drop⁺ (s≤s m≥n) [] = []
- drop⁺ (s≤s m≥n) (y ∷ʳ rs) = drop⁺ (ℕ.m≤n⇒m≤1+n m≥n) rs
- drop⁺ (s≤s m≥n) (r ∷ rs) = drop⁺ m≥n rs
-
- drop⁺-≥ : m ≥ n → Pointwise R as bs →
- Sublist R (drop m as) (drop n bs)
- drop⁺-≥ m≥n pw = drop⁺ m≥n (fromPointwise pw)
-
- drop⁺-⊆ : ∀ m → Sublist R as bs →
- Sublist R (drop m as) (drop m bs)
- drop⁺-⊆ m = drop⁺ (ℕ.≤-refl {m})
-
-module _ {R : REL A B r} {P : Pred A p} {Q : Pred B q}
- (P? : U.Decidable P) (Q? : U.Decidable Q) where
-
- ⊆-takeWhile-Sublist : (∀ {a b} → R a b → P a → Q b) →
- Pointwise R as bs →
- Sublist R (takeWhile P? as) (takeWhile Q? bs)
- ⊆-takeWhile-Sublist rp⇒q [] = []
- ⊆-takeWhile-Sublist {a ∷ as} {b ∷ bs} rp⇒q (p ∷ ps) with P? a | Q? b
- ... | false because _ | _ = minimum _
- ... | true because _ | true because _ = p ∷ ⊆-takeWhile-Sublist rp⇒q ps
- ... | yes pa | no ¬qb = contradiction (rp⇒q p pa) ¬qb
-
- ⊇-dropWhile-Sublist : (∀ {a b} → R a b → Q b → P a) →
- Pointwise R as bs →
- Sublist R (dropWhile P? as) (dropWhile Q? bs)
- ⊇-dropWhile-Sublist rq⇒p [] = []
- ⊇-dropWhile-Sublist {a ∷ as} {b ∷ bs} rq⇒p (p ∷ ps) with P? a | Q? b
- ... | true because _ | true because _ = ⊇-dropWhile-Sublist rq⇒p ps
- ... | true because _ | false because _ =
- b ∷ʳ dropWhile-Sublist P? (fromPointwise ps)
- ... | false because _ | false because _ = p ∷ fromPointwise ps
- ... | no ¬pa | yes qb = contradiction (rq⇒p p qb) ¬pa
-
- ⊆-filter-Sublist : (∀ {a b} → R a b → P a → Q b) →
- Sublist R as bs → Sublist R (filter P? as) (filter Q? bs)
- ⊆-filter-Sublist rp⇒q [] = []
- ⊆-filter-Sublist rp⇒q (y ∷ʳ rs) with does (Q? y)
- ... | true = y ∷ʳ ⊆-filter-Sublist rp⇒q rs
- ... | false = ⊆-filter-Sublist rp⇒q rs
- ⊆-filter-Sublist {a ∷ as} {b ∷ bs} rp⇒q (r ∷ rs) with P? a | Q? b
- ... | true because _ | true because _ = r ∷ ⊆-filter-Sublist rp⇒q rs
- ... | false because _ | true because _ = _ ∷ʳ ⊆-filter-Sublist rp⇒q rs
- ... | false because _ | false because _ = ⊆-filter-Sublist rp⇒q rs
- ... | yes pa | no ¬qb = contradiction (rp⇒q r pa) ¬qb
-
-module _ {R : Rel A r} {P : Pred A p} (P? : U.Decidable P) where
-
- takeWhile-filter : Pointwise R as as →
- Sublist R (takeWhile P? as) (filter P? as)
- takeWhile-filter [] = []
- takeWhile-filter {a ∷ as} (p ∷ ps) with does (P? a)
- ... | true = p ∷ takeWhile-filter ps
- ... | false = minimum _
-
- filter-dropWhile : Pointwise R as as →
- Sublist R (filter P? as) (dropWhile (¬? ∘ P?) as)
- filter-dropWhile [] = []
- filter-dropWhile {a ∷ as} (p ∷ ps) with does (P? a)
- ... | true = p ∷ filter-Sublist P? (fromPointwise ps)
- ... | false = filter-dropWhile ps
-
-
-
-
-module _ {R : REL A B r} where
-
- reverseAcc⁺ : Sublist R as bs → Sublist R cs ds →
- Sublist R (reverseAcc cs as) (reverseAcc ds bs)
- reverseAcc⁺ [] cds = cds
- reverseAcc⁺ (y ∷ʳ abs) cds = reverseAcc⁺ abs (y ∷ʳ cds)
- reverseAcc⁺ (r ∷ abs) cds = reverseAcc⁺ abs (r ∷ cds)
-
- ʳ++⁺ : Sublist R as bs → Sublist R cs ds →
- Sublist R (as ʳ++ cs) (bs ʳ++ ds)
- ʳ++⁺ = reverseAcc⁺
-
- reverse⁺ : Sublist R as bs → Sublist R (reverse as) (reverse bs)
- reverse⁺ rs = reverseAcc⁺ rs []
-
- reverse⁻ : Sublist R (reverse as) (reverse bs) → Sublist R as bs
- reverse⁻ {as = as} {bs = bs} p = cast (reverse⁺ p) where
- cast = ≡.subst₂ (Sublist R) (List.reverse-involutive as) (List.reverse-involutive bs)
-
-
-
-
-module _ {R : REL A B r} where
-
- ∷⁻¹ : R x y → Sublist R xs ys ⇔ Sublist R (x ∷ xs) (y ∷ ys)
- ∷⁻¹ r = mk⇔ (r ∷_) ∷⁻
-
- ∷ʳ⁻¹ : ¬ R x y → Sublist R (x ∷ xs) ys ⇔ Sublist R (x ∷ xs) (y ∷ ys)
- ∷ʳ⁻¹ ¬r = mk⇔ (_ ∷ʳ_) (∷ʳ⁻ ¬r)
-
-
-
-
-module _ {R : REL A B r} where
-
- Sublist-[]-universal : U.Universal (Sublist R [])
- Sublist-[]-universal [] = []
- Sublist-[]-universal (_ ∷ _) = _ ∷ʳ Sublist-[]-universal _
-
- Sublist-[]-irrelevant : U.Irrelevant (Sublist R [])
- Sublist-[]-irrelevant [] [] = ≡.refl
- Sublist-[]-irrelevant (y ∷ʳ p) (.y ∷ʳ q) = ≡.cong (y ∷ʳ_) (Sublist-[]-irrelevant p q)
-
-
-
-
- toAny-injective :{p q : Sublist R [ x ] xs} → toAny p ≡ toAny q → p ≡ q
- toAny-injective {p = y ∷ʳ p} {y ∷ʳ q} =
- ≡.cong (y ∷ʳ_) ∘′ toAny-injective ∘′ there-injective
- toAny-injective {p = _ ∷ p} {_ ∷ q} =
- ≡.cong₂ (flip _∷_) (Sublist-[]-irrelevant p q) ∘′ here-injective
-
- fromAny-injective : {p q : Any (R x) xs} →
- fromAny {R = R} p ≡ fromAny q → p ≡ q
- fromAny-injective {p = here px} {here qx} = ≡.cong here ∘′ ∷-injectiveˡ
- fromAny-injective {p = there p} {there q} =
- ≡.cong there ∘′ fromAny-injective ∘′ ∷ʳ-injective
-
- toAny∘fromAny≗id : (p : Any (R x) xs) → toAny (fromAny {R = R} p) ≡ p
- toAny∘fromAny≗id (here px) = ≡.refl
- toAny∘fromAny≗id (there p) = ≡.cong there (toAny∘fromAny≗id p)
-
- Sublist-[x]-bijection : (Sublist R [ x ] xs) ⤖ (Any (R x) xs)
- Sublist-[x]-bijection = mk⤖ (toAny-injective , strictlySurjective⇒surjective < fromAny , toAny∘fromAny≗id >)
-
-
-
-
-module Reflexivity
- {R : Rel A r}
- (R-refl : Reflexive R) where
-
- reflexive : _≡_ ⇒ Sublist R
- reflexive ≡.refl = fromPointwise (Pw.refl R-refl)
-
- refl : Reflexive (Sublist R)
- refl = reflexive ≡.refl
-
-open Reflexivity public
-
-module Transitivity
- {R : REL A B r} {S : REL B C s} {T : REL A C t}
- (rs⇒t : Trans R S T) where
-
- trans : Trans (Sublist R) (Sublist S) (Sublist T)
- trans rs (y ∷ʳ ss) = y ∷ʳ trans rs ss
- trans (y ∷ʳ rs) (s ∷ ss) = _ ∷ʳ trans rs ss
- trans (r ∷ rs) (s ∷ ss) = rs⇒t r s ∷ trans rs ss
- trans [] [] = []
-
-open Transitivity public
-
-module Antisymmetry
- {R : REL A B r} {S : REL B A s} {E : REL A B e}
- (rs⇒e : Antisym R S E) where
-
- open ℕ.≤-Reasoning
-
- antisym : Antisym (Sublist R) (Sublist S) (Pointwise E)
- antisym [] [] = []
- antisym (r ∷ rs) (s ∷ ss) = rs⇒e r s ∷ antisym rs ss
-
- antisym (_∷ʳ_ {xs} {ys₁} y rs) (_∷ʳ_ {ys₂} {zs} z ss) =
- contradiction (begin
- length (y ∷ ys₁) ≤⟨ length-mono-≤ ss ⟩
- length zs ≤⟨ ℕ.n≤1+n (length zs) ⟩
- length (z ∷ zs) ≤⟨ length-mono-≤ rs ⟩
- length ys₁ ∎) $ ℕ.<-irrefl ≡.refl
- antisym (_∷ʳ_ {xs} {ys₁} y rs) (_∷_ {y} {ys₂} {z} {zs} s ss) =
- contradiction (begin
- length (z ∷ zs) ≤⟨ length-mono-≤ rs ⟩
- length ys₁ ≤⟨ length-mono-≤ ss ⟩
- length zs ∎) $ ℕ.<-irrefl ≡.refl
- antisym (_∷_ {x} {xs} {y} {ys₁} r rs) (_∷ʳ_ {ys₂} {zs} z ss) =
- contradiction (begin
- length (y ∷ ys₁) ≤⟨ length-mono-≤ ss ⟩
- length xs ≤⟨ length-mono-≤ rs ⟩
- length ys₁ ∎) $ ℕ.<-irrefl ≡.refl
-
-open Antisymmetry public
-
-module _ {R : REL A B r} (R? : Decidable R) where
-
- sublist? : Decidable (Sublist R)
- sublist? [] ys = yes (minimum ys)
- sublist? (x ∷ xs) [] = no λ ()
- sublist? (x ∷ xs) (y ∷ ys) with R? x y
- ... | true because [r] =
- Dec.map (∷⁻¹ (invert [r])) (sublist? xs ys)
- ... | false because [¬r] =
- Dec.map (∷ʳ⁻¹ (invert [¬r])) (sublist? (x ∷ xs) ys)
-
-module _ {E : Rel A e} {R : Rel A r} where
-
- isPreorder : IsPreorder E R → IsPreorder (Pointwise E) (Sublist R)
- isPreorder ER-isPreorder = record
- { isEquivalence = Pw.isEquivalence ER.isEquivalence
- ; reflexive = fromPointwise ∘ Pw.map ER.reflexive
- ; trans = trans ER.trans
- } where module ER = IsPreorder ER-isPreorder
-
- isPartialOrder : IsPartialOrder E R → IsPartialOrder (Pointwise E) (Sublist R)
- isPartialOrder ER-isPartialOrder = record
- { isPreorder = isPreorder ER.isPreorder
- ; antisym = antisym ER.antisym
- } where module ER = IsPartialOrder ER-isPartialOrder
-
- isDecPartialOrder : IsDecPartialOrder E R →
- IsDecPartialOrder (Pointwise E) (Sublist R)
- isDecPartialOrder ER-isDecPartialOrder = record
- { isPartialOrder = isPartialOrder ER.isPartialOrder
- ; _≟_ = Pw.decidable ER._≟_
- ; _≤?_ = sublist? ER._≤?_
- } where module ER = IsDecPartialOrder ER-isDecPartialOrder
-
-preorder : Preorder a e r → Preorder _ _ _
-preorder ER-preorder = record
- { isPreorder = isPreorder ER.isPreorder
- } where module ER = Preorder ER-preorder
-
-poset : Poset a e r → Poset _ _ _
-poset ER-poset = record
- { isPartialOrder = isPartialOrder ER.isPartialOrder
- } where module ER = Poset ER-poset
-
-decPoset : DecPoset a e r → DecPoset _ _ _
-decPoset ER-poset = record
- { isDecPartialOrder = isDecPartialOrder ER.isDecPartialOrder
- } where module ER = DecPoset ER-poset
-
-
-
-
-module Disjointness {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
-
- private
- infix 4 _⊆_
- _⊆_ = Sublist R
-
-
-
- DisjointUnion→Disjoint : ∀ {xs ys zs us} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {τ : us ⊆ zs} →
- DisjointUnion τ₁ τ₂ τ → Disjoint τ₁ τ₂
- DisjointUnion→Disjoint [] = []
- DisjointUnion→Disjoint (y ∷ₙ u) = y ∷ₙ DisjointUnion→Disjoint u
- DisjointUnion→Disjoint (x≈y ∷ₗ u) = x≈y ∷ₗ DisjointUnion→Disjoint u
- DisjointUnion→Disjoint (x≈y ∷ᵣ u) = x≈y ∷ᵣ DisjointUnion→Disjoint u
-
-
-
- Disjoint→DisjointUnion : ∀ {xs ys zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} →
- Disjoint τ₁ τ₂ → ∃₂ λ us (τ : us ⊆ zs) → DisjointUnion τ₁ τ₂ τ
- Disjoint→DisjointUnion [] = _ , _ , []
- Disjoint→DisjointUnion (y ∷ₙ u) = _ , _ , y ∷ₙ proj₂ (proj₂ (Disjoint→DisjointUnion u))
- Disjoint→DisjointUnion (x≈y ∷ₗ u) = _ , _ , x≈y ∷ₗ proj₂ (proj₂ (Disjoint→DisjointUnion u))
- Disjoint→DisjointUnion (x≈y ∷ᵣ u) = _ , _ , x≈y ∷ᵣ proj₂ (proj₂ (Disjoint→DisjointUnion u))
-
-
-
- ⊆-disjoint? : ∀ {xs ys zs} (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) → Dec (Disjoint τ₁ τ₂)
- ⊆-disjoint? [] [] = yes []
-
- ⊆-disjoint? (x≈z ∷ τ₁) (y≈z ∷ τ₂) = no λ()
-
- ⊆-disjoint? (y ∷ʳ τ₁) (x≈y ∷ τ₂) =
- Dec.map′ (x≈y ∷ᵣ_) (λ{ (_ ∷ᵣ d) → d }) (⊆-disjoint? τ₁ τ₂)
- ⊆-disjoint? (x≈y ∷ τ₁) (y ∷ʳ τ₂) =
- Dec.map′ (x≈y ∷ₗ_) (λ{ (_ ∷ₗ d) → d }) (⊆-disjoint? τ₁ τ₂)
-
- ⊆-disjoint? (y ∷ʳ τ₁) (.y ∷ʳ τ₂) =
- Dec.map′ (y ∷ₙ_) (λ{ (_ ∷ₙ d) → d }) (⊆-disjoint? τ₁ τ₂)
-
-
-
- Disjoint-irrelevant : ∀{xs ys zs} → Irrelevant (Disjoint {R = R} {xs} {ys} {zs})
- Disjoint-irrelevant [] [] = ≡.refl
- Disjoint-irrelevant (y ∷ₙ d₁) (.y ∷ₙ d₂) = ≡.cong (y ∷ₙ_) (Disjoint-irrelevant d₁ d₂)
- Disjoint-irrelevant (x≈y ∷ₗ d₁) (.x≈y ∷ₗ d₂) = ≡.cong (x≈y ∷ₗ_) (Disjoint-irrelevant d₁ d₂)
- Disjoint-irrelevant (x≈y ∷ᵣ d₁) (.x≈y ∷ᵣ d₂) = ≡.cong (x≈y ∷ᵣ_) (Disjoint-irrelevant d₁ d₂)
-
-
-
-
-
-
-
-
-
-
- Disjoint-irrefl′ : ∀{xs ys} {τ : xs ⊆ ys} → Disjoint τ τ → Null xs
- Disjoint-irrefl′ [] = []
- Disjoint-irrefl′ (y ∷ₙ d) = Disjoint-irrefl′ d
-
- Disjoint-irrefl : ∀{x xs ys} → Irreflexive {A = x ∷ xs ⊆ ys } _≡_ Disjoint
- Disjoint-irrefl ≡.refl x with Disjoint-irrefl′ x
- ... | () ∷ _
-
-
-
- DisjointUnion-sym : ∀ {xs ys xys} {zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {τ : xys ⊆ zs} →
- DisjointUnion τ₁ τ₂ τ → DisjointUnion τ₂ τ₁ τ
- DisjointUnion-sym [] = []
- DisjointUnion-sym (y ∷ₙ d) = y ∷ₙ DisjointUnion-sym d
- DisjointUnion-sym (x≈y ∷ₗ d) = x≈y ∷ᵣ DisjointUnion-sym d
- DisjointUnion-sym (x≈y ∷ᵣ d) = x≈y ∷ₗ DisjointUnion-sym d
-
- Disjoint-sym : ∀ {xs ys} {zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} →
- Disjoint τ₁ τ₂ → Disjoint τ₂ τ₁
- Disjoint-sym [] = []
- Disjoint-sym (y ∷ₙ d) = y ∷ₙ Disjoint-sym d
- Disjoint-sym (x≈y ∷ₗ d) = x≈y ∷ᵣ Disjoint-sym d
- Disjoint-sym (x≈y ∷ᵣ d) = x≈y ∷ₗ Disjoint-sym d
-
-
-
- DisjointUnion-[]ˡ : ∀{xs ys} {ε : [] ⊆ ys} {τ : xs ⊆ ys} → DisjointUnion ε τ τ
- DisjointUnion-[]ˡ {ε = []} {τ = []} = []
- DisjointUnion-[]ˡ {ε = y ∷ʳ ε} {τ = y ∷ʳ τ} = y ∷ₙ DisjointUnion-[]ˡ
- DisjointUnion-[]ˡ {ε = y ∷ʳ ε} {τ = x≈y ∷ τ} = x≈y ∷ᵣ DisjointUnion-[]ˡ
-
- DisjointUnion-[]ʳ : ∀{xs ys} {ε : [] ⊆ ys} {τ : xs ⊆ ys} → DisjointUnion τ ε τ
- DisjointUnion-[]ʳ {ε = []} {τ = []} = []
- DisjointUnion-[]ʳ {ε = y ∷ʳ ε} {τ = y ∷ʳ τ} = y ∷ₙ DisjointUnion-[]ʳ
- DisjointUnion-[]ʳ {ε = y ∷ʳ ε} {τ = x≈y ∷ τ} = x≈y ∷ₗ DisjointUnion-[]ʳ
-
-
-
-
- DisjointUnion-fromAny∘toAny-∷ˡ⁻ : ∀ {x xs ys} (τ : (x ∷ xs) ⊆ ys) → DisjointUnion (fromAny (toAny τ)) (∷ˡ⁻ τ) τ
- DisjointUnion-fromAny∘toAny-∷ˡ⁻ (y ∷ʳ τ) = y ∷ₙ DisjointUnion-fromAny∘toAny-∷ˡ⁻ τ
- DisjointUnion-fromAny∘toAny-∷ˡ⁻ (xRy ∷ τ) = xRy ∷ₗ DisjointUnion-[]ˡ
-
-
-
-
-
- record DisjointUnion³
- {xs ys zs ts} (τ₁ : xs ⊆ ts) (τ₂ : ys ⊆ ts) (τ₃ : zs ⊆ ts)
- {xys xzs yzs} (τ₁₂ : xys ⊆ ts) (τ₁₃ : xzs ⊆ ts) (τ₂₃ : yzs ⊆ ts) : Set (a ⊔ b ⊔ r) where
- field
- {union³} : List A
- sub³ : union³ ⊆ ts
- join₁ : DisjointUnion τ₁ τ₂₃ sub³
- join₂ : DisjointUnion τ₂ τ₁₃ sub³
- join₃ : DisjointUnion τ₃ τ₁₂ sub³
-
- infixr 5 _∷ʳ-DisjointUnion³_ _∷₁-DisjointUnion³_ _∷₂-DisjointUnion³_ _∷₃-DisjointUnion³_
-
-
-
- _∷ʳ-DisjointUnion³_ :
- ∀ {xs ys zs ts} {τ₁ : xs ⊆ ts} {τ₂ : ys ⊆ ts} {τ₃ : zs ⊆ ts} →
- ∀ {xys xzs yzs} {τ₁₂ : xys ⊆ ts} {τ₁₃ : xzs ⊆ ts} {τ₂₃ : yzs ⊆ ts} →
- ∀ y →
- DisjointUnion³ τ₁ τ₂ τ₃ τ₁₂ τ₁₃ τ₂₃ →
- DisjointUnion³ (y ∷ʳ τ₁) (y ∷ʳ τ₂) (y ∷ʳ τ₃) (y ∷ʳ τ₁₂) (y ∷ʳ τ₁₃) (y ∷ʳ τ₂₃)
- y ∷ʳ-DisjointUnion³ record{ sub³ = σ ; join₁ = d₁ ; join₂ = d₂ ; join₃ = d₃ } = record
- { sub³ = y ∷ʳ σ
- ; join₁ = y ∷ₙ d₁
- ; join₂ = y ∷ₙ d₂
- ; join₃ = y ∷ₙ d₃
- }
-
-
-
- _∷₁-DisjointUnion³_ :
- ∀ {xs ys zs ts} {τ₁ : xs ⊆ ts} {τ₂ : ys ⊆ ts} {τ₃ : zs ⊆ ts} →
- ∀ {xys xzs yzs} {τ₁₂ : xys ⊆ ts} {τ₁₃ : xzs ⊆ ts} {τ₂₃ : yzs ⊆ ts} →
- ∀ {x y} (xRy : R x y) →
- DisjointUnion³ τ₁ τ₂ τ₃ τ₁₂ τ₁₃ τ₂₃ →
- DisjointUnion³ (xRy ∷ τ₁) (y ∷ʳ τ₂) (y ∷ʳ τ₃) (xRy ∷ τ₁₂) (xRy ∷ τ₁₃) (y ∷ʳ τ₂₃)
- xRy ∷₁-DisjointUnion³ record{ sub³ = σ ; join₁ = d₁ ; join₂ = d₂ ; join₃ = d₃ } = record
- { sub³ = xRy ∷ σ
- ; join₁ = xRy ∷ₗ d₁
- ; join₂ = xRy ∷ᵣ d₂
- ; join₃ = xRy ∷ᵣ d₃
- }
-
-
-
- _∷₂-DisjointUnion³_ :
- ∀ {xs ys zs ts} {τ₁ : xs ⊆ ts} {τ₂ : ys ⊆ ts} {τ₃ : zs ⊆ ts} →
- ∀ {xys xzs yzs} {τ₁₂ : xys ⊆ ts} {τ₁₃ : xzs ⊆ ts} {τ₂₃ : yzs ⊆ ts} →
- ∀ {x y} (xRy : R x y) →
- DisjointUnion³ τ₁ τ₂ τ₃ τ₁₂ τ₁₃ τ₂₃ →
- DisjointUnion³ (y ∷ʳ τ₁) (xRy ∷ τ₂) (y ∷ʳ τ₃) (xRy ∷ τ₁₂) (y ∷ʳ τ₁₃) (xRy ∷ τ₂₃)
- xRy ∷₂-DisjointUnion³ record{ sub³ = σ ; join₁ = d₁ ; join₂ = d₂ ; join₃ = d₃ } = record
- { sub³ = xRy ∷ σ
- ; join₁ = xRy ∷ᵣ d₁
- ; join₂ = xRy ∷ₗ d₂
- ; join₃ = xRy ∷ᵣ d₃
- }
-
-
-
- _∷₃-DisjointUnion³_ :
- ∀ {xs ys zs ts} {τ₁ : xs ⊆ ts} {τ₂ : ys ⊆ ts} {τ₃ : zs ⊆ ts} →
- ∀ {xys xzs yzs} {τ₁₂ : xys ⊆ ts} {τ₁₃ : xzs ⊆ ts} {τ₂₃ : yzs ⊆ ts} →
- ∀ {x y} (xRy : R x y) →
- DisjointUnion³ τ₁ τ₂ τ₃ τ₁₂ τ₁₃ τ₂₃ →
- DisjointUnion³ (y ∷ʳ τ₁) (y ∷ʳ τ₂) (xRy ∷ τ₃) (y ∷ʳ τ₁₂) (xRy ∷ τ₁₃) (xRy ∷ τ₂₃)
- xRy ∷₃-DisjointUnion³ record{ sub³ = σ ; join₁ = d₁ ; join₂ = d₂ ; join₃ = d₃ } = record
- { sub³ = xRy ∷ σ
- ; join₁ = xRy ∷ᵣ d₁
- ; join₂ = xRy ∷ᵣ d₂
- ; join₃ = xRy ∷ₗ d₃
- }
-
-
-
- disjointUnion³ : ∀{xs ys zs ts} {τ₁ : xs ⊆ ts} {τ₂ : ys ⊆ ts} {τ₃ : zs ⊆ ts}
- {xys xzs yzs} {τ₁₂ : xys ⊆ ts} {τ₁₃ : xzs ⊆ ts} {τ₂₃ : yzs ⊆ ts} →
- DisjointUnion τ₁ τ₂ τ₁₂ →
- DisjointUnion τ₁ τ₃ τ₁₃ →
- DisjointUnion τ₂ τ₃ τ₂₃ →
- DisjointUnion³ τ₁ τ₂ τ₃ τ₁₂ τ₁₃ τ₂₃
- disjointUnion³ [] [] [] = record { sub³ = [] ; join₁ = [] ; join₂ = [] ; join₃ = [] }
- disjointUnion³ (y ∷ₙ d₁₂) (.y ∷ₙ d₁₃) (.y ∷ₙ d₂₃) = y ∷ʳ-DisjointUnion³ disjointUnion³ d₁₂ d₁₃ d₂₃
- disjointUnion³ (y ∷ₙ d₁₂) (xRy ∷ᵣ d₁₃) (.xRy ∷ᵣ d₂₃) = xRy ∷₃-DisjointUnion³ disjointUnion³ d₁₂ d₁₃ d₂₃
- disjointUnion³ (xRy ∷ᵣ d₁₂) (y ∷ₙ d₁₃) (.xRy ∷ₗ d₂₃) = xRy ∷₂-DisjointUnion³ disjointUnion³ d₁₂ d₁₃ d₂₃
- disjointUnion³ (xRy ∷ₗ d₁₂) (.xRy ∷ₗ d₁₃) (y ∷ₙ d₂₃) = xRy ∷₁-DisjointUnion³ disjointUnion³ d₁₂ d₁₃ d₂₃
- disjointUnion³ (xRy ∷ᵣ d₁₂) (xRy′ ∷ᵣ d₁₃) ()
-
-
-
-
- disjoint⇒disjoint-to-union : ∀{xs ys zs yzs ts}
- {τ : xs ⊆ ts} {σ₁ : ys ⊆ ts} {σ₂ : zs ⊆ ts} {σ : yzs ⊆ ts} →
- Disjoint τ σ₁ → Disjoint τ σ₂ → DisjointUnion σ₁ σ₂ σ → Disjoint τ σ
- disjoint⇒disjoint-to-union d₁ d₂ u = let
- _ , _ , u₁ = Disjoint→DisjointUnion d₁
- _ , _ , u₂ = Disjoint→DisjointUnion d₂
- in DisjointUnion→Disjoint (DisjointUnion³.join₁ (disjointUnion³ u₁ u₂ u))
-
-open Disjointness public
-
-
-
-module DisjointnessMonotonicity
- {R : REL A B r} {S : REL B C s} {T : REL A C t}
- (rs⇒t : Trans R S T) where
-
-
-
- weakenDisjointUnion : ∀ {xs ys xys zs ws}
- {τ₁ : Sublist R xs zs}
- {τ₂ : Sublist R ys zs}
- {τ : Sublist R xys zs} (σ : Sublist S zs ws) →
- DisjointUnion τ₁ τ₂ τ →
- DisjointUnion (trans rs⇒t τ₁ σ) (trans rs⇒t τ₂ σ) (trans rs⇒t τ σ)
- weakenDisjointUnion [] [] = []
- weakenDisjointUnion (w ∷ʳ σ) d = w ∷ₙ weakenDisjointUnion σ d
- weakenDisjointUnion (_ ∷ σ) (y ∷ₙ d) = _ ∷ₙ weakenDisjointUnion σ d
- weakenDisjointUnion (zSw ∷ σ) (xRz ∷ₗ d) = rs⇒t xRz zSw ∷ₗ weakenDisjointUnion σ d
- weakenDisjointUnion (zSw ∷ σ) (yRz ∷ᵣ d) = rs⇒t yRz zSw ∷ᵣ weakenDisjointUnion σ d
-
- weakenDisjoint : ∀ {xs ys zs ws}
- {τ₁ : Sublist R xs zs}
- {τ₂ : Sublist R ys zs} (σ : Sublist S zs ws) →
- Disjoint τ₁ τ₂ →
- Disjoint (trans rs⇒t τ₁ σ) (trans rs⇒t τ₂ σ)
- weakenDisjoint [] [] = []
- weakenDisjoint (w ∷ʳ σ) d = w ∷ₙ weakenDisjoint σ d
- weakenDisjoint (_ ∷ σ) (y ∷ₙ d) = _ ∷ₙ weakenDisjoint σ d
- weakenDisjoint (zSw ∷ σ) (xRz ∷ₗ d) = rs⇒t xRz zSw ∷ₗ weakenDisjoint σ d
- weakenDisjoint (zSw ∷ σ) (yRz ∷ᵣ d) = rs⇒t yRz zSw ∷ᵣ weakenDisjoint σ d
-
-
-
- shrinkDisjoint : ∀ {us vs xs ys zs}
- (σ₁ : Sublist R us xs) {τ₁ : Sublist S xs zs}
- (σ₂ : Sublist R vs ys) {τ₂ : Sublist S ys zs} →
- Disjoint τ₁ τ₂ →
- Disjoint (trans rs⇒t σ₁ τ₁) (trans rs⇒t σ₂ τ₂)
- shrinkDisjoint σ₁ σ₂ (y ∷ₙ d) = y ∷ₙ shrinkDisjoint σ₁ σ₂ d
- shrinkDisjoint (x ∷ʳ σ₁) σ₂ (xSz ∷ₗ d) = _ ∷ₙ shrinkDisjoint σ₁ σ₂ d
- shrinkDisjoint (uRx ∷ σ₁) σ₂ (xSz ∷ₗ d) = rs⇒t uRx xSz ∷ₗ shrinkDisjoint σ₁ σ₂ d
- shrinkDisjoint σ₁ (y ∷ʳ σ₂) (ySz ∷ᵣ d) = _ ∷ₙ shrinkDisjoint σ₁ σ₂ d
- shrinkDisjoint σ₁ (vRy ∷ σ₂) (ySz ∷ᵣ d) = rs⇒t vRy ySz ∷ᵣ shrinkDisjoint σ₁ σ₂ d
- shrinkDisjoint [] [] [] = []
-
-open DisjointnessMonotonicity public
+ open ℕ.≤-Reasoning
+
+ antisym : Antisym (Sublist R) (Sublist S) (Pointwise E)
+ antisym [] [] = []
+ antisym (r ∷ rs) (s ∷ ss) = rs⇒e r s ∷ antisym rs ss
+
+ antisym (_∷ʳ_ {xs} {ys₁} y rs) (_∷ʳ_ {ys₂} {zs} z ss) =
+ contradiction (begin
+ length (y ∷ ys₁) ≤⟨ length-mono-≤ ss ⟩
+ length zs ≤⟨ ℕ.n≤1+n (length zs) ⟩
+ length (z ∷ zs) ≤⟨ length-mono-≤ rs ⟩
+ length ys₁ ∎) $ ℕ.<-irrefl ≡.refl
+ antisym (_∷ʳ_ {xs} {ys₁} y rs) (_∷_ {y} {ys₂} {z} {zs} s ss) =
+ contradiction (begin
+ length (z ∷ zs) ≤⟨ length-mono-≤ rs ⟩
+ length ys₁ ≤⟨ length-mono-≤ ss ⟩
+ length zs ∎) $ ℕ.<-irrefl ≡.refl
+ antisym (_∷_ {x} {xs} {y} {ys₁} r rs) (_∷ʳ_ {ys₂} {zs} z ss) =
+ contradiction (begin
+ length (y ∷ ys₁) ≤⟨ length-mono-≤ ss ⟩
+ length xs ≤⟨ length-mono-≤ rs ⟩
+ length ys₁ ∎) $ ℕ.<-irrefl ≡.refl
+
+open Antisymmetry public
+
+module _ {R : REL A B r} (R? : Decidable R) where
+
+ sublist? : Decidable (Sublist R)
+ sublist? [] ys = yes (minimum ys)
+ sublist? (x ∷ xs) [] = no λ ()
+ sublist? (x ∷ xs) (y ∷ ys) with R? x y
+ ... | true because [r] =
+ Dec.map (∷⁻¹ (invert [r])) (sublist? xs ys)
+ ... | false because [¬r] =
+ Dec.map (∷ʳ⁻¹ (invert [¬r])) (sublist? (x ∷ xs) ys)
+
+module _ {E : Rel A e} {R : Rel A r} where
+
+ isPreorder : IsPreorder E R → IsPreorder (Pointwise E) (Sublist R)
+ isPreorder ER-isPreorder = record
+ { isEquivalence = Pw.isEquivalence ER.isEquivalence
+ ; reflexive = fromPointwise ∘ Pw.map ER.reflexive
+ ; trans = trans ER.trans
+ } where module ER = IsPreorder ER-isPreorder
+
+ isPartialOrder : IsPartialOrder E R → IsPartialOrder (Pointwise E) (Sublist R)
+ isPartialOrder ER-isPartialOrder = record
+ { isPreorder = isPreorder ER.isPreorder
+ ; antisym = antisym ER.antisym
+ } where module ER = IsPartialOrder ER-isPartialOrder
+
+ isDecPartialOrder : IsDecPartialOrder E R →
+ IsDecPartialOrder (Pointwise E) (Sublist R)
+ isDecPartialOrder ER-isDecPartialOrder = record
+ { isPartialOrder = isPartialOrder ER.isPartialOrder
+ ; _≟_ = Pw.decidable ER._≟_
+ ; _≤?_ = sublist? ER._≤?_
+ } where module ER = IsDecPartialOrder ER-isDecPartialOrder
+
+preorder : Preorder a e r → Preorder _ _ _
+preorder ER-preorder = record
+ { isPreorder = isPreorder ER.isPreorder
+ } where module ER = Preorder ER-preorder
+
+poset : Poset a e r → Poset _ _ _
+poset ER-poset = record
+ { isPartialOrder = isPartialOrder ER.isPartialOrder
+ } where module ER = Poset ER-poset
+
+decPoset : DecPoset a e r → DecPoset _ _ _
+decPoset ER-poset = record
+ { isDecPartialOrder = isDecPartialOrder ER.isDecPartialOrder
+ } where module ER = DecPoset ER-poset
+
+
+
+
+
+module ⊆-Reasoning (≲ : Preorder a e r) where
+
+ open Preorder ≲ using (module Eq)
+
+ open ≲-Reasoning (preorder ≲) public
+ renaming (≲-go to ⊆-go; ≈-go to ≋-go)
+
+ open ⊆-syntax _IsRelatedTo_ _IsRelatedTo_ ⊆-go public
+ open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ ≋-go (Pw.symmetric Eq.sym) public
+
+
+
+
+module Disjointness {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
+
+ private
+ infix 4 _⊆_
+ _⊆_ = Sublist R
+
+
+
+ DisjointUnion→Disjoint : ∀ {xs ys zs us} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {τ : us ⊆ zs} →
+ DisjointUnion τ₁ τ₂ τ → Disjoint τ₁ τ₂
+ DisjointUnion→Disjoint [] = []
+ DisjointUnion→Disjoint (y ∷ₙ u) = y ∷ₙ DisjointUnion→Disjoint u
+ DisjointUnion→Disjoint (x≈y ∷ₗ u) = x≈y ∷ₗ DisjointUnion→Disjoint u
+ DisjointUnion→Disjoint (x≈y ∷ᵣ u) = x≈y ∷ᵣ DisjointUnion→Disjoint u
+
+
+
+ Disjoint→DisjointUnion : ∀ {xs ys zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} →
+ Disjoint τ₁ τ₂ → ∃₂ λ us (τ : us ⊆ zs) → DisjointUnion τ₁ τ₂ τ
+ Disjoint→DisjointUnion [] = _ , _ , []
+ Disjoint→DisjointUnion (y ∷ₙ u) = _ , _ , y ∷ₙ proj₂ (proj₂ (Disjoint→DisjointUnion u))
+ Disjoint→DisjointUnion (x≈y ∷ₗ u) = _ , _ , x≈y ∷ₗ proj₂ (proj₂ (Disjoint→DisjointUnion u))
+ Disjoint→DisjointUnion (x≈y ∷ᵣ u) = _ , _ , x≈y ∷ᵣ proj₂ (proj₂ (Disjoint→DisjointUnion u))
+
+
+
+ ⊆-disjoint? : ∀ {xs ys zs} (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) → Dec (Disjoint τ₁ τ₂)
+ ⊆-disjoint? [] [] = yes []
+
+ ⊆-disjoint? (x≈z ∷ τ₁) (y≈z ∷ τ₂) = no λ()
+
+ ⊆-disjoint? (y ∷ʳ τ₁) (x≈y ∷ τ₂) =
+ Dec.map′ (x≈y ∷ᵣ_) (λ{ (_ ∷ᵣ d) → d }) (⊆-disjoint? τ₁ τ₂)
+ ⊆-disjoint? (x≈y ∷ τ₁) (y ∷ʳ τ₂) =
+ Dec.map′ (x≈y ∷ₗ_) (λ{ (_ ∷ₗ d) → d }) (⊆-disjoint? τ₁ τ₂)
+
+ ⊆-disjoint? (y ∷ʳ τ₁) (.y ∷ʳ τ₂) =
+ Dec.map′ (y ∷ₙ_) (λ{ (_ ∷ₙ d) → d }) (⊆-disjoint? τ₁ τ₂)
+
+
+
+ Disjoint-irrelevant : ∀{xs ys zs} → Irrelevant (Disjoint {R = R} {xs} {ys} {zs})
+ Disjoint-irrelevant [] [] = ≡.refl
+ Disjoint-irrelevant (y ∷ₙ d₁) (.y ∷ₙ d₂) = ≡.cong (y ∷ₙ_) (Disjoint-irrelevant d₁ d₂)
+ Disjoint-irrelevant (x≈y ∷ₗ d₁) (.x≈y ∷ₗ d₂) = ≡.cong (x≈y ∷ₗ_) (Disjoint-irrelevant d₁ d₂)
+ Disjoint-irrelevant (x≈y ∷ᵣ d₁) (.x≈y ∷ᵣ d₂) = ≡.cong (x≈y ∷ᵣ_) (Disjoint-irrelevant d₁ d₂)
+
+
+
+
+
+
+
+
+
+
+ Disjoint-irrefl′ : ∀{xs ys} {τ : xs ⊆ ys} → Disjoint τ τ → Null xs
+ Disjoint-irrefl′ [] = []
+ Disjoint-irrefl′ (y ∷ₙ d) = Disjoint-irrefl′ d
+
+ Disjoint-irrefl : ∀{x xs ys} → Irreflexive {A = x ∷ xs ⊆ ys } _≡_ Disjoint
+ Disjoint-irrefl ≡.refl x with Disjoint-irrefl′ x
+ ... | () ∷ _
+
+
+
+ DisjointUnion-sym : ∀ {xs ys xys} {zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {τ : xys ⊆ zs} →
+ DisjointUnion τ₁ τ₂ τ → DisjointUnion τ₂ τ₁ τ
+ DisjointUnion-sym [] = []
+ DisjointUnion-sym (y ∷ₙ d) = y ∷ₙ DisjointUnion-sym d
+ DisjointUnion-sym (x≈y ∷ₗ d) = x≈y ∷ᵣ DisjointUnion-sym d
+ DisjointUnion-sym (x≈y ∷ᵣ d) = x≈y ∷ₗ DisjointUnion-sym d
+
+ Disjoint-sym : ∀ {xs ys} {zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} →
+ Disjoint τ₁ τ₂ → Disjoint τ₂ τ₁
+ Disjoint-sym [] = []
+ Disjoint-sym (y ∷ₙ d) = y ∷ₙ Disjoint-sym d
+ Disjoint-sym (x≈y ∷ₗ d) = x≈y ∷ᵣ Disjoint-sym d
+ Disjoint-sym (x≈y ∷ᵣ d) = x≈y ∷ₗ Disjoint-sym d
+
+
+
+ DisjointUnion-[]ˡ : ∀{xs ys} {ε : [] ⊆ ys} {τ : xs ⊆ ys} → DisjointUnion ε τ τ
+ DisjointUnion-[]ˡ {ε = []} {τ = []} = []
+ DisjointUnion-[]ˡ {ε = y ∷ʳ ε} {τ = y ∷ʳ τ} = y ∷ₙ DisjointUnion-[]ˡ
+ DisjointUnion-[]ˡ {ε = y ∷ʳ ε} {τ = x≈y ∷ τ} = x≈y ∷ᵣ DisjointUnion-[]ˡ
+
+ DisjointUnion-[]ʳ : ∀{xs ys} {ε : [] ⊆ ys} {τ : xs ⊆ ys} → DisjointUnion τ ε τ
+ DisjointUnion-[]ʳ {ε = []} {τ = []} = []
+ DisjointUnion-[]ʳ {ε = y ∷ʳ ε} {τ = y ∷ʳ τ} = y ∷ₙ DisjointUnion-[]ʳ
+ DisjointUnion-[]ʳ {ε = y ∷ʳ ε} {τ = x≈y ∷ τ} = x≈y ∷ₗ DisjointUnion-[]ʳ
+
+
+
+
+ DisjointUnion-fromAny∘toAny-∷ˡ⁻ : ∀ {x xs ys} (τ : (x ∷ xs) ⊆ ys) → DisjointUnion (fromAny (toAny τ)) (∷ˡ⁻ τ) τ
+ DisjointUnion-fromAny∘toAny-∷ˡ⁻ (y ∷ʳ τ) = y ∷ₙ DisjointUnion-fromAny∘toAny-∷ˡ⁻ τ
+ DisjointUnion-fromAny∘toAny-∷ˡ⁻ (xRy ∷ τ) = xRy ∷ₗ DisjointUnion-[]ˡ
+
+
+
+
+
+ record DisjointUnion³
+ {xs ys zs ts} (τ₁ : xs ⊆ ts) (τ₂ : ys ⊆ ts) (τ₃ : zs ⊆ ts)
+ {xys xzs yzs} (τ₁₂ : xys ⊆ ts) (τ₁₃ : xzs ⊆ ts) (τ₂₃ : yzs ⊆ ts) : Set (a ⊔ b ⊔ r) where
+ field
+ {union³} : List A
+ sub³ : union³ ⊆ ts
+ join₁ : DisjointUnion τ₁ τ₂₃ sub³
+ join₂ : DisjointUnion τ₂ τ₁₃ sub³
+ join₃ : DisjointUnion τ₃ τ₁₂ sub³
+
+ infixr 5 _∷ʳ-DisjointUnion³_ _∷₁-DisjointUnion³_ _∷₂-DisjointUnion³_ _∷₃-DisjointUnion³_
+
+
+
+ _∷ʳ-DisjointUnion³_ :
+ ∀ {xs ys zs ts} {τ₁ : xs ⊆ ts} {τ₂ : ys ⊆ ts} {τ₃ : zs ⊆ ts} →
+ ∀ {xys xzs yzs} {τ₁₂ : xys ⊆ ts} {τ₁₃ : xzs ⊆ ts} {τ₂₃ : yzs ⊆ ts} →
+ ∀ y →
+ DisjointUnion³ τ₁ τ₂ τ₃ τ₁₂ τ₁₃ τ₂₃ →
+ DisjointUnion³ (y ∷ʳ τ₁) (y ∷ʳ τ₂) (y ∷ʳ τ₃) (y ∷ʳ τ₁₂) (y ∷ʳ τ₁₃) (y ∷ʳ τ₂₃)
+ y ∷ʳ-DisjointUnion³ record{ sub³ = σ ; join₁ = d₁ ; join₂ = d₂ ; join₃ = d₃ } = record
+ { sub³ = y ∷ʳ σ
+ ; join₁ = y ∷ₙ d₁
+ ; join₂ = y ∷ₙ d₂
+ ; join₃ = y ∷ₙ d₃
+ }
+
+
+
+ _∷₁-DisjointUnion³_ :
+ ∀ {xs ys zs ts} {τ₁ : xs ⊆ ts} {τ₂ : ys ⊆ ts} {τ₃ : zs ⊆ ts} →
+ ∀ {xys xzs yzs} {τ₁₂ : xys ⊆ ts} {τ₁₃ : xzs ⊆ ts} {τ₂₃ : yzs ⊆ ts} →
+ ∀ {x y} (xRy : R x y) →
+ DisjointUnion³ τ₁ τ₂ τ₃ τ₁₂ τ₁₃ τ₂₃ →
+ DisjointUnion³ (xRy ∷ τ₁) (y ∷ʳ τ₂) (y ∷ʳ τ₃) (xRy ∷ τ₁₂) (xRy ∷ τ₁₃) (y ∷ʳ τ₂₃)
+ xRy ∷₁-DisjointUnion³ record{ sub³ = σ ; join₁ = d₁ ; join₂ = d₂ ; join₃ = d₃ } = record
+ { sub³ = xRy ∷ σ
+ ; join₁ = xRy ∷ₗ d₁
+ ; join₂ = xRy ∷ᵣ d₂
+ ; join₃ = xRy ∷ᵣ d₃
+ }
+
+
+
+ _∷₂-DisjointUnion³_ :
+ ∀ {xs ys zs ts} {τ₁ : xs ⊆ ts} {τ₂ : ys ⊆ ts} {τ₃ : zs ⊆ ts} →
+ ∀ {xys xzs yzs} {τ₁₂ : xys ⊆ ts} {τ₁₃ : xzs ⊆ ts} {τ₂₃ : yzs ⊆ ts} →
+ ∀ {x y} (xRy : R x y) →
+ DisjointUnion³ τ₁ τ₂ τ₃ τ₁₂ τ₁₃ τ₂₃ →
+ DisjointUnion³ (y ∷ʳ τ₁) (xRy ∷ τ₂) (y ∷ʳ τ₃) (xRy ∷ τ₁₂) (y ∷ʳ τ₁₃) (xRy ∷ τ₂₃)
+ xRy ∷₂-DisjointUnion³ record{ sub³ = σ ; join₁ = d₁ ; join₂ = d₂ ; join₃ = d₃ } = record
+ { sub³ = xRy ∷ σ
+ ; join₁ = xRy ∷ᵣ d₁
+ ; join₂ = xRy ∷ₗ d₂
+ ; join₃ = xRy ∷ᵣ d₃
+ }
+
+
+
+ _∷₃-DisjointUnion³_ :
+ ∀ {xs ys zs ts} {τ₁ : xs ⊆ ts} {τ₂ : ys ⊆ ts} {τ₃ : zs ⊆ ts} →
+ ∀ {xys xzs yzs} {τ₁₂ : xys ⊆ ts} {τ₁₃ : xzs ⊆ ts} {τ₂₃ : yzs ⊆ ts} →
+ ∀ {x y} (xRy : R x y) →
+ DisjointUnion³ τ₁ τ₂ τ₃ τ₁₂ τ₁₃ τ₂₃ →
+ DisjointUnion³ (y ∷ʳ τ₁) (y ∷ʳ τ₂) (xRy ∷ τ₃) (y ∷ʳ τ₁₂) (xRy ∷ τ₁₃) (xRy ∷ τ₂₃)
+ xRy ∷₃-DisjointUnion³ record{ sub³ = σ ; join₁ = d₁ ; join₂ = d₂ ; join₃ = d₃ } = record
+ { sub³ = xRy ∷ σ
+ ; join₁ = xRy ∷ᵣ d₁
+ ; join₂ = xRy ∷ᵣ d₂
+ ; join₃ = xRy ∷ₗ d₃
+ }
+
+
+
+ disjointUnion³ : ∀{xs ys zs ts} {τ₁ : xs ⊆ ts} {τ₂ : ys ⊆ ts} {τ₃ : zs ⊆ ts}
+ {xys xzs yzs} {τ₁₂ : xys ⊆ ts} {τ₁₃ : xzs ⊆ ts} {τ₂₃ : yzs ⊆ ts} →
+ DisjointUnion τ₁ τ₂ τ₁₂ →
+ DisjointUnion τ₁ τ₃ τ₁₃ →
+ DisjointUnion τ₂ τ₃ τ₂₃ →
+ DisjointUnion³ τ₁ τ₂ τ₃ τ₁₂ τ₁₃ τ₂₃
+ disjointUnion³ [] [] [] = record { sub³ = [] ; join₁ = [] ; join₂ = [] ; join₃ = [] }
+ disjointUnion³ (y ∷ₙ d₁₂) (.y ∷ₙ d₁₃) (.y ∷ₙ d₂₃) = y ∷ʳ-DisjointUnion³ disjointUnion³ d₁₂ d₁₃ d₂₃
+ disjointUnion³ (y ∷ₙ d₁₂) (xRy ∷ᵣ d₁₃) (.xRy ∷ᵣ d₂₃) = xRy ∷₃-DisjointUnion³ disjointUnion³ d₁₂ d₁₃ d₂₃
+ disjointUnion³ (xRy ∷ᵣ d₁₂) (y ∷ₙ d₁₃) (.xRy ∷ₗ d₂₃) = xRy ∷₂-DisjointUnion³ disjointUnion³ d₁₂ d₁₃ d₂₃
+ disjointUnion³ (xRy ∷ₗ d₁₂) (.xRy ∷ₗ d₁₃) (y ∷ₙ d₂₃) = xRy ∷₁-DisjointUnion³ disjointUnion³ d₁₂ d₁₃ d₂₃
+ disjointUnion³ (xRy ∷ᵣ d₁₂) (xRy′ ∷ᵣ d₁₃) ()
+
+
+
+
+ disjoint⇒disjoint-to-union : ∀{xs ys zs yzs ts}
+ {τ : xs ⊆ ts} {σ₁ : ys ⊆ ts} {σ₂ : zs ⊆ ts} {σ : yzs ⊆ ts} →
+ Disjoint τ σ₁ → Disjoint τ σ₂ → DisjointUnion σ₁ σ₂ σ → Disjoint τ σ
+ disjoint⇒disjoint-to-union d₁ d₂ u = let
+ _ , _ , u₁ = Disjoint→DisjointUnion d₁
+ _ , _ , u₂ = Disjoint→DisjointUnion d₂
+ in DisjointUnion→Disjoint (DisjointUnion³.join₁ (disjointUnion³ u₁ u₂ u))
+
+open Disjointness public
+
+
+
+module DisjointnessMonotonicity
+ {R : REL A B r} {S : REL B C s} {T : REL A C t}
+ (rs⇒t : Trans R S T) where
+
+
+
+ weakenDisjointUnion : ∀ {xs ys xys zs ws}
+ {τ₁ : Sublist R xs zs}
+ {τ₂ : Sublist R ys zs}
+ {τ : Sublist R xys zs} (σ : Sublist S zs ws) →
+ DisjointUnion τ₁ τ₂ τ →
+ DisjointUnion (trans rs⇒t τ₁ σ) (trans rs⇒t τ₂ σ) (trans rs⇒t τ σ)
+ weakenDisjointUnion [] [] = []
+ weakenDisjointUnion (w ∷ʳ σ) d = w ∷ₙ weakenDisjointUnion σ d
+ weakenDisjointUnion (_ ∷ σ) (y ∷ₙ d) = _ ∷ₙ weakenDisjointUnion σ d
+ weakenDisjointUnion (zSw ∷ σ) (xRz ∷ₗ d) = rs⇒t xRz zSw ∷ₗ weakenDisjointUnion σ d
+ weakenDisjointUnion (zSw ∷ σ) (yRz ∷ᵣ d) = rs⇒t yRz zSw ∷ᵣ weakenDisjointUnion σ d
+
+ weakenDisjoint : ∀ {xs ys zs ws}
+ {τ₁ : Sublist R xs zs}
+ {τ₂ : Sublist R ys zs} (σ : Sublist S zs ws) →
+ Disjoint τ₁ τ₂ →
+ Disjoint (trans rs⇒t τ₁ σ) (trans rs⇒t τ₂ σ)
+ weakenDisjoint [] [] = []
+ weakenDisjoint (w ∷ʳ σ) d = w ∷ₙ weakenDisjoint σ d
+ weakenDisjoint (_ ∷ σ) (y ∷ₙ d) = _ ∷ₙ weakenDisjoint σ d
+ weakenDisjoint (zSw ∷ σ) (xRz ∷ₗ d) = rs⇒t xRz zSw ∷ₗ weakenDisjoint σ d
+ weakenDisjoint (zSw ∷ σ) (yRz ∷ᵣ d) = rs⇒t yRz zSw ∷ᵣ weakenDisjoint σ d
+
+
+
+ shrinkDisjoint : ∀ {us vs xs ys zs}
+ (σ₁ : Sublist R us xs) {τ₁ : Sublist S xs zs}
+ (σ₂ : Sublist R vs ys) {τ₂ : Sublist S ys zs} →
+ Disjoint τ₁ τ₂ →
+ Disjoint (trans rs⇒t σ₁ τ₁) (trans rs⇒t σ₂ τ₂)
+ shrinkDisjoint σ₁ σ₂ (y ∷ₙ d) = y ∷ₙ shrinkDisjoint σ₁ σ₂ d
+ shrinkDisjoint (x ∷ʳ σ₁) σ₂ (xSz ∷ₗ d) = _ ∷ₙ shrinkDisjoint σ₁ σ₂ d
+ shrinkDisjoint (uRx ∷ σ₁) σ₂ (xSz ∷ₗ d) = rs⇒t uRx xSz ∷ₗ shrinkDisjoint σ₁ σ₂ d
+ shrinkDisjoint σ₁ (y ∷ʳ σ₂) (ySz ∷ᵣ d) = _ ∷ₙ shrinkDisjoint σ₁ σ₂ d
+ shrinkDisjoint σ₁ (vRy ∷ σ₂) (ySz ∷ᵣ d) = rs⇒t vRy ySz ∷ᵣ shrinkDisjoint σ₁ σ₂ d
+ shrinkDisjoint [] [] [] = []
+
+open DisjointnessMonotonicity public