{-# OPTIONS --allow-unsolved-metas #-}
module session06 where
{-
x ≡ (y ≡ z)
(x ≡ y) ≡ z
-}
{-
"Assuming A and B, then C."
lemma : A × B → C
lemma (x , y)
lemma : A → B → C
lemma x y
iso : (A × B → C) → (A → B → C)
osi : (A → B → C) → (A × B → C)
"Currying"
"Assuming A, then B and C."
theorem : A → B × C
theorem₁ : A → B
theorem₂ : A → C
_↔_ : Set → Set → Set
A ↔ B = (A → B) × (B → A)
eq?-correct : (x y : ℕ) → ((eq? x y ≡ true) ↔ (x ≡ y))
_≼_ : (ℕ → ℕ) → (ℕ → ℕ) → Set
f ≼ g = ((n : ℕ) → f n ≤ g n)
Then it's simply not the case that f ≼ g ⊎ g ≼ f for all functions f, g.
cmp? : (x y : A) → ¬ ¬ (x ≤ y ⊎ y ≤ x)
In constructive mathematics, we have A → ¬ ¬ A
but we do NOT have ¬ ¬ A → A. We read "¬ ¬ A" as
"we are given the promise that A holds but no witness of it".
Example from every-day life: Let A be the assertion
"there is a position where the keys to my apartment are".
A witness of A is a pair (x, p) where x is a position
and p is a witness that the keys are at position x.
If we can't find the keys right now, then right now we cannot
construct a witness of A. But if the keys still need to be somewhere
(no ghosts interfering), then we can construct a witness of ¬ ¬ A.
Firstly, we do have constructively: (x y : ℕ) → x ≡ y ⊎ x ≢ y.
Secondly, constructively we do NOT have: (f g : ℕ → ℕ) → f ≡ g ⊎ f ≢ g.
Thirdly, "secondly" does NOT mean that there actually are functions f, g : ℕ → ℕ
such that neither f ≡ g nor f ≢ g.
Fourthly, constructively we DO have again: (f g : ℕ → ℕ) → ¬ ¬ (f ≡ g ⊎ f ≢ g).
-}
{-
0. Your questions
1. Review what we did
2. Poll
Option A: Exercises
Option B: ???
Option C: one of the topics
Core curriculum
- "Strong induction"
Traditional computer science stuff
1 Simply-typed lambda calculus
2 Implementing a toy imperative programming language [5]
Beyond infinity / building alternative mathematical universes
3 More on ordinal numbers
4 Infinite-time Turing machines [with zero lines of Agda code] [3]
5 Expanding the mathematical universe by **forcing** for fun and profit:
realizing mathematical phantoms [1]
Foundations of mathematics
6 Sets as trees [3]
- Clarifying the relation between sets and types
- A possible answer to the question "what are sets, precisely?"
- Understanding the problem with powersets / impredicativity
- Relative consistency as an exercise in programming
7 Metamathematics [1]
- Encoding provability
- Peano arithmetic
8 Beyond standard Agda [3]
- Limitations of standard Agda
- Cubical Agda
9 Classical mathematics in Agda [4]
- The law of excluded middle as a helpful oracle
- The axiom of choice
- **Extracting computational content from classical proofs**
- Sarcastic interpretation of classical logic
-}
-- Ordinary induction: If P 0 and if P n → P (succ n), then P holds for all numbers.
-- "n = 0: ...; n → n + 1: ..."
-- Strong induction: If (if P holds for all predecessors of x, then P holds for x),
-- then P holds for all numbers.
-- "< n → n: ..."
open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic hiding (half)
-- For instance, `half four` should be `two`. (If required, we round down.)
half : ℕ → ℕ
half zero = zero
half (succ zero) = zero
half (succ (succ x)) = succ (half x)
-- The purpose of the `digits` function is to count the number of binary digits.
-- For instance, `digits four` should be `three` (because four in binary is 100).
-- For instance, `digits five` should be `three` (because five in binary is 101).
{-
digits : ℕ → ℕ
digits zero = zero
digits x@(succ _) = succ (digits (half x))
-}
-- Using strong induction, we could prove that this recursion terminates:
-- If we know that `digits y` terminates for all numbers `y` less than `x`,
-- then we can conclude that `digits x` will terminate, because this only
-- depends on the termination of `digits (half x)` and `half x < x`.
-- For any two numbers x, y, let's introduce the type `x < y` of witnesses
-- that x is strictly smaller than y.
data _<_ : ℕ → ℕ → Set where
base : {n : ℕ} → n < succ n
step : {a b : ℕ} → a < b → a < succ b
_ : two < five
_ = step (step base)
-- We can conclude that a number x is accessible if we have already established
-- that all predecessors of x are accessible.
--
-- This definition looks circular but isn't: The number zero does not have
-- any predecessors, so all of its predecessors are accessible, and hence zero is
-- accessible.
data Acc : ℕ → Set where
acc : {x : ℕ} → ({y : ℕ} → y < x → Acc y) → Acc x
-- "for all y, if y < x, then y is accessible"
zero-acc : Acc zero
zero-acc = acc λ () -- shorthand for "acc (λ ())"
one-acc : Acc one
one-acc = acc λ { base → zero-acc }
two-acc : Acc two
two-acc = acc λ
{ base → one-acc
; (step base) → zero-acc
}
ℕ-wellfounded : (x : ℕ) → Acc x
ℕ-wellfounded = {!!}
digits-brittle : ℕ → ℕ
digits-brittle n = go n (succ n)
where
go : ℕ → ℕ → ℕ
go n zero = five -- hopefully this piece of code is never reached
go zero (succ gas) = zero
go x@(succ _) (succ gas) = succ (go (half x) gas)
half-< : (x : ℕ) → half (succ x) < succ x
half-< x = {!!}
digits-robust : ℕ → ℕ
digits-robust n = go n (ℕ-wellfounded n)
where
go : (n : ℕ) → Acc n → ℕ
go zero p = zero
go x@(succ _) (acc f) = succ (go (half x) (f (half-< _)))
-- "The recursive call with input `half x` is okay, because `half x < x`."
-- The accessibility predicate gives us a sophisticated version of gas.
-- A toy imperative programming language
--
-- Let's not implement right now:
-- 0. a parser (for turning strings into abstract syntax trees)
--
-- Let's implement:
-- 1. abstract syntax trees
-- 2. an interpreter
-- 3. a virtual machine
-- 4. a compiler
-- 5. a correctness proof that the compiler compiles correctly
-- The Agda datatype of abstract syntax trees
data Expr : Set where
lit : ℕ → Expr
add : Expr → Expr → Expr
example : Expr
example = add (lit zero) (add (lit two) (lit three))
-- "0 + (2 + 3)"
-- The interpreter for our toy programming language
eval : Expr → ℕ
eval (lit x) = x
eval (add t t') = eval t + eval t'
open import Padova2025.ProvingBasics.Equality.Base
_ : eval example ≡ five
_ = refl
-- The Agda type of operations supported by our virtual machine
data Op : Set where
PUSH : ℕ → Op
SUM : Op
-- Our virtual machine is a so-called "stack machine".
-- As memory, it has a stack of numbers.
-- The PUSH operation adds a new number onto the stack.
-- The SUM operation removes the upper-most two numbers from the stack and replaces
-- them with their sum.
open import Padova2025.ProgrammingBasics.Lists
-- The Agda type of programs for our virtual machine
Code : Set
Code = List Op
-- The Agda type of stacks for our virtual machine
Stack : Set
Stack = List ℕ
-- `run` takes as input machine code and the current state of the stack
-- and outputs the new state of the stack after the code was executed.
run : Code → Stack → Stack
run [] s = s
run (PUSH x ∷ cs) s = run cs (x ∷ s)
run (SUM ∷ cs) (x ∷ y ∷ s) = run cs (y + x ∷ s)
run _ _ = []
_ : run (PUSH two ∷ PUSH three ∷ SUM ∷ []) [] ≡ (five ∷ [])
_ = refl
-- The task of `compile t c` is to output code, more precisely code which
-- has the purpose of pushing `eval t` on the stack but then continues with `c`.
compile : Expr → Code → Code
compile (lit x) c = PUSH x ∷ c
compile (add t t') c = compile t (compile t' (SUM ∷ c))
-- The `compile` function reads as input an expression of our toy programming language
-- and outputs code suitable for running on our virtual machine. More precisely,
-- `compile t` should be code which, when run on our virtual machine, pushes `eval t`
-- on the stack.
compile₀ : Expr → Code
compile₀ t = compile t []
-- Logical reading: For every expression `t` and for every code `c` and for every stack `s`,
-- running the compilation of `t` (with tail `c`) with `s` as the initial state of stack
-- results in whatever running `c` on the enlarged stack where the topmost element is `eval t` results in.
--
-- Logical reading: For every expression `t` and for every code `c` and for every stack `s`,
-- running the compilation of `t` (with tail `c`) with `s` as the initial state of stack
-- has the same effect as running c in the enlarged stack `eval t ∷ s`.
open import Padova2025.ProvingBasics.Equality.Reasoning.Core
theorem : (t : Expr) (c : Code) (s : Stack) → run (compile t c) s ≡ run c (eval t ∷ s)
theorem (lit x) c s = refl
theorem (add t t') c s = begin
run (compile (add t t') c) s ≡⟨ refl ⟩
run (compile t (compile t' (SUM ∷ c))) s ≡⟨ theorem t _ s ⟩
run (compile t' (SUM ∷ c)) (eval t ∷ s) ≡⟨ theorem t' _ (eval t ∷ s) ⟩
run (SUM ∷ c) (eval t' ∷ eval t ∷ s) ≡⟨ refl ⟩
run c (eval t + eval t' ∷ s) ≡⟨ refl ⟩
run c (eval (add t t') ∷ s) ∎
-- Option 1: Fill in this hole on the projector (using equational reasoning) [1]
-- Option 2: You try to fill in this hole (or do other exercises) [4]
-- Option 3: Classical logic in Agda [2]
theorem₀ : (t : Expr) → run (compile₀ t) [] ≡ (eval t ∷ [])
theorem₀ t = theorem t [] []