Tutorials.Thursday-Complete

Tutorials.Thursday-Complete
{-# OPTIONS --guardedness #-}

import Tutorials.Monday-Complete as Mon
import Tutorials.Tuesday-Complete as Tue
import Tutorials.Wednesday-Complete as Wed
open Mon using (; tt; ; zero; suc)
open Mon.Simple using (_⊎_; inl; inr)
open Tue.Product using (Σ; _,_; fst; snd; _×_)

module Tutorials.Thursday-Complete where

variable
A B C S : Set

-- Things that we skipped so far
--------------------------------

module WithAbstraction where
open Mon using (Bool; true; false; Pred; _≡_; refl; _+_; subst; +-comm)
open Mon.List using (List; []; _∷_)

-- With abstraction
-- You can use "with abstraction" to pattern match on intermediary computations
-- These can be nested, or executed simultaneously

filter : (A  Bool)  List A  List A
filter f [] = []
filter f (x  xs) with f x
filter f (x  xs) | true = x  filter f xs
filter f (x  xs) | false = filter f xs

-- Alternative notation
filter′ : (A  Bool)  List A  List A
filter′ f [] = []
filter′ f (x  xs) with f x
...                | true = x  filter′ f xs
...                | false = filter′ f xs

-- The goal type and the type of the arguments are generalised over the value of the scrutinee
thm : {P : Pred } (n m : )  P (n + m)  P (m + n)
-- 1) Here (p : P (n + m)) and (eq : n + m ≡ m + n)
-- thm n m p with +-comm n m
-- thm n m p | eq = {!!}
-- 2) Here (p : P x) and (eq : x ≡ m + n)
-- thm n m p with n + m | +-comm n m
-- thm n m p | x | eq = {!!}
-- 3) Pattern matching we get (p : P (m + n)), the dot signifies that the argument is uniquely determined
thm n m p with n + m | +-comm n m
thm n m p | .(m + n) | refl = p

-- This is such a common formula that there is special syntax for it
thm′ : {P : Pred } (n m : )  P (n + m)  P (m + n)
thm′ {P} n m pr rewrite +-comm n m = pr

-- We could use subst to be more explicit about *where* the rewrite happens
thm′′ : {P : Pred } (n m : )  P (n + m)  P (m + n)
thm′′ {P} n m p = subst {P = P} (+-comm n m) p

-- A little on coinductive types
--------------------------------

-- Stolen from https://github.com/pigworker/CS410-17/blob/master/lectures/Lec6Done.agda

ListT : Set  Set  Set
ListT X B =   (X × B)

module List where
data List (A : Set) : Set where
[] : List A
_∷_ : A  List A  List A

mkList : ListT A (List A)  List A
mkList (inl tt) = []
mkList (inr (a , as)) = a  as

foldr : (ListT A B  B)  List A  B
foldr alg [] = alg (inl tt)
foldr alg (x  xs) = alg (inr (x , foldr alg xs))

list-id : List A  List A
list-id = foldr mkList

incr : ListT A
incr (inl tt) = zero
incr (inr (_ , n)) = suc n

length : List A
length = foldr incr

module CoList where
record CoList (A : Set) : Set where
coinductive
field
-- next : ⊤ ⊎ (A × CoList A)
next : ListT A (CoList A)

open CoList

[] : CoList A
next [] = inl tt

_∷_ : A  CoList A  CoList A
next (x  xs) = inr (x , xs)

unfoldr : (S  ListT A S)  S  CoList A
next (unfoldr coalg s) with coalg s
next (unfoldr coalg s) | inl tt = inl tt
next (unfoldr coalg s) | inr (a , s') = inr (a , unfoldr coalg s')

repeat : A  CoList A
repeat = unfoldr λ x  inr (x , x)

take :   CoList A  List.List A
take zero xs = List.[]
take (suc n) xs with next xs
take (suc n) xs | inl tt = List.[]
take (suc n) xs | inr (a , xs') = a List.∷ take n xs'

module Stream where
record Stream (A : Set) : Set where
coinductive
field
tail : Stream A

open Stream

forever : A  Stream A
tail (forever x) = forever x

unfold : (S  A × S)  S  Stream A
head (unfold coalg s) = fst (coalg s)
tail (unfold coalg s) = unfold coalg (snd (coalg s))

---------------------------------------------
-- If you are interested in more