## Tutorials.Monday-Complete

Tutorials.Monday-Complete
open import Agda.Primitive using (Level)
module Tutorials.Monday-Complete where

-- Two dashes to comment out the rest of the line
{-
Opening {-
and closing -}
for a multi-line comment
-}

-- In Agda all the tokens are tokenised using whitespace (with the exception of parentheses and some other symbols)
-- Agda offers unicode support
-- We can input unicode using the backslash \ and (most of the time) typing what one would type in LaTeX
-- If in emacs, we can put the cursor over a characted and use M-x describe-char to see how that character is inputted
-- ⊥ is written using \bot
data ⊥ : Set where
-- AKA the empty set, bottom, falsehood, the absurd type, the empty type, the initial object
-- ⊥ : Set means ⊥ is a Type (Set = Type, for historical reasons)
-- The data keyword creates a data type where we list all the constructors of the types
-- ⊥ has no constructors: there is no way of making something of type ⊥

record ⊤ : Set where
-- AKA the singleton set, top, truth, the trivial type, the unit type, the terminal object
-- The record keyword creates a record type
-- Records have a single constructor
-- To create a record you must populate all of its fields
-- ⊤ has no fields: it is trivial to make one, and contains no information
constructor tt

data Bool : Set where
-- Bool has two constructors: one bit worth of information
true : Bool
false : Bool

--------
-- Simple composite types
--------

module Simple where
record _×_ (A : Set) (B : Set) : Set where
-- AKA logical and, product type

-- Agda offers support for mixfix notation
-- We use the underscores to specify where the arguments goal
-- In this case the arguments are the type parameters A and B, so we can write A × B

-- A × B models a type packing up *both* an A *and* a B
-- A and B are type parameters, both of type Set, i.e. types
-- A × B itself is of type Set, i.e. a type
-- We use the single record constructor _,_ to make something of type A × B
-- The constructor _,_ takes two parameters: the fields fst and snd, of type A and B, respectively
-- If we have a of type A and b of type B, then (a , b) is of type A × B
constructor _,_
field
fst : A
snd : B

-- Agda has a very expressive module system (more on modules later)
-- Every record has a module automatically attached to it
-- Opening a record exposes its constructor and it fields
-- The fields are projection functions out of the record
-- In the case of _×_, it exposes
-- fst : A × B → A
-- snd : A × B → B
open _×_

data _⊎_ (A B : Set) : Set where
-- AKA logical or, sum type, disjoint union
-- A ⊎ B models a type packing *either* an A *or* a B
-- A and B are type parameters, both of type Set, i.e. types
-- A ⊎ B itself is of type Set, i.e. a type
-- A ⊎ B has two constructors: inl and inr
-- The constructor inl takes something of type A as an argument and returns something of type A ⊎ B
-- The constructor inr takes something of type B as an argument and returns something of type A ⊎ B
-- We can make something of type A ⊎ B either by using inl and supplying an A, or by using inr and supplying a B
inl : A → A ⊎ B
inr : B → A ⊎ B

--------
-- Some simple proofs!
--------

-- In constructive mathematics logical implication is modelled as function types
-- An object of type A → B shows that assuming an object of type A, we can construct an object of type B
-- Below we want to show that assuming an object of type A × B, we can construct an object of type A
-- We want to show that this is the case regardless of what A and B actually are
-- We do this using a polymorphic function that is parametrised over A and B, both of type Set
-- We use curly braces {} to make these function parameters implicit
-- When we call this function we won't have to supply the arguments A and B unless we want to
-- When we define this function we won't have to accept A and B as arguments unless we want to
-- The first line below gives the type of the function get-fst
-- The second line gives its definition
get-fst : {A : Set} {B : Set} → A × B → A
get-fst (x , y) = x

-- Agda is an *interactive* proof assistant
-- We don't provide our proofs/programs all at once: we develop them iteratively
-- We write ? where we don't yet have a program to provide, and we reload the file
-- What we get back is a hole where we can place the cursor and have a conversation with Agda
-- ctrl+c is the prefix that we use to communicate with Agda
-- ctrl+c ctrl+l     reload the file
-- ctrl+c ctrl+,     shows the goal and the context
-- ctrl+c ctrl+.     shows the goal, the context, and what we have so far
-- ctrl+c ctrl+c     pattern matches against a given arguments
-- ctrl+c ctrl+space fill in hole
-- ctrl+c ctrl+r     refines the goal: it will ask Agda to insert the first constructor we need
-- ctrl+c ctrl+a     try to automatically fulfill the goal
get-snd : ∀ {A B} → A × B → B
get-snd (x , y) = y

-- The variable keyword enables us to declare convention for notation
-- Unless said otherwise, whenever we refer to A, B or C and these are not bound, we will refer to objects of type Set
variable
ℓ : Level
A B C : Set ℓ

