list - Coq 中的函数和类型替换或 View

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

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

这样的事情可能吗？

编辑:澄清一下，数字出现了类似的问题:我有一些使用 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 不会免费给你，你仍然
需要手动显示这些引理。有两件事可以帮助
减轻你的痛苦:

有一个 parametricity plugin对于 Coq (CoqParam) 应该
帮助自动为您派生样板证明。我有
不过，我从来没有用过它，所以我真的不能说它是多么容易使用。

Coq Effective Algebra Library(或简称 CoqEAL)使用
参数证明有关有效算法的事情，同时
推理更方便的。特别地，他们定义了
允许在 nat 之间切换的改进和 BinNat ， 作为
你建议。在内部，他们使用基于
类型类推断，你可以适应你的原始
例如，但我听说他们目前正在迁移他们的
使用 CoqParam 的实现。