Can I prove (s: Stream a) & # 8594; (head s :: tail s = s) in Idris?

Question

The following proof of Idris does not validate type.

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

The error I am getting is:

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

Similar proof for non-empty Vect typechecks is just fine:

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

So, I guess the problem is Stream laziness.

---

My working theory is that Idris does not like to simplify everything inside Delay , because it can end up in an endless loop this way. However, I want to force Idris to go down in all directions, as the definition of Prelude.Stream.tail ensures that the LHS then decreases to x :: Delay xs , completing my proof.

Is my suspicion right? And can I somehow fix the evidence?

Answer 1

Yes, it can be done. I used the 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