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

[Thorsten Altenkirch]

Hi Edsko,

> I don't understand; why doesn't there have to be a maximum delay?  
> Isn't that the point of using an inductive definition -- so that tau- 
> left and tau-right can be applied finitely many times? (Note that  
> rules bisim_cozero, bisim_cosucc and bisim_tau allow to "reset" the  
> maximum delay.)

Indeed, I missed the resetting bit. This is indeed a correct encoding  
of the mixed coinductive-inductive relation.

> Note that my data type above, however, is probably not good enough  
> because a proof of (exists i, bisim i m n) cannot use coinduction,  
> as (exists, ..) is not a coinductive type. I'm now trying to use

No, the datatype should be fine. I'll try to understand your problem.

> As regards your other question -- by using a nested coinductive/ 
> inductive definition Coq, do you mean something like
>
> Inductive weak (R : coN -> coN -> Prop) : coN -> coN -> Prop :=
>   | weak_base : forall m n,
>       R m n ->
>       weak R m n
>   | weak_tau_left : forall m n,
>       weak R m n ->
>       weak R (tau m) n
>   | weak_tau_right : forall m n,
>       weak R m n ->
>       weak R m (tau n).
>
> CoInductive weak_coN : coN -> coN -> Prop :=
>   | strong_coZ :
>       weak_coN coZ coZ
>   | strong_coS : forall m n,
>       weak_coN m n ->
>       weak_coN (coS m) (coS n)
>   | strong_tau : forall m n,
>       weak_coN m n ->
>       weak_coN (tau m) (tau n)
>   | weak_tau : forall m n,
>       weak weak_coN m n ->
>       weak_coN m n.
>
> This is a valid definition, but proofs are now painful; a proof L  
> over weak_coN by coinduction cannot recurse over the proof of (weak  
> weak_coN m n) passing L itself as an argument, because the  
> occurrence of L is now not guarded as it occurs as an argument to  
> the induction hypothesis (the recursor) for [weak] (this was the  
> essence of my separate email asking about mixing induction and  
> coinduction in Coq). There are some papers on how to do this ("Using  
> Structural Recursion for Corecursion" is one, but limited in scope  
> and I'm not sure it applies here; "A Unifying Approach to Recursive  
> and Co-recursive Definitions" is much more general, using complete  
> ordered families of equivalances, but is difficult and I haven't yet  
> been brave enough to try it.

I don't think this is going to help here.

The main issue here is that you have a nested definition and hence you  
don't get very far with the induction/coinduction principles Coq  
derives automatically. However, you should be able to derive your own  
using CoFixpoint and Fixpoint.

There was a discussion about this in '97, see
[Coq-Club] Inductive definitions that go through lists
I also posted something on this thread but it seems it didn't make it  
to the archive... The gist of it was:

> Indeed, every strictly positive operator on types F : Type -> Type  
> gives rise to a modality:
>
> 	P : A -> Type
> 	---------------------
> 	[] F : F A -> Type
>
> moreover, we have a dependent version of map
>
> 	f : forall a:A, P a
> 	---------------------------------
> 	dmap f : forall x:F A,[] P x
>
> Using this, one can formulate a generic eliminator for the inductive  
> type mu F:Type with the constructor
> in : F(mu F) -> mu F:
>
> 	P : mu F -> Type
>        m :  forall x:F(mu F), [] P x -> P (in x)
> 	------------------------------------------------
> 	elim P m : forall x:mu F,  P x
>
> and the computation rule
>
> 	elim P m (in x) = dmap (elim P m) x



>
> OTOH, it seems we get this for free in Agda -- so a simpler solution  
> should be possible?

There are certainly areas where you are better off with Coq (e.g.  
complex tactic-based proofs), but for playing around with mixed  
coinduction-induction, I think Agda is your choice.

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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090827/77df83bb/attachment-0001.html