Coq 中的函数和类型替换或视图

Question

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

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

一方面，我必须用模仿列表递归的专门函数替换每个列表递归。另一方面，事先我想用 H_app 和 H_nth 替换 ++ 和 nth，这样提取的算法会更快。问题是我在某些地方使用了 simpl 和 compute 之类的策略，如果我只是替换证明代码中的所有内容，这可能会失败。如果以后有可能 "overload" 功能就好了。

这样的事情可能吗？

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

Answer 1

为了清楚起见，我认为 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 不定义之间的同构 Heap A 和 list A 所有 A。相反，我们可以找到一个函数 g : forall A, list A -> Heap A 这样

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

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

我们可以通过一种精确而正式的方式来验证这个想法在具有 parametric polymorphism 的语言中，例如 Coq。这个原理，称为 parametricity，大致说参数多态函数尊重我们强加的关系在我们实例化它们的类型上。

这有点抽象，所以让我们试着让它更具体的。假设你有一个列表函数（比如，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 不会免费给你，你仍然需要手工展示这些引理。有两件事可以提供帮助减轻你的痛苦：

Coq (CoqParam) 有一个 parametricity plugin 应该帮助自动为您导出样板证明。我有不过从来没有用过，所以我不能说它有多容易使用。
Coq 有效代数库（或简称 CoqEAL）使用参数化来证明有关有效算法的事情，同时推理更方便的。特别地，他们定义允许在 nat 和 BinNat 之间切换的改进，如你建议。在内部，他们使用基于 type-class 推理，你可以适应你原来的例如，但我听说他们目前正在迁移他们的改为使用 CoqParam 的实现。

Coq 中的函数和类型替换或视图

Function- and Type substitutions or Views in Coq

list

heap

coq

isomorphism