------------------------------------------------------------------------
-- The Agda standard library
--
-- Documentation for the `All` predicate over `List`
------------------------------------------------------------------------

module README.Data.List.Relation.Unary.All where

open import Data.List.Base using ([]; _∷_)
open import Data.Nat using (ℕ; s≤s; z≤n; _≤_)
open import Data.Nat.Properties using (≤-trans; n≤1+n)

------------------------------------------------------------------------
-- All

-- The dual to `Any` is the predicate `All` which encodes the idea that
-- every element in a given list satisfies a given property.

open import Data.List.Relation.Unary.All

-- Proofs for `All` are constructed using exactly the same syntax as
-- is used to construct lists ("[]" & "_∷_"). For example to prove
-- that every element in a list is less than or equal to one:

lem₁ : All (_≤ ) ( ∷  ∷  ∷ [])
lem₁ = 1≤1 ∷ 0≤1 ∷ 1≤1 ∷ []
  where
  0≤1 = z≤n
  1≤1 = s≤s z≤n

-- As with `Any`, the module also provides the standard operators
-- `map`, `zip` etc. to manipulate proofs for `All`.

import Data.List.Relation.Unary.All as All

lem₂ : All (_≤ ) ( ∷  ∷  ∷ [])
lem₂ = All.map ≤1⇒≤2 lem₁
  where
  ≤1⇒≤2 : ∀ {x} → x ≤  → x ≤ 
  ≤1⇒≤2 x≤1 = ≤-trans x≤1 (n≤1+n )

-- Properties of how list functions interact with `All` can be
-- found in:

import Data.List.Relation.Unary.All.Properties