Import list


module Sets.Propositions where

open import Data.Nat using (ℕ; zero; suc)

Proofs as data

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:


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

infixr 1 _⊎_

Exercises

Construct one proof for each proposition if possible:

For example:


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

Remarks

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 predicate

We 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:

Proving non-emptiness

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

Exercise

Prove that 3 ≤ 7.

Proving emptiness

How could we prove that a set like 7 ≤ 3 is empty?

  1. If 7 ≤ 3 was non-empty, all its elements would look like s≤s x where x : 6 ≤ 2.

  2. If 6 ≤ 2 was non-empty, all its elements would look like s≤s x where x : 5 ≤ 1.

  3. If 5 ≤ 1 was non-empty, all its elements would look like s≤s x where x : 4 ≤ 0.

  4. 4 ≤ 0 is empty.

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.

Exercise

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.

Exercise

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.

Exercises

  1. 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.

  2. Define an indexed set Odd : ℕ → Set such that Odd n is non-empty iff n is odd.

  3. Define Even : ℕ → Set and Odd : ℕ → Set mutually.

  4. Define equality _≡_ : ℕ → ℕ → Set.

  5. Define non-equality _≠_ : ℕ → ℕ → Set.

Alternative representation of _≤_

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 ℕ₂,

Syntactic abbreviations

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 predicate

We 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!):

Definition of _+_≡_

_+_≡_ 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

Exercises

  1. Prove that 5 + 5 = 10.

  2. Prove that 2 + 2 ≠ 5.

  3. Define _⊓_≡_ : ℕ → ℕ → ℕ → Set such that m ⊓ n ≡ k iff k is the minimum of m and n.

  4. Define _⊔_≡_ : ℕ → ℕ → ℕ → Set such that m ⊔ n ≡ k iff k is the maximum of m and n.

Reusing definitions

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:

Exercises

  1. Define _isDoubleOf_ : ℕ → ℕ → Set atop _+_≡_.

  2. Define _*_≡_ : ℕ → ℕ → ℕ → Set with the help of _+_≡_.

  3. Define _≈_ : ℕ → ℕ⁺ → Set that represents the (canonical) isomorphism between ℕ and ℕ⁺.*

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.