<p>You can do mutually defined inductive types in Coq with <a href="https://coq.inria.fr/refman/language/core/inductive.html#mutually-defined-inductive-types" rel="nofollow noreferrer">the «with» syntax</a></p>
<p>You end up with this definition:</p>
<pre><code>Inductive Point : Type :=
  | Pt : Config -&gt; Config -&gt; Point
with Line : Type :=
  | Ln : Point -&gt; Point -&gt; Line
  | Ext : Line -&gt; Line
with Circle : Type :=
  | Crc : Point -&gt; Line -&gt; Circle
with Figure : Type :=
  | P : Point -&gt; Figure
  | L : Line -&gt; Figure
  | C : Circle -&gt; Figure
with Config : Type :=
  | Conf : list Figure -&gt; Config.
</code></pre>
<p>Here, I did make Config an inductive type (i.e. with a constructor) but you can also make it a <em>notation</em> for <code>list Figure</code> like this:</p>
<pre><code>Inductive Point : Type :=
  | Pt : list Figure -&gt; list Figure -&gt; Point
with Line : Type :=
  | Ln : Point -&gt; Point -&gt; Line
  | Ext : Line -&gt; Line
with Circle : Type :=
  | Crc : Point -&gt; Line -&gt; Circle
with Figure : Type :=
  | P : Point -&gt; Figure
  | L : Line -&gt; Figure
  | C : Circle -&gt; Figure.
Definition Config := list Figure.
</code></pre>
<p>You can then translate your code sample to Coq Syntax:</p>
<pre><code>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))).
</code></pre>
<p>With the second <em>definition</em> solution, the code is simpler to use :</p>
<pre><code>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)).
</code></pre>

CC BY-SA 4.0
2023-05-13T15:49:31.880Z
Thank you very much! that is awesome.
Henri_S
CC BY-SA 4.0
2023-05-13T09:24:55.037Z
2023-05-13T09:24:55.037Z
Mysaa
<p>I am trying to model the following in Coq, which works fine in Haskell (below is Haskell code):</p>
<pre><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]
</code></pre>
<p>Basically, <em>b</em> is a distinct point from <em>a</em>, <em>ln</em> is the straight line going through <em>a</em> and <em>b</em>, and <em>d</em> is a point on line <em>ln</em> but distinct from <em>a</em> and from <em>b</em>.
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?</p>
<p>If not, do you know another proof-assistant which allows such constructions?</p>

<dependent-type><coq>
Can I define nested mutually dependent types in Coq?
Henri_S
# Can I define nested mutually dependent types in Coq?

(Asked by: username_0 on 2023-05-13)

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?

**Tags:** dependent-type, coq

---

## 1 answers

### Answer by username_1 on 2023-05-13. Score: 1 | Accepted answer

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

> **Comments:**
> **username_0**: Thank you very much! that is awesome.  

---

