```{-# OPTIONS --allow-unsolved-metas #-}
-- {-# OPTIONS --safe #-}
-- In classical mathematics, we have:
-- Every statement A is either true or not true.

data _⊎_ (X Y : Set) : Set where
left  : X → X ⊎ Y
right : Y → X ⊎ Y

data ⊥ : Set where

postulate
law-of-excluded-middle : {A : Set} → A ⊎ (A → ⊥)
-- law-of-excluded-middle = {!!}

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

data _≡_ {X : Set} : X → X → Set where
refl : {x : X} → x ≡ x

-- Computational reading: "principle-of-explosion is a function
-- which reads as input a hypothetical value of ⊥ and outputs
-- a value of type A."
principle-of-explosion : {A : Set} → ⊥ → A
principle-of-explosion ()

theorem : zero ≡ succ zero

module Foo
(law-of-double-negation-elimination : {A : Set} → ((A → ⊥) → ⊥) → A) where
-- ^^^^^^^^^^^^
--  not not A
lemma : zero ≡ zero
lemma = {!!}

-- Let A be the statement: "There is a position x where the keys
-- to my apartment are." Constructively, if we do not know where
-- the keys are, we cannot defend the statement A. However,
-- as the keys couldn't simply vanish, the we can constructively
-- defend ¬¬A.

-- law-of-excluded-middle (...4....)

-- In constructive mathematics, the law of excluded middle
-- is not generally available; only in special cases.
-- Because Agda is a constructive system, there is no
-- way to fill in this hole.

-- Plan for today:
-- 2. Termination and wellfounded recursion :-)

-- Mode 1: Focus on Milly's type theory part, just a small Agda exercise.
-- Agda part: very short, 10 to 25 minutes

-- First question: "Please define the type of natural numbers."
{-
data ℕ : Set where
zero : ℕ
succ : ℕ → ℕ
-}

_+_ : ℕ → ℕ → ℕ
zero   + b = b
succ a + b = succ (a + b)

-- Third question: "Fill in the following hole."
lemma : (x : ℕ) → (zero + x) ≡ x
lemma x = {!!}

-- Second option: Small type theory exercises, then an Agda project.
-- Requirements:
-- 1. it takes a couple of afternoons
-- 2. it's interesting to you
-- 3. it contains at least one proof

{-
Possible examples for projects:

- detailed solutions to interesting exercises,
for instance regarding ordinals

- implement some algorithm and verify its correctness
(merge sort, some other sorting algorithm, Euclidean algorithm,
...)

- formalize some piece of mathematics/compsci/physics

- who wins at Tic Tac Toe?

- Graham's Number
+ * ^ ↑↑ ↑↑↑ ↑↑↑↑

4 * 2 = 2 + 2 + 2 + 2
2 ^ 4 = 2 * 2 * 2 * 2
2 ↑↑ 4 = 2 ^ (2 ^ (2 ^ 2))
2 ↑↑↑ 4 = 2 ↑↑ (2 ↑↑ (2 ↑↑ 2))

G₁ = 3 ↑↑↑↑ 3

G₂ = 3 ↑↑↑...↑↑↑ 3
^^^^^^^^^
G₁ many

G₃ = 3 ↑↑↑...↑↑↑ 3
^^^^^^^^^
G₂ many

...

G₆₄ = Graham's number.
The last digit of Graham's number is a 7.
-}

half : ℕ → ℕ
half zero            = zero
half (succ zero)     = zero
half (succ (succ n)) = succ (half n)

example : half (succ (succ (succ zero))) ≡ succ zero
example = refl

-- "digits n" should be the number of binary digits of the number "n".
-- For instance: Recall that the number 5 is written in binary as 101.
-- So "digits 5" should be "3". "number 7" should also be "3".
-- "digits 8" should be "4". The number 8 can be written in binary
-- as 00000000001000, but still "digits 8" should be "4".
{-
digits : ℕ → ℕ
digits zero     = zero
digits (succ n) = succ (digits (half (succ n)))
-}
-- Issue: Agda does not realize that this recursion is wellfounded.
-- This function definition does make sense, but Agda doesn't realize
-- that. To be on the safe side, Agda rejects this definition, out of
-- fear that this function might be trapped in an infinite viscious loop.

{-
loop : ℕ → ℕ
loop n = loop (succ n)
-}

module Option-1 where
{-# TERMINATING #-}
digits : ℕ → ℕ
digits zero     = zero
digits (succ n) = succ (digits (half (succ n)))

{-# TERMINATING #-}
loop : ℕ → ℕ
loop n = loop (succ n)
-- dangerous!

module Option-2 where
{-# NON_TERMINATING #-}
digits : ℕ → ℕ
digits zero     = zero
digits (succ n) = succ (digits (half (succ n)))

-- The following hole can NOT be filled:
new-lemma : (n : ℕ) → digits (succ n) ≡ succ (digits (half (succ n)))
new-lemma n = {!!}

module Option-3 where
-- employ a totally different algorithm

module Option-4 where
-- employ gas
digits : ℕ → ℕ
digits n = go (n + n) n
where
go : ℕ → ℕ → ℕ
go zero       n        = zero  -- bailout!
go (succ gas) zero     = zero
go (succ gas) (succ n) = succ (go gas (half (succ n)))
-- Agda recognizes this definition to be wellfounded,
-- because in the recursive call on the right-hand side,
-- the argument "gas" is strictly structurally smaller than
-- the argument "succ gas" on the left-hand side.

module Option-5 where
-- use a generalized kind of gas which is not brittle
-- and not ad hoc, but fundamental to the nature of
-- natural numbers
```