From 3dbd9f8d007782e0b227c7873519fb9de2b19079 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 17 Apr 2021 02:44:06 -0700 Subject: [PATCH] Add more homework solutions. --- HomeworkEleven.idr | 42 +++++++++++++++++++++++++++++++++++++++++ HomeworkFifteen.idr | 44 +++++++++++++++++++++++++++++++++++++++++++ HomeworkSeventeen.idr | 28 +++++++++++++++++++++++++++ HomeworkSixteen.idr | 40 +++++++++++++++++++++++++++++++++++++++ HomeworkTen.idr | 34 +++++++++++++++++++++++++++++++++ HomeworkThirteen.idr | 18 ++++++++++++++++++ HomeworkTwelve.idr | 22 ++++++++++++++++++++++ 7 files changed, 228 insertions(+) create mode 100644 HomeworkEleven.idr create mode 100644 HomeworkFifteen.idr create mode 100644 HomeworkSeventeen.idr create mode 100644 HomeworkSixteen.idr create mode 100644 HomeworkTen.idr create mode 100644 HomeworkThirteen.idr create mode 100644 HomeworkTwelve.idr diff --git a/HomeworkEleven.idr b/HomeworkEleven.idr new file mode 100644 index 0000000..c4543c1 --- /dev/null +++ b/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) diff --git a/HomeworkFifteen.idr b/HomeworkFifteen.idr new file mode 100644 index 0000000..8b8ef00 --- /dev/null +++ b/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) diff --git a/HomeworkSeventeen.idr b/HomeworkSeventeen.idr new file mode 100644 index 0000000..796413a --- /dev/null +++ b/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 diff --git a/HomeworkSixteen.idr b/HomeworkSixteen.idr new file mode 100644 index 0000000..8e181ce --- /dev/null +++ b/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 diff --git a/HomeworkTen.idr b/HomeworkTen.idr new file mode 100644 index 0000000..459a110 --- /dev/null +++ b/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 diff --git a/HomeworkThirteen.idr b/HomeworkThirteen.idr new file mode 100644 index 0000000..eb86810 --- /dev/null +++ b/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))) diff --git a/HomeworkTwelve.idr b/HomeworkTwelve.idr new file mode 100644 index 0000000..14e764d --- /dev/null +++ b/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))