module transcript07 where
{-
Plan for today:
0. Questions
1. Program verification
2. Sets as trees? (Aczel's celebrated model of set theory in type theory)
3. Limitations of Standard Agda? (and their resolution in Cubical Agda)
4. Exercises?
Poll:
A. One more example for program verification,
namely implementing a toy programming language (the "Hello World of Agda")
B. Sets as trees -- let's continue at 17:15
C. Limitations of Standard Agda
D. Exercises
-}
-- Two approaches to program verification.
-- Approach 1: Post-hoc verification.
-- Approach 2: Correct by construction.
open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic
open import Padova2025.ProgrammingBasics.Booleans
open import Padova2025.ProgrammingBasics.Lists
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General
open import Padova2025.ProvingBasics.Connectives.Disjunction hiding (eq?)
open import Padova2025.ProvingBasics.Negation
------ Approach 1: Post-hoc verification.
module FirstSteptsWithVerification where
-- This function should evaluate to true if and only if
-- the two inputs are the same.
eq? : ℕ → ℕ → Bool
eq? zero zero = true
eq? zero (succ y) = false
eq? (succ x) zero = false
eq? (succ x) (succ y) = eq? x y
eq?-correct₁ : (x y : ℕ) → eq? x y ≡ true → x ≡ y
eq?-correct₁ zero zero p = refl
eq?-correct₁ (succ x) (succ y) p = cong succ (eq?-correct₁ x y p)
succ-injective : {x y : ℕ} → succ x ≡ succ y → x ≡ y
succ-injective refl = refl
eq?-correct₂ : (x y : ℕ) → x ≡ y → eq? x y ≡ true
eq?-correct₂ zero zero p = refl
eq?-correct₂ (succ x) (succ y) p = eq?-correct₂ x y (succ-injective p)
------ Approach 2: Correct by construction.
dec : (x y : ℕ) → x ≡ y ⊎ x ≢ y
dec zero zero = left refl
dec zero (succ y) = right (λ ())
dec (succ x) zero = right (λ ())
dec (succ x) (succ y) with dec x y
... | left x≡y = left (cong succ x≡y)
... | right x≢y = right (λ p → x≢y (succ-injective p))
{-
- Correct-by-construction is often shorter than
post-hoc verification.
- The return values of correct-by-construction functions
are more informative than mere Booleans.
- Post-hoc verification disentangles the implementation
from the verification.
-}
-- Next, let's have a more complex example: insertion sort.
module Implementation
(A : Set)
(_≤_ : A → A → Set)
(cmp : (x y : A) → x ≤ y ⊎ y ≤ x) where
-- "insert x ys" should be the same list as "ys",
-- but with "x" inserted at a suitable location;
-- if "ys" is ascendingly ordered, so should be "insert x ys".
insert : A → List A → List A
insert x [] = x ∷ []
insert x (y ∷ ys) with cmp x y
... | left x≤y = x ∷ y ∷ ys
... | right y≤x = y ∷ insert x ys
sort : List A → List A
sort [] = []
sort (x ∷ xs) = insert x (sort xs)
module Verification
(A : Set)
(_≤_ : A → A → Set)
(cmp : (x y : A) → x ≤ y ⊎ y ≤ x) where
open Implementation A _≤_ cmp
-- The type "IsOrdered xs" is the type of witnesses
-- that the list "xs" is ascendingly ordered.
data IsOrdered : List A → Set where
empty : IsOrdered []
singleton : {x : A} → IsOrdered (x ∷ [])
cons
: {x y : A} {ys : List A}
→ x ≤ y → IsOrdered (y ∷ ys)
→ IsOrdered (x ∷ y ∷ ys)
lemma : (x : A) (ys : List A) → IsOrdered ys → IsOrdered (insert x ys)
lemma x [] p = singleton
lemma x (y ∷ ys) p with cmp x y
... | left x≤y = cons x≤y p
... | right y≤x = {!!}
theorem : (xs : List A) → IsOrdered (sort xs)
theorem [] = empty
theorem (x ∷ xs) = lemma x (sort xs) (theorem xs)
module CorrectByConstruction
(A : Set)
(_≤_ : A → A → Set)
(min : A) -- "minus infinity"
(min! : (x : A) → min ≤ x)
(cmp : (x y : A) → x ≤ y ⊎ y ≤ x) where
-- "OList l" is the type of ordered lists whose elements
-- are bounded from below by l (i.e. all elements are ≥ l).
data OList (l : A) : Set where
nil : OList l
cons : (x : A) → l ≤ x → (ys : OList x) → OList l
insert : {l : A} (x : A) → l ≤ x → OList l → OList l
insert x l≤x nil = cons x l≤x nil
insert x l≤x (cons y l≤y ys) with cmp x y
... | left x≤y = cons x l≤x (cons y x≤y ys)
... | right y≤x = cons y l≤y (insert x y≤x ys)
sort : List A → OList min
sort [] = nil
sort (x ∷ xs) = insert x (min! x) (sort xs)
module SetsAsTrees where
-- To a first approximation, sets and types are identical: Both are containers for elements.
-- But there are important differences:
-- 1. In set theory, there is a global membership relation: For any set x and for any set y,
-- the question "x ∈ y" is well-formed. In contrast, in type theory "x : y" is
-- a judgment (never an interesting question).
-- 2. In set theory, the question "x ∈ y" is interesting. In type theory, the judgment
-- "x : y" is decidable.
-- A central motto of set theory is to always keep going in creating new sets.
-- Aczel's "sets as trees" model is a model of a certain flavor of set theory in type theory,
-- where this motto is nicely visible. We will introduce a type V of sets, and we will
-- introduce a global membership relation _∈_ : V → V → Set, and we will introduce
-- constants like ∅ : V or N : V, and we will introduce operations like _∪_ : V → V → V.
data T : Set where
E : T -- empty
F : T → T → T -- fork
-- This is the type of (unbalanced) trees which can either be empty
-- (just a leaf) or a binary fork.
{-
* * E
/ \
/ \
* * F E (F E E) *
/ \ / \ F E E
* * * *
-}
total-amount-of-nodes : T → ℕ
total-amount-of-nodes E = one
total-amount-of-nodes (F x y) = succ (total-amount-of-nodes x + total-amount-of-nodes y)
data T' : Set where
E : T' -- empty
F₂ : T' → T' → T' -- binary fork
F₃ : T' → T' → T' → T' -- ternary fork
example : T'
example = F₂ E (F₃ E E E)
{-
*
/ \
* *
/|\
* * *
-}
-- Aczel's idea was to represent sets as (arbitrarily-branching) trees.
{-
The empty set is represented by the following tree: *
The set { x, {1,2,3}, y } is represented by the following tree:
*
/|\
/ | \
x * y
/|\
1 2 3
The set of natural numbers is represented by the following tree:
*
/|\ \ \
0 1 2 ......
-}
-- Introducing V, the type of all sets (actually the type of arbitrarily-branching trees).
-- This type is not a small type (unlike ℕ, Bool, ℕ → ℕ, ...). Instead, it is a large
-- type (contained in Set₁ instead of Set).
data V : Set₁ where
sup : {I : Set} → (I → V) → V -- "supremum"
∅ : V
∅ = sup {⊥} empty-function
where
empty-function : ⊥ → V
empty-function ()
-- { ∅ }, the singleton set which contains exactly one element, namely the empty set
-- (Note: { ∅ } ≠ ∅.)
ex : V
ex = sup {𝟙} f
where
data 𝟙 : Set where
tt : 𝟙
f : 𝟙 → V
f tt = ∅
-- { ∅, {∅} }
ex' : V
ex' = sup {Bool} f
where
f : Bool → V
f false = ∅
f true = ex
{-
Here is how to construct the natural numbers in set theory, starting from
just the empty set.
0 ≔ ∅ = {}
1 ≔ { 0 } = { {} } = next(0)
2 ≔ { 0, 1 } = { {}, {{}} } = next(1)
3 ≔ { 0, 1, 2 } = { {}, {{}}, {{},{{}}} } = next(2)
⋮
Where next(x) = x ∪ {x}.
-}
next : V → V
next x@(sup {I} f) = sup {J} g
where
data J : Set where
new : J
old : I → J
g : J → V
g new = x
g (old i) = f i
-- The following function converts Agda's natural numbers into set theory's numbers.
fromℕ : ℕ → V
fromℕ zero = ∅
fromℕ (succ x) = next (fromℕ x)
-- The set of natural numbers
N : V
N = sup {ℕ} fromℕ
the-set-of-all-sets : V
the-set-of-all-sets = {!sup {V} id!} -- accepted only with the option --type-in-type
where
id : V → V
id x = x
-- In ordinary set theory (but not in so-called "non-wellfounded set theory"),
-- every set is wellfounded. Approximately this means the following:
-- A set IS allowed to contain other sets as elements. And these are again allowed
-- to container yet other sets as elements. And so on. But there may NOT be an
-- infinite chain: x ∋ y ∋ z ∋ w ∋ a ∋ ...
-- In Standard Agda, we can verify that V satisfies all the axioms of CZF
-- (but not of IZF, nor ZF nor ZFC).
-- In IZF, ZF and ZFC, we have the powerset axiom: Every set has a powerset.
-- For every set x there is a set y whose elements are all the subsets of x.
-- IZF = CZF + Powerset
-- ZF = IZF + LEM (law of excluded middle)
-- ZFC = ZF + Axiom of choice
-- It is a fact of life that in Agda we cannot verify that V validates the powerset axiom.
-- The powerset of a set in V would be a set in V₁.
-- In set theory, we have the iterative conception of sets: Starting from the empty set,
-- we can construct more and more sets over time. One of several ways of constructing
-- sets is by the "axiom of separation": If X is a set and A(x) is a statement containing
-- a free variable x, then we can form the set { x ∈ X | A(x) } ("set comprehension").
-- (E.g.: Given ℕ, we can form the set ℙ = { n ∈ ℕ | n is prime }.) As we obtain more
-- sets over time, over time we will also be able to form new subsets of old sets
-- because we have more means available for expressing statements.
-- So far so good. The powerset axiom crashes this idea: It allows us to construct
-- the powerset of a given a set X in a single step, in one go.
-- So the powerset axiom (together with unbounded separation)
-- destroys the otherwise-natural order of sets coming into being
-- over time. For instance:
-- The set ℕ comes into being on day ω. The set of algebraic numbers
-- (like √2, √2+i, but not π) comes into being on day (roughly) ω + 1.
-- With the set of algebraic numbers at hand, we can construct the following new subset of ℕ:
-- { n ∈ ℕ | the n-th roots of unity are constructible by ruler and compass }.
-- This set comes into being on day ω + 2.
-- This is the reason why some people prefer their mathematics to be predicative.
-- (Standard Zermelo--Fraenkel set theory with the powerset axiom is called impredicative.)
-- In predicative mathematics, we distinguish between unbounded separation and bounded separation.
-- Unbounded separation: "If X is any set, and if A(x) is any statement, then { x ∈ X | A(x) } exists."
-- Bounded separation: "If X is any set, and if A(x) is any bounded statement, then { x ∈ X | A(x) } exists."
-- (A statement is bounded if and only if all quantifiers are of the form "∀a∈b" or "∃a∈b", but NOT
-- of the unbounded form "∀a" or "∃a".)
-- Using impredicativity, we can do "constructions" as follows:
-- Given a vector space V and a subset M ⊆ V, we can form the smallest subspace containing M as follows:
-- span(M) ≔ ⋂ { W ⊆ V | W is a subspace containing M }.
-- In predicative mathematics, this "construction" is no longer allowed. But the smallest subspace containing M
-- still exists, by the following more concrete construction:
-- span(M) ≔ the set of linear combinations of elements of M.