两个参数的结构递归

Question

我试图在 Coq 中创建一个函数，它有一个非常复杂的终止参数。为方便起见，我可以编写函数，使其具有自然数作为第一个参数，以便数字或它后面的参数在结构上更小。

当尝试使用嵌套修复方法对两个参数进行递归时，Coq 抱怨包含递减数语义的证明参数不是归纳类型。

我可能可以手动进行有根据的递归，但我想使用 Program Fixpoint 或 Equations。使用 Program Fixpoint，我得到了一个非常丑陋的有根据的证明版本。下面是一个演示丑陋的最小代码示例。

Require Import Program Omega.

Inductive tuple_lt : (nat * nat) -> (nat * nat) -> Prop :=
  fst_lt : forall a b c d, a < c -> tuple_lt (a, b) (c, d).

Program Fixpoint f (a : nat) (b : nat) {measure (a, b) (tuple_lt)} :=
match a with
| 0 => 0
| S n => f n b
end.

Next Obligation.
apply fst_lt. auto.
Qed.

Next Obligation.
unfold well_founded. unfold MR.

义务如下所示：

forall a : {_ : nat & nat}, Acc (fun x y : {_ : nat & nat} => tuple_lt (projT1 x, projT2 x) (projT1 y, projT2 y)) a

我能否以某种方式将Acc tuple_lt 的证明转换为丑陋的证明或避免生成它？

标准库中是否有关于两个参数的结构递归的证明？

我什至如何使用方程式编写手动 WF 证明？手册没有提到这一点。

Answer 1

在这种简单的情况下，您不必展开诸如well_founded 和MR 之类的定义，而是使用适当的引理。

要处理MR，可以在Program.Wf中使用引理measure_wf。

要证明tuple_lt 的有根据，您可以依靠引理来显示基于另一个关系的有根据的关系。在这里，我们可以使用well_founded_lt_compat。在其他情况下，您可能会发现其他引理很有用，例如 wf_inverse_image、well_founded_ltof 或 well_founded_gtof。

tuple_lt 有根据的证明变得简单。

Lemma tuple_lt_wf : well_founded tuple_lt.
Proof.
  apply well_founded_lt_compat with fst.
  intros ? ? []; assumption.
Defined.

第二项义务的证明也是如此。

Next Obligation.
apply measure_wf. apply tuple_lt_wf.
Defined.

（请注意，在这两种情况下，如果您希望由 Program Fixpoint 定义的函数在 Coq 内部计算（否则它会卡在不透明的证明上），您应该以 Defined 而不是 Qed 结束证明；它不过，您似乎可以用Qed 结束第一个义务的证明）。

您还可以对tuple_lt 使用以下更简单的定义：

Definition tuple_lt (p1 p2 : nat * nat) := fst p1 < fst p2.

在这种情况下，有根据的证明是微不足道的。

Lemma tuple_lt_wf : well_founded tuple_lt.
Proof.
  apply well_founded_ltof.
Defined.