------------------------------------------------------------------------ -- The Agda standard library -- -- Sublist-related properties ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} module Data.List.Relation.Binary.Sublist.Propositional.Properties where open import Data.Empty open import Data.List.Base hiding (lookup) open import Data.List.Properties open import Data.List.Relation.Unary.Any using (here; there) open import Data.List.Relation.Unary.Any.Properties using (here-injective; there-injective) open import Data.List.Membership.Propositional open import Data.List.Relation.Binary.Sublist.Propositional open import Data.Maybe as Maybe using (nothing; just) open import Data.Maybe.Relation.Unary.All as MAll using (nothing; just) open import Data.Nat.Base open import Data.Nat.Properties open import Function import Function.Bijection as Bij open import Function.Equivalence as Equiv using (_⇔_ ; equivalence) import Function.Injection as Inj open import Relation.Binary open import Relation.Binary.PropositionalEquality as Eq hiding ([_]) open import Relation.Nullary import Relation.Nullary.Decidable as D open import Relation.Unary as U using (Pred) ------------------------------------------------------------------------ -- The `loookup` function induced by a proof that `xs ⊆ ys` is injective module _ {a} {A : Set a} where lookup-injective : ∀ {x : A} {xs ys} {p : xs ⊆ ys} {v w : x ∈ xs} → lookup p v ≡ lookup p w → v ≡ w lookup-injective {p = skip p} {v} {w} eq = lookup-injective (there-injective eq) lookup-injective {p = keep p} {here px} {here qx} refl = refl lookup-injective {p = keep p} {there v} {there w} eq = cong there (lookup-injective (there-injective eq)) -- impossible cases lookup-injective {p = keep p} {here px} {there w} () lookup-injective {p = keep p} {there v} {here qx} () lookup-injective {p = base} {} []∈-irrelevant : U.Irrelevant {A = List A} ([] ⊆_) []∈-irrelevant base base = refl []∈-irrelevant (skip p) (skip q) = cong skip ([]∈-irrelevant p q) [x]⊆xs↔x∈xs : ∀ {x : A} {xs} → ([ x ] ⊆ xs) Bij.⤖ (x ∈ xs) [x]⊆xs↔x∈xs {x} = Bij.bijection to∈ from∈ (to∈-injective _ _ refl) to∈∘from∈≗id where to∈-injective : ∀ {xs x y} (p : [ x ] ⊆ xs) (q : [ y ] ⊆ xs) (eq : x ≡ y) → to∈ p ≡ lookup q (here eq) → subst ((_⊆ xs) ∘ [_]) eq p ≡ q to∈-injective (skip p) (skip q) refl eq = cong skip (to∈-injective p q refl (there-injective eq)) to∈-injective (keep p) (keep q) eq refl = cong keep ([]∈-irrelevant p q) to∈-injective (skip p) (keep q) refl () to∈-injective (keep p) (skip q) refl () to∈∘from∈≗id : ∀ {xs} (p : x ∈ xs) → to∈ (from∈ p) ≡ p to∈∘from∈≗id (here refl) = refl to∈∘from∈≗id (there p) = cong there (to∈∘from∈≗id p) ------------------------------------------------------------------------ -- Some properties module _ {a} {A : Set a} where ⊆-length : ∀ {xs ys : List A} → xs ⊆ ys → length xs ≤ length ys ⊆-length base = ≤-refl ⊆-length (skip p) = ≤-step (⊆-length p) ⊆-length (keep p) = s≤s (⊆-length p) ------------------------------------------------------------------------ -- Relational properties module _ {a} {A : Set a} where ⊆-reflexive : _≡_ ⇒ _⊆_ {A = A} ⊆-reflexive {[]} refl = base ⊆-reflexive {x ∷ xs} refl = keep (⊆-reflexive refl) ⊆-refl : Reflexive {A = List A} _⊆_ ⊆-refl = ⊆-reflexive refl ⊆-trans : Transitive {A = List A} _⊆_ ⊆-trans p base = p ⊆-trans p (skip q) = skip (⊆-trans p q) ⊆-trans (skip p) (keep q) = skip (⊆-trans p q) ⊆-trans (keep p) (keep q) = keep (⊆-trans p q) open ≤-Reasoning ⊆-antisym : Antisymmetric {A = List A} _≡_ _⊆_ ⊆-antisym = λ p q → ⊆-antisym′ p q refl where ⊆-antisym′ : ∀ {xs ys zs} → xs ⊆ ys → ys ⊆ zs → xs ≡ zs → xs ≡ ys -- Positive cases ⊆-antisym′ base base refl = refl ⊆-antisym′ (keep p) (keep q) eq = cong (_ ∷_) (⊆-antisym′ p q (cong (drop 1) eq)) -- Dismissing the impossible cases ⊆-antisym′ {x ∷ xs} {y ∷ ys} (skip p) (skip q) refl = ⊥-elim $ 1+n≰n $ begin length (y ∷ ys) ≤⟨ ⊆-length q ⟩ length xs ≤⟨ n≤1+n (length xs) ⟩ length (x ∷ xs) ≤⟨ ⊆-length p ⟩ length ys ∎ ⊆-antisym′ {x ∷ xs} {y ∷ ys} (skip p) (keep q) refl = ⊥-elim $ 1+n≰n $ begin length (x ∷ xs) ≤⟨ ⊆-length p ⟩ length ys ≤⟨ ⊆-length q ⟩ length xs ∎ ⊆-antisym′ {x ∷ xs} {y ∷ ys} (keep p) (skip q) refl = ⊥-elim $ 1+n≰n $ begin length (y ∷ ys) ≤⟨ ⊆-length q ⟩ length xs ≤⟨ ⊆-length p ⟩ length ys ∎ ⊆-minimum : Minimum (_⊆_ {A = A}) [] ⊆-minimum = []⊆_ module _ {a} (A : Set a) where ⊆-isPreorder : IsPreorder _≡_ (_⊆_ {A = A}) ⊆-isPreorder = record { isEquivalence = isEquivalence ; reflexive = ⊆-reflexive ; trans = ⊆-trans } ⊆-preorder : Preorder _ _ _ ⊆-preorder = record { isPreorder = ⊆-isPreorder } ⊆-isPartialOrder : IsPartialOrder _≡_ _⊆_ ⊆-isPartialOrder = record { isPreorder = ⊆-isPreorder ; antisym = ⊆-antisym } ⊆-poset : Poset _ _ _ ⊆-poset = record { isPartialOrder = ⊆-isPartialOrder } import Relation.Binary.Reasoning.PartialOrder as POR module ⊆-Reasoning {a} {A : Set a} where private module P = POR (⊆-poset A) open P public renaming (_≤⟨_⟩_ to _⊆⟨_⟩_) hiding (_≈⟨_⟩_; _≈˘⟨_⟩_; _≈⟨⟩_) ------------------------------------------------------------------------ -- Various functions' outputs are sublists module _ {a} {A : Set a} where tail-⊆ : (xs : List A) → MAll.All (_⊆ xs) (tail xs) tail-⊆ [] = nothing tail-⊆ (x ∷ xs) = just (skip ⊆-refl) take-⊆ : ∀ n (xs : List A) → take n xs ⊆ xs take-⊆ zero xs = []⊆ xs take-⊆ (suc n) [] = []⊆ [] take-⊆ (suc n) (x ∷ xs) = keep (take-⊆ n xs) drop-⊆ : ∀ n (xs : List A) → drop n xs ⊆ xs drop-⊆ zero xs = ⊆-refl drop-⊆ (suc n) [] = []⊆ [] drop-⊆ (suc n) (x ∷ xs) = skip (drop-⊆ n xs) module _ {a p} {A : Set a} {P : Pred A p} (P? : U.Decidable P) where takeWhile-⊆ : ∀ xs → takeWhile P? xs ⊆ xs takeWhile-⊆ [] = []⊆ [] takeWhile-⊆ (x ∷ xs) with P? x ... | yes p = keep (takeWhile-⊆ xs) ... | no ¬p = []⊆ x ∷ xs dropWhile-⊆ : ∀ xs → dropWhile P? xs ⊆ xs dropWhile-⊆ [] = []⊆ [] dropWhile-⊆ (x ∷ xs) with P? x ... | yes p = skip (dropWhile-⊆ xs) ... | no ¬p = ⊆-refl filter-⊆ : ∀ xs → filter P? xs ⊆ xs filter-⊆ [] = []⊆ [] filter-⊆ (x ∷ xs) with P? x ... | yes p = keep (filter-⊆ xs) ... | no ¬p = skip (filter-⊆ xs) ------------------------------------------------------------------------ -- Various functions are increasing wrt _⊆_ ------------------------------------------------------------------------ -- _∷_ module _ {a} {A : Set a} where ∷⁻ : ∀ {x y} {us vs : List A} → x ∷ us ⊆ y ∷ vs → us ⊆ vs ∷⁻ (skip p) = ⊆-trans (skip ⊆-refl) p ∷⁻ (keep p) = p -- map module _ {a b} {A : Set a} {B : Set b} where map⁺ : ∀ {xs ys} (f : A → B) → xs ⊆ ys → map f xs ⊆ map f ys map⁺ f base = base map⁺ f (skip p) = skip (map⁺ f p) map⁺ f (keep p) = keep (map⁺ f p) open Inj.Injection map⁻ : ∀ {xs ys} (inj : A Inj.↣ B) → map (inj ⟨$⟩_) xs ⊆ map (inj ⟨$⟩_) ys → xs ⊆ ys map⁻ {[]} {ys} inj p = []⊆ ys map⁻ {x ∷ xs} {[]} inj () map⁻ {x ∷ xs} {y ∷ ys} inj p with inj ⟨$⟩ x | inspect (inj ⟨$⟩_) x | inj ⟨$⟩ y | inspect (inj ⟨$⟩_) y | injective inj {x} {y} map⁻ {x ∷ xs} {y ∷ ys} inj (skip p) | fx | Eq.[ eq ] | fy | _ | _ = skip (map⁻ inj (coerce p)) where coerce = subst (λ fx → fx ∷ _ ⊆ _) (sym eq) map⁻ {x ∷ xs} {y ∷ ys} inj (keep p) | fx | _ | fx | _ | eq rewrite eq refl = keep (map⁻ inj p) -- _++_ module _ {a} {A : Set a} where ++⁺ : ∀ {xs ys us vs : List A} → xs ⊆ ys → us ⊆ vs → xs ++ us ⊆ ys ++ vs ++⁺ base q = q ++⁺ (skip p) q = skip (++⁺ p q) ++⁺ (keep p) q = keep (++⁺ p q) ++⁻ : ∀ xs {us vs : List A} → xs ++ us ⊆ xs ++ vs → us ⊆ vs ++⁻ [] p = p ++⁻ (x ∷ xs) p = ++⁻ xs (∷⁻ p) skips : ∀ {xs ys} (zs : List A) → xs ⊆ ys → xs ⊆ zs ++ ys skips zs = ++⁺ ([]⊆ zs) -- take / drop ≤-take-⊆ : ∀ {m n} → m ≤ n → (xs : List A) → take m xs ⊆ take n xs ≤-take-⊆ z≤n xs = []⊆ take _ xs ≤-take-⊆ (s≤s p) [] = []⊆ [] ≤-take-⊆ (s≤s p) (x ∷ xs) = keep (≤-take-⊆ p xs) ≥-drop-⊆ : ∀ {m n} → m ≥ n → (xs : List A) → drop m xs ⊆ drop n xs ≥-drop-⊆ {m} z≤n xs = drop-⊆ m xs ≥-drop-⊆ (s≤s p) [] = []⊆ [] ≥-drop-⊆ (s≤s p) (x ∷ xs) = ≥-drop-⊆ p xs drop⁺ : ∀ n {xs ys : List A} → xs ⊆ ys → drop n xs ⊆ drop n ys drop⁺ zero p = p drop⁺ (suc n) base = []⊆ [] drop⁺ (suc n) (keep p) = drop⁺ n p drop⁺ (suc n) {xs} {y ∷ ys} (skip p) = begin drop (suc n) xs ⊆⟨ ≥-drop-⊆ (n≤1+n n) xs ⟩ drop n xs ⊆⟨ drop⁺ n p ⟩ drop n ys ∎ where open ⊆-Reasoning module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} (P? : U.Decidable P) (Q? : U.Decidable Q) where ⊆-takeWhile-⊆ : (P U.⊆ Q) → ∀ xs → takeWhile P? xs ⊆ takeWhile Q? xs ⊆-takeWhile-⊆ P⊆Q [] = []⊆ [] ⊆-takeWhile-⊆ P⊆Q (x ∷ xs) with P? x | Q? x ... | yes px | yes qx = keep (⊆-takeWhile-⊆ P⊆Q xs) ... | yes px | no ¬qx = ⊥-elim $ ¬qx (P⊆Q px) ... | no ¬px | _ = []⊆ _ ⊇-dropWhile-⊆ : (P U.⊇ Q) → ∀ xs → dropWhile P? xs ⊆ dropWhile Q? xs ⊇-dropWhile-⊆ P⊇Q [] = []⊆ [] ⊇-dropWhile-⊆ P⊇Q (x ∷ xs) with P? x | Q? x ... | yes px | yes qx = ⊇-dropWhile-⊆ P⊇Q xs ... | yes px | no ¬qx = skip (dropWhile-⊆ P? xs) ... | no ¬px | yes qx = ⊥-elim $ ¬px (P⊇Q qx) ... | no ¬px | no ¬qx = ⊆-refl -- filter ⊆-filter-⊆ : (P U.⊆ Q) → ∀ xs → filter P? xs ⊆ filter Q? xs ⊆-filter-⊆ P⊆Q [] = []⊆ [] ⊆-filter-⊆ P⊆Q (x ∷ xs) with P? x | Q? x ... | yes px | yes qx = keep (⊆-filter-⊆ P⊆Q xs) ... | yes px | no ¬qx = ⊥-elim $ ¬qx (P⊆Q px) ... | no ¬px | yes qx = skip (⊆-filter-⊆ P⊆Q xs) ... | no ¬px | no ¬qx = ⊆-filter-⊆ P⊆Q xs module _ {a p} {A : Set a} {P : Pred A p} (P? : U.Decidable P) where filter⁺ : ∀ {xs ys : List A} → xs ⊆ ys → filter P? xs ⊆ filter P? ys filter⁺ base = base filter⁺ {xs} {y ∷ ys} (skip p) with P? y ... | yes py = skip (filter⁺ p) ... | no ¬py = filter⁺ p filter⁺ {x ∷ xs} {x ∷ ys} (keep p) with P? x ... | yes px = keep (filter⁺ p) ... | no ¬px = filter⁺ p -- reverse module _ {a} {A : Set a} where open ⊆-Reasoning reverse⁺ : {xs ys : List A} → xs ⊆ ys → reverse xs ⊆ reverse ys reverse⁺ base = []⊆ [] reverse⁺ {xs} {y ∷ ys} (skip p) = begin reverse xs ≡⟨ sym $ ++-identityʳ _ ⟩ reverse xs ++ [] ⊆⟨ ++⁺ (reverse⁺ p) ([]⊆ _) ⟩ reverse ys ∷ʳ y ≡⟨ sym $ unfold-reverse y ys ⟩ reverse (y ∷ ys) ∎ reverse⁺ {x ∷ xs} {x ∷ ys} (keep p) = begin reverse (x ∷ xs) ≡⟨ unfold-reverse x xs ⟩ reverse xs ∷ʳ x ⊆⟨ ++⁺ (reverse⁺ p) ⊆-refl ⟩ reverse ys ∷ʳ x ≡⟨ sym $ unfold-reverse x ys ⟩ reverse (x ∷ ys) ∎ reverse⁻ : {xs ys : List A} → reverse xs ⊆ reverse ys → xs ⊆ ys reverse⁻ {xs} {ys} p = cast (reverse⁺ p) where cast = subst₂ _⊆_ (reverse-involutive xs) (reverse-involutive ys) ------------------------------------------------------------------------ -- Inversion lemmas module _ {a} {A : Set a} where keep⁻¹ : ∀ (x : A) {xs ys} → (xs ⊆ ys) ⇔ (x ∷ xs ⊆ x ∷ ys) keep⁻¹ x = equivalence keep ∷⁻ skip⁻¹ : ∀ {x y : A} {xs ys} → x ≢ y → (x ∷ xs ⊆ ys) ⇔ (x ∷ xs ⊆ y ∷ ys) skip⁻¹ ¬eq = equivalence skip $ λ where (skip p) → p (keep p) → ⊥-elim (¬eq refl) ++⁻¹ : ∀ (ps : List A) {xs ys} → (xs ⊆ ys) ⇔ (ps ++ xs ⊆ ps ++ ys) ++⁻¹ ps = equivalence (++⁺ ⊆-refl) (++⁻ ps) ------------------------------------------------------------------------ -- Decidability of the order module Decidable {a} {A : Set a} (eq? : Decidable {A = A} _≡_) where infix 3 _⊆?_ _⊆?_ : Decidable {A = List A} _⊆_ [] ⊆? ys = yes ([]⊆ ys) x ∷ xs ⊆? [] = no λ () x ∷ xs ⊆? y ∷ ys with eq? x y ... | yes refl = D.map (keep⁻¹ x) (xs ⊆? ys) ... | no ¬eq = D.map (skip⁻¹ ¬eq) (x ∷ xs ⊆? ys)