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

Question

遵循章节GeneralRec 中给出的示例在 Chlipala 书中，我正在尝试编写归并排序算法。

这是我的代码

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).

相反，可以使用命令 Program Fixpoint或 Definition使用术语 Fix (如在 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)。

回想一下，模式匹配的目的是(松散地说)

解压缩归纳数据类型的某些值的组件并将它们绑定(bind)到某些名称(我们将在答案的第二部分中需要它)和

用相应模式匹配分支中的特殊情况替换原始定义。

现在，观察 split l在我们对其进行模式匹配之前，它不会出现在目标或上下文中的任何地方。我们只是随意地将其引入定义中。这就是为什么模式匹配没有给我们任何东西——我们不能替换 split l在目标或上下文中使用其“特殊情况”( (ll,lr) )，因为没有 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短于 l当 2 <= length l .

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

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

要么我们记得leb 2 (length l)作为一个方程(就像我们在第一部分中所做的那样)，或

我们可以使用一些比较函数，其结果类型类似于 bool (因此它可以代表两种选择)，但它还应该记住我们需要的一些额外信息。然后我们可以对比较结果进行模式匹配并提取信息，当然，在这种情况下必须是 2 <= length l 的证明。 .

我们需要的是能够携带 m <= n 证明的类型在 leb m n 的情况下返回 true和一个证明，比如说， 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 .它的优势超过 bool当您使用 if 对其进行案例分析时显示: 你得到 A 的证明在 then分支和 B 的证明在 else分支。换句话说，您可以使用事先保存的上下文，而 bool不携带任何上下文(仅在程序员的脑海中)。

而我们正是需要的!好吧，不在 else分支，但我们想得到 2 <= length l在我们的 then分支。所以，让我们问问 Coq 是否已经有一个返回类型的比较函数:

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在证明上下文中，这将使我们完成证明。