From 202ef8c368d08a3af27655e71772febdd7554351 Mon Sep 17 00:00:00 2001
From: Kjetil Orbekk <kjetil.orbekk@gmail.com>
Date: Mon, 13 Feb 2017 19:09:52 -0500
Subject: Exercises from Idris book.

Chapters 8 and 9.
---
 DepType.idr  |  5 +++-
 Theorems.idr | 87 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 91 insertions(+), 1 deletion(-)
 create mode 100644 Theorems.idr

diff --git a/DepType.idr b/DepType.idr
index 54ac7ad..f85a595 100644
--- a/DepType.idr
+++ b/DepType.idr
@@ -1,4 +1,6 @@
 module DepType
+  
+import Data.Fin
 
 isSingleton : Bool -> Type
 isSingleton True = Nat
@@ -16,4 +18,5 @@ data MyVect : Nat -> Type -> Type where
 (++) [] ys = ys
 (++) (x :: xs) ys = x :: xs ++ ys
 
--- The finite sets.
+length : MyVect n a -> Nat
+length xs {n} = n
diff --git a/Theorems.idr b/Theorems.idr
new file mode 100644
index 0000000..f3d1984
--- /dev/null
+++ b/Theorems.idr
@@ -0,0 +1,87 @@
+module Theorems
+  
+import Data.Vect
+  
+%default total
+  
+fiveIsFive : 5 = 5
+fiveIsFive = Refl
+  
+plusReduces : (n:Nat) -> plus Z n = n
+plusReduces n = Refl
+  
+plusReducesZ : (n:Nat) -> plus n Z = n
+plusReducesZ Z = Refl
+plusReducesZ (S k) = cong (plusReducesZ k)
+
+plus' : Nat -> Nat -> Nat
+plus' Z     m = m
+plus' (S k) m = S (plus' k m)
+  
+plus_commutes_Z : m = plus' m 0
+plus_commutes_Z {m = Z} = Refl
+plus_commutes_Z {m = (S k)} = rewrite plus_commutes_Z {m=k} in Refl
+                              
+plus_commutes_S : (k,m : Nat) -> S (plus m k) = plus m (S k)                             
+plus_commutes_S k Z = Refl
+plus_commutes_S k (S j) = rewrite plus_commutes_S  k j in Refl
+
+plus_commutes : (n, m : Nat) -> plus' n m = plus' m n
+plus_commutes Z     m = plus_commutes_Z
+plus_commutes (S k) m = rewrite plus_commutes k m in plus_commutes_S k m
+
+plus_assoc    : (n, m, k : Nat) -> plus' n (plus' m k) = plus' (plus' n m) k
+plus_assoc Z m k = Refl
+plus_assoc (S j) m k = rewrite plus_assoc j m k in Refl
+
+same_lists : {xs : List a} -> {ys : List a} -> x = y -> xs = ys
+            -> x :: xs = y :: ys
+same_lists {x = x} {y = x} {xs = ys} {ys = ys} Refl Refl = Refl
+ 
+data ThreeEq : (x, y, z : Nat) -> Type where
+  Equals : ThreeEq x x x
+
+allSameS : (x, y, z : Nat) -> ThreeEq x y z -> ThreeEq (S x) (S y) (S z)
+allSameS z z z Equals = Equals
+
+plusCommutes2 : (n : Nat) -> (m : Nat) -> n + m = m + n
+plusCommutes2 Z m = rewrite plusZeroRightNeutral m in Refl
+plusCommutes2 (S k) m = rewrite plusCommutes2 k m in
+                        plusSuccRightSucc m k
+
+headUnequal : DecEq a => {xs : Vect n a} -> {ys : Vect n a} ->
+              (contra : (x = y) -> Void) -> (x :: xs = y :: ys) -> Void
+headUnequal contra Refl = contra Refl
+  
+tailUnequal : DecEq a => {xs : Vect n a} -> {ys : Vect n a} ->
+              (contra : (xs = ys) -> Void) -> ((x :: xs) = (y :: ys)) -> Void
+tailUnequal contra Refl = contra Refl
+ 
+[myimpl] DecEq a => DecEq (Vect n a) where
+    decEq [] [] = Yes Refl
+    decEq (x :: xs) (y :: ys) = case decEq x y of
+      Yes Refl => case decEq xs ys of
+        Yes Refl => Yes Refl
+        No contra => No (tailUnequal contra)
+      No contra => No (headUnequal contra)
+  
+data Last : List a -> a -> Type where
+  LastOne : Last [value] value
+  LastCons : (prf : Last xs value) -> Last (x :: xs) value
+
+notInNil : (Last [] value) -> Void
+notInNil LastOne impossible
+notInNil (LastCons _) impossible
+  
+lastDiff : (x = y -> Void) -> Last [x] y -> Void
+lastDiff contra LastOne = contra Refl
+lastDiff contra (LastCons prf) = notInNil prf
+
+isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value)
+isLast [] value = No notInNil
+isLast [x] value = case decEq x value of
+  Yes Refl => Yes LastOne
+  No contra => No (lastDiff contra)
+isLast (x :: x' :: xs) value = case isLast (x' :: xs) value of
+  Yes prf => Yes (LastCons prf)
+  No contra => No (\(LastCons prf) => contra prf)
-- 
cgit v1.2.3