# Proposal for today and tomorrow :-)

* Random fun facts
  * There is the so-called "universal algorithm": A specific Turing machine
    which, depending on in which universe we run it, will output whatever
    you want. (When run in the standard universe, this machine
    will never terminate.)
  * There is the notion of infinite-time Turing machines: Turing machines
    which can run for longer than infinity.

* Agda as a programming language
  * Booleans, naturals, lists
  * definitions by pattern matching
  * running code
  * higher-order functions
  * implicit parameters
  * arithmetic
  * decision procedures

* Agda as a proof language
  * Propositions as types
  * Even, Odd
  * implication
  * universal quantification
  * Barbara mood
  * negation

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

data Bool : Set where
  false : Bool
  true  : Bool

data ListOfNats : Set where
  []  : ListOfNats
  _∷_ : ℕ → ListOfNats → ListOfNats
  -- `_∷_` is a function which takes as input
  -- 1. a natural number
  -- 2. a list of natural numbers
  -- and which outputs a new, freshly-minted list of natural numbers.

-- `add` is a function which takes as input two numbers and outputs a number.
-- On a blackboard, we would write `add : ℕ × ℕ → ℕ`.
_+_ : ℕ → ℕ → ℕ
zero   + y = y
succ a + y = succ (a + y)
-- C-c C-c: case split
-- C-c C-SPACE: check hole

one : ℕ
one = succ zero

four : ℕ
four = succ (succ (succ (succ zero)))
-- C-c C-v: run code   (in local Agda, C-c C-n)
-- C-c C-a: automatic mode

exampleList : ListOfNats
exampleList = six ∷ (four ∷ [])
-- In Haskell, `[6, 4]` or `6 :: 4 :: []` or `6 :: (4 :: [])`
  where
  six : ℕ
  six = four + (one + one)

-- For instance, `eq? one four` should result in `false`.
-- For instance, `eq? four (succ (succ (succ (succ zero))))` should result in true.
eq? : ℕ → ℕ → Bool
eq? zero     zero     = true
eq? zero     (succ y) = false
eq? (succ x) zero     = false
eq? (succ x) (succ y) = eq? x y  -- a "recursive call"

bar : ℕ → Bool
bar = eq? four
-- Here we "partially apply" the `eq?` function.
-- The result is NOT a Boolean, but instead a function of type ℕ → Bool
-- awaiting further input and only then outputting a result of type Bool.

exampleUsage : Bool
exampleUsage = bar one

-- For instance, `≤? one four` should result in `true`.
-- For instance, `≤? four (succ (succ (succ (succ zero))))` should result in `true`.
-- For instance, `≤? four zero` should result in `false`.
-- The function `≤?` should read two natural numbers as input and output
-- a boolean indicating whether the first number is smaller than or equal to the second number.
≤? : ℕ → ℕ → Bool
≤? zero     y        = true
≤? (succ x) zero     = false
≤? (succ x) (succ y) = ≤? x y

not : Bool → Bool
not false = true
not true  = false

-- Unlike most mainstream programming languages, Agda has "dependent types".
-- These are types which depend on values.
-- For instance, type of length-n lists of natural numbers depends on the number n.

-- Define a function even? which determines whether its input is even.
-- For instance, even? zero and even? two should both reduce to true,
-- while even? three should evaluate to false.
even? : (n : ℕ) → Bool
even? zero     = true
even? (succ x) = not (even? x)

even?' : ℕ → Bool
even?' zero            = true
even?' (succ zero)     = false
even?' (succ (succ x)) = even?' x

-- First, write down `?`.
-- Second, load the file using C-c C-l.
-- Third, move the cursor into the hole.
-- Fourth, do the case split using C-c C-c.

-- What is "induction" on a blackboard, is "recursion" in Agda.

-- C-c C-l: load file

-- Agda has excellent support for higher-order functions.

-- The `foo` function reads as input a natural number
-- and outputs a small type.
-- (Recall that `Set` is the type of all small types.)
foo : ℕ → Set
foo zero            = ℕ
foo (succ zero)     = Bool
foo (succ (succ x)) = (ℕ → Bool)
-- C-c C-.: display goal and current hole content and context
-- C-c C-,: display goal and context

exampleUsageOfFoo : foo (succ zero)
exampleUsageOfFoo = false

baz : Set → Set
baz X = X
-- The type ℕ is a value of the type Set.
-- The type Set is a value of the type Set₁.

baz' : Set → Set
baz' X = ℕ

baz'' : Set → Set
baz'' X = (X → X)

idℕ : ℕ → ℕ
idℕ x = x

idBool : Bool → Bool
idBool x = x

