diff --git a/src/Decidable.lagda b/src/Decidable.lagda index ecb5bd98..5fad5243 100644 --- a/src/Decidable.lagda +++ b/src/Decidable.lagda @@ -22,6 +22,8 @@ open import Relation.Nullary using (¬_) open import Relation.Nullary.Negation using (contraposition) open import Data.Unit using (⊤; tt) open import Data.Empty using (⊥; ⊥-elim) +open import Data.List using (List; []; _∷_; foldr; map) +open import Function using (_∘_) \end{code} ## Evidence vs Computation @@ -361,8 +363,8 @@ infixr 6 _×-dec_ _×-dec_ : {A B : Set} → Dec A → Dec B → Dec (A × B) yes x ×-dec yes y = yes ⟨ x , y ⟩ -no ¬x ×-dec _ = no (λ { ⟨ x , y ⟩ → ¬x x }) -_ ×-dec no ¬y = no (λ { ⟨ x , y ⟩ → ¬y y }) +no ¬x ×-dec _ = no λ{ ⟨ x , y ⟩ → ¬x x } +_ ×-dec no ¬y = no λ{ ⟨ x , y ⟩ → ¬y y } \end{code} The conjunction of two propositions holds if they both hold, and its negation holds if the negation of either holds. @@ -392,9 +394,9 @@ decide their disjunction. infixr 5 _⊎-dec_ _⊎-dec_ : {A B : Set} → Dec A → Dec B → Dec (A ⊎ B) -_ ⊎-dec yes y = yes (inj₂ y) yes x ⊎-dec _ = yes (inj₁ x) -no ¬x ⊎-dec no ¬y = no (λ { (inj₁ x) → ¬x x ; (inj₂ y) → ¬y y }) +_ ⊎-dec yes y = yes (inj₂ y) +no ¬x ⊎-dec no ¬y = no λ{ (inj₁ x) → ¬x x ; (inj₂ y) → ¬y y } \end{code} The disjunction of two propositions holds if either holds, and its negation holds if the negation of both hold. @@ -413,13 +415,13 @@ Correspondingly, given a decidable proposition, we can decide its negation. \begin{code} not? : {A : Set} → Dec A → Dec (¬ A) -not? (yes x) = no (λ { ¬x → ¬x x }) +not? (yes x) = no λ{ ¬x → ¬x x } not? (no ¬x) = yes ¬x \end{code} We simply swap yes and no. In the first equation, the right-hand side asserts that the negation of `¬ A` holds, in other words, that `¬ ¬ A` holds, which is an easy consequence -of `A`. +of the fact that `A` holds. There is also a slightly less familiar connective, corresponding to implication. @@ -457,13 +459,61 @@ we apply the evidence of the implication `f` to the evidence of the first `x`, yielding a contradiction with the evidence `¬y` of the negation of the second. -## All and Any +## Decidability of All +Recall that in Chapter [Lists](Lists#All) we defined a predicate `All P` +that holds if a given predicate is satisfied by every element of a list. +\begin{code} +data All {A : Set} (P : A → Set) : List A → Set where + [] : All P [] + _∷_ : {x : A} {xs : List A} → P x → All P xs → All P (x ∷ xs) +\end{code} +If instead we consider a predicate as a function that yields a boolean, +it is easy to define an analogue of `All`, which returns true if +a given predicate returns true for every element of a list. +\begin{code} +all : ∀ {A : Set} → (A → Bool) → List A → Bool +all p = foldr _∧_ true ∘ map p +\end{code} +The function can be written in a particularly compact style by +using the higher-order functions `map` and `foldr` as defined in +the sections on [Map](Lists#Map) and [Fold](Lists#Fold). + +As one would hope, if we replace booleans by decidables there is again +an analogue of `All`. First, return to the notion of a predicate `P` as +a function of type `A → Set`, taking a value `x` of type `A` into evidence +`P x` that a property holds for `x`. Say that a predicate `P` is *decidable* +if we have a function that for a given `x` can decide `P x`. +\begin{code} +Decidable : ∀ {A : Set} → (A → Set) → Set +Decidable {A} P = (x : A) → Dec (P x) +\end{code} +Then if predicate `P` is decidable, it is also decidable whether every +element of a list satisfies the predicate. +\begin{code} +all? : ∀ {A : Set} {P : A → Set} → Decidable P → Decidable (All P) +all? p? [] = yes [] +all? p? (x ∷ xs) with p? x | all? p? xs +... | yes px | yes pxs = yes (px ∷ pxs) +... | no ¬px | _ = no λ{ (px ∷ pxs) → ¬px px } +... | _ | no ¬pxs = no λ{ (px ∷ pxs) → ¬pxs pxs } +\end{code} +If the list is empty, then trivially `P` holds for every element of +the list. Otherwise, the structure of the proof is similar to that +showing that the conjuction of two decidable propositions is itself +decidable, using `_∷_` rather than `⟨_,_⟩` to combine the evidence for +the head and tail of the list. + +*Exercise* `any` `any?` + +Just as `All` has analogues `all` and `all?` which determine whether a +predicate holds for every element of a list, so does `Any` have +analogues `any` and `any?` which determine whether a predicates holds +for some element of a list. Give their definitions. + + ## Unicode - ∷ U+2237 PROPORTION (\::) - ⊗ U+2297 CIRCLED TIMES (\otimes) - ∈ U+2208 ELEMENT OF (\in) - ∉ U+2209 NOT AN ELEMENT OF (\inn) + ᵇ U+1D47 MODIFIER LETTER SMALL B (\^b) diff --git a/src/Lists.lagda b/src/Lists.lagda index 2ee78f75..9d259cb6 100644 --- a/src/Lists.lagda +++ b/src/Lists.lagda @@ -463,7 +463,7 @@ ex₄ = \end{code} Now the time to reverse a list is linear in the length of the list. -## Map +## Map {#Map} Map applies a function to every element of a list to generate a corresponding list. Map is an example of a *higher-order function*, one which takes a function as an @@ -542,7 +542,7 @@ Prove the following relationship between map and append. map f (xs ++ ys) ≡ map f xs ++ map f ys -## Fold +## Fold {#Fold} Fold takes an operator and a value, and uses the operator to combine each of the elements of the list, taking the given value as the result @@ -707,9 +707,10 @@ foldr-monoid-++ _⊗_ e monoid-⊗ xs ys = ∎ \end{code} -## All +## All {#All} -We can also define predicates over lists. Two of the most important are `All` and `Any`. +We can also define predicates over lists. Two of the most important +are `All` and `Any`. Predicate `All P` holds if predicate `P` is satisfied by every element of a list. \begin{code} @@ -718,11 +719,11 @@ data All {A : Set} (P : A → Set) : List A → Set where _∷_ : {x : A} {xs : List A} → P x → All P xs → All P (x ∷ xs) \end{code} The type has two constructors, reusing the names of the same constructors for lists. -The first asserts that `All P` always holds of the empty list. -The second asserts that if `P` holds of the head of a list, and if `All P` -holds of the tail of the list, then `All P` holds for the entire list. -Agda uses type information to distinguish whether the constructor is building -a list, or evidence that `All P` holds. +The first asserts that `P` holds for ever element of the empty list. +The second asserts that if `P` holds of the head of a list and for every +element of the tail of a list, then `P` holds for every element of the list. +Agda uses types to disambiguate whether the constructor is building +a list or evidence that `All P` holds. For example, `All (_≤ 2)` holds of a list where every element is less than or equal to two. Recall that `z≤n` proves `zero ≤ n` for any @@ -743,9 +744,10 @@ data Any {A : Set} (P : A → Set) : List A → Set where here : {x : A} {xs : List A} → P x → Any P (x ∷ xs) there : {x : A} {xs : List A} → Any P xs → Any P (x ∷ xs) \end{code} -The first constructor provides evidence that the head of the list satisfies `P`, -while the second provides evidence that the tail of the list satisfies `Any P`. -For example, we can define list membership as follows. +The first constructor provides evidence that the head of the list +satisfies `P`, while the second provides evidence that some element of +the tail of the list satisfies `P`. For example, we can define list +membership as follows. \begin{code} infix 4 _∈_