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?