{-# 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 = {!!} contradiction : ⊥ data ℕ : Set where zero : ℕ succ : ℕ → ℕ data _≡_ {X : Set} : X → X → Set where refl : {x : X} → x ≡ x -- Logical reading: "From a contradiction, everything follows." -- 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 theorem = principle-of-explosion contradiction 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: -- 1. About the exam -- 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 : ℕ → ℕ -} -- Second question: "Please define addition." _+_ : ℕ → ℕ → ℕ 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