The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

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

Attachment: signature.asc
Description: OpenPGP digital signature