Idris Vect shrinking

gistfile1.idr

module Main

data ElemMV : (f : Fin (S n)) -> a -> Vect n a -> Type where
  NotThereMV : ElemMV fZ x xs
  HereMV : ElemMV f x xs -> ElemMV (fS f) x (x :: xs) 
  ThereMV : ElemMV f x xs -> ElemMV (weaken f) x (y :: xs)

elemMV : DecEq a => (x : a) -> (xs : Vect n a) -> (f ** (ElemMV f x xs))
elemMV x [] = (fZ ** NotThereMV)
elemMV x (y :: xs) with (decEq x y)
  elemMV x (x :: xs) | (Yes refl) with (elemMV x xs)
    elemMV x (x :: xs) | (Yes refl) | (f ** elt) = ((fS f) ** HereMV elt)
  elemMV x (y :: xs) | (No notThere) with (elemMV x xs)
    elemMV x (y :: xs) | (No notThere) | (f ** elt) = ((weaken f) ** ThereMV elt)


finRest : (f : Fin (S n)) -> Fin (S n)
finRest {n = Z} fZ = fZ  
finRest {n = (S m)} fZ = fS (finRest fZ) 
finRest {n = Z} (fS fp) with (fp)
  finRest {n = Z} (fS fp) | fZ impossible
finRest {n = (S m)} (fS fp) = weaken (finRest fp) 

finRestZ : (n : Nat) -> finToNat (finRest (fZ {k = n})) = n
finRestZ Z = refl
finRestZ (S k) = let inductiveHypthesis = finRestZ k in ?finRestZ_rhs_2

finWeakenToNat : (f : Fin n) -> finToNat f = finToNat (weaken f)
finWeakenToNat fZ = refl
finWeakenToNat (fS fp) = let inductiveHypothesis = finWeakenToNat fp in ?finWeakenToNat_rhs_2

weakenfSCommutative : (f : Fin n) -> fS (weaken f) = weaken (fS f)
weakenfSCommutative fZ = refl
weakenfSCommutative (fS fp) = ?weakenfSCommutative_rhs_2

finRestWeaken : (f : Fin (S l)) -> fS (finRest f) = finRest (weaken f)
finRestWeaken fZ = refl
finRestWeaken {l = S (lp)} (fS fp) = let inductiveHypothesis = finRestWeaken fp
                                         wc = weakenfSCommutative (finRest fp)
                                     in ?finRestWeaken_rhs_2


shrinkMV : (x : a) -> (v: Vect n a) -> (ElemMV f x v) -> Vect (finToNat (finRest f)) a
shrinkMV {n=n} {f=fZ} x xs NotThereMV = rewrite finRestZ n in xs 
shrinkMV {n=(S np)} {f} x (y :: xs) prf with (prf)
  shrinkMV {n=(S np)} {f=(fS fp)} x (x :: xs) prf | (HereMV elt) = rewrite sym(finWeakenToNat (finRest fp)) in shrinkMV x xs elt
  shrinkMV {n=(S np)} {f=(weaken fp)} x (y :: xs) prf | (ThereMV elt) = rewrite sym(finRestWeaken fp) in y :: (shrinkMV x xs elt)

x : Int
x = 3 

xs : Vect 4 Int
xs = 2 :: 1 :: 2 :: 3 :: Nil

e : (f ** ElemMV f x xs)
e = elemMV x xs

shrunk : String
shrunk with (e)
  shrunk | (_ ** pf) = show $ shrinkMV x xs pf

main : IO ()
main = putStrLn shrunk 

---------- Proofs ----------

Main.finRestWeaken_rhs_2 = proof
  intros
  rewrite inductiveHypothesis
  trivial


Main.weakenfSCommutative_rhs_2 = proof
  intros
  trivial


Main.finWeakenToNat_rhs_2 = proof
  intros
  rewrite inductiveHypothesis 
  trivial


Main.finRestZ_rhs_2 = proof
  intros
  rewrite inductiveHypthesis
  trivial