Add more homework solutions.

HomeworkEleven.idr

@@ -0,0 +1,42 @@
+module HomeworkEleven
+%default total
+
+data Move = Up | Rgt | Seq Move Move | Rev Move
+
+Vec : Type
+Vec = (Int, Int)
+
+add : Vec -> Vec -> Vec
+add (x1, y1) (x2, y2) = (x1+x2, y1+y2)
+
+neg : Vec -> Vec
+neg (x1, y1) = (negate x1, negate y1)
+
+sem : Move -> Vec
+sem Up = (0, 1)
+sem Rgt = (1, 0)
+sem (Seq s1 s2) = sem s1 `add` sem s2
+sem (Rev s1) = neg $ sem s1
+
+data Final : Move -> Vec -> Type where
+  FUp : Final Up (0, 1)
+  FRgt : Final Rgt (1, 0)
+  FSeq : Final s1 v1 -> Final s2 v2 -> Final (Seq s1 s2) (v1 `add` v2)
+  FRev : Final s v -> Final (Rev s) (neg v)
+
+finalEx : Final ((Up `Seq` Up) `Seq` Rgt) (1, 2)
+finalEx = (FUp `FSeq` FUp) `FSeq` FRgt
+
+finalSem : Final s v -> sem s = v
+finalSem FUp = Refl
+finalSem FRgt = Refl
+finalSem (FRev f) with (finalSem f) | Refl = Refl
+finalSem (FSeq f1 f2) with (finalSem f1, finalSem f2) | (Refl, Refl) = Refl
+
+semFinal : sem s = v -> Final s v
+semFinal {s=Up} Refl = FUp
+semFinal {s=Rgt} Refl = FRgt
+semFinal {s=Rev s1} Refl with (sem s1) proof p1
+  | _ = FRev (semFinal (sym p1))
+semFinal {s=Seq s1 s2} Refl with (sem s1, sem s2) proof p
+  | (_, _) = let Refl = p in FSeq (semFinal Refl) (semFinal Refl)

HomeworkFifteen.idr

