module Padova2025.ProgrammingBasics.Naturals.Arithmetic where
Arithmetic
open import Padova2025.ProgrammingBasics.Naturals.Base
Beyond the definition of the natural numbers, a canonical next step is to define basic arithmetic. For instance, addition can be defined by pattern matching as follows.
infixl 6 _+_ _+_ : ℕ → ℕ → ℕ zero + b = b succ a + b = succ (a + b)
As in the section on Operators, the underscores in the name of the addition function allow us to use it as an infix operator.
The right-hand side of the second clause in the definition is lifted straight from the Peano axioms. It is mostly a matter of taste whether to do the case split on the first argument, as done above, or instead on the second argument. One way to obtain this definition if one is familiar with high school mathematical laws but not the Peano axioms is as follows:
-- (intuitively, in blackboard mathematics) -- succ a + b = (1+a) + b = 1 + (a+b) = succ (a + b)
As a sanity check, put some example computation in the hole below
(for instance two + two) and verify using
C-c C-v that the result is what you would expect:
example-computation : ℕ
example-computation = {!!}
Exercise: Halving
Define a function half which divides its input by two,
rounding down if required. For instance half four should
reduce to two and half three should reduce to
one.
half : ℕ → ℕ
half = {!!}
We could also write the type signature of half as
follows:
half : (x : ℕ) → ℕThis style is especially useful in case we want the result type, in
this case ℕ, to depend on the input value x.
This syntax is reminiscent of the notation for the universal quantifier
used in the beginning of the 20th century: What we now write as “∀(x ∈ X). …” used to be
written as “(x ∈ X) (…)”, as in “(x ∈ ℕ) (y ∈ ℕ) ((x + y)² = x² + 2xy + y²).
And indeed, a function associates to every input some output,
so mimicking the notation of the universal quantifier makes sense.
Exercise: Predecessor
Implement the predecessor function. For simplicity, let us agree that
the predecessor of zero is zero again (instead
of introducing negative numbers or error handling).
pred : ℕ → ℕ
pred = {!!}
Again, we could also write the type signature as
pred : (x : ℕ) → ℕ.
Exercise: Subtraction
Define (cut-off) subtraction. For instance one - one and
one - two should both result in zero.
infixl 6 _-_
_-_ : ℕ → ℕ → ℕ
zero - b = {!!}
succ a - zero = {!!}
succ a - succ b = {!!}
Exercise: Multiplication and exponentiation
Define multiplication and exponentiation.
infixl 7 _·_
_·_ : ℕ → ℕ → ℕ
zero · b = {!!}
succ a · b = {!!}
Exercise: Squaring
Define squaring, without using the exponentiation operator introduced below.
infixr 8 _²
_² : ℕ → ℕ
_² x = {!!}
We could define squaring by reducing to exponentiation, i.e. defining
x ² = x ^ 2. This alternative definition would give the
same results as the definition envisioned here, and we will be able to
state and prove this fact in Agda. However, it is sometimes useful that
x ² is the same as x · x by
definition instead of by a nontrivial proof. We will touch
on this fine point again later.
Exercise: Exponentiation
infixr 8 _^_
_^_ : ℕ → ℕ → ℕ
a ^ zero = {!!}
a ^ succ b = {!!}
Exercise: Maximum
Define a function max which returns the maximum of two
inputs. For instance max one four should be
four.
max : ℕ → ℕ → ℕ
max = {!!}