Coq: соответствие внутри индуктивного определения

Question

Я хотел бы реализовать в Coq что-то вроде следующего кода:

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

Но невозможно сопоставить неопределенный тип. Как преодолеть это препятствие?

(Мне нужно проверить некоторые свойства термина перед его использованием. Например, цель - проверить правильность подформулы перед построением формулы большего размера.)

Answer 1

Требуется то, что известно как индуктивно-рекурсивное определение . К сожалению, Coq не поддерживает эту функцию, хотя другие помощники, такие как Agda и Idris, поддерживают ее.

Лучший способ избежать индукции-рекурсии для вашего типа - это, вероятно, определить необработанный индуктивный тип без ограничений и определить отдельный предикат, который выделяет правильно сформированные элементы:

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
}.

Библиотека математических компонентов имеет хорошую поддержку этого шаблона программирования; найдите класс subType в приведенной выше ссылке.