------------------------------------------------------------------------ -- The Agda standard library -- -- Properties related to All ------------------------------------------------------------------------ module Data.List.All.Properties where open import Data.Bool open import Data.Bool.Properties open import Data.Empty open import Data.List as List import Data.List.Any as Any; open Any.Membership-≡ open import Data.List.All as All using (All; []; _∷_) open import Data.List.Any using (Any; here; there) open import Data.Product as Prod open import Function open import Function.Equality using (_⟨$⟩_) open import Function.Equivalence using (_⇔_; module Equivalence) open import Function.Inverse using (_↔_) open import Function.Surjection using (_↠_) open import Relation.Binary.PropositionalEquality as P using (_≡_) open import Relation.Nullary open import Relation.Unary using (Decidable) renaming (_⊆_ to _⋐_) -- Functions can be shifted between the predicate and the list. All-map : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p} {f : A → B} {xs} → All (P ∘ f) xs → All P (List.map f xs) All-map [] = [] All-map (p ∷ ps) = p ∷ All-map ps map-All : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p} {f : A → B} {xs} → All P (List.map f xs) → All (P ∘ f) xs map-All {xs = []} [] = [] map-All {xs = _ ∷ _} (p ∷ ps) = p ∷ map-All ps -- A variant of All.map. gmap : ∀ {a b p q} {A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q} {f : A → B} → P ⋐ Q ∘ f → All P ⋐ All Q ∘ List.map f gmap g = All-map ∘ All.map g -- All and all are related via T. All-all : ∀ {a} {A : Set a} (p : A → Bool) {xs} → All (T ∘ p) xs → T (all p xs) All-all p [] = _ All-all p (px ∷ pxs) = Equivalence.from T-∧ ⟨$⟩ (px , All-all p pxs) all-All : ∀ {a} {A : Set a} (p : A → Bool) xs → T (all p xs) → All (T ∘ p) xs all-All p [] _ = [] all-All p (x ∷ xs) px∷xs with Equivalence.to (T-∧ {p x}) ⟨$⟩ px∷xs all-All p (x ∷ xs) px∷xs | (px , pxs) = px ∷ all-All p xs pxs -- All is anti-monotone. anti-mono : ∀ {a p} {A : Set a} {P : A → Set p} {xs ys} → xs ⊆ ys → All P ys → All P xs anti-mono xs⊆ys pys = All.tabulate (All.lookup pys ∘ xs⊆ys) -- all is anti-monotone. all-anti-mono : ∀ {a} {A : Set a} (p : A → Bool) {xs ys} → xs ⊆ ys → T (all p ys) → T (all p xs) all-anti-mono p xs⊆ys = All-all p ∘ anti-mono xs⊆ys ∘ all-All p _ -- All P (xs ++ ys) is isomorphic to All P xs and All P ys. private ++⁺ : ∀ {a p} {A : Set a} {P : A → Set p} {xs ys : List A} → All P xs → All P ys → All P (xs ++ ys) ++⁺ [] pys = pys ++⁺ (px ∷ pxs) pys = px ∷ ++⁺ pxs pys ++⁻ : ∀ {a p} {A : Set a} {P : A → Set p} (xs : List A) {ys} → All P (xs ++ ys) → All P xs × All P ys ++⁻ [] p = [] , p ++⁻ (x ∷ xs) (px ∷ pxs) = Prod.map (_∷_ px) id $ ++⁻ _ pxs ++⁺∘++⁻ : ∀ {a p} {A : Set a} {P : A → Set p} xs {ys} (p : All P (xs ++ ys)) → uncurry′ ++⁺ (++⁻ xs p) ≡ p ++⁺∘++⁻ [] p = P.refl ++⁺∘++⁻ (x ∷ xs) (px ∷ pxs) = P.cong (_∷_ px) $ ++⁺∘++⁻ xs pxs ++⁻∘++⁺ : ∀ {a p} {A : Set a} {P : A → Set p} {xs ys} (p : All P xs × All P ys) → ++⁻ xs (uncurry ++⁺ p) ≡ p ++⁻∘++⁺ ([] , pys) = P.refl ++⁻∘++⁺ (px ∷ pxs , pys) rewrite ++⁻∘++⁺ (pxs , pys) = P.refl ++↔ : ∀ {a p} {A : Set a} {P : A → Set p} {xs ys} → (All P xs × All P ys) ↔ All P (xs ++ ys) ++↔ {P = P} {xs = xs} = record { to = P.→-to-⟶ $ uncurry ++⁺ ; from = P.→-to-⟶ $ ++⁻ xs ; inverse-of = record { left-inverse-of = ++⁻∘++⁺ ; right-inverse-of = ++⁺∘++⁻ xs } } -- Three lemmas relating Any, All and negation. ¬Any↠All¬ : ∀ {a p} {A : Set a} {P : A → Set p} {xs} → ¬ Any P xs ↠ All (¬_ ∘ P) xs ¬Any↠All¬ {P = P} = record { to = P.→-to-⟶ (to _) ; surjective = record { from = P.→-to-⟶ from ; right-inverse-of = to∘from } } where to : ∀ xs → ¬ Any P xs → All (¬_ ∘ P) xs to [] ¬p = [] to (x ∷ xs) ¬p = ¬p ∘ here ∷ to xs (¬p ∘ there) from : ∀ {xs} → All (¬_ ∘ P) xs → ¬ Any P xs from [] () from (¬p ∷ _) (here p) = ¬p p from (_ ∷ ¬p) (there p) = from ¬p p to∘from : ∀ {xs} (¬p : All (¬_ ∘ P) xs) → to xs (from ¬p) ≡ ¬p to∘from [] = P.refl to∘from (¬p ∷ ¬ps) = P.cong₂ _∷_ P.refl (to∘from ¬ps) -- If equality of functions were extensional, then the surjection -- could be strengthened to a bijection. from∘to : P.Extensionality _ _ → ∀ xs → (¬p : ¬ Any P xs) → from (to xs ¬p) ≡ ¬p from∘to ext [] ¬p = ext λ () from∘to ext (x ∷ xs) ¬p = ext λ { (here p) → P.refl ; (there p) → P.cong (λ f → f p) $ from∘to ext xs (¬p ∘ there) } Any¬→¬All : ∀ {a p} {A : Set a} {P : A → Set p} {xs} → Any (¬_ ∘ P) xs → ¬ All P xs Any¬→¬All (here ¬p) = ¬p ∘ All.head Any¬→¬All (there ¬p) = Any¬→¬All ¬p ∘ All.tail Any¬⇔¬All : ∀ {a p} {A : Set a} {P : A → Set p} {xs} → Decidable P → Any (¬_ ∘ P) xs ⇔ ¬ All P xs Any¬⇔¬All {P = P} dec = record { to = P.→-to-⟶ Any¬→¬All ; from = P.→-to-⟶ (from _) } where from : ∀ xs → ¬ All P xs → Any (¬_ ∘ P) xs from [] ¬∀ = ⊥-elim (¬∀ []) from (x ∷ xs) ¬∀ with dec x ... | yes p = there (from xs (¬∀ ∘ _∷_ p)) ... | no ¬p = here ¬p -- If equality of functions were extensional, then the logical -- equivalence could be strengthened to a surjection. to∘from : P.Extensionality _ _ → ∀ {xs} (¬∀ : ¬ All P xs) → Any¬→¬All (from xs ¬∀) ≡ ¬∀ to∘from ext ¬∀ = ext (⊥-elim ∘ ¬∀)