From 92395434829b6ee6badfd23058ffb79612754b36 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Wed, 15 May 2024 02:19:39 +0100 Subject: [PATCH] Add `Data.List.Relation.Binary.Sublist.Setoid` categorical properties (#2385) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * refactor: `variable` declarations and `contradiction` * refactor: one more `contradiction` * left- and right-unit lemmas * left- and right-unit lemmas * `CHANGELOG` * `CHANGELOG` * associativity; fixes #816 * Use cong2 to save rewrites * Make splits for ⊆-assoc exact, simplifying the [] case * Simplify ⊆-assoc not using rewrite * Remove now unused private helper * fix up names and `assoc` orientation; misc. cleanup * new proofs can now move upwards * delegate proofs to `Setoid.Properties` --------- Co-authored-by: Andreas Abel --- CHANGELOG.md | 12 + .../Sublist/Heterogeneous/Properties.agda | 214 +++++++++--------- .../Sublist/Propositional/Properties.agda | 22 +- .../Binary/Sublist/Setoid/Properties.agda | 102 ++++++--- 4 files changed, 197 insertions(+), 153 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7732f9ea1f..9d1bb7c58b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -380,6 +380,18 @@ Additions to existing modules map-catMaybes : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f) ``` +* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`: + ```agda + ⊆-trans-idˡ : (trans-reflˡ : ∀ {x y} (p : x ≈ y) → trans ≈-refl p ≡ p) → + (pxs : xs ⊆ ys) → ⊆-trans ⊆-refl pxs ≡ pxs + ⊆-trans-idʳ : (trans-reflʳ : ∀ {x y} (p : x ≈ y) → trans p ≈-refl ≡ p) → + (pxs : xs ⊆ ys) → ⊆-trans pxs ⊆-refl ≡ pxs + ⊆-trans-assoc : (≈-assoc : ∀ {w x y z} (p : w ≈ x) (q : x ≈ y) (r : y ≈ z) → + trans p (trans q r) ≡ trans (trans p q) r) → + (ps : as ⊆ bs) (qs : bs ⊆ cs) (rs : cs ⊆ ds) → + ⊆-trans ps (⊆-trans qs rs) ≡ ⊆-trans (⊆-trans ps qs) rs + ``` + * In `Data.List.Relation.Binary.Subset.Setoid.Properties`: ```agda map⁺ : f Preserves _≈_ ⟶ _≈′_ → as ⊆ bs → map f as ⊆′ map f bs diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda index b760e0287f..8dd94d8b3b 100644 --- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda @@ -11,7 +11,6 @@ module Data.List.Relation.Binary.Sublist.Heterogeneous.Properties where open import Level open import Data.Bool.Base using (true; false) -open import Data.Empty open import Data.List.Relation.Unary.All using (Null; []; _∷_) open import Data.List.Relation.Unary.Any using (Any; here; there) open import Data.List.Base as List hiding (map; _∷ʳ_) @@ -29,9 +28,9 @@ open import Data.Product.Base using (∃₂; _×_; _,_; <_,_>; proj₂; uncurry) open import Function.Base open import Function.Bundles using (_⤖_; _⇔_ ; mk⤖; mk⇔) open import Function.Consequences.Propositional using (strictlySurjective⇒surjective) +open import Relation.Nullary.Decidable as Dec using (Dec; does; _because_; yes; no; ¬?) +open import Relation.Nullary.Negation using (¬_; contradiction) open import Relation.Nullary.Reflects using (invert) -open import Relation.Nullary using (Dec; does; _because_; yes; no; ¬_) -open import Relation.Nullary.Decidable as Dec using (¬?) open import Relation.Unary as U using (Pred) open import Relation.Binary.Core using (Rel; REL; _⇒_) open import Relation.Binary.Bundles using (Preorder; Poset; DecPoset) @@ -41,26 +40,41 @@ open import Relation.Binary.Structures using (IsPreorder; IsPartialOrder; IsDecPartialOrder) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) +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 : ℕ + ------------------------------------------------------------------------ -- Injectivity of constructors -module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where +module _ {R : REL A B r} where - ∷-injectiveˡ : ∀ {x y xs ys} {px qx : R x y} {pxs qxs : Sublist R xs ys} → + ∷-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ʳ : ∀ {x y xs ys} {px qx : R x y} {pxs qxs : Sublist R xs ys} → + ∷-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 : ∀ {y xs ys} {pxs qxs : Sublist R xs ys} → + ∷ʳ-injective : {pxs qxs : Sublist R xs ys} → (Sublist R xs (y ∷ ys) ∋ y ∷ʳ pxs) ≡ (y ∷ʳ qxs) → pxs ≡ qxs ∷ʳ-injective ≡.refl = ≡.refl -module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where +module _ {R : REL A B r} where - length-mono-≤ : ∀ {as bs} → Sublist R as bs → length as ≤ length bs + 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) @@ -72,12 +86,12 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where fromPointwise [] = [] fromPointwise (p ∷ ps) = p ∷ fromPointwise ps - toPointwise : ∀ {as bs} → length as ≡ length bs → + 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) = - ⊥-elim $ ℕ.<-irrefl eq (s≤s (length-mono-≤ rs)) + contradiction (s≤s (length-mono-≤ rs)) (ℕ.<-irrefl eq) ------------------------------------------------------------------------ -- Various functions' outputs are sublists @@ -87,15 +101,15 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where -- indeed obtain `f xs ⊆ xs` from `xs ⊆ ys → f xs ⊆ ys`. The other -- direction is only true if R is both reflexive and transitive. -module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where +module _ {R : REL A B r} where - tail-Sublist : ∀ {as bs} → Sublist R as bs → + 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 : ∀ {as bs} n → Sublist R as bs → Sublist R (take n as) bs + 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) [] = [] @@ -107,24 +121,23 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where drop-Sublist (suc n) [] = [] drop-Sublist (suc n) (r ∷ rs) = _ ∷ʳ drop-Sublist n rs -module _ {a b r p} {A : Set a} {B : Set b} - {R : REL A B r} {P : Pred A p} (P? : U.Decidable P) where +module _ {R : REL A B r} {P : Pred A p} (P? : U.Decidable P) where - takeWhile-Sublist : ∀ {as bs} → Sublist R as bs → Sublist R (takeWhile P? as) bs + 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 : ∀ {as bs} → Sublist R as bs → Sublist R (dropWhile P? as) bs + 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 : ∀ {as bs} → Sublist R as bs → Sublist R (filter P? as) bs + 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) @@ -137,65 +150,64 @@ module _ {a b r p} {A : Set a} {B : Set b} -- We write f⁺ for the proof that `xs ⊆ ys → f xs ⊆ f ys` -- and f⁻ for the one that `f xs ⊆ f ys → xs ⊆ ys`. -module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where +module _ {R : REL A B r} where ------------------------------------------------------------------------ -- _∷_ - ∷ˡ⁻ : ∀ {a as bs} → Sublist R (a ∷ as) bs → Sublist R as bs + ∷ˡ⁻ : Sublist R (x ∷ xs) ys → Sublist R xs ys ∷ˡ⁻ (y ∷ʳ rs) = y ∷ʳ ∷ˡ⁻ rs ∷ˡ⁻ (r ∷ rs) = _ ∷ʳ rs - ∷ʳ⁻ : ∀ {a as b bs} → ¬ R a b → Sublist R (a ∷ as) (b ∷ bs) → - Sublist R (a ∷ as) bs + ∷ʳ⁻ : ¬ R x y → Sublist R (x ∷ xs) (y ∷ ys) → + Sublist R (x ∷ xs) ys ∷ʳ⁻ ¬r (y ∷ʳ rs) = rs - ∷ʳ⁻ ¬r (r ∷ rs) = ⊥-elim (¬r r) + ∷ʳ⁻ ¬r (r ∷ rs) = contradiction r ¬r - ∷⁻ : ∀ {a as b bs} → Sublist R (a ∷ as) (b ∷ bs) → Sublist R as bs + ∷⁻ : Sublist R (x ∷ xs) (y ∷ ys) → Sublist R xs ys ∷⁻ (y ∷ʳ rs) = ∷ˡ⁻ rs ∷⁻ (x ∷ rs) = rs -module _ {a b c d r} {A : Set a} {B : Set b} {C : Set c} {D : Set d} - {R : REL C D r} where +module _ {R : REL C D r} where ------------------------------------------------------------------------ -- map - map⁺ : ∀ {as bs} (f : A → C) (g : B → D) → + 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⁻ : ∀ {as bs} (f : A → C) (g : B → D) → + 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⁻ {[]} {bs} f g rs = minimum _ - map⁻ {a ∷ as} {b ∷ bs} f g (_ ∷ʳ rs) = b ∷ʳ map⁻ f g rs - map⁻ {a ∷ as} {b ∷ bs} f g (r ∷ rs) = r ∷ map⁻ f g rs + 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 _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where +module _ {R : REL A B r} where ------------------------------------------------------------------------ -- _++_ - ++⁺ : ∀ {as bs cs ds} → Sublist R as bs → Sublist R cs ds → + ++⁺ : 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 - ++⁻ : ∀ {as bs cs ds} → length as ≡ length bs → + ++⁻ : length as ≡ length bs → Sublist R (as ++ cs) (bs ++ ds) → Sublist R cs ds - ++⁻ {[]} {[]} eq rs = rs - ++⁻ {a ∷ as} {b ∷ bs} eq rs = ++⁻ (ℕ.suc-injective eq) (∷⁻ rs) + ++⁻ {as = []} {[]} eq rs = rs + ++⁻ {as = a ∷ as} {b ∷ bs} eq rs = ++⁻ (ℕ.suc-injective eq) (∷⁻ rs) - ++ˡ : ∀ {as bs} (cs : List B) → Sublist R as bs → Sublist R as (cs ++ bs) + ++ˡ : (cs : List B) → Sublist R as bs → Sublist R as (cs ++ bs) ++ˡ zs = ++⁺ (minimum zs) - ++ʳ : ∀ {as bs} (cs : List B) → Sublist R as bs → Sublist R as (bs ++ cs) + ++ʳ : (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 @@ -204,7 +216,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where ------------------------------------------------------------------------ -- concat - concat⁺ : ∀ {ass bss} → Sublist (Sublist R) ass bss → + concat⁺ : Sublist (Sublist R) ass bss → Sublist R (concat ass) (concat bss) concat⁺ [] = [] concat⁺ (y ∷ʳ rss) = ++ˡ y (concat⁺ rss) @@ -213,52 +225,51 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where ------------------------------------------------------------------------ -- take / drop - take⁺ : ∀ {m n as bs} → m ≤ n → Pointwise R as bs → + 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 as bs} → m ≥ n → Sublist R as bs → + drop⁺ : m ≥ n → Sublist R as bs → Sublist R (drop m as) (drop n bs) - drop⁺ {m} z≤n 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⁺ (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 as bs} → m ≥ n → Pointwise R as bs → + 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⁺-⊆ : ∀ {as bs} m → Sublist R as bs → + drop⁺-⊆ : ∀ m → Sublist R as bs → Sublist R (drop m as) (drop m bs) drop⁺-⊆ m = drop⁺ (ℕ.≤-refl {m}) -module _ {a b r p q} {A : Set a} {B : Set b} - {R : REL A B r} {P : Pred A p} {Q : Pred B q} +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 : ∀ {as bs} → - (∀ {a b} → R a b → P a → Q b) → - Pointwise R as bs → Sublist R (takeWhile P? as) (takeWhile Q? bs) + ⊆-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 = ⊥-elim $ ¬qb $ rp⇒q p pa + ... | yes pa | no ¬qb = contradiction (rp⇒q p pa) ¬qb - ⊇-dropWhile-Sublist : ∀ {as bs} → - (∀ {a b} → R a b → Q b → P a) → - Pointwise R as bs → Sublist R (dropWhile P? as) (dropWhile Q? bs) + ⊇-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 = ⊥-elim $ ¬pa $ rq⇒p p qb + ... | no ¬pa | yes qb = contradiction (rq⇒p p qb) ¬pa - ⊆-filter-Sublist : ∀ {as bs} → (∀ {a b} → R a b → P a → Q b) → + ⊆-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) @@ -268,18 +279,18 @@ module _ {a b r p q} {A : Set a} {B : Set 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 = ⊥-elim $ ¬qb $ rp⇒q r pa + ... | yes pa | no ¬qb = contradiction (rp⇒q r pa) ¬qb -module _ {a r p} {A : Set a} {R : Rel A r} {P : Pred A p} (P? : U.Decidable P) where +module _ {R : Rel A r} {P : Pred A p} (P? : U.Decidable P) where - takeWhile-filter : ∀ {as} → Pointwise R as as → + 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 : ∀ {as} → Pointwise R as as → + 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) @@ -289,42 +300,40 @@ module _ {a r p} {A : Set a} {R : Rel A r} {P : Pred A p} (P? : U.Decidable P) w ------------------------------------------------------------------------ -- reverse -module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where +module _ {R : REL A B r} where - reverseAcc⁺ : ∀ {as bs cs ds} → Sublist R as bs → Sublist R cs ds → + 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) - ʳ++⁺ : ∀ {as bs cs ds} → - Sublist R as bs → - Sublist R cs ds → + ʳ++⁺ : Sublist R as bs → Sublist R cs ds → Sublist R (as ʳ++ cs) (bs ʳ++ ds) ʳ++⁺ = reverseAcc⁺ - reverse⁺ : ∀ {as bs} → Sublist R as bs → Sublist R (reverse as) (reverse bs) + reverse⁺ : Sublist R as bs → Sublist R (reverse as) (reverse bs) reverse⁺ rs = reverseAcc⁺ rs [] - reverse⁻ : ∀ {as bs} → Sublist R (reverse as) (reverse bs) → Sublist R as bs - reverse⁻ {as} {bs} p = cast (reverse⁺ p) where + 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) ------------------------------------------------------------------------ -- Inversion lemmas -module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} {a as b bs} where +module _ {R : REL A B r} where - ∷⁻¹ : R a b → Sublist R as bs ⇔ Sublist R (a ∷ as) (b ∷ bs) + ∷⁻¹ : R x y → Sublist R xs ys ⇔ Sublist R (x ∷ xs) (y ∷ ys) ∷⁻¹ r = mk⇔ (r ∷_) ∷⁻ - ∷ʳ⁻¹ : ¬ R a b → Sublist R (a ∷ as) bs ⇔ Sublist R (a ∷ as) (b ∷ bs) + ∷ʳ⁻¹ : ¬ R x y → Sublist R (x ∷ xs) ys ⇔ Sublist R (x ∷ xs) (y ∷ ys) ∷ʳ⁻¹ ¬r = mk⇔ (_ ∷ʳ_) (∷ʳ⁻ ¬r) ------------------------------------------------------------------------ -- Irrelevant special case -module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where +module _ {R : REL A B r} where Sublist-[]-irrelevant : U.Irrelevant (Sublist R []) Sublist-[]-irrelevant [] [] = ≡.refl @@ -333,30 +342,30 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where ------------------------------------------------------------------------ -- (to/from)Any is a bijection - toAny-injective : ∀ {xs x} {p q : Sublist R [ x ] xs} → toAny p ≡ toAny q → 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 : ∀ {xs x} {p q : Any (R x) xs} → + 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 : ∀ {xs x} (p : Any (R x) xs) → toAny (fromAny {R = R} p) ≡ p + 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 : ∀ {x xs} → (Sublist R [ x ] xs) ⤖ (Any (R x) xs) + Sublist-[x]-bijection : (Sublist R [ x ] xs) ⤖ (Any (R x) xs) Sublist-[x]-bijection = mk⤖ (toAny-injective , strictlySurjective⇒surjective < fromAny , toAny∘fromAny≗id >) ------------------------------------------------------------------------ -- Relational properties module Reflexivity - {a r} {A : Set a} {R : Rel A r} + {R : Rel A r} (R-refl : Reflexive R) where reflexive : _≡_ ⇒ Sublist R @@ -368,7 +377,6 @@ module Reflexivity open Reflexivity public module Transitivity - {a b c r s t} {A : Set a} {B : Set b} {C : Set c} {R : REL A B r} {S : REL B C s} {T : REL A C t} (rs⇒t : Trans R S T) where @@ -381,7 +389,6 @@ module Transitivity open Transitivity public module Antisymmetry - {a b r s e} {A : Set a} {B : Set b} {R : REL A B r} {S : REL B A s} {E : REL A B e} (rs⇒e : Antisym R S E) where @@ -392,25 +399,25 @@ module Antisymmetry antisym (r ∷ rs) (s ∷ ss) = rs⇒e r s ∷ antisym rs ss -- impossible cases antisym (_∷ʳ_ {xs} {ys₁} y rs) (_∷ʳ_ {ys₂} {zs} z ss) = - ⊥-elim $ ℕ.<-irrefl ≡.refl $ begin + contradiction (begin length (y ∷ ys₁) ≤⟨ length-mono-≤ ss ⟩ length zs ≤⟨ ℕ.n≤1+n (length zs) ⟩ length (z ∷ zs) ≤⟨ length-mono-≤ rs ⟩ - length ys₁ ∎ + length ys₁ ∎) $ ℕ.<-irrefl ≡.refl antisym (_∷ʳ_ {xs} {ys₁} y rs) (_∷_ {y} {ys₂} {z} {zs} s ss) = - ⊥-elim $ ℕ.<-irrefl ≡.refl $ begin + contradiction (begin length (z ∷ zs) ≤⟨ length-mono-≤ rs ⟩ length ys₁ ≤⟨ length-mono-≤ ss ⟩ - length zs ∎ + length zs ∎) $ ℕ.<-irrefl ≡.refl antisym (_∷_ {x} {xs} {y} {ys₁} r rs) (_∷ʳ_ {ys₂} {zs} z ss) = - ⊥-elim $ ℕ.<-irrefl ≡.refl $ begin + contradiction (begin length (y ∷ ys₁) ≤⟨ length-mono-≤ ss ⟩ length xs ≤⟨ length-mono-≤ rs ⟩ - length ys₁ ∎ + length ys₁ ∎) $ ℕ.<-irrefl ≡.refl open Antisymmetry public -module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} (R? : Decidable R) where +module _ {R : REL A B r} (R? : Decidable R) where sublist? : Decidable (Sublist R) sublist? [] ys = yes (minimum ys) @@ -421,7 +428,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} (R? : Decidable R) wher ... | false because [¬r] = Dec.map (∷ʳ⁻¹ (invert [¬r])) (sublist? (x ∷ xs) ys) -module _ {a e r} {A : Set a} {E : Rel A e} {R : Rel A r} where +module _ {E : Rel A e} {R : Rel A r} where isPreorder : IsPreorder E R → IsPreorder (Pointwise E) (Sublist R) isPreorder ER-isPreorder = record @@ -444,22 +451,20 @@ module _ {a e r} {A : Set a} {E : Rel A e} {R : Rel A r} where ; _≤?_ = sublist? ER._≤?_ } where module ER = IsDecPartialOrder ER-isDecPartialOrder -module _ {a e r} where - - preorder : Preorder a e r → Preorder _ _ _ - preorder ER-preorder = record - { isPreorder = isPreorder ER.isPreorder - } where module ER = Preorder ER-preorder +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 +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 +decPoset : DecPoset a e r → DecPoset _ _ _ +decPoset ER-poset = record + { isDecPartialOrder = isDecPartialOrder ER.isDecPartialOrder + } where module ER = DecPoset ER-poset ------------------------------------------------------------------------ -- Properties of disjoint sublists @@ -670,7 +675,6 @@ open Disjointness public -- Monotonicity of disjointness. module DisjointnessMonotonicity - {a b c r s t} {A : Set a} {B : Set b} {C : Set c} {R : REL A B r} {S : REL B C s} {T : REL A C t} (rs⇒t : Trans R S T) where diff --git a/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda index 94ccb9038b..aeb7c74e23 100644 --- a/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda @@ -23,10 +23,10 @@ open import Data.Product.Base using (∃; _,_; proj₂) open import Function.Base using (id; _∘_; _∘′_) open import Level using (Level) open import Relation.Binary.Definitions using (_Respects_) -open import Relation.Binary.PropositionalEquality.Core +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl; cong; _≗_; trans) open import Relation.Binary.PropositionalEquality.Properties - using (setoid; subst-injective) + using (setoid; subst-injective; trans-reflʳ; trans-assoc) open import Relation.Unary using (Pred) private @@ -38,7 +38,7 @@ private -- Re-exporting setoid properties open SetoidProperties (setoid A) public - hiding (map⁺) + hiding (map⁺; ⊆-trans-idˡ; ⊆-trans-idʳ; ⊆-trans-assoc) map⁺ : ∀ {as bs} (f : A → B) → as ⊆ bs → map f as ⊆ map f bs map⁺ {B = B} f = SetoidProperties.map⁺ (setoid A) (setoid B) (cong f) @@ -48,16 +48,11 @@ map⁺ {B = B} f = SetoidProperties.map⁺ (setoid A) (setoid B) (cong f) ⊆-trans-idˡ : ∀ {xs ys : List A} {τ : xs ⊆ ys} → ⊆-trans ⊆-refl τ ≡ τ -⊆-trans-idˡ {_} {τ = [] } = refl -⊆-trans-idˡ {_} {τ = _ ∷ _} = cong (_ ∷_ ) ⊆-trans-idˡ -⊆-trans-idˡ {[]} {τ = _ ∷ʳ _} = cong (_ ∷ʳ_) ⊆-trans-idˡ -⊆-trans-idˡ {_ ∷ _} {τ = _ ∷ʳ _} = cong (_ ∷ʳ_) ⊆-trans-idˡ +⊆-trans-idˡ {τ = τ} = SetoidProperties.⊆-trans-idˡ (setoid A) (λ _ → refl) τ ⊆-trans-idʳ : ∀ {xs ys : List A} {τ : xs ⊆ ys} → ⊆-trans τ ⊆-refl ≡ τ -⊆-trans-idʳ {τ = [] } = refl -⊆-trans-idʳ {τ = _ ∷ʳ _ } = cong (_ ∷ʳ_ ) ⊆-trans-idʳ -⊆-trans-idʳ {τ = refl ∷ _} = cong (refl ∷_) ⊆-trans-idʳ +⊆-trans-idʳ {τ = τ} = SetoidProperties.⊆-trans-idʳ (setoid A) trans-reflʳ τ -- Note: The associativity law is oriented such that rewriting with it -- may trigger reductions of ⊆-trans, which matches first on its @@ -66,11 +61,8 @@ map⁺ {B = B} f = SetoidProperties.map⁺ (setoid A) (setoid B) (cong f) ⊆-trans-assoc : ∀ {ws xs ys zs : List A} {τ₁ : ws ⊆ xs} {τ₂ : xs ⊆ ys} {τ₃ : ys ⊆ zs} → ⊆-trans τ₁ (⊆-trans τ₂ τ₃) ≡ ⊆-trans (⊆-trans τ₁ τ₂) τ₃ -⊆-trans-assoc {τ₁ = _} {_} {_ ∷ʳ _} = cong (_ ∷ʳ_) ⊆-trans-assoc -⊆-trans-assoc {τ₁ = _} {_ ∷ʳ _} {_ ∷ _} = cong (_ ∷ʳ_) ⊆-trans-assoc -⊆-trans-assoc {τ₁ = _ ∷ʳ _ } {_ ∷ _} {_ ∷ _} = cong (_ ∷ʳ_) ⊆-trans-assoc -⊆-trans-assoc {τ₁ = refl ∷ _} {_ ∷ _} {_ ∷ _} = cong (_ ∷_ ) ⊆-trans-assoc -⊆-trans-assoc {τ₁ = []} {[]} {[]} = refl +⊆-trans-assoc {τ₁ = τ₁} {τ₂ = τ₂} {τ₃ = τ₃} = + SetoidProperties.⊆-trans-assoc (setoid A) (λ p _ _ → ≡.sym (trans-assoc p)) τ₁ τ₂ τ₃ ------------------------------------------------------------------------ -- Laws concerning ⊆-trans and ∷ˡ⁻ diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda index cf12328323..60be70aac1 100644 --- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda @@ -15,14 +15,14 @@ module Data.List.Relation.Binary.Sublist.Setoid.Properties open import Data.List.Base hiding (_∷ʳ_) open import Data.List.Relation.Unary.Any using (Any) import Data.Maybe.Relation.Unary.All as Maybe -open import Data.Nat.Base using (_≤_; _≥_) +open import Data.Nat.Base using (ℕ; _≤_; _≥_) import Data.Nat.Properties as ℕ open import Data.Product.Base using (∃; _,_; proj₂) open import Function.Base open import Function.Bundles using (_⇔_; _⤖_) open import Level open import Relation.Binary.Definitions using () renaming (Decidable to Decidable₂) -open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong) +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl; cong; cong₂) open import Relation.Binary.Structures using (IsDecTotalOrder) open import Relation.Unary using (Pred; Decidable; Irrelevant) open import Relation.Nullary.Negation using (¬_) @@ -39,23 +39,63 @@ open SetoidEquality S using (_≋_; ≋-refl) open SetoidSublist S hiding (map) open SetoidMembership S using (_∈_) +private + variable + p q r s t : Level + a b x y : A + as bs cs ds xs ys : List A + P : Pred A p + Q : Pred A q + m n : ℕ + + ------------------------------------------------------------------------ -- Injectivity of constructors ------------------------------------------------------------------------ -module _ {xs ys : List A} where +module _ where - ∷-injectiveˡ : ∀ {x y} {px qx : x ≈ y} {pxs qxs : xs ⊆ ys} → + ∷-injectiveˡ : ∀ {px qx : x ≈ y} {pxs qxs : xs ⊆ ys} → ((x ∷ xs) ⊆ (y ∷ ys) ∋ px ∷ pxs) ≡ (qx ∷ qxs) → px ≡ qx ∷-injectiveˡ refl = refl - ∷-injectiveʳ : ∀ {x y} {px qx : x ≈ y} {pxs qxs : xs ⊆ ys} → + ∷-injectiveʳ : ∀ {px qx : x ≈ y} {pxs qxs : xs ⊆ ys} → ((x ∷ xs) ⊆ (y ∷ ys) ∋ px ∷ pxs) ≡ (qx ∷ qxs) → pxs ≡ qxs ∷-injectiveʳ refl = refl - ∷ʳ-injective : ∀ {y} {pxs qxs : xs ⊆ ys} → y ∷ʳ pxs ≡ y ∷ʳ qxs → pxs ≡ qxs + ∷ʳ-injective : ∀ {pxs qxs : xs ⊆ ys} → y ∷ʳ pxs ≡ y ∷ʳ qxs → pxs ≡ qxs ∷ʳ-injective refl = refl +------------------------------------------------------------------------ +-- Categorical properties +------------------------------------------------------------------------ + +module _ (trans-reflˡ : ∀ {x y} (p : x ≈ y) → trans ≈-refl p ≡ p) where + + ⊆-trans-idˡ : (pxs : xs ⊆ ys) → ⊆-trans ⊆-refl pxs ≡ pxs + ⊆-trans-idˡ [] = refl + ⊆-trans-idˡ (y ∷ʳ pxs) = cong (y ∷ʳ_) (⊆-trans-idˡ pxs) + ⊆-trans-idˡ (x ∷ pxs) = cong₂ _∷_ (trans-reflˡ x) (⊆-trans-idˡ pxs) + +module _ (trans-reflʳ : ∀ {x y} (p : x ≈ y) → trans p ≈-refl ≡ p) where + + ⊆-trans-idʳ : (pxs : xs ⊆ ys) → ⊆-trans pxs ⊆-refl ≡ pxs + ⊆-trans-idʳ [] = refl + ⊆-trans-idʳ (y ∷ʳ pxs) = cong (y ∷ʳ_) (⊆-trans-idʳ pxs) + ⊆-trans-idʳ (x ∷ pxs) = cong₂ _∷_ (trans-reflʳ x) (⊆-trans-idʳ pxs) + +module _ (≈-assoc : ∀ {w x y z} (p : w ≈ x) (q : x ≈ y) (r : y ≈ z) → + trans p (trans q r) ≡ trans (trans p q) r) where + + ⊆-trans-assoc : (ps : as ⊆ bs) (qs : bs ⊆ cs) (rs : cs ⊆ ds) → + ⊆-trans ps (⊆-trans qs rs) ≡ ⊆-trans (⊆-trans ps qs) rs + ⊆-trans-assoc ps qs (_ ∷ʳ rs) = cong (_ ∷ʳ_) (⊆-trans-assoc ps qs rs) + ⊆-trans-assoc ps (_ ∷ʳ qs) (_ ∷ rs) = cong (_ ∷ʳ_) (⊆-trans-assoc ps qs rs) + ⊆-trans-assoc (_ ∷ʳ ps) (_ ∷ qs) (_ ∷ rs) = cong (_ ∷ʳ_) (⊆-trans-assoc ps qs rs) + ⊆-trans-assoc (p ∷ ps) (q ∷ qs) (r ∷ rs) = cong₂ _∷_ (≈-assoc p q r) (⊆-trans-assoc ps qs rs) + ⊆-trans-assoc [] [] [] = refl + + ------------------------------------------------------------------------ -- Various functions' outputs are sublists ------------------------------------------------------------------------ @@ -69,7 +109,7 @@ take-⊆ n xs = HeteroProperties.take-Sublist n ⊆-refl drop-⊆ : ∀ n xs → drop n xs ⊆ xs drop-⊆ n xs = HeteroProperties.drop-Sublist n ⊆-refl -module _ {p} {P : Pred A p} (P? : Decidable P) where +module _ (P? : Decidable P) where takeWhile-⊆ : ∀ xs → takeWhile P? xs ⊆ xs takeWhile-⊆ xs = HeteroProperties.takeWhile-Sublist P? ⊆-refl @@ -80,7 +120,7 @@ module _ {p} {P : Pred A p} (P? : Decidable P) where filter-⊆ : ∀ xs → filter P? xs ⊆ xs filter-⊆ xs = HeteroProperties.filter-Sublist P? ⊆-refl -module _ {p} {P : Pred A p} (P? : Decidable P) where +module _ (P? : Decidable P) where takeWhile⊆filter : ∀ xs → takeWhile P? xs ⊆ filter P? xs takeWhile⊆filter xs = HeteroProperties.takeWhile-filter P? {xs} ≋-refl @@ -94,15 +134,15 @@ module _ {p} {P : Pred A p} (P? : Decidable P) where -- We write f⁺ for the proof that `xs ⊆ ys → f xs ⊆ f ys` -- and f⁻ for the one that `f xs ⊆ f ys → xs ⊆ ys`. -module _ {as bs : List A} where +module _ where - ∷ˡ⁻ : ∀ {a} → a ∷ as ⊆ bs → as ⊆ bs + ∷ˡ⁻ : a ∷ as ⊆ bs → as ⊆ bs ∷ˡ⁻ = HeteroProperties.∷ˡ⁻ - ∷ʳ⁻ : ∀ {a b} → ¬ (a ≈ b) → a ∷ as ⊆ b ∷ bs → a ∷ as ⊆ bs + ∷ʳ⁻ : ¬ (a ≈ b) → a ∷ as ⊆ b ∷ bs → a ∷ as ⊆ bs ∷ʳ⁻ = HeteroProperties.∷ʳ⁻ - ∷⁻ : ∀ {a b} → a ∷ as ⊆ b ∷ bs → as ⊆ bs + ∷⁻ : a ∷ as ⊆ b ∷ bs → as ⊆ bs ∷⁻ = HeteroProperties.∷⁻ ------------------------------------------------------------------------ @@ -121,7 +161,7 @@ module _ {b ℓ} (R : Setoid b ℓ) where ------------------------------------------------------------------------ -- _++_ -module _ {as bs : List A} where +module _ where ++⁺ˡ : ∀ cs → as ⊆ bs → as ⊆ cs ++ bs ++⁺ˡ = HeteroProperties.++ˡ @@ -129,16 +169,16 @@ module _ {as bs : List A} where ++⁺ʳ : ∀ cs → as ⊆ bs → as ⊆ bs ++ cs ++⁺ʳ = HeteroProperties.++ʳ - ++⁺ : ∀ {cs ds} → as ⊆ bs → cs ⊆ ds → as ++ cs ⊆ bs ++ ds + ++⁺ : as ⊆ bs → cs ⊆ ds → as ++ cs ⊆ bs ++ ds ++⁺ = HeteroProperties.++⁺ - ++⁻ : ∀ {cs ds} → length as ≡ length bs → as ++ cs ⊆ bs ++ ds → cs ⊆ ds + ++⁻ : length as ≡ length bs → as ++ cs ⊆ bs ++ ds → cs ⊆ ds ++⁻ = HeteroProperties.++⁻ ------------------------------------------------------------------------ -- take -module _ {m n} {xs} where +module _ where take⁺ : m ≤ n → take m xs ⊆ take n xs take⁺ m≤n = HeteroProperties.take⁺ m≤n ≋-refl @@ -146,17 +186,17 @@ module _ {m n} {xs} where ------------------------------------------------------------------------ -- drop -module _ {m n} {xs ys : List A} where +module _ where drop⁺ : m ≥ n → xs ⊆ ys → drop m xs ⊆ drop n ys drop⁺ = HeteroProperties.drop⁺ -module _ {m n} {xs : List A} where +module _ where drop⁺-≥ : m ≥ n → drop m xs ⊆ drop n xs drop⁺-≥ m≥n = drop⁺ m≥n ⊆-refl -module _ {xs ys : List A} where +module _ where drop⁺-⊆ : ∀ n → xs ⊆ ys → drop n xs ⊆ drop n ys drop⁺-⊆ n xs⊆ys = drop⁺ {n} ℕ.≤-refl xs⊆ys @@ -164,8 +204,7 @@ module _ {xs ys : List A} where ------------------------------------------------------------------------ -- takeWhile / dropWhile -module _ {p q} {P : Pred A p} {Q : Pred A q} - (P? : Decidable P) (Q? : Decidable Q) where +module _ (P? : Decidable P) (Q? : Decidable Q) where takeWhile⁺ : ∀ {xs} → (∀ {a b} → a ≈ b → P a → Q b) → takeWhile P? xs ⊆ takeWhile Q? xs @@ -178,25 +217,22 @@ module _ {p q} {P : Pred A p} {Q : Pred A q} ------------------------------------------------------------------------ -- filter -module _ {p q} {P : Pred A p} {Q : Pred A q} - (P? : Decidable P) (Q? : Decidable Q) where +module _ (P? : Decidable P) (Q? : Decidable Q) where - filter⁺ : ∀ {as bs} → (∀ {a b} → a ≈ b → P a → Q b) → + filter⁺ : (∀ {a b} → a ≈ b → P a → Q b) → as ⊆ bs → filter P? as ⊆ filter Q? bs filter⁺ = HeteroProperties.⊆-filter-Sublist P? Q? ------------------------------------------------------------------------ -- reverse -module _ {as bs : List A} where +module _ where - reverseAcc⁺ : ∀ {cs ds} → as ⊆ bs → cs ⊆ ds → + reverseAcc⁺ : as ⊆ bs → cs ⊆ ds → reverseAcc cs as ⊆ reverseAcc ds bs reverseAcc⁺ = HeteroProperties.reverseAcc⁺ - ʳ++⁺ : ∀ {cs ds} → - as ⊆ bs → - cs ⊆ ds → + ʳ++⁺ : as ⊆ bs → cs ⊆ ds → as ʳ++ cs ⊆ bs ʳ++ ds ʳ++⁺ = reverseAcc⁺ @@ -233,7 +269,7 @@ module _ {ℓ′} {_≤_ : Rel A ℓ′} (_≤?_ : Decidable₂ _≤_) where -- Inversion lemmas ------------------------------------------------------------------------ -module _ {a as b bs} where +module _ where ∷⁻¹ : a ≈ b → as ⊆ bs ⇔ a ∷ as ⊆ b ∷ bs ∷⁻¹ = HeteroProperties.∷⁻¹ @@ -247,13 +283,13 @@ module _ {a as b bs} where module _ where - length-mono-≤ : ∀ {as bs} → as ⊆ bs → length as ≤ length bs + length-mono-≤ : as ⊆ bs → length as ≤ length bs length-mono-≤ = HeteroProperties.length-mono-≤ ------------------------------------------------------------------------ -- Conversion to and from list equality - to-≋ : ∀ {as bs} → length as ≡ length bs → as ⊆ bs → as ≋ bs + to-≋ : length as ≡ length bs → as ⊆ bs → as ≋ bs to-≋ = HeteroProperties.toPointwise ------------------------------------------------------------------------ @@ -265,7 +301,7 @@ module _ where ------------------------------------------------------------------------ -- (to/from)∈ is a bijection -module _ {x xs} where +module _ where to∈-injective : ∀ {p q : [ x ] ⊆ xs} → to∈ p ≡ to∈ q → p ≡ q to∈-injective = HeteroProperties.toAny-injective