-- Let's write down the polymorphic identity function.
-- This function reads as input
-- 1. a type X
-- 2. a value a : X
-- and outputs a.
id : (X : Set) → X → X
id X a = a

funWithId : ℕ
funWithId = id ℕ four

funWithId' : ℕ
funWithId' = id _ four

-- Let's rewrite `id` with implicit parameters.
-- This function reads as input
-- 1. a type X (implicit)
-- 2. a value a : X
-- and outputs a.
implicit-id : {X : Set} → X → X
implicit-id a = a

funWithImplicitId : ℕ
funWithImplicitId = implicit-id four
-- Agda will infer the value of the implicit parameter.

funWithImplicitId' : ℕ
funWithImplicitId' = implicit-id {ℕ} four
-- Here we use curly braces at the call site as antidote
-- for the curly braces in the declaration of `implicit-id`
-- to allow us, exceptionally, to supply the value of the
-- otherwise-implicit parameter.

-- K reads as input two values and outputs the first one.

K : {X : Set} → {Y : Set} → X → Y → X
K a b = a

K' : {X : Set} {Y : Set} → X → Y → X
K' a b = a

K'' : {X Y : Set} → X → Y → X
K'' a b = a

funWithK = K four true

-- Now: Agda as a proof language :-)

-- Let's prove that Socrates is mortal. From the following axioms:
-- 1. A type of entities (Socrates, the king, all the cats, ...)
-- 2. There is a predicate "being mortal".
-- 3. There is a predicate "being human".
-- 4. Every human is mortal.
-- 5. Socrates is a human.

postulate
  -- Axiom 1
  Entity   : Set
  socrates : Entity
  king     : Entity
  cat47    : Entity
  god      : Entity

  -- Axioms 2 and 3
  Mortal   : Entity → Set
  Human    : Entity → Set
  -- `Mortal` is a function which maps an entity (for instance socrates)
  -- to the type of witnesses that this entity is mortal.
  -- For instance, as we shall prove, the type `Mortal socrates`
  -- should be inhabited. In contrast, the type `Mortal god`
  -- should be empty. "Propositions as types"

  -- Axiom 4. Every human is mortal.
  human-mortality : (x : Entity) → Human x → Mortal x
  -- There are two ways of reading this.
  -- Logical reading: For every entity x, is x is human, then x is mortal.
  -- Computational reading: `human-mortality` is a function which inputs
  -- an entity `x` and a witness that `x` is human and which outputs a
  -- witness that `x` is mortal.

  -- Axiom 5. Socrates is a human.
  socrates-human : Human socrates

-- Statement: Socrates is mortal.
socrates-mortal : Mortal socrates
socrates-mortal = human-mortality socrates socrates-human
-- By Axiom 5, Socrates is human. By Axiom 4, every human is mortal. As a special instance of Axiom 4, we obtain
-- the fact that if Socrates is human, then Socrates is mortal. Using modus ponens, Socrates is mortal.
-- C-c C-r: refine hole

-- What's "using a lemma" on a blackboard is "calling a function" in Agda.

-- Tasks.
-- 1. Prove that two is even.
-- 2. Prove that four is even.
-- 3. Prove that if x is even, then succ x is odd.
-- 4. Prove that double x is even.
-- 5. Prove that if x is even and odd, then four equals two.

-- We'll set up a type `Even x` of witnesses that `x` is even.
-- For instance, the type `Even four` should be inhabited.
-- For instance, the type `Even one` should be empty.
-- Without any arguments, `Even` will be a function which reads as input
-- a number `x` and which outputs the type of witnesses that `x` is even.
data Even : ℕ → Set where
  base-even : Even zero
  step-even : {x : ℕ} → Even x → Even (succ (succ x))
  -- Logical reading: For every number x, if x is even, then succ (succ x) is even.
  -- Computational reading: `step-even` is a function which reads as inputs
  -- a number `x` and a witness that `x` is even and which outputs a new
  -- freshly-minted witness that `succ (succ x)` is even.

data Odd : ℕ → Set where
  base-odd : Odd one
  step-odd : {x : ℕ} → Odd x → Odd (succ (succ x))

four-even : Even four
-- four-even = step-even {two} (step-even {zero} base-even)
four-even = step-even (step-even base-even)

-- Logical reading: For every number x, is x is even, then succ x is odd.
-- Computational reading: `lemma` is a function which inputs a number `x`
-- and a witness that `x` is even and which outputs a witness that `succ x` is odd.
lemma : {x : ℕ} → Even x → Odd (succ x)
lemma base-even     = base-odd
lemma (step-even p) = step-odd (lemma p)

five : ℕ
five = succ four

corollary : Odd five
corollary = lemma four-even
```