📥 Download raw
module Padova2025.ProvingBasics.Connectives.More where

All and Any

open import Padova2025.ProgrammingBasics.Lists
open import Padova2025.ProvingBasics.Negation
open import Padova2025.ProvingBasics.Equality.Base

The predicate All P xs expresses that P holds for all elements of the list xs.

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)

The predicate Any P xs expresses that P holds for at least one element of the list.

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)

As an application, Any can be used to define the membership predicate:

infix 4 _∈_ _∉_
_∈_ : {A : Set} → A → List A → Set
x ∈ xs = Any (x ≡_) xs

_∉_ : {A : Set} → A → List A → Set
x ∉ xs = ¬ (x ∈ xs)

Exercise: All and Any as functors

All-map : {A : Set} {P Q : A → Set} {xs : List A} → ({x : A} → P x → Q x) → All P xs → All Q xs
All-map = {!!}

Any-map : {A : Set} {P Q : A → Set} {xs : List A} → ({x : A} → P x → Q x) → Any P xs → Any Q xs
Any-map = {!!}

Exercise: De Morgan’s laws

Related to the exercise on De Morgan’s laws in the binary case.

de-morgan₁ : {A : Set} {P : A → Set} {xs : List A} → All (λ x → ¬ P x) xs → ¬ Any P xs
de-morgan₁ = {!!}

de-morgan₂ : {A : Set} {P : A → Set} {xs : List A} → ¬ Any P xs → All (λ x → ¬ P x) xs
de-morgan₂ = {!!}

de-morgan₃ : {A : Set} {P : A → Set} {xs : List A} → Any (λ x → ¬ P x) xs → ¬ All P xs
de-morgan₃ = {!!}

Exercise: Zero sum, revisited

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Connectives.Conjunction

Prove that, if the sum over the elements of a list of natural numbers is zero, then all elements are individually zero. The function sum-zero might come in handy, but the direct solution is also attractive.

sum-zero' : (xs : List ℕ) → sum xs ≡ zero → All (_≡ zero) xs
sum-zero' = {!!}

The converse also holds:

sum-zero'' : (xs : List ℕ) → All (_≡ zero) xs → sum xs ≡ zero
sum-zero'' = {!!}

Decidable truth values

open import Padova2025.ProvingBasics.Negation
open import Padova2025.ProvingBasics.Connectives.Disjunction
open import Padova2025.ProgrammingBasics.HigherOrder

In classical mathematics, where the law of excluded middle is available, we have A ∨ ¬A for any proposition A. In constructive mathematics, where we strive to be more informative, we don’t have this principle available for arbitrary propositions, but we do have it in many important special cases. If A ∨ ¬A holds, we say that A is decidable.

In Agda, we define the type Dec A of witnesses that A is decidable as follows.

data Dec (A : Set) : Set where
  yes : A   → Dec A
  no  : ¬ A → Dec A

In other words, Dec A is just a variant of A ⊎ ¬ A with the descriptive constructor names yes and no instead of left and `right.

Decidability of equality

infix 4 _≟_
_≟_ : (a b : ℕ) → Dec (a ≡ b)
a ≟ b = {!!}

Decidability of implication

Prove that, if A and B are decidable, so is A → B.

dec-→ : {A B : Set} → Dec A → Dec B → Dec (A → B)
dec-→ = {!!}

Finding elements with a specified property

find : {A : Set} {P : A → Set} → ((x : A) → Dec (P x)) → (xs : List A) → Any P xs ⊎ All (λ x → ¬ (P x)) xs
find = {!!}