The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

Hi Daniel,

this is coinduction and is not provable in Coq - this is basically the same 
issue as for functional extensionality. If you have functional extensionality 
you can encode coinductive types so that coinduction is provable but this may 
be a bit inconvenient. The extensionality axiom can be eliminated as we have 
described a few years ago in our "Observational Type Theory, now" paper which 
appeared in PLPV 08.

Cheers,
Thorsten

On 26 Apr 2011, at 17:56, Daniel Schepler wrote:

> I was looking at proving monad properties of:
> 
> CoInductive Coroutine (X:Type) : Type :=
> | coroutine_return : X -> Coroutine X
> | yield_with_continuation : Coroutine X -> Coroutine X.
> 
> Implicit Arguments coroutine_return [[X]].
> Implicit Arguments yield_with_continuation [[X]].
> 
> I was eventually able to prove the necessary identities, assuming the axiom:
> 
> CoInductive coroutine_eq {X} : Coroutine X -> Coroutine X -> Prop :=
> | coroutine_return_eq: forall x0:X,
>    coroutine_eq (coroutine_return x0) (coroutine_return x0)
> | yield_eq: forall x y:Coroutine X, coroutine_eq x y ->
>    coroutine_eq (yield_with_continuation x) (yield_with_continuation y).
> Axiom coroutine_eq_eq: forall {X} (x y:Coroutine X),
>  coroutine_eq x y -> x = y.
> 
> My question is: is there any way to prove that axiom?  Maybe using a single 
> axiom which would also imply corresponding statements for Stream, 
> PossiblyTerminatingStream, InfinitelyBranchingBinaryTree, etc.?
> -- 
> Daniel Schepler