```
{-# 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](Padova2025.ProvingBasics.Connectives.Conjunction.html#exercise-de-morgans-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`](Padova2025.ProvingBasics.Connectives.Conjunction.html#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 \vee \neg 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`](Padova2025.ProvingBasics.Connectives.Disjunction.html#_⊎_.left)
and [`right`](Padova2025.ProvingBasics.Connectives.Disjunction.html#_⊎_.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.