时间戳

首页 > 解决方案 > 引理作为记录中的类型

coq - 引理作为记录中的类型

问题描述

初学者在这里！我们如何解释看起来像这样的记录？

 Record test A B :=
{
  CA: forall m, A m; 
  CB: forall a b m, CA m ==> B(a,b);
}

我试图了解这个记录的一个实例会是什么样子，此外，将量化的引理作为一种类型意味着什么。

标签： coq

解决方案

您所写的内容没有意义，因为该符号_ ==> _应该链接两个布尔值。但是CA有 type A m，它本身就是一种类型，而不是布尔值。

前进的一种可能性是制作CA一个可以表示A谓词的布尔函数。

您假设记录的另一个困难是我们不知道 and 的输入类型是什么A，B所以我假设我们生活在一个T出现量化的环境类型中。所以这里有一个变种：

Record test (T : Type) (A : T -> Prop) (B : T * T -> bool) :=
{
  CA : T -> bool;
  CA_A : forall m, CA m = true -> A m;
  CB : forall a b m, (CA m ==> B(a, b)) = true
}.

这个例子迫使你理解这种逻辑语言中有两个不同的概念：bool值和Prop值。它们代表不同的东西，有时可以合并，但您需要在头脑中明确区分才能离开初学者的类别。

对于您的最后一句话“将量化的引理作为一种类型意味着什么”，这是另一种解释。

使用传统编程语言进行编程时，您可以返回整数数组。但是，您不能明确地说要返回特定长度的整数数组。在 Gallina（Coq 的基本编程语言）中，您可以定义一种长度为 10 的数组类型。让我们假设这样的类型将被编写array n。所以array 10和array 11将是两种不同的类型。n将一个数字作为输入并返回一个长度数组作为输出的函数n将具有以下类型：

forall n, array n

因此，具有量化公式作为类型的对象只是一个函数。

从逻辑的角度来看，该语句forall n, array n通常被读取为每个n存在的数组size n。这种说法可能对你来说并不奇怪。

所以数组的类型取决于索引。现在我们可以考虑另一种类型，例如质数的证明类型n。让我们假设这种类型是写的prime n。当然，有些数字不是素数，因此例如该类型prime 4根本不应该包含任何证明。现在我可以编写一个test_prime : nat -> bool使用属性调用的函数，当它返回时，true我可以保证输入是素数。这将这样写：

forall n, test_prime n = true -> prime n

现在，如果我想定义所有正确的素数测试函数的集合，我想在一个数据中关联函数和它正确的证明，所以我将定义以下数据类型。

Record certified_prime_test :=
  {
     test_prime : nat -> bool;
     certificate : forall n, test_prime n = true -> prime nat
  }.

因此，包含通用量化公式的记录可以属于以下两个类别之一：一个组件是此函数之一，其输出在同一族的几种类型中有所不同（如 的示例array），或者其中一个组件实际上带来了更合乎逻辑的关于作为函数的另一个组件的信息。在certified_prime_test示例中，certificate组件带来了有关该test_prime功能的更多信息。

推荐阅读