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 _,_
      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
  -- key bindings: https://agda.readthedocs.io/en/v2.6.1.3/getting-started/quick-guide.html
  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
     : 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 ℓ
   : 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))
three' : 
three' = 3

-- Whenever we say n or m and they haven't been bound, they refer to natural numbers
  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
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
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


-- 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)