module Sets.Propositions where open import Data.Nat using (ℕ; zero; suc)

It is beneficial to represent proofs as ordinary data — we can manipulate them like natural numbers. The proofs of each proposition will have a distinct type.

We represent the proofs of the **true proposition** by the type `⊤`

. The true proposition has a trivial proof: `tt`

(trivially true).

data ⊤ : Set where tt : ⊤

We represent the proofs of the **false proposition** by the type `⊥`

. False proposition have no proofs (thus they cannot be proven).

data ⊥ : Set where

We represent the proofs of the **conjunction** of two propositions `A`

and `B`

by the type `A × B`

. `A × B`

has proofs of form `a , b`

where `a`

is a proof of `A`

and `b`

is a proof of `B`

.

data _×_ (A B : Set) : Set where _,_ : A → B → A × B infixr 4 _,_ infixr 2 _×_

We represent the proofs of the **disjunction** of two propositions `A`

and `B`

by the type `A ⊎ B`

. `A ⊎ B`

has two different kinds of proofs:

`inj₁ a`

, where`a`

is proof of`A`

,`inj₂ b`

, where`b`

is proof of`B`

.

data _⊎_ (A B : Set) : Set where inj₁ : A → A ⊎ B inj₂ : B → A ⊎ B infixr 1 _⊎_

Construct one proof for each proposition if possible:

`⊤ × ⊤`

`⊤ × ⊥`

`⊥ × ⊥`

`⊤ ⊎ ⊤`

`⊤ ⊎ ⊥`

`⊥ ⊎ ⊥`

`⊥ ⊎ ⊤ ⊎ ⊤ × (⊥ ⊎ ⊥) ⊎ ⊤`

For example:

⊤×⊤ : ⊤ × ⊤ ⊤×⊤ = tt , tt

We will discuss the representation of implication, negation, universal, and existential quantification later.

Note that `_⊎_`

represents a *constructive* disjunction. We are going to formalize the classical disjunction that way and compare the obtained concepts as we proceed.

`_≤_`

: Less-or-equal predicateWe wish to represent proofs of propositions n ≤ m (n, m = 0, 1, ...). For this, we define a set indexed with two natural numbers:

data _≤_ : ℕ → ℕ → Set where z≤n : {n : ℕ} → zero ≤ n s≤s : {m : ℕ} → {n : ℕ} → m ≤ n → suc m ≤ suc n infix 4 _≤_

This yields the following judgements:

```
z≤n {0} : 0 ≤ 0
z≤n {1} : 0 ≤ 1
z≤n {2} : 0 ≤ 2
...
s≤s (z≤n {0}) : 1 ≤ 1
s≤s (z≤n {1}) : 1 ≤ 2
s≤s (z≤n {2}) : 1 ≤ 3
...
s≤s (s≤s (z≤n {0})) : 2 ≤ 2
s≤s (s≤s (z≤n {1})) : 2 ≤ 3
s≤s (s≤s (z≤n {2})) : 2 ≤ 4
...
...
```

that means that the following propositions have proofs:

```
0 ≤ 0
0 ≤ 1, 1 ≤ 1
0 ≤ 2, 1 ≤ 2, 2 ≤ 2
0 ≤ 3, 1 ≤ 3, 2 ≤ 3, 3 ≤ 3
... ...
```

Notes:

- The
`z≤n`

constructor yields the first column of judgements. - The
`s≤s`

constructor yields the successive columns of judgements. `1 ≤ 0`

is also a valid expression that denotes an empty set.

We can prove that a set is non-empty if we can construct any of its elements (recall how constants may be defined):

1≤10 : 1 ≤ 10 1≤10 = s≤s z≤n

Prove that 3 ≤ 7.

How could we prove that a set like `7 ≤ 3`

is empty?

If

`7 ≤ 3`

was non-empty, all its elements would look like`s≤s x`

where`x : 6 ≤ 2`

.`z≤n`

yields an element in`0 ≤ n`

and`0`

≠`7`

.

If

`6 ≤ 2`

was non-empty, all its elements would look like`s≤s x`

where`x : 5 ≤ 1`

.`z≤n`

yields an element in`0 ≤ n`

and`0`

≠`6`

.

If

`5 ≤ 1`

was non-empty, all its elements would look like`s≤s x`

where`x : 4 ≤ 0`

.`z≤n`

yields an element in`0 ≤ n`

and`0`

≠`5`

.

`4 ≤ 0`

is empty.`z≤n`

yields an element in`0 ≤ n`

and`0`

≠`4`

.`s≤s`

yields an element in`suc m ≤ suc n`

and`suc n`

≠`0`

.

Although we will discuss all the details later, here we have a look at how this chain of inference could be given in Agda:*

