Restricted Inductive Type Definition

Using Coq
1

Hello,

For a project I have in mind, I’m trying to investigate if Coq could suit my need.

I’m trying to model a data flow diagram. In a data flow diagram, I have assets that can be either processes, or data stores, or data flows.

Data flows can only be between two processes, or between a process and a data store. It is not correct to specify a data flow between to 2 data stores, or if at least one of the assets is a data flow itself.

I could do something like this:

Inductive Asset : Type :=
| Process
| DataStore
| DataFlow (a b : Asset).

But this is not correct enough for me, because at allows incorrect combinations of Asset to build a DataFlow.

How can I constrain my DataFlow constructor to only accept a pair of (Process, Process), or (Process, DataStore) or (DataStore, Process) ?

Or maybe, suggestions to do it completely differently ?

Thanks in advance.

1 Like
2

Your asset type is recursive, is that intended?

What do you think of turning data flows into their own types with individual constructors for the various combinations?

Inductive process : Type := (* ... *) .
Inductive data_store : Type := (* ... *) .
Inductive data_flow : Type :=
| FlowPP (p1 p2 : process)
| FlowPS (p1 : process) (s2 : data_store)
| FlowSP (p1 : data_store) (p2 : process)
.

Inductive asset : Type :=
| Process (p : process)
| DataStore (s : data_store)
| DataFlow (f : data_flow)
.
3

Thanks !
I will explore this approach.

Somehow I understand it this way: that I should define the type of the diagram elements on their own first, then only after collectively type them as assets.