📥 Download raw
{-# OPTIONS --cubical-compatible #-}
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
open import Padova2025.ProvingBasics.Equality.General
open import Padova2025.ProvingBasics.Connectives.Existential

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:

satisfied : {A : Set} {P : A → Set} {xs : List A} → Any P xs → Σ[ x ∈ A ] P x
satisfied = {!!}

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 = {!!}

Tabulation

tabulate : {A : Set} {P : A → Set} (xs : List A) → ({x : A} → x ∈ xs → P x) → All P xs
tabulate = {!!}

All distributes over append

All-++-left : {A : Set} {P : A → Set} {ys : List A} (xs : List A) → All P (xs ++ ys) → All P xs
All-++-left = {!!}

All-++-right : {A : Set} {P : A → Set} {ys : List A} (xs : List A) → All P (xs ++ ys) → All P ys
All-++-right = {!!}

infixr 5 _++ᴬ_
_++ᴬ_ : {A : Set} {P : A → Set} {xs ys : List A} → All P xs → All P ys → All P (xs ++ ys)
[]       ++ᴬ ps' = {!!}
(p ∷ ps) ++ᴬ ps' = {!!}

Any distributes over append

Any-++-left : {A : Set} {P : A → Set} {xs : List A} {ys : List A} → Any P xs → Any P (xs ++ ys)
Any-++-left = {!!}

Any-++-right : {A : Set} {P : A → Set} {xs : List A} {ys : List A} → Any P ys → Any P (xs ++ ys)
Any-++-right = {!!}

∈-concat
  : {A : Set} {x : A} {xs : List A} {xss : List (List A)}
  → x ∈ xs → xs ∈ xss → x ∈ concat xss
∈-concat = {!!}

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 = {!!}

Decidability of All

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

Almost everywhere equal functions

Two functions are deemed almost everywhere equal iff they differ only on finitely many inputs

_≗*_ : {X Y : Set} → (X → Y) → (X → Y) → Set
f ≗* g = Σ[ xs ∈ List _ ] ((x : _) → f x ≡ g x ⊎ x ∈ xs)

Pointwise equal functions are equal almost everywhere:

≗→≗* : {X Y : Set} {f g : X → Y} → f ≗ g → f ≗* g
≗→≗* = {!!}

The relation _≗*_ is indeed an equivalence relation by the following lemmas.

≗*-refl : {X Y : Set} {f : X → Y} → f ≗* f
≗*-refl = {!!}

≗*-sym : {X Y : Set} {f g : X → Y} → f ≗* g → g ≗* f
≗*-sym = {!!}

≗*-trans : {X Y : Set} {f g h : X → Y} → f ≗* g → g ≗* h → f ≗* h
≗*-trans = {!!}

We will also use the occasion to define the notion of a normalizer for functions X → Y. A normalizer picks for each _≗*_-equivalence class a representative. Such normalizers exist by the axiom of choice (which we will occasionally assume, to explore its consequences).

TODO explain records

record Normalizer (X Y : Set) : Set where
  field
    rep      : (X → Y) → (X → Y)
    rep≗*    : (f : X → Y) → rep f ≗* f
    respects : {f g : X → Y} → f ≗* g → rep f ≗ rep g

Unpacking: rep is the representative-picking function; rep≗* says that what rep picks always lies in the same equivalence class as its input; and respects is the defining property of a choice function, stating that rep returns the same representative for any two _≗*_-equivalent configurations.