The Coq mailing list

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

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.