Co-inductive proofs?

[Carl Factora]

Hi,

I'm trying to see what Idris can do with a proof like this (I've included a screenshot and the file):

I'm trying to prove that two Streams of nats are equivalent. I've included the error that I get (which I don't understand). I've seen something like this done in Coq, but I want to see how it's done in Idris

Anything helps.

[David Feuer]

I think you meant

StreamEq ones ones'

rather than

ones seq ones'

in the type signature for the simple theorem.

--
You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Carl Factora]

Hello again, David.

Make sense, since that's actually the type (derp). What are the commands for handling codata? I get this as the beginning of the proof:

----------                 Goal:                  ----------
{hole0} : StreamEq (1 :: Delay (repeat 1))   (1 :: Delay (map S (0 :: Delay (repeat 0))))

I think it would be best to make the constructors to appear (i.e. seq).

[Carl Factora]

I also thought that maybe of a proof of:

map_repeat_thm : (f : a -> b) -> map f (repeat a) = repeat b

would help, but I'm not sure if it's necessary.

[David Feuer]

Dunno. I've never used coinduction.

[Carl Factora]

I see. Seems to be the norm as of the moment. I've been trying to find something about co-induction in Idris for about 2 weeks now.

[Brian McKenna]

Here's how to use coinduction to prove Stream's functor laws:

http://stackoverflow.com/q/30448651/108359

I think you've gotten close but I'd avoid using head and tail in the seq constructor and instead turn them into variables, just constructing a StreamEq of the right type.