7≰3 : 7 ≤ 3 → ⊥ 7≰3 (s≤s (s≤s (s≤s ())))

where `()`

denotes a value in a trivially empty set.

Prove that `4 ≤ 2`

is empty.

Note that emptiness proofs can be used in other emptiness proofs:

8≰4 : 8 ≤ 4 → ⊥ 8≰4 (s≤s x) = 7≰3 x

where `x`

is an arbitrary variable name.

Guess what kind of code can be generated from emptiness proofs.

*: `7 ≤ 3 → ⊥`

denotes a function from `7 ≤ 3`

to `⊥`

so we are proving that `7 ≤ 3`

is empty by giving a function that maps `7 ≤ 3`

to a trivially empty set. Here, we show that `7 ≤ 3`

has no elements hence the function is defined. We are going to discuss functions in details later.

Define an indexed set

`_isDoubleOf_ : ℕ → ℕ → Set`

such that`m isDoubleOf n`

is non-empty iff (if and only if)`m`

is the double of`n`

.- Prove that
`8 isDoubleOf 4`

is non-empty. - Prove that
`9 isDoubleOf 4`

is empty.

- Prove that
Define an indexed set

`Odd : ℕ → Set`

such that`Odd n`

is non-empty iff`n`

is odd.- Prove that
`Odd 9`

is non-empty. - Prove that
`Odd 8`

is empty.

- Prove that
Define

`Even : ℕ → Set`

and`Odd : ℕ → Set`

mutually.Define equality

`_≡_ : ℕ → ℕ → Set`

.Define non-equality

`_≠_ : ℕ → ℕ → Set`

.

`_≤_`

Consider the following indexed type:

data _≤′_ : ℕ → ℕ → Set where ≤′-refl : {m : ℕ} → m ≤′ m ≤′-step : {m : ℕ} → {n : ℕ} → m ≤′ n → m ≤′ suc n infix 4 _≤′_

that yields the following:

```
≤′-refl : 0 ≤ 0
≤′-step ≤′-refl : 0 ≤ 1
≤′-step (≤′-step ≤′-refl) : 0 ≤ 2
...
≤′-refl : 1 ≤ 1
≤′-step ≤′-refl : 1 ≤ 2
≤′-step (≤′-step ≤′-refl) : 1 ≤ 3
...
≤′-refl : 2 ≤ 2
≤′-step ≤′-refl : 2 ≤ 3
≤′-step (≤′-step ≤′-refl) : 2 ≤ 4
...
...
```

As with `ℕ`

and `ℕ₂`

,

- the structure of the
`m ≤ n`

and`m ≤′ n`

set elements are different, - different representations are good for different tasks.

All code on this slide is valid.

Original definition:

```
data _≤_ : ℕ → ℕ → Set where
z≤n : {n : ℕ} → zero ≤ n
s≤s : {m : ℕ} → {n : ℕ} → m ≤ n → suc m ≤ suc n
```

The arrows between typed variables are not needed (also in case of round parenthesis):

```
data _≤_ : ℕ → ℕ → Set where
z≤n : {n : ℕ} → zero ≤ n
s≤s : {m : ℕ} {n : ℕ} → m ≤ n → suc m ≤ suc n
```

Typed variables with the same type can be merged (also in case of round parenthesis):

```
data _≤_ : ℕ → ℕ → Set where
z≤n : {n : ℕ} → zero ≤ n
s≤s : {m n : ℕ} → m ≤ n → suc m ≤ suc n
```

Inferable expressions can be replaced by an underscore:

```
data _≤_ : ℕ → ℕ → Set where
z≤n : {n : _} → zero ≤ n
s≤s : {m n : _} → m ≤ n → suc m ≤ suc n
```

Variables with inferred types can be introduced by `∀`

:

```
data _≤_ : ℕ → ℕ → Set where
z≤n : ∀ {n} → zero ≤ n
s≤s : ∀ {m n} → m ≤ n → suc m ≤ suc n
```

`_+_≡_`

: Addition predicateWe wish to give a definition that yields an infinite set of true propositions:

```
0 + 0 ≡ 0, 1 + 0 ≡ 1, 2 + 0 ≡ 2, ...
0 + 1 ≡ 1, 1 + 1 ≡ 2, 2 + 1 ≡ 3, ...
0 + 2 ≡ 2, 1 + 2 ≡ 3, 2 + 2 ≡ 4, ...
...
```

The outline of the solution:

```
(n : ℕ) zero + n ≡ n -- yields the first column of judgements
(m : ℕ) (n : ℕ) m + n ≡ k → suc m + n ≡ suc k -- yields the successive columns of judgements
```

Technical details of the solution (nothing new but better to repeat!):

