The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

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