-- Notice how we don't have to declare A, B and C anymore
curry : (A → B → C) → (A × B → C)
curry f (a , b) = f a b

uncurry : (A × B → C) → (A → B → C)
uncurry f a b = f (a , b)

×-comm : A × B → B × A
×-comm (a , b) = b , a

×-assoc : (A × B) × C → A × (B × C)
×-assoc ((a , b) , c) = a , (b , c)

-- Pattern matching has to be exhaustive: all cases must be addressed
⊎-comm : A ⊎ B → B ⊎ A
⊎-comm (inl x) = inr x
⊎-comm (inr x) = inl x

⊎-assoc : (A ⊎ B) ⊎ C → A ⊎ (B ⊎ C)
⊎-assoc (inl (inl x)) = inl x
⊎-assoc (inl (inr x)) = inr (inl x)
⊎-assoc (inr x) = inr (inr x)

-- If there are no cases to be addressed there is nothing for us left to do
-- If you believe ⊥ exist you believe anything
absurd : ⊥ → A
absurd ()

-- In constructive mathematics all proofs are constructions
-- How do we show that an object of type A cannot possibly be constructed, while using a construction to show so?
-- We take the cannonically impossible-to-construct object ⊥, and show that if we were to assume the existence of A, we could use it to construct ⊥
¬_ : Set ℓ → Set ℓ
¬ A = A → ⊥

-- In classical logic double negation can be eliminated: ¬ ¬ A ⇒ A
-- That is however not the case in constructive mathematics:
-- The proof ¬ ¬ A is a function that takes (A → ⊥) into ⊥, and offers no witness for A
-- The opposite direction is however constructive:
⇒¬¬ : A → ¬ ¬ A
⇒¬¬ a f = f a

-- Moreover, double negation can be eliminated from non-witnesses
¬¬¬⇒¬ : ¬ ¬ ¬ A → ¬ A
¬¬¬⇒¬ f a = f (⇒¬¬ a)

-- Here we have a choice of two programs to write
×-⇒-⊎₁ : A × B → A ⊎ B
×-⇒-⊎₁ (a , b) = inl a

×-⇒-⊎₂ : A × B → A ⊎ B
×-⇒-⊎₂ (a , b) = inr b

-- A little more involved
-- Show that the implication (A ⊎ B → A × B) is not always true for all A and Bs
⊎-⇏-× : ¬ (∀ {A B} → A ⊎ B → A × B)
⊎-⇏-× f = snd (f {A = ⊤} {B = ⊥} (inl tt))

-- -> \to → \-> → \forall ∀ \ell ℓ
variable
ℓ : Level
A B C : Set ℓ

--------
-- Inductive data types
--------
-- \bN ℕ
data ℕ : Set where
-- The type of unary natural numbers
-- The zero constructor takes no arguments; the base case
-- The suc constructor takes one argument: an existing natural number; the inductive case
-- We represent natural numbers by using ticks: ||| ≈ 3
-- zero: no ticks
-- suc: one more tick
-- suc (suc (suc zero)) ≈ ||| ≈ 3
zero : ℕ
suc  : ℕ → ℕ

three : ℕ
three = suc (suc (suc zero))

