4

我证明了一些关于列表的定理，并从中提取了算法。现在我想改用堆，因为查找和连接更快。我目前为实现这一目标所做的只是对提取的列表类型使用自定义定义。我想以更正式的方式来做这件事，但理想情况下不必重做所有的证明。可以说我有一个类型

Heap : Set -> Set

和同构

f : forall A, Heap A -> List A.

此外，我有函数 H_app 和 H_nth，这样

H_app (f a) (f b) = f (a ++ b)

和

H_nth (f a) = nth a

一方面，我必须用一个模拟列表递归的专用函数来替换每个列表递归。另一方面，事先我想用 and 替换and ，++因此提取的算法会更快。问题是我在某些地方使用了类似and的策略，如果我只是替换证明代码中的所有内容，这可能会失败。以后有可能“重载”这些功能会很好。nthH_appH_nthsimplcompute

这样的事情可能吗？

编辑：澄清一下，数字也出现了类似的问题：我有一些使用的旧证明nat，但是数字变得太大了。使用BinNat会更好，但是是否可以在没有太多修改的情况下使用BinNat而不是在旧的证明中使用？（特别是，用更有效的定义nat替换 ? 的低效用法）+BinNat

4

1 回答 1

3

只是为了清楚起见，我认为它Heap必须看起来像这样：

Inductive Heap A : Type :=
| Node : Heap A -> A -> Heap A -> Heap A
| Leaf : Heap A.

被f定义为

Fixpoint f A (h : Heap A) : list A :=
  match h with
  | Node h1 a h2 => f h1 ++ a :: f h2
  | Leaf => []
  end.

如果是这种情况，则不f定义and for all 之间的 同构。相反，我们可以找到 这样的函数Heap Alist AAg : forall A, list A -> Heap A

forall A (l : list A), f (g l) = l

然而，我们想说，当它们用于实现相同的抽象，即某种类型的元素集时Heap，list它们在某种意义上是等价的。

有一种精确和正式的方式可以让我们在具有参数多态性的语言中验证这个想法，例如 Coq。这个原则，称为参数性，粗略地说参数多态函数尊重我们对实例化它们的类型施加的关系。

这有点抽象，所以让我们尝试使其更具体。假设您有一个foo仅使用++和的列表（例如 ）上的函数nth。为了能够用参数化foo的等效版本替换Heap，我们需要使 foo' 的定义多态，对列表中的函数进行抽象：

Definition foo (T : Set -> Set)
               (app : forall A, T A -> T A -> T A)
               (nth : forall A, T A -> nat -> option A)
               A (l : T A) : T A :=
  (* ... *)

您将首先通过在列表上实例化它来证明 foo 的属性：

Definition list_foo := foo list @app @nth.

Lemma list_foo_lemma : (* Some statement *).

现在，因为我们现在H_app和H_nth它们的列表对应物兼容，并且因为foo是多态的，所以参数理论说我们可以证明

Definition H_foo := foo Heap @H_app @H_nth.

Lemma foo_param : forall A (h : Heap A),
                    f (H_foo h) = list_foo (f h).

有了这个引理，应该可以将 的属性传输list_foo到 的类似属性H_foo。例如，作为一个简单的例子，我们可以证明它H_app是关联的，直到转换为列表：

forall A (h1 h2 h3 : Heap A),
  list_foo (H_app h1 (H_app h2 h3)) =
  list_foo (H_app (H_app h1 h2) h3).

参数化的好处在于它适用于任何 参数化多态函数：只要您的类型具有适当的兼容性条件，就应该可以以类似的方式将给定函数的两个实例化关联到 foo_param.

然而，有两个问题。第一个是必须将基本定义更改为多态定义，这可能还不错。然而，更糟糕的是，尽管参数化确保了foo_param在某些条件下总是可以证明引理，但 Coq 并没有免费为您提供，您仍然需要手动显示这些引理。有两件事可以帮助减轻你的痛苦：

  1. Coq (CoqParam)有一个参数化插件，它应该有助于自动为您导出样板证明。不过，我从来没有使用过它，所以我不能说它是多么容易使用。

  2. Coq Effective Algebra Library（或CoqEAL，简称）使用参数来证明关于高效算法的事情，同时对更方便的算法进行推理。特别是，它们定义了允许在nat和之间切换的改进BinNat，如您所建议的。在内部，他们使用基于类型类推断的基础架构，您可以将其调整为原始示例，但我听说他们目前正在迁移他们的实现以使用 CoqParam。

于 2015-04-26T16:45:26.700 回答