We define the

*set*`n + m ≡ k`

for each`n : ℕ`

,`m : ℕ`

and`k : ℕ`

.

(`2 + 2 ≡ 5`

is a valid set too.)The set

`n + m ≡ k`

will be non-empty iff`n`

+`m`

=`k`

.

(`2 + 2 ≡ 4`

is non-empty,`2 + 2 ≡ 5`

is empty.)

`_+_≡_`

`_+_≡_`

is an indexed set with three natural number indices and two constructors:*

data _+_≡_ : ℕ → ℕ → ℕ → Set where znn : ∀ {n} → zero + n ≡ n sns : ∀ {m n k} → m + n ≡ k → suc m + n ≡ suc k

that yields the following judgements:

```
znn : 0 + 0 ≡ 0
znn : 0 + 1 ≡ 1
znn : 0 + 2 ≡ 2
...
sns znn : 1 + 0 ≡ 1
sns znn : 1 + 1 ≡ 2
sns znn : 1 + 2 ≡ 3
...
sns (sns znn) : 2 + 0 ≡ 2
sns (sns znn) : 2 + 1 ≡ 3
sns (sns znn) : 2 + 2 ≡ 4
...
...
```

Note that the underscores in `_+_≡_`

denote the space for the operands (i.e. mixfix notation).

*: That is the same as follows:

```
data _+_≡_ : ℕ → ℕ → ℕ → Set where
znn : {n : ℕ} → zero + n ≡ n
sns : {m : ℕ} → {n : ℕ} → {k : ℕ} → m + n ≡ k → suc m + n ≡ suc k
```

Prove that 5 + 5 = 10.

Prove that 2 + 2 ≠ 5.

Define

`_⊓_≡_ : ℕ → ℕ → ℕ → Set`

such that`m ⊓ n ≡ k`

iff`k`

is the minimum of`m`

and`n`

.- Prove that both
`3 ⊓ 5 ≡ 3`

and`5 ⊓ 3 ≡ 3`

are non-empty. - Prove that
`3 ⊓ 5 ≡ 5`

is empty.

- Prove that both
Define

`_⊔_≡_ : ℕ → ℕ → ℕ → Set`

such that`m ⊔ n ≡ k`

iff`k`

is the maximum of`m`

and`n`

.- Prove that
`3 ⊔ 5 ≡ 5`

is non-empty. - Prove that
`3 ⊔ 5 ≡ 3`

is empty.

- Prove that

Consider another definition of the `_≤_`

type:

data _≤″_ : ℕ → ℕ → Set where ≤+ : ∀ {m n k} → m + n ≡ k → m ≤″ k

that yields the following:

```
≤+ znn : 0 ≤″ 0
≤+ znn : 0 ≤″ 1
≤+ znn : 0 ≤″ 2
...
≤+ (sns znn) : 1 ≤″ 1
≤+ (sns znn) : 1 ≤″ 2
≤+ (sns znn) : 1 ≤″ 3
...
≤+ (sns (sns znn)) : 2 ≤″ 2
≤+ (sns (sns znn)) : 2 ≤″ 3
≤+ (sns (sns znn)) : 2 ≤″ 4
...
...
```

Notes:

- This representation of less-than-or-equal is similar to
`_≤_`

. - If we were to wrote
`≤+ : ∀ {m n k} → m + n ≡ k → n ≤″ k`

(that is, use`n`

instead of`m`

at the end) we would get a representation of less-than-or-equal similar to`_≤′_`

on the previous slides.

Define

`_isDoubleOf_ : ℕ → ℕ → Set`

atop`_+_≡_`

.- Prove that
`8 isDoubleOf 4`

is non-empty. - Prove that
`9 isDoubleOf 4`

is empty.

- Prove that
Define

`_*_≡_ : ℕ → ℕ → ℕ → Set`

with the help of`_+_≡_`

.- Prove that
`3 * 3 ≡ 9`

is non-empty. - Prove that
`3 * 3 ≡ 8`

is empty.

- Prove that
Define

`_≈_ : ℕ → ℕ⁺ → Set`

that represents the (canonical) isomorphism between`ℕ`

and`ℕ⁺`

.*- Prove that
`5 ≈ double+1 (double one)`

is non-empty. - Prove that
`4 ≈ double+1 (double one)`

is empty.

- Prove that

*Hint.* Recall the definition of `ℕ⁺`

, `one`

, `double`

, `double+1`

:

data ℕ⁺ : Set where one : ℕ⁺ double : ℕ⁺ → ℕ⁺ double+1 : ℕ⁺ → ℕ⁺

*: There are many isomorphisms between `ℕ`

and `ℕ⁺`

, here we are referring to the most natural one.