Can I define nested mutually dependent types in Coq?

Question

I am trying to model the following in Coq, which works fine in Haskell (below is Haskell code):

data Point = Pt Config Config 
data Line = Ln Point Point | Ext Line 
data Circle = Crc Point Line
data Figure = P Point | L Line | C Circle
type Config = [Figure]


a = Pt [] []
b = Pt [] [P a]
ln = Ln a b
d = Pt [L ln] [P a, P b]

Basically, b is a distinct point from a, ln is the straight line going through a and b, and d is a point on line ln but distinct from a and from b. The problem is that Config depends on Point, Line and Circle, and then Point depends on Config. I have seen that mutually dependent types existed in Coq, but do they work after multiple levels of nesting or indirection like this?

If not, do you know another proof-assistant which allows such constructions?

Answer 1

You can do mutually defined inductive types in Coq with the «with» syntax

You end up with this definition:

Inductive Point : Type :=
  | Pt : Config -> Config -> Point
with Line : Type :=
  | Ln : Point -> Point -> Line
  | Ext : Line -> Line
with Circle : Type :=
  | Crc : Point -> Line -> Circle
with Figure : Type :=
  | P : Point -> Figure
  | L : Line -> Figure
  | C : Circle -> Figure
with Config : Type :=
  | Conf : list Figure -> Config.

Here, I did make Config an inductive type (i.e. with a constructor) but you can also make it a notation for list Figure like this:

Inductive Point : Type :=
  | Pt : list Figure -> list Figure -> Point
with Line : Type :=
  | Ln : Point -> Point -> Line
  | Ext : Line -> Line
with Circle : Type :=
  | Crc : Point -> Line -> Circle
with Figure : Type :=
  | P : Point -> Figure
  | L : Line -> Figure
  | C : Circle -> Figure.
Definition Config := list Figure.

You can then translate your code sample to Coq Syntax:

Definition a := Pt (Conf nil) (Conf nil).
Definition b := Pt (Conf nil) (Conf (cons (P a) nil)).
Definition ln := Ln a b.
Definition d := Pt (Conf (cons (L ln) nil)) (Conf (cons (P b) (cons (P a) nil))).

With the second definition solution, the code is simpler to use :

Definition a := Pt nil nil.
Definition b := Pt nil (cons (P a) nil).
Definition ln := Ln a b.
Definition d := Pt (cons (L ln) nil) (cons (P b) (cons (P a) nil)).