CODEWITHSUNDEEP
coq
Frank Sheng
Frank Sheng

Reputation: 205

Defining the syntax with constraints

I want to define the syntax of the time delay in Coq as follows:

Inductive tcs : Type :=
| delay : nat -> tcs
| atomic : nat-> tcs.

But the natural number 0 is not allowed in the constructor delay. I also find using the subset type to define the syntax. However, the introduction of subset type leads to more complications for defining semantics. Is there an easy way to define such sytax?

Upvotes: 1

Views: 99

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23592

In your particular case, I think the easiest thing to do is to change the interpretation of the number in the delay constructor: note that nat is isomorphic to {n : nat | n > 0} via the successor function. Therefore, all you have to do is add one to the argument of delay whenever you use it in a match expression. For instance:

Definition nat_of_tcs t :=
  match t with
  | delay n => S n
  | atomic n => n
  end.

Alternatively, you can replace nat by positive, a type defined in the standard library to represent numbers greater than 0.

In general, subset types would be the way to go. You could add a n != 0 constraint in the type of delay, or define a separate predicate on elements of tcs describing when elements are well-formed:

Definition well_formed t :=
  match t with
  | delay 0 => false
  | _       => true
  end.

Definition wftcs := { t : tcs | well_formed t = true }.

The Mathematical Components and related libraries use this pattern pervasively; check the subType class in the eqtype module, for instance. In my extensional structures library, I use the subType class to define a type of finite sets (here) by packaging a list with a proof that the list is sorted.

Upvotes: 4

Related Questions