1
$\begingroup$

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?

$\endgroup$

1 Answer 1

1
$\begingroup$

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)).
$\endgroup$
1
  • $\begingroup$ Thank you very much! that is awesome. $\endgroup$
    – Henri_S
    Commented May 13, 2023 at 15:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.