# Proposal for a plan

- Polymorphic data types
- More Even/Odd
- Equality
- State and prove lemmas about natural numbers involving equality (e.g. x + y = y + x)
- Logical connectives: ¬, ∧, ∨, ∃, ...

```
data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

data Bool : Set where
  false : Bool
  true  : Bool

infixr  _∷_
data ListOfNats : Set where
  []  : ListOfNats
  _∷_ : ℕ → ListOfNats → ListOfNats

exampleList : ListOfNats
exampleList = zero ∷ zero ∷ succ (succ zero) ∷ zero ∷ []

data ListOfBools : Set where
  []  : ListOfBools
  _∷_ : Bool → ListOfBools → ListOfBools

-- `List` will be a function of type Set → Set; this function reads a type `X`
-- as input and outputs the type of lists of elements of `X`.
data List (X : Set) : Set where   -- a "parameterized definition"
  []  : List X
  _∷_ : X → List X → List X

data List' : Set → Set₁ where   -- an "indexed definition"
  []  : {X : Set} → List' X
  _∷_ : {X : Set} → X → List' X → List' X

data Weird : Set where
  succ : Weird → Weird
-- This type is empty.
-- The constructor `succ` reads as input an inhabitant of type `Weird`
-- and outputs a new freshly-minted inhabitant of type `Weird`.
-- However, this constructor is of no use, as we don't have any inhabitants
-- of type `Weird` to begin with.

-- The following definition is not accepted by Agda's termination checker:
-- foo : Weird
-- foo = succ foo
-- spelled out: succ (succ (succ (succ ...)))
-- We need to turn to so-called co-datatypes to have something like this work.

-- Let's define the type `Vec ℕ three` of vectors of natural numbers of length precisely three.
-- More generally, for every number `n` and for every small type `X`, let's define
-- the type `Vec X n` of vectors of elements of `X` of length precisely `n`.
data Vec (X : Set) : ℕ → Set where
  []  : Vec X zero
  _∷_ : {n : ℕ} → X → Vec X n → Vec X (succ n)

three : ℕ
three = succ (succ (succ zero))

example-vector : Vec ℕ three
example-vector = succ zero ∷ zero ∷ succ (succ zero) ∷ []

_+_ : ℕ → ℕ → ℕ
zero   + y = y
succ x + y = succ (x + y)

-- The concatenation operator. For instance, `example-vector ++ example-vector`
-- should result in `succ zero ∷ zero ∷ succ (succ zero) ∷ succ zero ∷ zero ∷ succ (succ zero) ∷ []`.
_++_ : {X : Set} {n m : ℕ} → Vec X n → Vec X m → Vec X (n + m)
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

data Even : ℕ → Set where
  base-even : Even zero
  step-even : {n : ℕ} → Even n → Even (succ (succ n))

-- Logical reading: For every number x, for every number y, if x is
-- even, and if y is even, then x + y is even.
-- Computational reading: `sum-even` is a function which inputs
-- 1. a number `x` (implicit)
-- 2. a number `y` (implicit)
-- 3. a witness that `x` is even
-- 4. a witness that `y` is even
-- and which outputs a witness that `x + y` is even.
sum-even : {x y : ℕ} → Even x → Even y → Even (x + y)
sum-even base-even     q = q
sum-even (step-even p) q = step-even (sum-even p q)

-- Equality! :-)
two : ℕ
two = succ (succ zero)

four : ℕ
four = succ (succ (succ (succ zero)))

-- {-# BUILTIN NATURAL ℕ #-}
-- meaning-of-life : ℕ
-- meaning-of-life = 42

-- For every type X, and for every inhabitant a : X, and for every inhabitant b : X,
-- there is the type `a ≡ b` of witnesses that `a` equals `b`.
-- For instance, the type `two + two ≡ four` is inhabited, while the type `two + two ≡ zero`
-- is empty.

infix  _≡_
data _≡_ {X : Set} : X → X → Set where
  refl : {x : X} → x ≡ x
  -- bailout : two + two ≡ zero

grande-teorema : two + two ≡ four  -- \==
grande-teorema = refl
-- We can use `refl` if and only if it's obvious to Agda (by unfolding the definitions,
-- i.e. by running the code as far as possible) that the two sides of
-- the equation are the same.

-- Logical reading: For every number y, zero + y equals y.
-- Computational reading: `thm` is a function which inputs a number `y` and
-- which outputs a witness that `zero + y` equals `y`.
thm : (y : ℕ) → zero + y ≡ y
thm y = refl

-- Logical reading: For every small type X, for every small type Y,
-- for every elements a, b : X, for every function f : X → Y, if `a`
-- equals `b`, then also `f a` equals `f b`.
-- Computational reading: `cong` is a function which inputs
-- 1. a small type X (implicitly)
-- 2. a small type Y (implicitly)
-- 3. an element a : X (implicitly)
-- 4. an element b : X (implicitly)
-- 5. a function f : X → Y
-- 6. a witness that a equals b
-- and which outputs a witness that f a equals f b.
cong : {X Y : Set} {a b : X} (f : X → Y) → a ≡ b → f a ≡ f b
cong f refl = refl

sym : {X : Set} {a b : X} → a ≡ b → b ≡ a
sym refl = refl

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

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

-- Agda is a calculator, but not for numbers, and instead for logic!

trans : {X : Set} {a b c : X} → a ≡ b → b ≡ c → a ≡ c
trans = ?

+-comm : (x y : ℕ) → x + y ≡ y + x
+-comm zero     y = sym (+-zero y)
+-comm (succ x) y = trans (sym (+-succ x y)) (trans (+-comm x (succ y)) (sym (+-succ y x)))
```