{-# OPTIONS --cubical-compatible #-}
module Padova2025.ProvingBasics.Equality.NaturalNumbers where

Results on natural numbers#

open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General
open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic

Exercise: Associativity of addition#

Exercise 1+-assoc

+-assoc : (a b c : ℕ) → (a + b) + c ≡ a + (b + c)
+-assoc = {!!}

The reference solution uses: zero refl succ cong

Your solution

Reference solution

+-assoc : (a b c : ℕ) → (a + b) + c ≡ a + (b + c)
+-assoc zero     b c = refl
+-assoc (succ a) b c = cong succ (+-assoc a b c)

Exercise: Commutativity of addition#

Establishing commutativity is a little bit more involved than establishing associativity. Recall that the definition of addition involved a somewhat arbitrary choice of whether to case split on the first or on the second argument. The key idea in the commutativity proof developed in this exercise is to establish that the other choice would have worked as well.

Exercise 2+-zero

+-zero : (a : ℕ) → (a + zero) ≡ a
-- This does not hold by definition, the definition would state zero + b = b.
+-zero = {!!}

The reference solution uses: refl succ cong

Your solution

Reference solution

+-zero : (a : ℕ) → (a + zero) ≡ a
-- This does not hold by definition, the definition would state zero + b = b.
+-zero zero     = refl
+-zero (succ a) = cong succ (+-zero a)

Exercise 3+-succ

+-succ : (a b : ℕ) → a + succ b ≡ succ (a + b)
-- This does not hold by definition, the definition would state succ a + b = succ (a + b).
+-succ = {!!}

The reference solution uses: zero refl cong

Your solution

Reference solution

+-succ : (a b : ℕ) → a + succ b ≡ succ (a + b)
-- This does not hold by definition, the definition would state succ a + b = succ (a + b).
+-succ zero     b = refl
+-succ (succ a) b = cong succ (+-succ a b)

Exercise 4+-comm

+-comm : (a b : ℕ) → a + b ≡ b + a
+-comm = {!!}

The reference solution uses: zero sym +-zero succ trans cong +-succ

Your solution

Reference solution

+-comm : (a b : ℕ) → a + b ≡ b + a
+-comm zero     b = sym (+-zero b)
+-comm (succ a) b =
  trans (cong succ (+-comm a b)) (sym (+-succ b a))

Exercise: Two ways of doubling#

Exercise 5two-+-+

two-+-+ : (a : ℕ) → a + a ≡ two · a
two-+-+ = {!!}

The reference solution uses: cong sym +-zero

Your solution

Reference solution

two-+-+ : (a : ℕ) → a + a ≡ two · a
two-+-+ a = cong (a +_) (sym (+-zero a))

Exercise: Distributivity#

Exercise 6·-distribʳ-+

·-distribʳ-+ : (a b c : ℕ) → (a + b) · c ≡ a · c + b · c
·-distribʳ-+ = {!!}

The reference solution uses: zero refl succ trans cong sym +-assoc

Your solution

Reference solution

·-distribʳ-+ : (a b c : ℕ) → (a + b) · c ≡ a · c + b · c
·-distribʳ-+ zero     b c = refl
·-distribʳ-+ (succ a) b c =
  trans (cong (c +_) (·-distribʳ-+ a b c)) (sym (+-assoc c (a · c) (b · c)))

A word of warning: The proof here will only barely be readable. When we introduce equational reasoning, we will be able to format this proof in a much more accessible manner.

Exercise: One not zero, revisited#

open import Padova2025.ProvingBasics.Negation

Earlier we have informally argued that there is no value of type one ≡ zero. Now let us formally prove that if there was such a value, a contradiction would ensue.

Exercise 7one≠zero

one≠zero : ¬ (one ≡ zero)
one≠zero = {!!}

Your solution

Reference solution

one≠zero : ¬ (one ≡ zero)
one≠zero ()

As a corollary, prove that it is not the case that for all numbers a, succ (pred a) is the same as a:

Exercise 8lemma-succ-pred

lemma-succ-pred : ((a : ℕ) → succ (pred a) ≡ a) → ⊥
lemma-succ-pred f = {!!}

The reference solution uses: one≠zero zero

Your solution

Reference solution

lemma-succ-pred : ((a : ℕ) → succ (pred a) ≡ a) → ⊥
lemma-succ-pred f = one≠zero (f zero)

Instead, the equation succ(pred(a)) = a only holds for positive numbers. State and prove this fact, making use of the predicate IsPositive from before.

open import Padova2025.ProvingBasics.EvenOdd

Exercise 9lemma-succ-pred'

lemma-succ-pred' : (a : ℕ) → {!!} → succ (pred a) ≡ a
lemma-succ-pred' = {!!}

The reference solution uses: IsPositive case-succ refl

Your solution

Reference solution

lemma-succ-pred' : (a : ℕ) → IsPositive a → succ (pred a) ≡ a
lemma-succ-pred' a (case-succ _) = refl

Exercise: Injectivity of successor#

Prove that the successor function is injective:

Exercise 10succ-injective

succ-injective : {n m : ℕ} → succ n ≡ succ m → n ≡ m
succ-injective = {!!}

The reference solution uses: cong pred

Your solution

Reference solution

succ-injective : {n m : ℕ} → succ n ≡ succ m → n ≡ m
succ-injective = cong pred

Exercise: Cancelling on the left#

Exercise 11+-cancelₗ

+-cancelₗ : (a x y : ℕ) → a + x ≡ a + y → x ≡ y
+-cancelₗ = {!!}

The reference solution uses: zero succ succ-injective

Your solution

Reference solution

+-cancelₗ : (a x y : ℕ) → a + x ≡ a + y → x ≡ y
+-cancelₗ zero     x y p = p
+-cancelₗ (succ a) x y p = +-cancelₗ a x y (succ-injective p)

Exercise: Half twice#

Exercise 12half-twice

half-twice : (x : ℕ) → half (twice x) ≡ x
half-twice = {!!}

The reference solution uses: zero refl succ cong

Your solution

Reference solution

half-twice : (x : ℕ) → half (twice x) ≡ x
half-twice zero     = refl
half-twice (succ x) = cong succ (half-twice x)

Exercise: Twice even#

State and prove that for every number a, the number twice a is even.

Exercise 13twice-even

twice-even : (a : ℕ) → Even (twice a)
twice-even = {!!}

The reference solution uses: zero base-even succ step-even

Your solution

Reference solution

twice-even : (a : ℕ) → Even (twice a)
twice-even zero     = base-even
twice-even (succ a) = step-even (twice-even a)

First introduce a variable a in front of the = symbol and then reload the file using C-c C-l, so that the line reads twice-even a = {!!}.
Then use C-c C-c to ask Agda to case split on the variable a.
Navigate into the first hole and press C-c , to obtain a summary of the situation.
Notice that base-even fits the bill (or use Agda’s automatic mode, C-c C-a). Press C-c C-SPACE to conclude.
Now navigate to the second hole and inspect the situation with C-c ,.
Recognize that we are asked to verify the evenness of a number of the form succ (succ _). Hence use the step-even constructor, write step-even ? into the hole and press C-c C-SPACE.
In the new hole, press C-c , to get hold of the changed situation.
Notice that the recursive call twice-even a (in blackboard mathematics that would be an appeal to the induction hypothesis) fits the bill. Conclude by C-c C-SPACE followed by C-c C-l.

The following exercise is similar but more involved. We will require the subst function.

Exercise 14twice-even'

twice-even' : (a : ℕ) → Even (a + a)
twice-even' = {!!}

The reference solution uses: zero base-even succ subst step-even _≡_ cong sym +-succ

Your solution

Reference solution

twice-even' : (a : ℕ) → Even (a + a)
twice-even' zero     = base-even
twice-even' (succ a) =
  subst Even lemma (step-even (twice-even' a))
  where
  lemma : succ (succ (a + a)) ≡ succ (a + succ a)
  lemma = cong succ (sym (+-succ a a))

Exercise: Even twice#

Conversely, let us prove that even numbers are of the form twice a, more preceisely let us prove:

Exercise 15even-twice

even-twice : {x : ℕ} → Even x → x ≡ twice (half x)
even-twice = {!!}

The reference solution uses: base-even refl step-even cong succ

Your solution

Reference solution

even-twice : {x : ℕ} → Even x → x ≡ twice (half x)
even-twice base-even     = refl
even-twice (step-even p) = cong (λ a → succ (succ a)) (even-twice p)

Exercise: An impossible twice situation#

Exercise 16impossible-twice

impossible-twice : {x y : ℕ} → twice x ≡ succ (twice y) → ⊥
impossible-twice = {!!}

The reference solution uses: sym succ-injective

Your solution

Reference solution

impossible-twice : {x y : ℕ} → twice x ≡ succ (twice y) → ⊥
impossible-twice {succ x} {y} p = impossible-twice (sym (succ-injective p))

Exercise: Twice as a homomorphism#

Exercise 17twice-homo

twice-homo : (x y : ℕ) → twice (x + y) ≡ twice x + twice y
twice-homo = {!!}

The reference solution uses: zero refl succ cong

Your solution

Reference solution

twice-homo : (x y : ℕ) → twice (x + y) ≡ twice x + twice y
twice-homo zero     y = refl
twice-homo (succ x) y = cong succ (cong succ (twice-homo x y))

Exercise: Injectivity of twice#

Exercise 18twice-injective

twice-injective : {x y : ℕ} → twice x ≡ twice y → x ≡ y
twice-injective = {!!}

The reference solution uses: zero succ cong succ-injective

Your solution

Reference solution

twice-injective : {x y : ℕ} → twice x ≡ twice y → x ≡ y
twice-injective {zero}   {zero}   p = p
twice-injective {succ x} {succ y} p = cong succ (twice-injective (succ-injective (succ-injective p)))

Exercise: Two deciders of evenness#

open import Padova2025.ProgrammingBasics.Booleans
open import Padova2025.ProvingBasics.Equality.Booleans

Back in the section on decision procedures, we have discussed the function even? : ℕ → Bool, which has the purpose of returning true if the input number is even, and false otherwise.

We can imagine at least two implementations of even?:

even?₁ : ℕ → Bool
even?₁ zero            = true
even?₁ (succ zero)     = false
even?₁ (succ (succ n)) = even?₁ n

even?₂ : ℕ → Bool
even?₂ zero     = true
even?₂ (succ n) = not (even?₂ n)

In this exercise, verify that these two implementations yield the same result on all inputs.

Exercise 19even?₁-even?₂

even?₁-even?₂ : (a : ℕ) → even?₁ a ≡ even?₂ a
even?₁-even?₂ = {!!}

The reference solution uses: zero refl succ trans sym not²

Your solution

Reference solution

even?₁-even?₂ : (a : ℕ) → even?₁ a ≡ even?₂ a
even?₁-even?₂ zero            = refl
even?₁-even?₂ (succ zero)     = refl
even?₁-even?₂ (succ (succ a)) = trans (even?₁-even?₂ a) (sym (not² (even?₂ a)))