使用 Fix 或 Program Fixpoint 在 Coq 中编写有根据的程序

Question

按照 Chlipala 书 GeneralRec 章中给出的示例，我正在尝试编写合并排序算法。

这是我的代码

Require Import Nat.

Fixpoint insert (x:nat) (l: list nat) : list nat :=
  match l with
  | nil => x::nil
  | y::l' => if leb x y then
              x::l
            else
              y::(insert x l')
  end.

Fixpoint merge (l1 l2 : list nat) : list nat :=
  match l1 with
  | nil => l2
  | x::l1' => insert x (merge l1' l2)
  end.

Fixpoint split (l : list nat) : list nat * list nat :=
  match l with
  | nil => (nil,nil)
  | x::nil => (x::nil,nil)
  | x::y::l' =>
    let (ll,lr) := split l' in
    (x::ll,y::lr)
  end.

Definition lengthOrder (l1 l2 : list nat) :=
  length l1 < length l2.

Theorem lengthOrder_wf : well_founded lengthOrder.
Admitted.

问题是无法使用命令 Fixpoint 编写 mergeSort 函数，因为该函数在结构上不是递减的：

Fixpoint mergeSort (l: list nat) : list nat :=
  if leb (length l) 1 then l
  else
    let (ll,lr) := split l in
    merge (mergeSort ll) (mergeSort lr).

相反，可以使用带有术语 Fix 的命令 Program Fixpoint 或 Definition（如 Chlipala 书中所述）。

但是，如果我正在写这篇文章

Definition mergeSort : list nat -> list nat.
refine (Fix lengthOrder_wf (fun (l: list nat) => list nat)
      (fun (l : list nat) => (fun mergeSort : (forall ls : list nat, lengthOrder ls l -> list nat )=>
                           if leb (length l) 1 then
                             let (ll,lr) := split l in
                             merge (mergeSort ll _) (mergeSort lr _)
                           else
                             l))).

我正在实现不可能的目标：

2 subgoals, subgoal 1 (ID 65)

  l : list nat
  mergeSort : forall ls : list nat, lengthOrder ls l -> list nat
  ll, lr : list nat
  ============================
  lengthOrder ll l

subgoal 2 (ID 66) is:
 lengthOrder lr l

这就是 Chlipala 建议以这种方式更改 mergeSort 定义的原因：

Definition mergeSort : list nat -> list nat.
  refine (Fix lengthOrder_wf (fun _ => list nat)
              (fun (ls : list nat)
                 (mergeSort : forall ls' : list nat, lengthOrder ls' ls -> list nat) =>
                 if Compare_dec.le_lt_dec 2 (length ls)
                 then let lss := split ls in
                      merge (mergeSort (fst lss) _) (mergeSort (snd lss) _)
                 else ls)).

产生以下目标：

2 subgoals, subgoal 1 (ID 68)

  ls : list nat
  mergeSort : forall ls' : list nat, lengthOrder ls' ls -> list nat
  l : 2 <= length ls
  lss := split ls : list nat * list nat
  ============================
  lengthOrder (fst lss) ls

subgoal 2 (ID 69) is:
 lengthOrder (snd lss) ls

这个新定义对我来说听起来很神奇。所以我想知道：

根据第一个定义，是否仍然可以证明函数的有效性？
不然为什么第一个定义不行？
基本用户如何轻松地从第一个定义过渡到第二个定义？

Answer 1

很容易看出您需要进行两项更改才能获得 A. Chlipala 的解决方案。

1) 在执行 split 时，你需要记住 ll 和 lr 来自 split，否则它们将是一些任意列表，不可能比原始列表 l.

以下代码无法保存此类信息：

let (ll,lr) := split l in
  merge (mergeSort ll _) (mergeSort lr _)

因此需要替换为

let lss := split ls in
  merge (mergeSort (fst lss) _) (mergeSort (snd lss) _)

它保留了我们需要的东西。

失败是由于 Coq 无法记住 ll 和 lr 来自 split l 而发生的，因为 let (ll,lr) 只是 match伪装（参见手册，§2.2.3）。

回想一下 pattern-matching 的目的是（粗略地说）

解压缩归纳数据类型的某些值的组件，并将它们绑定到某些名称（我们将在我的回答的第二部分中需要它）和
在相应的 pattern-match 分支中用其特殊情况替换原始定义。

现在，观察 split l 不会在我们 pattern-match 之前出现在目标或上下文中的任何地方。我们只是随意将其引入定义中。这就是为什么 pattern-matching 没有给我们任何东西——我们不能在目标或上下文中用它的 "special case" ((ll,lr)) 替换 split l，因为没有 split l任何地方。

还有一种使用逻辑相等性 (=) 的替代方法：

(let (ll, lr) as s return (s = split l -> list nat) := split l in
   fun split_eq => merge (mergeSort ll _) (mergeSort lr _)) eq_refl

这类似于使用 remember 策略。我们已经摆脱了 fst 和 snd，但这是一个巨大的矫枉过正，我不推荐它。

2) 我们需要证明的另一件事是 ll 和 lr 在 2 <= length l.

时比 l 短

由于 if 表达式也是伪装的 match（它适用于具有正好两个构造函数的任何归纳数据类型），我们需要一些机制来记住 leb 2 (length l) = true 在 then 分支中。同样，由于我们在任何地方都没有 leb，因此此信息会丢失。

问题至少有两种可能的解决方案：

要么我们将 leb 2 (length l) 记为方程式（就像我们在第一部分所做的那样），要么
我们可以使用一些比较函数，其结果类型表现得像 bool（因此它可以表示两种选择），但它还应该记住我们需要的一些额外信息。然后我们可以pattern-match比较结果并提取信息，当然，在这种情况下必须是2 <= length l的证明。

我们需要的是一种类型，它能够在 leb m n returns true 的情况下携带 m <= n 的证明和证明，比如说, m > n 否则。标准库中有一种类型可以做到这一点！它被称为 sumbool:

Inductive sumbool (A B : Prop) : Set :=
    left : A -> {A} + {B} | right : B -> {A} + {B}

{A} + {B}只是sumbool A B的一个符号（语法糖）。就像 bool 一样，它有两个构造函数，但除此之外它还记得两个命题 A 和 B 之一的证明。当您使用 if 对其进行案例分析时，它优于 bool 的优势就会显现出来：您在 then 分支中获得了 A 的证明和 [=53= 的证明] 在 else 分支中。换句话说，您可以使用事先保存的上下文，而 bool 不包含任何上下文（仅在程序员的脑海中）。

而我们正是需要它！好吧，不在 else 分支中，但我们希望在我们的 then 分支中获得 2 <= length l。所以，让我们问 Coq 是否已经有一个与 return 类型的比较函数：

Search (_ -> _ -> {_ <= _} + {_}).

(*
output:
le_lt_dec: forall n m : nat, {n <= m} + {m < n}
le_le_S_dec: forall n m : nat, {n <= m} + {S m <= n}
le_ge_dec: forall n m : nat, {n <= m} + {n >= m}
le_gt_dec: forall n m : nat, {n <= m} + {n > m}
le_dec: forall n m : nat, {n <= m} + {~ n <= m}
*)

五个结果中的任何一个都可以，因为我们只需要在一种情况下证明。

因此，我们可以将if leb 2 (length l) then ...替换为if le_lt_dec 2 (length l) ...，得到证明上下文中的2 <= length，这样就可以完成证明了。

使用 Fix 或 Program Fixpoint 在 Coq 中编写有根据的程序

Writing well-founded programs in Coq using Fix or Program Fixpoint

coq