Can I prove (s : Stream a) -> (head s :: tail s = s) in Idris?

Question

The following Idris proof doesn’t typecheck.

hts : (s : Stream a) -> (head s :: tail s = s)
hts (x::xs) = Refl

The error I get is:

    Type mismatch between
            x :: Delay xs = x :: Delay xs
    and
            x :: Delay (tail (x :: Delay xs)) = x :: Delay xs

A similar proof for non-empty Vects typechecks just fine:

import Data.Vect
htv : (s : Vect (S k) a) -> (head s :: tail s = s)
htv (x::xs) = Refl

So I’m guessing the issue is in the laziness of Stream.

---

My working theory is that Idris doesn’t like simplifying whatever is inside of Delay, because it might get into an infinite loop that way. However, I want to coerce Idris to dip its toes in anyway, as the definition of Prelude.Stream.tail guarantees that the LHS would then reduce to x :: Delay xs, completing my proof.

Is my suspicion correct? And can I fix the proof somehow?

Answer 1

Yes, it can be done. I used an auxiliary congruence lemma:

%default total

consCong : {xs, ys : Stream a} -> (x : a) -> xs = ys -> x :: xs = x :: ys
consCong _ Refl = Refl

to prove the main lemma:

hts : (s : Stream a) -> (head s :: tail s = s)
hts (x :: xs) = consCong _ $ Refl