1

我试图在 Coq 中定义一个弱指定类型的函数。具体来说，我有一个由一组递归构造函数归纳定义的类型，并且我想定义一个函数，该函数仅在使用其中的一个子集构造参数时才定义。

更具体地说，我有以下类型定义：

Inductive Example : Set :=
  | Example_cons0 : nat -> Example
  | Example_cons1 : Example -> Example
  .

现在，我有一个仅适用于地面案例的功能。（以下定义显然不起作用，但旨在表明我的意图。）

Definition example (x:Example) : nat :=
  match x with
    | Example_cons0 n => n
  end.

理想情况下，我想说明我的参数 x 是使用通用类型构造函数的子集构造的，在本例中为 Example_cons0。我认为我可以通过定义一个陈述这一事实的谓词并将谓词的证明作为参数传递来做到这一点。例如：

Definition example_pred (x:Example) : Prop :=
  match x with
    | Example_cons0 _ => True
    | _ => False
  end.

然后（按照 Robin Green 的建议）类似，

Definition example2 (x:Example) : example_pred x -> nat :=
  (use proof to define example2?)

不幸的是，我不确定我将如何去做这些。我什至不确定这是在弱指定类型上定义受限函数的正确方法。

任何指导、提示或建议将不胜感激！- 李

更新：

按照 jozefg 的建议，示例函数可以定义为：

Definition example (x:Example) : example_pred x -> nat :=
  match x with
    | Example_cons0 n => fun _ => n
    | _               => fun proof => match proof with end 
  end.

有关详细信息，请参阅他的评论。可以使用以下语法评估此函数，这也演示了证明术语在 Coq 中的表示方式：

Coq < Eval compute in Example.example (Example.Example_cons0 0) (I : Example.example_pred (Example.Example_cons0 0)).
    = 0
    : nat
4

2 回答 2

2

这是我将其编写为简化示例的方式

考虑一个简单的数据类型

Inductive Foo :=
| Bar : nat -> Foo
| Baz.

现在我们定义一个有用的函数

Definition bar f :=
  match f with
    | Bar _ => True
    | Baz   => False
  end.

最后你想写什么：

Definition example f :=
  match f return bar f -> nat with
    | Bar n => fun _ => n
    | Baz   => fun p => match p with end
  end.

这有类型forall f : Foo, bar f -> nat。这是通过确保在example未提供 a的情况下，Bar用户必须提供虚假证明（不可能）来实现的。

可以这样调用

example (Bar n) I

但问题是，您可能必须手动证明某些项是由 构造的Bar，否则 Coq 应该如何知道？

于 2013-12-10T22:28:48.807 回答
1

是的，你在正确的路线上。你要：

Definition example2 (x:Example) (example_pred x) : nat :=

以及如何进一步进行取决于您要证明的内容。

您可能会发现通过使用 Curry-Howard 对应关系用战术证明来做出定义很有帮助：

Definition example2 (x:Example) (example_pred x) : nat.
Proof.
  some proof
Defined.

另外，我想指出，sigandsigT类型通常用于将“弱指定类型”与谓词结合起来以约束它们。

于 2013-12-10T21:53:04.973 回答