时间戳

首页 > 解决方案 > Coq：在归纳定义中匹配

pattern-matching - Coq：在归纳定义中匹配

问题描述

我想在 Coq 中实现如下代码：

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

但是不可能匹配未定义的类型。如何克服这个障碍？

（我需要在使用它之前检查术语的一些属性。例如，目的 - 在构造更大的公式之前检查子公式的正确性。）

标签： pattern-matchingcoq

解决方案

您需要所谓的归纳递归定义。不幸的是，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在上面的链接中查找课程。

推荐阅读