Coq: matching inside Inductive definition

Question

I'd like to implement in Coq something like the following code:

Inductive IT :=
| c1 : IT
| c2 (x:IT) (H:
 match x as x return Prop with 
 | c1 => True
 | c2 y => False
 end): IT.

But it is not possible to match undefined type. How to overcome this obstacle?

(I need to check some property of term before using it. For example, the aim - to check the correctness of subformula before constructing larger formula.)

Arthur Azevedo De Amorim Arthur Azevedo De Amorim · Accepted Answer · 2018-08-24T13:54:13

You want what is known as an inductive-recursive definition. Coq unfortunately does not support this feature, although other proof assistants such as Agda and Idris do.

The best way of avoiding induction-recursion for your type is probably to define a raw inductive type without the constraints, and define a separate predicate that carves out well-formed elements:

Inductive preIT :=
| c1 : preIT
| c2 : preIT -> preIT.

Definition wfIT (x : preIT) :=
  match x with
  | c1        => true
  | c2 c1     => true
  | c2 (c2 _) => false
  end.

Record IT := {
  it_val : preIT;
  _      : wfIT it_val
}.

The Mathematical Components library has good support for this programming pattern; look for the subType class in the above link.

Coq: matching inside Inductive definition

1 Answers