coq - 如何形式化 Coq 中术语归约关系的终止？

Question

我有一个术语重写系统 (A, →)，其中 A 是一个集合并且 → A 上的中缀二元关系。给定 A 的 x 和 y，x → y 意味着 x 归约为 y。

为了实现一些属性，我只使用了 Coq.Relations.Relation_Definitions 和 Coq.Relations.Relation_Operators 中的定义。

现在我想形式化以下属性:

• → 是终止的，即:不存在无限下降链 a0 → a1 → ...

我怎样才能在 Coq 中实现它？

Answer 1

显示重写关系终止与显示它是有根据的是一回事。这可以用 Coq 中的归纳谓词编码:

Inductive Acc {A} (R : A -> A -> Prop) (x: A) : Prop :=
  Acc_intro : (forall y:A, R x y -> Acc R y) -> Acc R x.

Definition well_founded {A} (R : A -> A -> Prop) :=
  forall a:A, Acc R a.

(此定义与 standard library 中的 Acc 和 well_founded 谓词基本相同，但我更改了关系的顺序以匹配重写系统中使用的约定。)

给定类型 A 和 A 上的关系 R，Acc R x 意味着每个序列R 减少从 x 开始:A 正在终止；因此，well_founded R 意味着从任何 点开始的每个序列都将终止。 (Acc 代表“可访问”。)

这个定义为什么有效可能不是很清楚；首先，我们如何证明 Acc R x 对任何 x 都成立？请注意，如果 x 是一个不归约的元素(即 R x y 永远不会对任何 y 成立)，则前提Acc_intro 简单成立，我们可以得出 Acc R x。例如，这将允许我们显示 Acc gt 0。如果 R 确实是有根据的，那么我们可以从这些基本情况向后工作，并得出结论 A 的其他元素是可访问的。有根据的正式证明比这更复杂，因为它必须对每个 x 通用，但这至少说明了我们如何证明每个元素都可以单独访问。

好的，也许我们可以证明 Acc R x 成立。那我们怎么用呢？ 借助 Coq 为 Acc 生成的归纳和递归原则；例如:

Acc_ind : forall A (R : A -> A -> Prop) (P : A -> Prop),
   (forall x : A, (forall y : A, R x y -> P y) -> P x) ->
   forall x : A, Acc R x -> P x

当R是有根据的，这就是有根据的归纳法则。我们可以这样解释它。假设我们可以证明 P x 对任何 x : A 都成立，同时利用归纳假设表明 P y 在任何时候都成立 R x y。 (根据 R 的含义，这可能意味着 x 步进到 y，或者 y 是严格的小于 x 等)然后，P x 对满足 Acc R x 的任何 x 成立。有根据的递归的工作原理类似，并且直观地表示如果每次递归调用都在“较小”元素上执行，则递归定义是有效的。

Adam Chlipala 的 CPDT 有一个 chapter on general recursion对该 Material 有更全面的介绍。