The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hello Alex,

You can use "Inductive ... with  " for defining simultaneously two 
inductive types:

Inductive A: Set := a : A
                  | f : B -> A
with B : Set := g : A -> B.


Similarly you can define mutually recursive functions.

Fixpoint size (x:A) : nat  :=
 match x with a => 0
            | f b => S (sizeB b)
         end
with sizeB (y:B) : nat :=
 match y with g x => S (size x) end.

Eval compute in (size (f (g a))).
2


For doing proofs by mutuial induction, use the command Scheme (an 
example is given in the
reference manual (trees and forests)).

Pierre




Alex Suzuki wrote:

> Hello list,
>
> I'm a CS student at ETH Zurich and I'm using Coq to formalize a
> translation from Java Bytecode to a guarded command language used
> for verification. This is probably not the last question regarding
> Coq from my side. ;-)
>
> When a situation arises where we have types that depend on each
> other, how do you do write this in Coq?
>
> Inductive A: Set :=
>   | A1
>   | A2 (x: B).
>
> Inductive B: Set :=
>   | B1
>   | B2 (x: A).
>
> This will not work as Coq will complain that the reference B was
> not found in the current environment. Is there some way to
> "forward declare" type B, or am I doing something very wrong? :)
>
> Regards,
>   Alex