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 ⊥.
The false proposition has no proofs (it 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:
⊤ × ⊤⊤ × ⊥⊥ × ⊥⊤ ⊎ ⊤⊤ ⊎ ⊥⊥ ⊎ ⊥⊥ ⊎ ⊤ ⊎ ⊤ × (⊥ ⊎ ⊥) ⊎ ⊤Example:
⊤×⊤ : ⊤ × ⊤ ⊤×⊤ = tt , tt
We represent implication, negation, universal and existential quantification later.
_⊎_ represents constructive disjunction, we represent classical disjunction later and compare them.
_≤_: 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 statements
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
...
...which 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
z≤n constructor yields the first column of statements.s≤s constructor yields the successive columns of statements.1 ≤ 0 is also a valid expression which denotes an empty set.We can prove that a set is non-empty by giving an element
(remember the syntax of constant definition):
0≤1 : 1 ≤ 10 0≤1 = s≤s z≤n
Exercise: Prove that 3 ≤ 7!
How can we prove that a set like 7 ≤ 3 is empty?
7 ≤ 3 would be 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.6 ≤ 2 would be 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.5 ≤ 1 would be 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 can this chain of inference be given in Agda:*
7≰3 : 7 ≤ 3 → ⊥ 7≰3 (s≤s (s≤s (s≤s ())))
() denotes a value in a trivially empty set.Exercise: prove that 4 ≤ 2 is empty!
We can use an emptiness proof in another emptiness proof:
8≰4 : 8 ≤ 4 → ⊥ 8≰4 (s≤s x) = 7≰3 x
x is an arbitrary variable name.Question: Guess what kind of code can be generated from emptiness proofs!
*7 ≤ 3 → ⊥ denotes a function from 7 ≤ 3 to ⊥ so we prove that 7 ≤ 3 is empty by giving a function which maps 7 ≤ 3 to a trivially empty set.
During the function definition we show that 7 ≤ 3 has no element so the function is defined.
We discuss functions in detail later.
_isDoubleOf_ : ℕ → ℕ → Set such that m isDoubleOf n is non-empty iff m is the double of n!
8 isDoubleOf 4 is non-empty!9 isDoubleOf 4 is empty!Odd : ℕ → Set such that odd n is non-empty iff n is odd!
Odd 9 is non-empty!Odd 8 is empty!Even : ℕ → Set and Odd : ℕ → Set mutually!_≡_ : ℕ → ℕ → Set!_≠_ : ℕ → ℕ → Set!
data _≤′_ : ℕ → ℕ → Set where
≤′-refl : {m : ℕ} → m ≤′ m
≤′-step : {m : ℕ} → {n : ℕ} → m ≤′ n → m ≤′ suc n
infix 4 _≤′_
yields
≤′-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 ℕ₂,
m ≤ n and m ≤′ n set elements are differentAll 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 nThe 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 nTyped variables with the same type can be contracted (also in case of round parenthesis):
data _≤_ : ℕ → ℕ → Set where
z≤n : {n : ℕ} → zero ≤ n
s≤s : {m n : ℕ} → m ≤ n → suc m ≤ suc nInferable expressions can be replaced by an underscore:
data _≤_ : ℕ → ℕ → Set where
z≤n : {n : _} → zero ≤ n
s≤s : {m n : _} → m ≤ n → suc m ≤ suc nVariables 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 which yields the 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 statements
(m : ℕ) (n : ℕ) m + n ≡ k → suc m + n ≡ suc k -- yields the successive columns of statementsTechnical details of the solution
(nothing new but better to repeat):
n + m ≡ k for each n : ℕ, m : ℕ and k : ℕ.2 + 2 ≡ 5 is a valid set too.)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 with two constructors:*
data _+_≡_ : ℕ → ℕ → ℕ → Set where
znn : ∀ {n} → zero + n ≡ n
sns : ∀ {m n k} → m + n ≡ k → suc m + n ≡ suc k
which yields the statements
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
...
...Notes
_+_≡_ denote the space for the operands (mixfix notation).*this is the same as
data _+_≡_ : ℕ → ℕ → ℕ → Set where
znn : {n : ℕ} → zero + n ≡ n
sns : {m : ℕ} → {n : ℕ} → m + n ≡ k → suc m + n ≡ suc k_⊓_≡_ : ℕ → ℕ → ℕ → Set such that n ⊓ m ≡ k iff k is the minimum of n and m!
3 ⊓ 5 ≡ 3 is non-empty!3 ⊓ 5 ≡ 5 is empty!_⊔_≡_ : ℕ → ℕ → ℕ → Set such that n ⊔ m ≡ k iff k is the maximum of n and m!
3 ⊔ 5 ≡ 5 is non-empty!3 ⊔ 5 ≡ 3 is empty!Another definition of _≤_:
data _≤″_ : ℕ → ℕ → Set where
≤+ : ∀ {m n k} → m + n ≡ k → m ≤″ k
which yields
≤+ 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
_≤_.≤+ : ∀ {m n k} → m + n ≡ k → n ≤″ k (use n instead of m at the end) we get a representation of less-than-or-equal similar to _≤′_ on the previous slides._isDoubleOf_ : ℕ → ℕ → Set on top of _+_≡_!
8 isDoubleOf 4 is non-empty!9 isDoubleOf 4 is empty!_*_≡_ : ℕ → ℕ → Set with the help of _+_≡_!
3 * 3 ≡ 9 is non-empty!3 * 3 ≡ 8 is empty!_≈_ : ℕ → ℕ⁺ → Set which represents the (canonical) isomorphism between the non-zero elements of ℕ and ℕ⁺!*
5 ≈ double+1 (double one) is non-empty!4 ≈ double+1 (double one) is empty!*There are lots of isomorphisms between ℕ and ℕ⁺, we mean here the most natural one.