引理作为记录中的一种类型

Question

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

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

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

Answer 1

你写的东西没有意义，因为符号_ ==> _应该链接两个布尔值。但CA有类型A m，它本身是一个类型，而不是布尔值。

前进的一种可能性是使CA成为可以代表A谓词的布尔函数。

您的假设记录的另一个困难是我们不知道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函数的更多信息。