# Can I define nested mutually dependent types in Coq?

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?

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)).

• Thank you very much! that is awesome. Commented May 13, 2023 at 15:49