coq

Defining mutually recursive types in Coq?

Suppose I have types A,B,C,D,E,F. One of the constructors of A takes an argument with type F; a constructor of B requires A, a constructor of D requires arguments of types C and A, E requires D and F requires E. How should I define them?

I searched on the internet and found that I can use the keyword "with" to link them, but it doesn't work for me. Type C is a function type between two previous types that are not any of the 6 types listed above. When I try to use "with", somehow the arrow in the definition of C is highlighted, and I was shown the message Syntax error: '.' expected after [gallina] (in [vernac_aux]).

My code roughly follow this structure:

Inductive A : Type :=
  | a : F -> A
  | ... (other constructors unrelated to the problem)
 
with B : Type :=
  | b: xxx -> A -> B -> B
  | ...

with C : Type := xxx -> yyy
with D : Type := 
  | d : C -> xxx -> zzz -> B -> D
  | ...
with E := list D
with F : Type :=
  | f : E -> F
  | ...
.
Solution

  • Regarding C, you have to give names to the constructors, and the constructors should take some (zero or more) arguments and return something of type C.

    So C should be like

    Inductive C : Type := c1 :(xxx -> yyy) -> C.

    Same for E.

    Variable (xxx yyy zzz :Type).

Inductive A : Type :=
  | a : F -> A
 
with B : Type :=
  | b: xxx -> A -> B -> B

with C : Type := c1 :(xxx -> yyy) -> C

with D : Type := 
  | d : C -> xxx -> zzz -> B -> D

with E := e1: list D -> E
with F : Type :=
  | f : E -> F
.

    In this case C is not a function between xxx and yyy, but its constructor takes such a function as argument.

    If you want it to be definitionally equal to xxx->yyy, just do

    Definition C := xxx -> yyy.

    and use that in your code instead.