-- Compiler pragmas allow us to give instructions to Agda
-- They are introduced with an opening {-# and a closing #-}
-- Here we the pragma BUILTIN to tell Agda to use ℕ as the builtin type for natural numbers
-- This allows us to say 3 instead of suc (suc (suc zero))
{-# BUILTIN NATURAL ℕ #-}
three' : ℕ
three' = 3

-- Whenever we say n or m and they haven't been bound, they refer to natural numbers
variable
n m l : ℕ

-- Brief interlude: we declare the fixity of certain functions
-- By default, all definitions have precedence 20
-- The higher the precedence, the tighter they bind
-- Here we also declare that _+_ is left associative, i.e. 1 + 2 + 3 is parsed as (1 + 2) + 3
infixl 20 _+_
-- x + y + z ≡ (x + y) + z

-- Define addition of natural numbers by structural recursion
_+_ : ℕ → ℕ → ℕ
zero + y = y
(suc x) + y = suc (x + y)

-- In functions recursion must always occur on structurally smaller values (otherwise the computation might never terminate)
-- In Agda *all computations must terminate*
-- We can tell Agda to ignore non-termination with this pragma
{-# TERMINATING #-}
non-terminating : ℕ → ℕ
non-terminating n = non-terminating n

-- However, doing so would allow us to define elements of the type ⊥
-- This is not considered safe: running Agda with the --safe option will make type-checking fail
{-# TERMINATING #-}
loop : ⊥
loop = loop

-- Use structural recursion to define multiplication
_*_ : ℕ → ℕ → ℕ
zero * y = zero
suc x * y = y + (x * y)

-- The module keyword allows us to define modules (namespaces)
module List where
infixr 15 _∷_ _++_
data List (A : Set) : Set where
-- Lists are another example of inductive types
-- The type parameter A is the type of every element in the list
-- They are like natural numbers, but the successor case contains an A
[]  : List A
_∷_ : A → List A → List A

example₁ : List Bool
example₁ = true ∷ false ∷ []  -- [true, false]

-- List concatenation by structural recursion
_++_ : List A → List A → List A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

-- Apply a function (A → B) to every element of a list
map : (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

-- A base case B and an inductive case A → B → B is all we need to take a List A and make a B
foldr : (A → B → B) → B → List A → B
foldr f b [] = b
foldr f b (x ∷ xs) = f x (foldr f b xs)

--------
-- Dependent Types
--------

-- Dependent types are types that depend on values, objects of another type
-- Dependent types allow us to model predicates on types
-- A predicate P on a type A is a function taking elements of A into types
Pred : Set → Set₁
Pred A = A → Set

-- Let us define a predicate on ℕ that models the even numbers
-- Even numbers are taken to the type ⊤, which is trivial to satisfy
-- Odd numbers are taken to the type ⊥, which is impossible to satisfy
Even : Pred ℕ
Even zero = ⊤
Even (suc zero) = ⊥
Even (suc (suc x)) = Even x

-- We can now use Even as a precondition on a previous arguments
-- Here we bind the first argument of type ℕ to the name n
-- We then use n as an argument to the type Even
-- As we expose the constructors of n, Even will compute
half : (n : ℕ) → Even n → ℕ
half zero n-even = zero
half (suc (suc n)) n-even = suc (half n n-even)

-- There is an alternative way of definiting dependent types
-- EvenData is a data type indexed by elements of the type ℕ
-- That is, for every (n : ℕ), EvenData n is a type
-- The constructor zero constructs an element of the type EvenData zero
-- The constructor 2+_ takes an element of the type EvenData n and constructs one of type EvenData (suc (suc n))
-- Note that there is no constructors that constructs elements of the type Evendata (suc zero)
data EvenData : ℕ → Set where -- Pred ℕ
zero : EvenData zero
2+_  : EvenData n → EvenData (suc (suc n))

-- We can use EvenData as a precondition too
-- The difference is that while Even n computes automatically, we have to take EvenData n appart by pattern matching
-- It leaves a trace of *why* n is even
half-data : (n : ℕ) → EvenData n → ℕ
half-data zero zero = zero
half-data (suc (suc n)) (2+ n-even) = suc (half-data n n-even)

-- Function composition: (f ∘ g) composes two functions f and g
-- The result takes the input, feeds it through g, then feeds the result through f
infixr 20 _∘_
_∘_ : (B → C) → (A → B) → (A → C)
(f ∘ g) x = f (g x)

--------
-- Example of common uses of dependent types
--------

module Fin where
-- The type Fin n has n distinct inhabitants
data Fin : ℕ → Set where
zero : Fin (suc n)
suc  : Fin n → Fin (suc n)

-- Note that there is no constructor for Fin zero
Fin0 : Fin zero → ⊥
Fin0 ()

-- We can erase the type level information to get a ℕ back
to-ℕ : Fin n → ℕ
to-ℕ zero = zero
to-ℕ (suc x) = suc (to-ℕ x)

module Vec where
open Fin

-- Vectors are like lists, but they keep track of their length
-- The type Vec A n is the type of lists of length n containing values of type A
-- Notice that while A is a parameter (remains unchanged in all constructors), n is an index
-- We can bind parameters to names (since they don't change) but we cannot bind indices
data Vec (A : Set) : ℕ → Set where
[]  : Vec A zero
_∷_ : A → Vec A n → Vec A (suc n)

-- Now we can define concatenation, but giving more assurances about the resulting length
_++_ : Vec A n → Vec A m → Vec A (n + m)
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

map : (A → B) → Vec A n → Vec B n
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

-- Given a vector and a fin, we can use the latter as a lookup index into the former
-- Question: what happens if there vector is empty?
_!_ : Vec A n → Fin n → A
(x ∷ xs) ! zero = x
(x ∷ xs) ! suc i = xs ! i

-- A vector Vec A n is just the inductive form of a function Fin n → A
tabulate : ∀ {n} → (Fin n → A) → Vec A n
tabulate {n = zero}  f = []
tabulate {n = suc n} f = f zero ∷ tabulate (f ∘ suc)

untabulate : Vec A n → (Fin n → A)
untabulate [] ()
untabulate (x ∷ xs) zero = x
untabulate (x ∷ xs) (suc i) = untabulate xs i

-- Predicates need not be unary, they can be binary! (i.e. relations)
Rel : Set → Set₁
Rel A = A → A → Set

-- Question: how many proofs are there for any n ≤ m
data _≤_ : Rel ℕ where
z≤n :         zero  ≤ n
s≤s : n ≤ m → suc n ≤ suc m

_<_ : ℕ → ℕ → Set
n < m = suc n ≤ m

-- _≤_ is reflexive and transitive
≤-refl : ∀ n → n ≤ n
≤-refl zero = z≤n
≤-refl (suc n) = s≤s (≤-refl n)

≤-trans : n ≤ m → m ≤ l → n ≤ l
≤-trans z≤n b = z≤n
≤-trans (s≤s a) (s≤s b) = s≤s (≤-trans a b)

-----------
-- Propositional Equality
-----------

-- Things get interesting: we can use type indices to define propositional equality
-- For any (x y : A) the type x ≡ y is a proof showing that x and y are in fact definitionally equal
-- It has a single constructor refl which limits the ways of making something of type x ≡ y to those where x and y are in fact the same, i.e. x ≡ x
-- When we pattern match against something of type x ≡ y, the constructor refl will make x and y unify: Agda will internalise the equality
infix 10 _≡_
-- \== ≡
data _≡_ (x : A) : A → Set where
refl : x ≡ x

{-# BUILTIN EQUALITY _≡_ #-}

-- Definitional equality holds when the two sides compute to the same symbols
2+2≡4 : 2 + 2 ≡ 4
2+2≡4 = refl

-- Because of the way in which defined _+_, zero + x ≡ x holds definitionally (the first case in the definition)
+-idˡ : ∀ x → (zero + x) ≡ x
+-idˡ x = refl

-- We show that equality respects congruence
cong : {x y : A} (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl

-- However this does not hold definitionally
-- We need to use proof by induction
-- We miss some pieces to prove this
+-idʳ : ∀ x → (x + zero) ≡ x
+-idʳ zero = refl
+-idʳ (suc x) = cong suc (+-idʳ x)

example₃ : ∀ x → (1 + x) + zero ≡ (1 + x)
example₃ x = +-idʳ _

+-idʳ′ : ∀ {x} → (x + zero) ≡ x
+-idʳ′ {x} = +-idʳ x

example₄ : ∀ x → (1 + x) + zero ≡ (1 + x)
example₄ x = +-idʳ′

-- Propositional equality is reflexive by construction, here we show it is also symmetric and transitive
sym : {x y : A} → x ≡ y → y ≡ x
sym refl = refl

trans : {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl q = q

-- A binary version that will come in use later on
cong₂ : {x y : A} {w z : B} (f : A → B → C) → x ≡ y → w ≡ z → f x w ≡ f y z
cong₂ f refl refl = refl

-- Leibniz equality, transport
subst : {x y : A} {P : Pred A} → x ≡ y → P x → P y
subst refl p = p

-- Now we can start proving slightly more interesting things!
+-assoc : ∀ x y z → (x + y) + z ≡ x + (y + z)
+-assoc zero y z = refl
+-assoc (suc x) y z = cong suc (+-assoc x y z)

+-suc : ∀ x y → x + (suc y) ≡ (suc x) + y
+-suc zero y = refl
+-suc (suc x) y = cong suc (+-suc x y)

-- Introduce underscores on the RHS
+-comm : ∀ x y → x + y ≡ y + x
+-comm x zero = +-idʳ _
+-comm x (suc y) = trans (+-suc _ _) (cong suc (+-comm x y))
-- The keyword where allows us to introduce local definitions

-----------
-- Some tooling for equational reasoning
-----------

infix  3 _∎
infixr 2 step-≡
infix  1 begin_

begin_ : ∀{x y : A} → x ≡ y → x ≡ y
begin_ x≡y = x≡y

step-≡ : ∀ (x {y z} : A) → y ≡ z → x ≡ y → x ≡ z
step-≡ _ y≡z x≡y = trans x≡y y≡z

syntax step-≡  x y≡z x≡y = x ≡⟨  x≡y ⟩ y≡z

_∎ : ∀ (x : A) → x ≡ x
_∎ _ = refl

-- The equational resoning style allows us to explicitly write down the goals at each stage
-- This starts to look like what one would do on the whiteboard
+-comm′ : ∀ x y → x + y ≡ y + x
+-comm′ x zero = +-idʳ _
+-comm′ x (suc y) = begin
(x + suc y)  ≡⟨ +-suc _ _ ⟩
suc (x + y)  ≡⟨ cong suc (+-comm′ x y) ⟩
suc (y + x)  ∎