Translate the Maude code into Coq

Question

I want to translate the Maude code I wrote before to Coq since Coq has more powerful expression than Maude.

I have no idea how to represent the following code:

As shown above, the GuardPostfix has three subsorts: GuardPostfix1, GuardPostfix2 and GuardPostfix3.

I use inductive type to denote the GCcomponent. However, when defining the type GComponent, GComponent1 has two constructors that use the constructor GuardPostfix1 and GuardPostfix2 respectively.

How can I define these types in Coq?

Tej Chajed Tej Chajed · Accepted Answer · 2018-02-03T14:18:47

I think the general recipe is to translate all Maude sorts into Coq types, and to represent Maude subsort relationships as the supersort having constructors for all of its subsorts (eg, subsort A B < C becomes Definition C := A + B). Following that general rule here's how I translated your example. Note that I don't know Maude, so it's possibly I missed something about the example itself. Also, I would strongly consider using a new inductive rather than the generic sum type (+) for GuardPostfix and GComponent, but that's up to you.

Module GuardedComponent.

  Parameter BoolExp:Type.
  Parameter Assignment:Type.
  Parameter Program:Type.
  Parameter Index:Type.
  Parameter EndPoint:Type.
  Parameter Null:Type.
  Parameter EventGuard:Type.
  Parameter TimeControl:Type.

  Inductive AssignmentGuard :=
  | mkAssignmentGuard (_:BoolExp) (_:Assignment).

  Inductive GuardPostfix1 :=
  | mkGuardPostfix1 (_:Program) (_:Index).

  Inductive GuardPostfix2 :=
  | mkGuardPostfix2 (_:Program) (_:EndPoint).

  Inductive GuardPostfix3 :=
  | mkGuardPostfix3 (_:Program) (_:Null).

  Definition GuardPostfix : Type :=
    GuardPostfix1 + GuardPostfix2 + GuardPostfix3.

  Inductive GComponent1 :=
  | comp1_post1 (_:GuardPostfix1)
  | comp1_post2 (_:GuardPostfix2).

  Inductive GComponent2 :=
  | mkGComponent2 (_:EventGuard) (_:GuardPostfix3).

  Inductive GComponent3 :=
  | mkGComponent3 (_:TimeControl) (_:GuardPostfix3).

  Definition GComponent : Type :=
    GComponent1 + GComponent2 + GComponent3.

End GuardedComponent.

Translate the Maude code into Coq

1 Answers