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)