exercises.idr

module partition

%default total

even : Nat -> Bool
even x = (mod x 2) == 0

partition' : (a -> Bool) -> List a -> List a
partition' f [] = []
partition' f (x :: xs) with (partition' f xs)
 | fxs = 
   if f x then
     x :: fxs
   else fxs

part : (a -> Bool) -> Vect n a ->  ((m ** Vect m a), (o ** Vect o a))
part f [] = ((_ ** []),(_ ** []))
part f (x :: xs) with (part f xs)
  | ((j ** ys), (k ** zs)) =
    if (f x) then
      (((S j) ** x :: ys), (k ** zs))
   else
      ((j ** ys), ((S k) ** x :: zs))


rev : Vect n a -> Vect n a
rev = rev' [] 
  where
    rev' : Vect m a -> Vect n a -> Vect (m + n) a
    rev' ys [] ?= ys
    rev' ys (x::xs) ?= rev' (x :: ys) xs

rev'_lemma_1 = proof 
  intros
  rewrite sym $ plusZeroRightNeutral m
  trivial

rev'_lemma_2 = proof
  intros
  rewrite (plusSuccRightSucc m n1)
  trivial

filter' : (a -> Bool) -> Vect n a -> (m ** Vect m a)
filter' f [] = (_ ** [])
filter' f (x :: xs) with (filter' f xs)
                      | (k ** ys) = 
                      if f x then 
                        ((S k) ** (x :: ys))
                      else
                        (k ** ys)


vtake : {n : Nat} -> (m : Fin (S n)) -> Vect n a -> Vect (cast m) a
vtake fZ _ = []
vtake (fS x) [] = FinZElim x
vtake (fS x) (y :: xs) = y :: take x xs

vdrop : {n : Nat} -> (m : Fin (S n)) -> Vect n a -> Vect (n - (cast m)) a
vdrop fZ xs ?= xs
vdrop (fS x) [] = FinZElim x
vdrop (fS x) (_ :: xs) = vdrop x xs

vdrop_lemma_1 = proof
  intros
  rewrite sym (minusZeroRight n)
  trivial

repeat : (n : Nat) -> a -> Vect n a
repeat Z _ = []
repeat (S k) x = x :: repeat k x

Matrix' : Nat -> Nat -> Type -> Type
Matrix' n m a = Vect n (Vect m a)

trans : Matrix' n m a -> Matrix' m n a
trans [] = repeat _ []
trans (x::xs) = zipWith (::) x (trans xs)

data Cmp : Nat -> Nat -> Type where
  cmpLT : (y : Nat) -> Cmp x (x + S y)
  cmpEQ : Cmp x x
  cmpGT : (x : Nat)-> Cmp (y + S x) y

cmp : (n : Nat) -> (m : Nat) -> Cmp n m
cmp Z Z = cmpEQ
cmp Z (S j) = cmpLT j
cmp (S j) Z = cmpGT j
cmp (S j) (S k) with (cmp j k)
  cmp (S i) (S i) | cmpEQ = cmpEQ
  cmp (S i) (S (i + (S l))) | cmpLT l = cmpLT l
  cmp (S (i + (S l))) (S i) | cmpGT l = cmpGT l

plus_nSm : (n : Nat) -> (m : Nat) -> n + S m = S (n + m)
plus_nSm n m = ?plus_nSm_rhs1

partition.plus_nSm_rhs1 = proof {
  intros
  induction n
  compute
  trivial
  intros
  compute
  rewrite ihn__0
  trivial
}

plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
plus_commutes n m = ?plus_commutes_rhs

plus_commutes_rhs = proof {
  intros
  induction m
  compute
  rewrite sym $ plusZeroRightNeutral n
  trivial
  intros
  compute
  rewrite ihn__0
  rewrite sym $ plusSuccRightSucc n n__0
  trivial
}

plus_assoc : (n : Nat) -> (m : Nat) -> (p : Nat) -> n + (m + p) = (n + m) + p
plus_assoc n m p = ?plus_assoc_rhs

plus_assoc_rhs = proof {
  intros
  induction n
  compute
  trivial
  intros
  compute
  rewrite ihn__0
  trivial
}