@@ -0,0 +1,44 @@
+module HomeworkFifteen
+%default total
+
+data Term = Tru | Fls | Not Term | Cond Term Term Term
+
+data Et : Term -> Type where
+  ETru : Et Tru
+  EFls : Et (Not Fls)
+  ENot : Et t -> Et (Not (Not t))
+  ECondT : Et tc -> Et tt -> Et (Cond tc tt te)
+  ECondF : Et (Not tc) -> Et te -> Et (Cond tc tt te)
+
+ex1 : Et (Not (Not (Not Fls)))
+ex1 = ENot EFls
+
+ex2 : Et (Cond Tru (Not Fls) Tru)
+ex2 = ECondT ETru EFls
+
+ex3 : Et (Cond Fls Fls Tru)
+ex3 = ECondF EFls ETru
+
+infixl 5 !!
+
+data (!!) : Term -> Term -> Type where
+  STru : Tru !! Tru
+  SFls : Fls !! Fls
+  SNotT : t !! Tru -> Not t !! Fls
+  SNotF : t !! Fls -> Not t !! Tru
+  SCondT : tc !! Tru -> tt !! v -> (Cond tc tt te) !! v
+  SCondF : tc !! Fls -> te !! v -> (Cond tc tt te) !! v
+
+lemma : Et t -> t !! Tru
+lemma ETru = STru
+lemma EFls = SNotF SFls
+lemma (ENot e) = SNotF $ SNotT $ lemma e
+lemma (ECondT c t) = SCondT (lemma c) (lemma t)
+lemma (ECondF c e) with (lemma c)
+  | SNotF pc = SCondF pc (lemma e)
+
+lemma' : t !! Tru -> Et t
+lemma' STru = ETru
+lemma' (SNotF f) = ?stuckHere
+lemma' (SCondT tc tt) = ECondT (lemma' tc) (lemma' tt)
+lemma' (SCondF tc te) = ECondF (lemma' $ SNotF tc) (lemma' te)

HomeworkSeventeen.idr

@@ -0,0 +1,28 @@
+module HomeworkSeventeen
+
+%default total
+
+data Prog = Push Nat | Pop | Add | Seq Prog Prog
+
+Stack : Type
+Stack = List Nat
+
+data BS : Stack -> Prog -> Stack -> Type where
+  BS_Push : BS s (Push n) (n::s)
+  BS_Pop  : BS (n::s) Pop s
+  BS_Add  : BS (n::m::s) Add (n+m::s)
+  BS_Seq  : BS s p s0 -> BS s0 q s' -> BS s (Seq p q) s'
+
+pushPop : BS s (Push n `Seq` Pop) s
+pushPop = BS_Seq BS_Push BS_Pop
+
+sumProg : BS s ((Push n1 `Seq` Push n2) `Seq` Add) ((n2+n1)::s)
+sumProg = (BS_Push `BS_Seq` BS_Push) `BS_Seq` BS_Add
+
+gen : Nat -> Prog
+gen Z = Seq (Seq (Push 1) (Push 1)) Add
+gen (S n) = Seq (Seq (gen n) (Push 1)) Add
+
+p : (n : Nat) -> BS s (gen n) ((n+2)::s)
+p Z = sumProg
+p (S m) = ((p m) `BS_Seq` BS_Push) `BS_Seq` BS_Add

HomeworkSixteen.idr

@@ -0,0 +1,40 @@
+module HomeworkSixteen
+
+%default total
+
+data Term = T | F | Q | And Term Term
+
+data Val : Term -> Type where
+  ValT : Val T
+  ValF : Val F
+  ValQ : Val Q
+
+infixl 10 |->
+data (|->) : Term -> Term -> Type where
+  AndFirst : (t1 |-> t1') -> (And t1 t2) |-> (And t1' t2)
+  AndSecond : Val t1 -> (t2 |-> t2') -> (And t1 t2) |-> (And t1 t2')
+  AndF : Val t2 -> And F t2 |-> F
+  AndT : Val t2 -> And T t2 |-> t2
+  AndQF : And Q F |-> F
+  AndQT : And Q T |-> Q
+  AndQQ : And Q Q |-> Q
+
+infixl 10 |-->
+data (|-->) : Term -> Term -> Type where
+  AndLFirst : (t1 |--> t1') -> (And t1 t2) |--> (And t1' t2)
+  AndLSecond : Val t1 -> (t2 |--> t2') -> (And t1 t2) |--> (And t1 t2')
+  AndLF : And F t2 |--> F
+  AndLT : And T t2 |--> t2
+  AndLQF : And Q F |--> F
+  AndLQT : And Q T |--> Q
+  AndLQQ : And Q Q |--> Q
+
+infixl 10 !!
+data (!!) : Term -> Term -> Type where
+  SemT : T !! T
+  SemF : F !! F
+  SemQ : Q !! Q
+  SemAndF : t1 !! F -> And t1 t2 !! F
+  SemAndT : t1 !! T -> t2 !! v -> And t1 t2 !! v
+  SemAndQF : t1 !! Q -> t2 !! F -> And t1 t2 !! F
+  SemAndQ : t1 !! Q -> Either (t2 !! T) (t2 !! Q) -> And t1 t2 !! Q

HomeworkTen.idr

@@ -0,0 +1,34 @@
+module HomeworkTen
+%default total
+
+data Less : Nat -> Nat -> Type where
+  Suc : Less n (S n)
+  Trans : Less k n -> Less n m -> Less k m
+
+data Sorted : List Nat -> Type where
+  SortedEmpty : Sorted []
+  SortedSingle : Sorted [x]
+  SortedCons : Less x y -> Sorted (y::tail) -> Sorted (x::y::tail)
+
+threeLessThanFive : Less 3 5
+threeLessThanFive = Trans Suc Suc
+
+threeFiveSorted : Sorted [3,5]
+threeFiveSorted = SortedCons threeLessThanFive SortedSingle
+
+tailSorted : Sorted (x::xs) -> Sorted xs
+tailSorted SortedEmpty impossible
+tailSorted SortedSingle = SortedEmpty
+tailSorted (SortedCons _ st) = st
+
+firstSecondLess : Sorted (x::y::xs) -> Less x y
+firstSecondLess SortedEmpty impossible
+firstSecondLess SortedSingle impossible
+firstSecondLess (SortedCons l _) = l
+
+removeSecondSorted : Sorted (x::y::xs) -> Sorted (x::xs)
+removeSecondSorted SortedEmpty impossible
+removeSecondSorted SortedSingle impossible
+removeSecondSorted (SortedCons _ SortedEmpty) impossible
+removeSecondSorted (SortedCons _ SortedSingle) = SortedSingle
+removeSecondSorted (SortedCons lxy (SortedCons lyr t)) = SortedCons (Trans lxy lyr) t

HomeworkThirteen.idr

@@ -0,0 +1,18 @@
+module HomeworkThirteen
+%default total
+
+infix 0 <=>
+(<=>) : Type -> Type -> Type
+a <=> b = (a -> b, b -> a)
+
+exA : (p, q) <=> (q, p)
+exA = (swap, swap)
+
+exB : (p, (q, r)) <=> ((p, q), r)
+exB = (\(a, (b, c)) => ((a, b), c), \((a, b), c) => (a, (b, c)))
+
+pair : a -> b -> (a,b)
+pair a b = (a, b)
+
+exC : (p, Either q r) <=> Either (p, q) (p, r)
+exC = (\(p, eqr) => either (Left . pair p) (Right . pair p) eqr, either (\(p, q) => (p, Left q)) (\(p, r) => (p, Right r)))

HomeworkTwelve.idr

@@ -0,0 +1,22 @@
+module HomeworkTwelve
+%default total
+
+data Op = Push Nat | Pop | Add
+
+Stack : Type 
+Stack = List Nat
+
+data Step : Stack -> Op -> Stack -> Type where
+  SPush : Step xs (Push n) (n::xs)
+  SPop : Step (n::xs) Pop xs
+  SAdd : Step (n1::n2::xs) Add ((n1+n2)::xs)
+
+Ops : Type
+Ops = List Op
+
+data Steps : Stack -> Ops -> Stack -> Type where
+  SEmpty : Steps xs [] xs
+  SSeq : Step xs o ys -> Steps ys os zs -> Steps xs (o::os) zs
+
+stepsEx : Steps [] [Push 3, Push 5, Add] [8]
+stepsEx = SSeq SPush (SSeq SPush (SSeq SAdd SEmpty))