Natural numbers, Equational Reasoning, UF-style Proofs By Contradiction
Quick Recap:
The last post delved into basic inductive types, introduced the univalent notion of equality, and proofs by case analysis. The first post can be found here.
As always, our primary sources are:
- Introduction to Univalent Foundations of Mathematics with Agda by Martín Hötzel Escardó
- Software Foundations by Pierce et al.
- Verified Functional Programming in Agda by Aaron Stump
Note, I make no claim that any proof given is the best one possible regardless of your criteria of best.
Now to Begin
To begin we declare the same options as before and our define our module.
{-# OPTIONS --without-K --exact-split --safe #-}
module Naturals where
We import our previous work.
open import Utilities public
open import Booleans public
{-
open import Basics
-}
I reorganized the last post’s contents into two modules: one dealing with Booleans and another that contains the foundational constructs we have used thus far in UF-style reasoning. Those two modules are available with this text here.
The last post in this series is available as a literate Agda file here. You can optionally comment out the lines importing Utilities and Booleans and instead import the last blog post by un-commenting open import Basics. I just thought refactoring as I went was the polite thing to do for my future self.
The Naturals
We finally introduce the natural numbers.
data ℕ : Set where
Z : ℕ
S : ℕ → ℕ
_+_ _×_ : ℕ → ℕ → ℕ
m + Z = m
m + S n = S (m + n)
m × Z = Z
m × S n = m + m × n
infixl 20 _+_
infixr 21 _×_
{-# BUILTIN NATURAL ℕ #-}
Like we did with the our Boolean type, we hint to Agda that our newly-defined type is equivalent to Agda’s built-in notion of natural numbers. Unlike our Boolean type 𝔹, we did not need to instruct Agda which constructor corresponds to the built-in notion of zero and successor. Agda can determine the correspondence on its own by looking at the distinct type signatures of our constructors Z and S. The built-in notion of natural numbers allow us to use numerals denote elements of ℕ. Writing 5 instead of ’S (S (S (S (S Z))))` is just too convenient.
For those unfamiliar with Peano arithmetic, Wikipedia is sufficient for a quick introduction. There are builds on the Open Logic Project which include Peano arithmetic if you want a free resource that goes more in-depth.
The induction, recursion and iteration principles for ℕ
ℕ-induction : (A : ℕ → Set ℓ)
→ A Z
→ ((n : ℕ) → A n → A (S n))
→ (n : ℕ) → A n
ℕ-induction A a₀ f Z = a₀
ℕ-induction A a₀ f (S n) = f n ih
where
ih = ℕ-induction A a₀ f n
ih is so-named because it represents what would be our induction hypothesis in a classical proof by induction over natural numbers.
ℕ-recursion : (B : Set ℓ)
→ B
→ (ℕ → B → B)
→ ℕ → B
ℕ-recursion B = ℕ-induction λ _ → B
The non-dependent version is how we would classically construct a function from the naturals via primitive recursion.
There is also less general iteratorℕ-iterator : (B : Set ℓ)
→ B
→ (B → B)
→ ℕ → B
ℕ-iterator B b₀ f = ℕ-recursion B b₀ λ _ → f
where if h is defined via ℕ-iterator then h n is equivalent to applying n times the function f to initial value b₀.
_+_ and _×_ directly via iteration instead of pattern matching and show that the two definitions coincide.
_+'_ _×'_ : ℕ → ℕ → ℕ _+'_ = λ m → ℕ-iterator ℕ m S _×'_ = λ m → ℕ-iterator ℕ Z (m +_)
Agda lets us partially apply mix-fix operators which is nice of it.
We aren’t quite in the position to prove the equivalence of our two different definitions of addition and multiplication but will be soon.
“Less-than-or-equals” and multiple definitions.
Consider the “less than or equals relationship”. We could define it as a Boolean-valued function and that does indeed work._≤?_ : ℕ → ℕ → 𝔹 Z ≤? _ = tt S _ ≤? Z = ff S m ≤? S n = m ≤? nBut why have proposition as types if we don’t exploit them? Here is a similar definition that uses types instead of Booleans as return values.
_≤_ _≥_ : ℕ → ℕ → Set Z ≤ _ = 𝟙 S _ ≤ Z = 𝟘 S m ≤ S n = m ≤ n m ≥ n = n ≤ n
Unless we assumed a contradiction at some early point, we should never be able to construct a proof that 1 ≤ 0 because then we would have constructed a term which inhabits the empty type 𝟘. It should just not be possible to write such a proof/program without Agda yelling at us, and that’s a good thing.
We can prove that our two concepts of “less-than-or-equal-to” (“lte” for brevity) coincide.
≤-implies-≤? : (m n : ℕ) → (m ≤ n) → (m ≤? n) ≡ tt ≤-implies-≤? Z _ _ = refl _ ≤-implies-≤? (S m) (S n) p = ≤-implies-≤? m n p ≤?-implies-≤ : (m n : ℕ) → (m ≤? n) ≡ tt → m ≤ n ≤?-implies-≤ Z Z _ = * ≤?-implies-≤ Z (S _) _ = * ≤?-implies-≤ (S m) (S n) p = ≤?-implies-≤ m n p
For any given mathematical definition there is usually too many equivalent definitions. The following is an adaptation of “lte” as defined in the Idris prelude and a proof that our new definition implies our old definition and vice-versa.
data _≤'_ : ℕ → ℕ → Set where
LTE-Z : {n : ℕ} → Z ≤' n
LTE-S : {m n : ℕ} → m ≤' n → S m ≤' S n
≤-implies-≤' : (m n : ℕ) → m ≤ n → m ≤' n
≤-implies-≤' Z n _ = LTE-Z
≤-implies-≤' (S m) (S n) p = LTE-S (≤-implies-≤' m n p)
Notice Agda allows takes care of the absurd case S m ≤ Z for us. To prove the other way we first need a small helper lemma.
LTE-S-injective : {m n : ℕ} → S m ≤' S n → m ≤' n
LTE-S-injective (LTE-S p) = p
≤'-implies-≤ : (m n : ℕ) → m ≤' n → m ≤ n
≤'-implies-≤ Z n _ = *
≤'-implies-≤ (S m) (S n) p = ≤'-implies-≤ m n (LTE-S-injective p)
Now that we are starting to prove more interesting theorems, we will need to be able to express richer logical statements. We have logical truth with 𝟙 and falsehood with 𝟘. Dependent functions are how we express statements like “for all”, and non-dependent functions are how we express “implies”, and we defined the function ¬_ for logical negation.
But we are still missing a few like bi-implication (bi-conditional/if-and-only-if). ≤-implies-≤? is a formal proof of the statement “for all m,n in ℕ, m ≤? n equals tt if m ≤ n and ≤?-implies-? is a formal proof of the converse statement”for all m,n in ℕ, n ≤ n if m ≤? n is equal to tt." We can say informally say that we have proof m ≤ n if and only if m ≤? n is equal to tt. However, we don’t have a proof object of the formal statement that describes “m ≤? n' is equal tott` if and only if ‘m ≤ n’”.
Sigma Types
To say “if and only if” (which we’ll just write as “iff”) , we need to first be able to say “and”. We already see how the connective implication (A → B is “if A then B”) is the non-dependent case of universal quantification ((x : A) → B x is “forall x in A, B x holds”). Conjunction (“and”) will be the non-dependent case of existential quantification (“there exists”).
Σ types which can be implemented in Agda with dependent records.
record Σ {X : Set ℓ} (Y : X → Set ℓ') : Set (ℓ ⊔ ℓ') where
constructor
_,_
field
x : X
y : Y x
infixr 4 _,_
We define the projections from a pair.
fst : {X : Set ℓ} {Y : X → Set ℓ'} → Σ Y → X
fst (x , _) = x
snd : {X : Set ℓ} {Y : X → Set ℓ'} → (z : Σ Y) → Y (fst z)
snd (_ , y) = y
We read Σ Y as corresponding to the first-order logical sentence ∃ x ∈ X , Y x. The type of Y contains the term X so we don’t strictly need to add X as an explicit parameter to Σ. An element x , y of Σ Y contains a witness x along with proof y : Y x.
Suppose, the type family is constant, then the pair x , y is a pair where x is a proof of X, and y is a proof of Y, and thus x , y can naturally be thought of as a proof of X and Y. We write conjunction with ∧ and will define it as such.
Σ that makes the witness type explicit.
-Σ : (X : Set ℓ) → (Y : X → Set ℓ') → Set (ℓ ⊔ ℓ') -Σ X Y = Σ Y syntax -Σ X (λ x → Y) = Σ[ x ∈ X ] Y _∧_ : Set ℓ → Set ℓ' → Set (ℓ ⊔ ℓ') X ∧ Y = Σ[ x ∈ X ] Y infixr 2 _∧_
I wish we could use : instead of ∈ but : is reserved. You can use a Unicode character which is virtually, if not entirely, indistinguishable from : but not reserved like ː, ꞉, or even ˸ but that introduces other complications which I personally feel are not worth the benefit.
Σ elimination rule or currying. The induction principle turns a dependent function on the single variable (x , y) : Σ Y into a two variable function from the “simpler” types x : X, y : Y x
Σ-induction : {X : Set ℓ} {Y : X → Set ℓ'} {A : Σ Y → Set ℓ''}
→ ((x : X) (y : Y x) → A (x , y))
→ ( z : Σ Y) → A z
Σ-induction g (x , y) = g x y
There is also an inverse procedure which is appropriately called uncurrying. If you have fooled around with OCaml you might have experienced a lot of implicit currying and uncurrying when writing partial applications of functions whose domains are tuples.
uncurry : {X : Set ℓ} {Y : X → Set ℓ'} {A : Σ Y → Set ℓ''}
→ ((z : Σ Y) → A z)
→ (x : X) (y : Y x) → A (x , y)
uncurry g x y = g (x , y)
We now have enough to define bi-implication (“if-and-only-if” statements) and package our two proofs about our representations of even “lte” into one formal statement.
_⇔_ : Set ℓ → Set ℓ' → Set (ℓ ⊔ ℓ') X ⇔ Y = (X → Y) ∧ (Y → X) ≤-iff-≤' : (m n : ℕ) → (m ≤ n) ⇔ (m ≤' n) ≤-iff-≤' m n = ≤-implies-≤' m n , ≤'-implies-≤ m nWe should be clear that
X ⇔ Y is about the weakest way we can say X is equivalent to Y. It is not a very informative relationship in our setting. For example…
unhelpful : ℕ ⇔ 𝟙 unhelpful = (λ _- → *) , λ _ → Z
So bi-implication says nothing about the internal structure of types. All it really says is we know how to construct elements of one type given the other. We know in a constructive sense that if one is inhabited so is the other, and if one is empty then both are.
We have enough to define a third form of the less than or equal relationship._≼_ : ℕ → ℕ → Set m ≼ n = Σ[ o ∈ ℕ ] ((m + o) ≡ n)
But we need some simple results to reason about this type and even to talk about the natural numbers.
Equational Reasoning
We didn’t state the induction principle for equality types in the last post so let’s do that now.
Id-induction : (X : Set ℓ) (A : (x y : X) → x ≡ y → Set ℓ')
→ ((x : X) → A x x (refl x))
→ (x y : X) (p : x ≡ y) → A x y p
Id-induction X A f x .x (refl .x) = f x
Note: To define A x y p everywhere, we only need to define the diagonal A x x (refl x).
𝕁
𝕁 : (X : Set ℓ) (A : (x y : X) → x ≡ y → Set ℓ') → ((x : X) → A x x (refl x)) → (x y : X) (p : x ≡ y) → A x y p 𝕁 = Id-induction
Thankfully, the paper Pattern Matching Without K by Cockx, Devriese and Piessens proves we that pattern matching on refl with the --without-K pragma has the same expressive power as 𝕁.
We need to define substitution via equality. In the UF interpretation of equality, the terms x and y represent points in the type X which we can think of as a space. An element p : x ≡ y then represents a path from x to y in the space X. The specific constructor refl x represents the trivial/constant path from a point to itself. When viewed in this context 𝕁 is an impressive statement: to derive a property on all paths, we need only prove proof of the property holds on the trivial ones.
Then substitution can be thought of as transport along paths.
First define implicit and explicit identity functions, and some certain utilities to recover the end points given a pathp : x ≡ y.
id : {X : Set ℓ} → X → X
id x = x
id' : (X : Set ℓ) → X → X
id' X = id
lhs : {X : Set ℓ} {x y : X} → x ≡ y → X
lhs {ℓ} {X} {x} {y} p = x
rhs : {X : Set ℓ} {x y : X} → x ≡ y → X
rhs {ℓ} {X} {x} {y} p = y
transport : {X : Set ℓ} (A : X → Set ℓ') {x y : X}
→ x ≡ y → A x → A y
transport A (refl x) = id
We could have defined transport via 𝕁.
transport𝕁 : {X : Set ℓ} (A : X → Set ℓ') {x y : X}
→ x ≡ y → A x → A y
transport𝕁 {ℓ} {ℓ'} {X} A {x} {y} = 𝕁 X (λ x' y' _ → A x' → A y') (λ x' → id' (A x')) x y
transport𝕁-agreement : {X : Set ℓ} (A : X → Set ℓ') {x y : X} (p : x ≡ y)
→ transport𝕁 A p ≡ transport A p
transport𝕁-agreement A (refl x) = refl (transport A (refl x))
What can we naturally do reverse paths? We can reverse them, and concatenate them.
_∙_ : {X : Set ℓ } {x y z : X} → x ≡ y → y ≡ z → x ≡ z
p ∙ q = transport (lhs p ≡_) q p
_⁻¹ : {X : Set ℓ} {x y : X} → x ≡ y → y ≡ x
p ⁻¹ = transport (_≡ lhs p) p (refl (lhs p))
The above definition of _∙_ uses q to transport to transport the proposition A y to A z where A = λ t → (x ≡ t).
p to transport but the definition feels slightly less natural since we technically have transport along p ⁻¹.
_∙'_ : {X : Set ℓ} {x y z : X} → x ≡ y → y ≡ z → x ≡ z
p ∙' q = transport (_≡ rhs q) (p ⁻¹) q
∙-agreement : {X : Set ℓ} {x y z : X} (p : x ≡ y) (q : y ≡ z)
→ (p ∙' q) ≡ (p ∙ q)
∙-agreement (refl x) (refl .x) = refl _
We almost have enough to start proving non-trivial properties about the natural numbers. transport will roughly correspond to rewriting terms, while _∙_ and _⁻¹ will be the underlying means we use to manipulate statements of equality.
ap : {X : Set ℓ} {Y : Set ℓ'} (f : X → Y) {x x' : X}
→ x ≡ x' → f x ≡ f x'
ap f {x} {x'} p = transport (λ - → f x ≡ f -) p (refl (f x))
_≡⟨_⟩_ : {X : Set ℓ} (x : X) {y z : X}
→ x ≡ y → y ≡ z → x ≡ z
x ≡⟨ p ⟩ q = p ∙ q
infixr 3 _≡⟨_⟩_
The postfix notation for refl will often be useful equation reasoning
_∎ : {X : Set ℓ} (x : X) → x ≡ x
x ∎ = refl x
Reasoning About The Naturals.
We have to be cognizant of our definitions. A statement can be trivial with respect to one definition and difficult with another.
+-Z-r : (n : ℕ) → (n + Z) ≡ n
+-Z-r _ = refl _
+-Z-l : (n : ℕ) → (Z + n) ≡ n
+-Z-l Z = refl _
+-Z-l (S n) =
(Z + S n) ≡⟨ refl _ ⟩
S (Z + n) ≡⟨ ap S ih ⟩
(S n ∎)
where
ih : (Z + n) ≡ n
ih = +-Z-l n
+-Z-l isn’t difficult to prove, but it does not immediately follows from the definition of addition. +-Z-l would have been trivial, and +-Z-r would have been the more complicated case if we defined m + n by induction on the left argument m instead of the second argument n. A good heuristic to use i that our proofs by induction should mirror the induction structure of our definitions. So if we want to prove some property of m + n or m × n, we should split on n.
+-S-r : (m n : ℕ) → (m + S n) ≡ S (m + n) +-S-r _ _ = refl _ +-S-l : (m n : ℕ) → (S m + n) ≡ S (m + n) +-S-l m Z = refl _ +-S-l m (S n) = ap S (+-S-l m n)The predecessor function is sometimes useful.
pred : ℕ → ℕ
pred Z = Z
pred (S n) = n
S-inj : {m n : ℕ} → S m ≡ S n → m ≡ n
S-inj {m} {n} p = ap pred p
Proofs Involving Negation
We can’t always rely on Agda’s pattern matching to rule out impossible cases. If we are left with an impossible pattern then we try to construct an element of the empty type 𝟘. After constructing such an element, it is trivial to prove our conclusion using “ex falso quodlibet”. In our notes we write !𝟘 instead of Latin.
_≢_ : {X : Set ℓ} → X → X → Set ℓ
x ≢ y = ¬ (x ≡ y)
Proving two terms aren’t equal usually involves a function that separates the two terms. But we need a starting point; we need a foundational inequality. If we could prove 𝟙 ≢ 𝟘, then in general we can prove x ≢ y by finding a function that maps x to 𝟙 and y to 𝟘.
transport id' (Set ℓ) has type X ≡ Y → X → Y after normalizing. If we set Y to be 𝟘, then this gives us a way to construct ¬ X if we have an identification X ≡ 𝟘.
𝟙-≢-𝟘 : 𝟙 ≢ 𝟘 𝟙-≢-𝟘 p = transport (id' Set) p *and in general.
≡-to-fun : {X Y : Set ℓ} → X ≡ Y → X → Y
≡-to-fun {ℓ} = transport (id' (Set ℓ))
The distinction between 𝟙 and 𝟘 allows us to partition a type X with a function f : X → Set by mapping elements to either 𝟘 or 𝟙.
S-≢-Z : (n : ℕ) → S n ≢ Z
S-≢-Z n p = 𝟙-≢-𝟘 (ap f p)
where
f : ℕ → Set
f Z = 𝟘
f (S n) = 𝟙
When we dealt with Booleans we relied on Agda eliminating the absurd cases cases for us but we no longer need to rely upon Agda to eliminate such cases nor are we stuck when Agda isn’t able to eliminate those cases.
≢-sym : {X : Set ℓ} {x y : X} → x ≢ y → y ≢ x
≢-sym {ℓ} {X} {x} {y} u p = u (p ⁻¹ )
tt-≢-ff : tt ≢ ff
tt-≢-ff p = 𝟙-≢-𝟘 (ap f p)
where
f : 𝔹 → Set
f tt = 𝟙
f ff = 𝟘
~-≢ : (b : 𝔹) → (~ b) ≢ b
~-≢ tt = ≢-sym tt-≢-ff
~-≢ ff = tt-≢-ff
xor-anti' : (b c : 𝔹) → (b xor c) ≡ tt → b ≢ c
xor-anti' tt ff _ = tt-≢-ff
xor-anti' ff tt _ = ≢-sym tt-≢-ff
We can return to our definition of “lte” based on Σ types.
≼-implies-≤ : (m n : ℕ) → m ≼ n → m ≤ n
≼-implies-≤ Z _ _ = *
≼-implies-≤ (S m) Z (k , p) = S-≢-Z (m + k)
(S (m + k) ≡⟨ +-S-l m k ⁻¹ ⟩
S m + k ≡⟨ p ⟩
(Z ∎))
≼-implies-≤ (S m) (S n) (k , p) = ≼-implies-≤ m n (k , ap pred q)
where
q : S (m + k) ≡ S n
q = S (m + k) ≡⟨ +-S-l m k ⁻¹ ⟩
S m + k ≡⟨ p ⟩
(S n ∎)
≤-implies-≼ : (m n : ℕ) → m ≤ n → m ≼ n
≤-implies-≼ Z n p = n , +-Z-l n
≤-implies-≼ (S m) (S n) p = k , (S m + k ≡⟨ +-S-l m k ⟩
S (m + k) ≡⟨ ap S q ⟩
(S n ∎))
where
ih : m ≼ n
ih = ≤-implies-≼ m n p
k : ℕ
k = fst ih
q : (m + k) ≡ n
q = snd ih
≤-iff-≼ : (m n : ℕ) → (m ≤ n) ⇔ (m ≼ n)
≤-iff-≼ m n = ≤-implies-≼ m n , ≼-implies-≤ m n
Verifying Middle School Knowledge
We are at a point now that we can verify the algebraic properties of the natural numbers we learned in grade school. We start with the commutativity and associativity of natural numbers.+-assoc : (m n o : ℕ) → (m + (n + o)) ≡ (m + n + o) +-assoc m n Z = refl _ +-assoc m n (S o) = m + (n + S o) ≡⟨ ap S (+-assoc m n o) ⟩ ((m + n + S o) ∎) +-comm : (m n : ℕ) → (m + n) ≡ (n + m) +-comm Z n = +-Z-l n +-comm (S m) n = S m + n ≡⟨ +-S-l m n ⟩ S (m + n) ≡⟨ ap S (+-comm m n) ⟩ S (n + m) ≡⟨ refl _ ⟩ ((n + S m) ∎)Establish the basic properties of multiplication including commutativity.
×-Z-r : (n : ℕ) → (n × Z) ≡ Z
×-Z-r _ = refl _
×-Z-l : (n : ℕ) → (Z × n) ≡ Z
×-Z-l Z = refl _
×-Z-l (S n) =
Z × S n ≡⟨ refl _ ⟩
Z + Z × n ≡⟨ +-Z-l (Z × n) ⟩
Z × n ≡⟨ ×-Z-l n ⟩
(Z ∎)
×-S-l : (m n : ℕ) → (S m × n) ≡ (n + m × n)
×-S-l m Z = refl _
×-S-l m (S n) =
S m × S n ≡⟨ refl _ ⟩
S m + S m × n ≡⟨ ap (λ k → S m + k) (×-S-l m n) ⟩
S m + (n + m × n) ≡⟨ +-assoc (S m) n (m × n) ⟩
S m + n + m × n ≡⟨ ap (λ k → k + m × n) q ⟩
S n + m + m × n ≡⟨ +-assoc (S n) m (m × n) ⁻¹ ⟩
S n + (m + m × n) ≡⟨ refl _ ⟩
((S n + m × S n) ∎)
where
q : (S m + n) ≡ (S n + m)
q = S m + n ≡⟨ +-S-l m n ⟩
S (m + n) ≡⟨ ap S (+-comm m n) ⟩
S (n + m) ≡⟨ +-S-l n m ⁻¹ ⟩
((S n + m) ∎)
×-1-r : (k : ℕ) → (k × 1) ≡ k
×-1-r _ = refl _
×-1-l : (k : ℕ) → 1 × k ≡ k
×-1-l Z = refl _
×-1-l (S k) = 1 + 1 × k ≡⟨ +-comm 1 (1 × k) ⟩
1 × k + 1 ≡⟨ ap S (×-1-l k) ⟩
(S k ∎)
×-comm : (m n : ℕ) → (m × n) ≡ (n × m)
×-comm Z n = ×-Z-l n
×-comm (S m) n = S m × n ≡⟨ ×-S-l m n ⟩
n + m × n ≡⟨ ap (λ k → n + k) (×-comm m n) ⟩
n + n × m ≡⟨ refl _ ⟩
((n × S m) ∎)
The distributive properties, associativity of multiplication and cancellation of addition.
×-l-dist-over-+ : (k m n : ℕ) → (k × (m + n)) ≡ (k × m + k × n)
×-l-dist-over-+ k m Z = refl _
×-l-dist-over-+ k m (S n) =
k × (m + S n) ≡⟨ refl _ ⟩
k + k × (m + n) ≡⟨ ap (λ l → k + l ) (×-l-dist-over-+ k m n) ⟩
k + (k × m + k × n) ≡⟨ +-assoc k (k × m) (k × n) ⟩
k + k × m + k × n ≡⟨ ap (λ l → l + k × n) (+-comm k (k × m)) ⟩
k × m + k + k × n ≡⟨ +-assoc (k × m) k (k × n) ⁻¹ ⟩
k × m + (k + k × n) ≡⟨ refl _ ⟩
((k × m + k × S n) ∎)
×-r-dist-over-+ : (k m n : ℕ) → ((m + n) × k) ≡ (m × k + n × k)
×-r-dist-over-+ k m n =
(m + n) × k ≡⟨ ×-comm (m + n) k ⟩
k × (m + n) ≡⟨ ×-l-dist-over-+ k m n ⟩
k × m + k × n ≡⟨ ap (λ l → l + k × n) (×-comm k m) ⟩
m × k + k × n ≡⟨ ap (λ l → m × k + l) (×-comm k n) ⟩
((m × k + n × k) ∎)
×-assoc : (m n o : ℕ) → ((m × n) × o) ≡ (m × n × o)
×-assoc m n Z = refl _
×-assoc m n (S o) =
(m × n) × S o ≡⟨ refl _ ⟩
m × n + (m × n) × o ≡⟨ ap (λ k → m × n + k) (×-assoc m n o) ⟩
m × n + m × n × o ≡⟨ ×-l-dist-over-+ m n (n × o) ⁻¹ ⟩
m × (n + n × o) ≡⟨ refl _ ⟩
((m × n × S o) ∎)
+-r-cancel : (k m n : ℕ) → (m + k) ≡ (n + k) → m ≡ n
+-r-cancel Z m n p = p
+-r-cancel (S k) m n p = +-r-cancel k m n (S-inj p)
+-l-cancel : (k m n : ℕ) → (k + m) ≡ (k + n) → m ≡ n
+-l-cancel k m n p = +-r-cancel k m n
(m + k ≡⟨ +-comm m k ⟩
k + m ≡⟨ p ⟩
k + n ≡⟨ +-comm k n ⟩
((n + k) ∎))
Disjunction : our final connective.
We have almost completed the Curry Howard correspondence. The only logical construct we are missing is disjunction (“or”). It’s time to introduce disjunction and its associated induction/recursion principles.
data _∨_ (X : Set ℓ) (Y : Set ℓ') : Set (ℓ ⊔ ℓ') where
inl : X → X ∨ Y
inr : Y → X ∨ Y
infixr 1 _∨_
∨-induction : {X : Set ℓ} {Y : Set ℓ'} (A : X ∨ Y → Set ℓ'')
→ ((x : X) → A (inl x))
→ ((y : Y) → A (inr y))
→ (z : X ∨ Y) → A z
∨-induction A f g (inl x) = f x
∨-induction A f g (inr y) = g y
∨-recursion : {X : Set ℓ} {Y : Set ℓ'} (B : Set ℓ'')
→ (X → B) → (Y → B)
→ X ∨ Y → B
∨-recursion B f g (inl x) = f x
∨-recursion B f g (inr y) = g y
We are in a constructive setting so we are not able to prove everything we could in classical logic. Certain directions of De Morgan’s laws are not provable. We will delve deeper into the difference between constructive and classical logic later. But for now, we still have some classical elimination rules.
∨-l-elim : {X : Set ℓ} {Y : Set ℓ'}
→ (X ∨ Y) → (¬ X) → Y
∨-l-elim (inl x) u = !𝟘 (u x)
∨-l-elim (inr y) u = y
∨-r-elim : {X : Set ℓ} {Y : Set ℓ'}
→ (X ∨ Y) → (¬ Y) → X
∨-r-elim (inl x) u = x
∨-r-elim (inr y) u = !𝟘 (u y)
And we define some natural utilities.
_→∨_ : {X X' : Set ℓ} {Y Y' : Set ℓ'} → (X → X') → (Y → Y') → (X ∨ Y) → (X' ∨ Y')
(f →∨ g) (inl x) = inl (f x)
(f →∨ g) (inr y) = inr (g y)
_→∧_ : {X X' : Set ℓ} {Y Y' : Set ℓ'} → (X → X') → (Y → Y') → (X ∧ Y) → (X' ∧ Y')
(f →∧ g) (x , y) = f x , g y
More Properties of Natural Numbers.
We now prove properties we could not prove or express before. If I misuse any terminology, please correct and forgive me. My algebra is a bit rusty.0-only-×-zero-divisor : (m n : ℕ) → (m × n) ≡ Z → (m ≡ Z) ∨ (n ≡ Z)
0-only-×-zero-divisor Z _ _ = inl (refl _)
0-only-×-zero-divisor (S _) Z _ = inr (refl _)
0-only-×-zero-divisor (S m) (S n) p = !𝟘 (S-≢-Z (m + S m × n) q)
where
q : (S (m + S m × n)) ≡ Z
q = S (m + S m × n) ≡⟨ +-S-l m (S m × n) ⁻¹ ⟩
S m + S m × n ≡⟨ p ⟩
(Z ∎)
×-l-cancel : (k m n : ℕ) → (S k × m) ≡ (S k × n) → m ≡ n
×-l-cancel k m Z p = ∨-l-elim (0-only-×-zero-divisor (S k) m p) (S-≢-Z k)
×-l-cancel k Z (S n) p = !𝟘 (S-≢-Z (k + S k × n) q)
where
q : S (k + S k × n) ≡ Z
q = S (k + S k × n) ≡⟨ +-S-l k (S k × n) ⁻¹ ⟩
S k + S k × n ≡⟨ p ⁻¹ ⟩
(Z ∎)
×-l-cancel k (S m) (S n) p = ap S (×-l-cancel k m n (+-l-cancel (S k) (S k × m) (S k × n) p))
×-r-cancel : (k m n : ℕ) → (m × S k) ≡ (n × S k) → m ≡ n
×-r-cancel k m n p = ×-l-cancel k m n q
where
q : (S k × m) ≡ (S k × n)
q = S k × m ≡⟨ ×-comm (S k) m ⟩
m × S k ≡⟨ p ⟩
n × S k ≡⟨ ×-comm n (S k) ⟩
((S k × n) ∎)
0-only-ℕ-+-unit-divisor : (m n : ℕ) → (m + n) ≡ Z → (m ≡ Z) ∧ (n ≡ Z)
0-only-ℕ-+-unit-divisor Z Z p = refl _ , refl _
1-only-ℕ-×-unit-divisor : (m n : ℕ) → (m × n) ≡ 1 → (m ≡ 1) ∧ (n ≡ 1)
1-only-ℕ-×-unit-divisor Z (S n) p = !𝟘 (S-≢-Z Z q)
where
q : 1 ≡ 0
q = 1 ≡⟨ p ⁻¹ ⟩
Z × S n ≡⟨ ×-Z-l (S n) ⟩
(0 ∎)
1-only-ℕ-×-unit-divisor (S m) (S n) p = ap S (fst η) , ap S q'
where
q : S (m + S m × n) ≡ 1
q = S (m + S m × n) ≡⟨ +-S-l m (S m × n) ⁻¹ ⟩
S m × S n ≡⟨ p ⟩
(1 ∎)
η : (m ≡ 0) ∧ ((S m × n) ≡ 0)
η = 0-only-ℕ-+-unit-divisor m (S m × n) (ap pred q)
q' : n ≡ 0
q' = n ≡⟨ ×-1-l n ⁻¹ ⟩
S Z × n ≡⟨ ap (λ - → S - × n) (fst η) ⁻¹ ⟩
S m × n ≡⟨ snd η ⟩
(0 ∎)
We can construct arbitrarily complex statements, including statements beyond our ability to prove.
is-prime : ℕ → Set is-prime n = (n ≥ 2) ∧ ((k m : ℕ) → (k × m) ≡ n → (k ≡ 1) ∨ (k ≡ n)) twin-prime-conjecture : Set twin-prime-conjecture = (n : ℕ) → Σ[ p ∈ ℕ ] ((p ≥ n) ∧ is-prime p ∧ is-prime (S (S p))) goldbach-conjecture : Set goldbach-conjecture = (n : ℕ) → n ≥ 3 → Σ[ p₁ ∈ ℕ ] Σ[ p₂ ∈ ℕ ] (is-prime p₁ ∧ is-prime p₂ ∧ ((2 × n) ≡ (p₁ + p₂)))We are not limited to statements about
ℕ. We have introduced enough material to pose and prove statements about quite general objects. For example, equality, our _≤_ relation, and its analogs are all examples of binary relations. We often want to prove or assume certain properties of such relations. Some of the most common properties are reflectivity, symmetry, anti-symmetry, and transitivity.
is-refl : {X : Set ℓ} → ( _R_ : X → X → Set ℓ') → Set (ℓ ⊔ ℓ')
is-refl {ℓ} {ℓ'} {X} _R_ = (x : X) → x R x
≤-refl : is-refl _≤_
≤-refl Z = *
≤-refl (S k) = ≤-refl k
≡-refl : {X : Set ℓ} → is-refl {ℓ} {ℓ} {X} _≡_
≡-refl x = refl x
is-symm : {X : Set ℓ} → (_R_ : X → X → Set ℓ') → Set (ℓ ⊔ ℓ')
is-symm {ℓ} {ℓ'} {X} _R_ = (x y : X) → x R y → y R x
≡-symm : {X : Set ℓ} → is-symm {ℓ} {ℓ} {X} _≡_
≡-symm _ _ p = p ⁻¹
is-anti : {X : Set ℓ} → (_R_ : X → X → Set ℓ') → Set (ℓ ⊔ ℓ')
is-anti {ℓ} {ℓ'} {X} _R_ = (x y : X) → x R y → y R x → x ≡ y
≤-anti : is-anti _≤_
≤-anti Z Z p q = refl _
≤-anti (S m) (S n) p q = ap S (≤-anti m n p q)
is-tran : {X : Set ℓ} → (_R_ : X → X → Set ℓ') → Set (ℓ ⊔ ℓ')
is-tran {ℓ} {ℓ'} {X} _R_ = (x y z : X) → x R y → y R z → x R z
≤-tran : is-tran _≤_
≤-tran Z m n p q = *
≤-tran (S k) (S m) (S n) p q = ≤-tran k m n p q
Divisibility is another important relation on the natural numbers.
_div_ : ℕ → ℕ → Set
m div n = Σ[ k ∈ ℕ ] ((k × m) ≡ n)
div-tran : is-tran _div_
div-tran m n o (k , p) (l , q) = l × k ,
((l × k) × m ≡⟨ ×-assoc l k m ⟩
l × k × m ≡⟨ ap (λ - → l × -) p ⟩
l × n ≡⟨ q ⟩
(o ∎))
div-refl : is-refl _div_
div-refl n = 1 , ×-1-l n
We finish off by showing _div_ is anti-symmetric. We also introduce a new Agda feature: @-patterns. If we have a pattern m@(S m'), then both m' and m are in scope and m is definitionally equal to S m'. So we get to save a few key-strokes and write m instead of S m' while guaranteeing the shape of m.
div-anti : is-anti _div_
div-anti Z Z (k , p) (l , q) = refl _
div-anti m@(S m') n@(S n') (k , p) (l , q) = m ≡⟨ q ⁻¹ ⟩
l × n ≡⟨ ap (λ - → - × n) (snd q''') ⟩
1 × n ≡⟨ ×-1-l n ⟩
(n ∎)
where
q' : ((k × l) × n) ≡ (1 × n)
q' = (k × l) × n ≡⟨ ×-assoc k l n ⟩
k × l × n ≡⟨ ap (λ - → k × -) q ⟩
k × m ≡⟨ p ⟩
n ≡⟨ ×-1-l n ⁻¹ ⟩
((1 × n) ∎)
q'' : (k × l) ≡ 1
q'' = ×-r-cancel n' (k × l) 1 q'
q''' : (k ≡ 1) ∧ (l ≡ 1)
q''' = 1-only-ℕ-×-unit-divisor k l q''
The Many Properties and Equivalent Definitions of “lte”
We can complete showing all our versions of “lte” are equivalent in the “if-and-only-if” sense. To aid, we give the definition of dependent function composition and the following properties of bi-implication._∘_ : {X : Set ℓ} {Y : Set ℓ'} {Z : Y → Set ℓ''}
→ ((y : Y) → Z y)
→ (f : X → Y)
→ (x : X) → Z (f x)
g ∘ f = λ x → g (f x)
⇔-symm : {X Y : Set ℓ} → X ⇔ Y → Y ⇔ X
⇔-symm (f , g) = g , f
⇔-tran : {X Y Z : Set ℓ} → (X ⇔ Y) → (Y ⇔ Z) → X ⇔ Z
⇔-tran (f , g) (f' , g') = (f' ∘ f) , (g ∘ g')
These utilities allow us to recycle our previous reasoning.
≤'-iff-≼ : (m n : ℕ) → (m ≤' n) ⇔ (m ≼ n) ≤'-iff-≼ m n = ⇔-tran (⇔-symm (≤-iff-≤' m n)) (≤-iff-≼ m n)We also define the “less than” and “greater than” relations.
_<_ _>_ : ℕ → ℕ → Set m < n = S m ≤ n m > n = n < mSome more theorems about “lte”.
zero-minimal : (n : ℕ) → n ≤ Z → n ≡ Z
zero-minimal Z p = refl _
≤-S : (k : ℕ) → k ≤ S k
≤-S Z = *
≤-S (S k) = ≤-S k
≤-+-r : (k m n : ℕ) → k ≤ m → k ≤ (m + n)
≤-+-r k m Z p = p
≤-+-r k m (S n) p = ≤-tran k (m + n) (m + S n) (≤-+-r k m n p) (≤-S (m + n))
where
f : (o : ℕ) → o ≤ S o
f Z = *
f (S o) = f o
≤-+-monotonic : (k m n : ℕ) → k ≤ m → (k + n) ≤ (m + n)
≤-+-monotonic k m Z p = p
≤-+-monotonic k m (S n) p = ≤-+-monotonic k m n p
≤-+-combine : (k l m n : ℕ) → k ≤ l → m ≤ n → (k + m) ≤ (l + n)
≤-+-combine k l Z n p q = ≤-+-r k l n p
≤-+-combine k l (S m) (S n) p q = ≤-+-combine k l m n p q
≤-×-monotonic : (k m n : ℕ) → m ≤ n → (m × k) ≤ (n × k)
≤-×-monotonic Z m n p = *
≤-×-monotonic (S k) m n p = ≤-+-combine m n (m × k) (n × k) p (≤-×-monotonic k m n p)
≤-×-combine : (k l m n : ℕ) → k ≤ l → m ≤ n → (k × m) ≤ (l × n)
≤-×-combine k l Z n p q = *
≤-×-combine k l (S m) (S n) p q = ≤-+-combine k l (k × m) (l × n) p (≤-×-combine k l m n p q)
One of the axioms we left behind when we left the world of classical logic and mathematics is the excluded middle. In our setting, the excluded middle would say for any type X, we can either construct a term which inhabits X, or construct an element of ¬ X. However, while we can cannot claim to construct an element of X ∨ ¬ X for any arbitrary X, we can construct such terms for certain types. We say such a type is decidable. It is particularly useful to know if a type X has decidable equality; the type x ≡ y is decidable for all terms x,y in X. Many of the types we’ve encountered thus far possess decidable equality.
decidable : Set ℓ → Set ℓ decidable X = X ∨ ¬ X has-decidable-equality : Set ℓ → Set ℓ has-decidable-equality X = (x y : X) → decidable (x ≡ y) 𝟙-has-decidable-equality : has-decidable-equality 𝟙 𝟙-has-decidable-equality * * = inl (refl *) 𝔹-has-decidable-equality : has-decidable-equality 𝔹 𝔹-has-decidable-equality tt tt = inl (refl _) 𝔹-has-decidable-equality tt ff = inr tt-≢-ff 𝔹-has-decidable-equality ff tt = inr (≢-sym tt-≢-ff) 𝔹-has-decidable-equality ff ff = inl (refl _)
𝟘 vacuously has this property.
𝟘-has-decidable-equality : has-decidable-equality 𝟘 𝟘-has-decidable-equality a b = !𝟘 aMore interestingly,
ℕ also has decidable equality. We can even prove a stronger statement and show the classical trichotomy property on ℕ.
ℕ-has-decidable-equality : has-decidable-equality ℕ
ℕ-has-decidable-equality Z Z = inl (refl _)
ℕ-has-decidable-equality Z (S n) = inr (≢-sym (S-≢-Z n))
ℕ-has-decidable-equality (S m) Z = inr (S-≢-Z m)
ℕ-has-decidable-equality (S m) (S n) = (f →∨ g) (ℕ-has-decidable-equality m n)
where
f : m ≡ n → S m ≡ S n
f = ap S
g : ¬ (m ≡ n) → ¬ (S m ≡ S n)
g u p = u (ap pred p)
ℕ-trichotomy : (m n : ℕ) → (m ≡ n) ∨ (m < n) ∨ (m > n)
ℕ-trichotomy Z Z = inl (refl _)
ℕ-trichotomy Z (S n) = inr (inl *)
ℕ-trichotomy (S m) Z = inr (inr *)
ℕ-trichotomy (S m) (S n) = (ap S →∨ id) (ℕ-trichotomy m n)
≤-S-r : (n : ℕ) → n ≤ S n
≤-S-r Z = *
≤-S-r (S n) = ≤-S-r n
split-case-≤ : (m n : ℕ) → m ≤ n → (m ≡ n) ∨ (m < n)
split-case-≤ Z Z p = inl (refl _)
split-case-≤ Z (S n) p = inr *
split-case-≤ (S m) (S n) p = (ap S →∨ id) (split-case-≤ m n p)
data _≤''_ : ℕ → ℕ → Set where
LTE-= : {n : ℕ} → n ≤'' n
LTE-inc : {m n : ℕ} → m ≤'' n → m ≤'' S n
≤-implies-≤'' : (m n : ℕ) → m ≤ n → m ≤'' n
≤-implies-≤'' Z Z p = LTE-=
≤-implies-≤'' Z (S n) p = LTE-inc (≤-implies-≤'' Z n p)
≤-implies-≤'' (S m) (S n) p with split-case-≤ m n p
≤-implies-≤'' (S m) (S n) p | inl q = transport (λ l → S m ≤'' S l) q LTE-=
≤-implies-≤'' (S m) (S n) p | inr q = LTE-inc (≤-implies-≤'' (S m) n q)
We can always write helpers to recover implicit arguments explicitly.
≤''-implies-≤ : (m n : ℕ) → m ≤'' n → m ≤ n
≤''-implies-≤ m .m LTE-= = ≤-refl m
≤''-implies-≤ m .(S _) (LTE-inc q) = ≤-tran m n (S n) (≤''-implies-≤ m _ q) (≤-S-r n)
where
rhs-≤'' : {m n : ℕ} → m ≤'' n → ℕ
rhs-≤'' {m} {n} q = n
n : ℕ
n = rhs-≤'' q
≤-iff-≤'' : (m n : ℕ) → (m ≤ n) ⇔ (m ≤'' n)
≤-iff-≤'' m n = ≤-implies-≤'' m n , ≤''-implies-≤ m n
Evens.
If you want to another example using a familiar property over the natural numbers, consider what it is to be even.
double : ℕ → ℕ
double Z = Z
double (S n) = S (S (double n))
data Even : ℕ → Set where
Even-Z : Even Z
Even-SS : {n : ℕ} → Even n → Even (S (S n))
is-even : ℕ → Set
is-even Z = 𝟙
is-even (S Z) = 𝟘
is-even (S (S n)) = is-even n
is-even-2 : ℕ → Set
is-even-2 n = Σ[ k ∈ ℕ ] ((2 × k) ≡ n)
is-even-d : ℕ → Set
is-even-d n = Σ[ k ∈ ℕ ] (double k ≡ n)
Then we can prove the equivalence of these four definitions.
is-even-implies-i : (n : ℕ) → is-even n → Even n
is-even-implies-i Z p = Even-Z
is-even-implies-i (S (S n)) p = Even-SS (is-even-implies-i n p)
is-even-implies-2 : (n : ℕ) → is-even n → is-even-2 n
is-even-implies-2 Z p = Z , refl _
is-even-implies-2 (S (S n)) p with is-even-implies-2 n p
is-even-implies-2 (S (S n)) p | k , q = S k ,
(2 × S k ≡⟨ refl _ ⟩
2 + 2 × k ≡⟨ +-S-l 1 (2 × k) ⟩
S (1 + 2 × k) ≡⟨ ap S (+-S-l 0 (2 × k)) ⟩
S (S (Z + 2 × k)) ≡⟨ ap (S ∘ S) (+-Z-l (2 × k)) ⟩
S (S (2 × k)) ≡⟨ ap (S ∘ S) q ⟩
(S (S n) ∎))
is-even-implies-d : (n : ℕ) → is-even n → is-even-d n
is-even-implies-d Z p = Z , refl _
is-even-implies-d (S (S n)) p with is-even-implies-d n p
is-even-implies-d (S (S n)) p | k , q = S k ,
(double (S k) ≡⟨ refl _ ⟩
S (S (double k)) ≡⟨ ap (S ∘ S) q ⟩
(S (S n) ∎))
Even-implies-is-even : (n : ℕ) → Even n → is-even n
Even-implies-is-even .0 Even-Z = *
Even-implies-is-even .(S (S _)) (Even-SS p) = Even-implies-is-even _ p
We have filled in enough edges for anyone to complete the graph showing each of these definitions implies any other.
Afterwards
Here was my writing process for this post:
- Have fun proving various things about natural numbers
- Realize I’ve written over a 1000 LOC and cut myself off
- Rearrange chunks into something resembling a logical flow
- Flesh out my stubby comments to myself into actual exposition
It is not an ideal process so any questions or (polite) corrections/criticisms are appreciated.
Next time: Lists, Singletons, Sub-singletons and Sets.