import Data.Vect
import Syntax.PreorderReasoning
import even
import lecture_11
import lecture_12
% default total
% auto_implicits on
-- Recall the Functor, Applicative, and Monad instances for Vect n:
implementation [VectFunctor] Functor (Vect n) where
-- map : (a -> b) -> Vect n a -> Vect n b
map f [] = []
map f (x :: xs) = f x :: map f xs
implementation [VectApplicative] Applicative (Vect n) where
-- pure : a -> Vect n a
pure {n = Z} x = []
pure {n = (S n)} x = x :: pure x
-- (<*>) : Vect n (a -> b) -> Vect n a -> Vect n b
[] <*> [] = []
(f :: fs) <*> (x :: xs) = f x :: (fs <*> xs)
implementation [VectMonad] Monad (Vect n) where
-- join : Vect n (Vect n a) -> Vect n a
join [] = []
join (xs :: xss) = head xs :: join (map tail xss)
-- Working with equality assumptions:
-- This one is easy, just case analyse the assumptions:
plus_cong : {m₀ , m₁ , n₀ , n₁ : Nat} -> m₀ = m₁ -> n₀ = n₁ -> m₀ + n₀ = m₁ + n₁
plus_cong Refl Refl = Refl
-- For this one, case analysing the assumption doesn't help,
-- because Idris doesn't know that not is injective (that's what we're trying to show!)
not_injective : (not a) = (not b) -> a = b
not_injective {a = False} {b = False} prf = Refl
not_injective {a = False} {b = True} prf = sym prf
not_injective {a = True} {b = False} prf = sym prf
not_injective {a = True} {b = True} prf = Refl
-- Using transport (i.e. replace) to move between types
-- via an equation between their indices:
{-
Even (S m + n) Even (m + S n)
________ ________
/ \ / \
/ p \ transport Even path / tr... p \
| | ------------------> | |
\ / \ /
\________/ \________/
path
S m + n =============================== m + S n : Nat
-}
even_plus_succ : {m , n : Nat} -> Even (S m + n) -> Even (m + S n)
even_plus_succ {m = m} {n = n} = replace {P = Even} $
(S m + n)
={ plus_succ_left }=
(S (m + n))
={ sym plus_succ_right }=
(m + S n)
QED