:PROPERTIES:
:ID:       3aef24fd-b220-4408-aa1e-c3538d661b62
:END:
#+title: afp_lec_1
#+filetags: :notes:uni:
<2025-01-21 Tue> 
[[file:~/master-folder/Uni/ADVFUNC/afp-learning-2024-2025/files/LectureNotes/files/introduction.lagda.md][Week 1 Handout]]
* Week 1 lec 1
if you want to put a hole in the file (ie the { }1 ) then put a ? and load the file

types are default called 'sets' in agda but we will call them types. 

data Bool : Type where
 true false : Bool

Here we create a type called Bool

--

data Maybe (A : Type) : Type where
 nothing : Maybe A
 just    : A → Maybe A

Given the type A we produce another type 
Then we have two constructors, we can actually call them whatever we want, the only rule is that it shouldnt have spaces in the middle. For example, instead of nothing we can call 'nothing' as 'Nothingljfsdsdj'.

The below is known as coercion or the disjoint union
Considering Blah = Either ℕ Bool
left 0: Blah
right false: Blah

--

data ℕ : Type where
 zero : ℕ
 suc  : ℕ → ℕ

-- 4 = suc (suc (suc (suc zero)))

--

data List (A : Type) : Type where
 []   : List A
 _::_ : A → List A → List A

Below is a function that maps a type to a type:
myList : Type -> Type
myList = List

-- N -> Type ... this is called 'Dependant Type' which depends on elements of another type.
When it comes to types, its often the case where the language we use doesnt exactly define the type we want it to. For example in haskell, the binary tree, when we want to use the binary search tree its a little difficult. In agda we can define a precise type; including the binary search tree. In summary agda can write precise types.

-- 

if_then_else_ : {A : Type} → Bool → A → A → A
if true then x else y = x
if false then x else y = y

this above is known as mixfix operation, we use the _ to denote where the arguments of the function are going to be places

--

_+_ : ℕ → ℕ → ℕ
zero + y = y
suc x + y = suc (x + y)

here we can pattern match on any of x or y
in haskell, recursion can be done and there arent restrictions on it. in Agda we have structural recursion as there is a termination on recursion. Structural recursion is when you follow the structure of the definition, for example in suc x + y, we get suc (x + y), we keep removing the x from suc until we are left with 0. scrcpy

--

_*_ : ℕ → ℕ → ℕ
zero * y = zero
suc x * y = x * y + y

for suc x * y:
(1 + x) * y
y + x * y

in infixr, the r means the brackets are explicitly on the right, if we use infixl then its on the left:
x + y + z
x + (y + z) : r
(x + y) + z : l

-- research implicit arguements.


reverse : {A : Type} → List A → List A
reverse [] = []
reverse (x :: xs) = reverse xs ++ [ x ]

although this program works, its inefficient. 

rev-append : {A : Type} → List A → List A → List A
rev-append []        ys = ys
rev-append (x :: xs) ys = rev-append xs (x :: ys)

rev : {A : Type} → List A → List A
rev xs = rev-append xs []

the revappend is a helper function. you can see theres no ++ (concatenation) involved. 
* Week 1 lec 2

N-Induction : (P: N -> Type)
   -> P 0
   -> ((k:N) -> Pk (P (suc k))
choose k = 0
 
P0 : P0
f0 p1 : P1
f1 p2 : p2

   -> (n:N) -> Pn

This is proof by induction,

ℕ-induction P p0 f 0 = P0
ℕ-induction P p0 f(suc n) = goal
where
  ℍ : Pn
  ℍ = ℕ-induction P p0 f n

ℕ-induction P p0 f 3 =
              f3(f2(f1 p0))
essentially this is a for loop.

--
indstep : (k:N) -> k≣k -> suc k ≣ suc k
indstep k e = e

ℕ-refl n = ℕ-induction (λx -> x≣x) * (λke -> e)

introduction and elimination rules


--
List-induction : { x : Type }
               -> (P : List X -> Type)
               -> P []
               -> ((x:X)(xs:List X) -> Pxs -> P(x::xs))
               
               -> (xs : List X ) -> P xs

List-induction 


* Keybindings:
- C-c C-l : to load the agda file
- SPC-w for the windows
- C-c C-c : case split (agda mode) (put x, or b or whatever the first one is, then use this - very useful).
- C-c C-SPC: give: tries to fill the hole
- C-shift - : undo
- C-c C-r : refine
- C-c C-, : show the context