The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

Hi Greg,

I have actually thought a lot recently about modeling non-terminating systems, and have mostly come to a similar conclusion as you, that (nat-> A) equivalent to (Stream A), and that the former does not require co-inductive types (which I don't like for a number of theoretical and practical reasons).

Adam has actually defined a non-termination monad based upon this idea, which you can find if you google for "non-termination monad" (or you can probably just ask him). If you are interested, I was also working on a non-termination monad transformer a few months ago, that adds a similar notion of non-termination to any monad, and I can send it to you if you are interested.

-Eddy

Sent from my iPhone

On Dec 7, 2015, at 11:06 AM, Gregory Malecha <gmalecha AT gmail.com> wrote:

Thanks, Pierre-Marie --

At the moment I just prove that this are [Proper], which isn't really too big of a problem since you can define combinators that handle the properness proofs for the most part. I guess I'm wondering more from a model point of view, are there any corner cases that one definition covers that the other does not?

If the co-inductive lists could also be finite, i.e. with this definition

CoInductive ftrace (st : Type) : Type :=

| Cons : st -> ftrace st -> ftrace st

| Done.

Then with functions you need to add some notion of "equal up to the occurrence of 'Done'" which is a bit cumbersome to express. But it seems that for truly infinite, non-dependent structures you might always be able to play this trick of "functions from paths to values". Is that the case, or is there a reason to prefer the CoInductive definition?

On Mon, Dec 7, 2015 at 10:48 AM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

On 07/12/2015 19:11, Gregory Malecha wrote:
> To reason about the first I use co-induction and I do not need
> functional extensionality.

You'll actually need some form of extensionality to use it with ease.
Indeed, you cannot disprove the following in Coq, and it's pretty useful
in practical use:

CoInductive trace (state : Type) : Type :=
| Cons : state -> trace state -> trace state.

CoInductive bisimilar {state} : trace state -> trace state -> Prop :=
| Bisimilar : forall s t1 t2, bisimilar t1 t2 -> bisimilar (Cons _ s t1)
(Cons _ s t2).

Axiom trace_extensionality : forall state (t1 t2 : trace state),
bisimilar t1 t2 -> t1 = t2.

If you don't assume it, you'll have to show that all of your predicates
are Proper (and they meta-are), just like for the functional case.

PMP

--

gregory malecha