{-
Fun facts about even and odd numbers:
1. Even(0)
2. ∀a. Even(a) ⇒ Even(2+a)
1'. Odd(1)
2'. ∀a. Odd(a) ⇒ Odd(2+a)
----------------------------------------
3. ∀a. Even(a) ⇒ Odd(1+a)
4. ∀a. ∀b. Even(a) ∧ Even(b) ⇒ Even(a+b)
5. ∀a. ¬(Even(a) ∧ Odd(a))
6. ∀a. Even(a) ∨ Odd(a)
To formalize these facts, we will set up a family
of types, called "Even n", one such type for each
number "n". We picture "Even n" as the type of
witnesses that the number "n" is even.
For instance, the type "Even four" should be inhabited.
In constrast, the type "Even three" should be empty.
-}
{-
Most types of witnesses are either empty (for instance the type "Even three")
or are inhabited by exactly one inhabitant (for instance the type "Even zero"
or the type "Even two" or the type "Even four").
But there are also types of witnesses which are inhabited by many inhabitants.
For instance the type of witnesses that there are prime numbers beyond 10.
This type is inhabited by:
(a) (11 , p), where p is a witness that 11 is a prime beyond 10
(b) (13 , q), where q is a witness that 13 is a prime beyond 10
(c) (17 , r)
(d) (19 , s)
...
-}
{-
There are two possible definitions of a set X of numbers being infinite:
(a) "For every number a ∈ ℕ, there is a number b ∈ X such that b ≥ a."
(b) "It is not the case that X consists only of finitely many numbers."
In ordinary blackboard mathematics, we have (a) ⇔ (b).
In constructive blackboard mathematics, we have (a) ⇒ (b) but the other way round.
(Constructive blackboard mathematics = blackboard mathematics, but without
the axiom of choice and without proof by contradiction.)
The axiom of choice states: Given a set M of inhabited sets, there is a function
f : M → ... such that f(X) ∈ X for all X ∈ M.
For instance, for the set M = "the set of cities on earth", a suitable function f
would be: f(X) = the youngest inhabitant of X.
There is a (constructively proven) metatheorem in logic stating the following:
Every ZFC-proof of an arithmetical Π₂-assertion can be transformed into an IZF-proof.
∀∀∀... ∃∃∃... no more quantifiers here
(ZFC is a possible foundation for classical blackboard mathematics.
IZF is a possible foundation for constructive blackboard mathematics.)
A very intriguing alternative foundation for constructive blackboard mathematics,
and then by postulating choice and proof by contradiction also for classical blackboard
mathematics, is the so-called "Minimalist Foundation" pioneered by Milly Maietti.
-}
data ℕ : Set where
zero : ℕ
succ : ℕ → ℕ
one : ℕ
one = succ zero
two : ℕ
two = succ (succ zero)
four : ℕ
four = succ (succ (succ (succ zero)))
data Even : ℕ → Set where
base-even : Even zero
step-even : {a : ℕ} → Even a → Even (succ (succ a))
-- Logical reading: For every number a, if a is even, then so is succ (succ a).
-- Computational reading: "step-even" is a function which reads as input
-- 1. a number "a" (implicit)
-- 2. a witness that "a" is even
-- and outputs a witness that "succ (succ a)" is even.
-- In blackboard mathematics, we often prove implications A ⇒ B.
-- In Agda, we write programs which transform witnesses of A into witnesses of B.
-- In Agda, we write programs which read witnesses of A as input and output witnesses of B.
first-result : Even zero
first-result = base-even
second-result : Even two
second-result = step-even base-even
third-result : Even four
third-result = step-even {two} second-result
-- C-c .: display goal and what we currently have
-- In Agda, to prove a result, we write down a witness of the result,
-- so we exhibit a value of the type of witnesses.
data Odd : ℕ → Set where
base-odd : Odd one
step-odd : {a : ℕ} → Odd a → Odd (succ (succ a))
-- Alternative definitions of oddity:
-- (a) "A number is odd iff its predecessor is even."
-- (a') "If a number is even, then its successor is odd."
-- (b) "A number is odd iff it not even."
-- (c) "A number is odd iff it is of the form 2k+1."
-- 3. ∀a∈ℕ. Even(a) ⇒ Odd(1+a)
-- (a∈ℕ)(Even(a) ⇒ Odd(1+a)) -- 20th century notation for the universal quantifier
-- Logical reading: For every number a, if a is even, then succ(a) is odd.
-- Computational reading: "next-number-odd" is a function which reads as input
-- (a) a number "a"
-- (b) a witness that "a" is even
-- and outputs a witness that "succ a" is odd.
next-number-odd : {a : ℕ} → Even a → Odd (succ a)
next-number-odd base-even = base-odd
next-number-odd (step-even p) = step-odd (next-number-odd p)
five : ℕ
five = succ four
example-run : Odd five
example-run = next-number-odd third-result
-- In blackboard mathematics, we can apply a lemma to some result in order to obtain a new result.
-- In Agda, we can apply a function to a witness in order to obtain a new witness.
{-
In blackboard mathematics. Claim: For every number a, if a is even, then succ(a) is odd.
Proof. By induction on a.
Induction base case a = 0: In this case we need to verify that succ(0) is odd.
This is by definition of oddity.
Induction step a → 2+a: By assumption, we know that a is even.
By induction hypothesis, we may conclude that 1+a is odd.
By definition of oddity, we may conclude that 2+(1+a) is odd.
That is what we needed to show, because our goal was to
verify that 1+(2+a) is odd.
-}
_+_ : ℕ → ℕ → ℕ
zero + b = b
succ a + b = succ (a + b)
-- 4. ∀a. ∀b. Even(a) ∧ Even(b) ⇒ Even(a+b)
-- Logical reading: For every number "a", for every number "b", if "a" and "b" are both even,
-- then "a+b" is also even.
-- Computational reading: "lemma-sum-even" is a function which inputs four arguments...
-- (a) a number "a" (implicitly)
-- (b) a number "b" (implicitly)
-- (c) a witness that "a" is even
-- (d) a witness that "b" is even
-- ...and outputs a witness that "a+b" is even.
-- lemma-sum-even : {a : ℕ} → {b : ℕ} → Even a → Even b → Even (a + b)
lemma-sum-even : {a b : ℕ} → Even a → Even b → Even (a + b)
-- lemma-sum-even {firstnumber} {secondnumber} p q = {!!}
lemma-sum-even base-even q = q
lemma-sum-even (step-even p) q = {!!}
-- For every "a" and "b", we will introduce a type "a ≡ b".
-- This type will be the type of witnesses that "a" and "b" are equal.
-- For instance, the type "zero ≡ zero" should be inhabited.
-- For instance, the type "(two + two) ≡ four" should be inhabited.
-- For instance, type type "zero ≡ one" should not be inhabited.
data _≡_ : ℕ → ℕ → Set where
refl : {x : ℕ} → (x ≡ x) -- "reflexivity"
-- logical reading: For every x, it is the case that x equals x.
-- computational reading: "refl" is a function which inputs (implicitly) an x,
-- and which outputs a witness that x equals x.
-- logical reading: For every number x, zero + x equals x.
-- computational reading: "lemma" is a function which inputs a number "x" and outputs
-- a witness that "zero + x" equals "x".
lemma : (x : ℕ) → ((zero + x) ≡ x)
lemma x = refl
lemma' : (x : ℕ) → ((x + zero) ≡ x)
lemma' x = {!!}
grande-teorema : ((two + two) ≡ four)
grande-teorema = refl
-- We can use "refl" in those situations where the two sides of the equality
-- are manifestly equal. Equal in a sense which does not require complex arguments,
-- but instead mere computation, unfolding all definitions.
-- blackboard mathematics: "This is trivial by definition."
-- Agda: refl