[Agda] Re: [Coq-Club] Need help with coinductive proof

[Thorsten Altenkirch]

Hi Edsko,

> So far, so good. However, now consider the proof mentioned at the  
> start. The standard bisimulation on conat's is defined like Thorsten  
> did, except that I index the maximum delay (number of taus) using a  
> natural number, rather than mixing coinduction and induction:
>
> CoInductive bisimilar_conat : nat -> conat -> conat -> Prop :=
>   | bisim_cozero : forall d,
>       bisimilar_conat d cozero cozero
>   | bisim_cosucc : forall d' d m n,
>       bisimilar_conat d' m n ->
>       bisimilar_conat d (cosucc m) (cosucc n)
>   | bisim_tau : forall d' d m n,
>       bisimilar_conat d' m n ->
>       bisimilar_conat d (tau_conat m) (tau_conat n)
>   | bisim_tau_left : forall d m n,
>       bisimilar_conat d m n ->
>       bisimilar_conat (S d) (tau_conat m) n
>   | bisim_tau_right : forall d m n,
>       bisimilar_conat d m n ->
>       bisimilar_conat (S d) m (tau_conat n).


However, (exists n:nat,bisimilar_conat n a b) is different from a ≈ b  
because there doesn't have to be a maximum delay (it is easy to  
construct a counterexample).

Isn't is possible to construct nested coinductive-inductive types in  
Coq?

Cheers,
Thorsten


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.