Idris rewrite did not change the type

Question

I'm trying to prove that after splitting a Vect into three parts, every parts' length is less equal than the original vector. And here is my implementation:

||| Split into three parts: two lists and a single element
data Sp : Type -> Type where
 MkSp : List a -> a -> List a -> Sp a

||| cons an element into the left list
spConsL : a -> Sp a -> Sp a
spConsL x (MkSp xs y ys) = MkSp (x :: xs) y ys

||| split a vector according to a predicate
sp : (a -> Bool) -> Bool -> Vect (S l) a -> Sp a
sp f b (x :: []) = MkSp [] x []
sp f False (x :: (y :: xs)) =
  let s' = sp f (f x) (y :: xs)
  in  spConsL x s'
sp f True (x :: xs) = MkSp [] x (toList xs)

||| get the left list from a split
lSp : Sp a -> List a
lSp (MkSp xs x ys) = xs


spConsLEq : {x : a} -> {s : Sp a} ->
            x :: (lSp s) = lSp (spConsL x s)
spConsLEq {x} {s = (MkSp xs y ys)} = Refl


lSpLTE : (vect : Vect (S len) a) ->
         (p : a -> Bool) ->
         (b : Bool) ->
         length (lSp (sp p b vect)) `LTE` S len
lSpLTE (x :: []) p b = LTEZero
lSpLTE (x :: (y :: xs)) p True = LTEZero
lSpLTE (x :: (y :: xs)) p False =
  let ih = lSpLTE (y :: xs) p (p x)
  in  rewrite sym spConsLEq in
      ?lSpLTE_rhs_1

But unfortunately, idris will raise an error:

rewriting
  lSp (spConsL x s) to x :: lSp s
did not change type
  (length
    (lSp (spConsL x (sp p (p x) (y :: xs)))))
  `LTE`
  (S (S len))

And even after I introduced s as following, the error still occurred

rewrite sym $ spConsLEq {s = sp p (p x) (y :: xs)}

So why cannot rewrite work here?

Jeroen Noels Jeroen Noels · Accepted Answer · 2018-05-15T20:02:00

I do not have a satisfying answer to the "why?" question, but you are very close to a complete proof. With the following modification, the rewrite succeeds:

let ih = lSpLTE (y :: xs) p (p x)
    rule = spConsLEq {x} {s = sp p (p x) (y :: xs)}
in rewrite sym rule in ?hole

And substituting LTESucc ih for the hole completes the proof:

rewrite sym eq in LTESucc ih

So it seems both {s} and {x} must be supplied to spConsLEq, and LTESucc fullfils the role of the following lemma:

lemma : {xs : List a} -> LTE (length xs) k -> LTE (length (_ :: xs)) (S k)
lemma = LTESucc

Idris rewrite did not change the type

1 Answers