使用Fix或Program Fixpoint在Coq中编写有良好基础的程序 [英] Writing well-founded programs in Coq using Fix or Program Fixpoint

问题描述

按照Chlipala的 GeneralRec 一章中给出的示例进行操作，我正在尝试编写mergesort算法。

Following the example given in the chapter GeneralRec of Chlipala book, I'm trying to write the mergesort algorithm.

这是我的代码

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 ，因为该函数在结构上并未降低：

The problem is that it is not possible to write the mergeSort function with the command Fixpoint since the function is not structurally decreasing :

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 或定义，并用术语修复（如Chlipala书中所述）。

Instead, one can use the command Program Fixpoint or Definition with the term Fix (as in Chlipala book).

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

However, if I'm writing this

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

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

I'm getting impossible goals :

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的定义：

That is why Chlipala suggests to change the definition of mergeSort this way:

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

这个新定义对我来说听起来像是魔术。所以我想知道：

This new definition sounds like magic to me. So I wonder:

• 第一个定义是否仍然可以证明该函数的正确性？


• 否则第一个定义为什么行不通？


• 基本用户如何轻松地从第一个定义转到第二个定义？

推荐答案

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

It's easy to see that you need to make two changes in order to get to A. Chlipala's solution.

1）执行拆分时，您需要以某种方式记住 ll 和 lr 来自拆分，否则它们将是一些任意列表，不能短于原始列表 l 。

1) When doing split you somehow need to remember that ll and lr came from split, otherwise they would be some arbitrary lists, which cannot possibly be shorter than the original list l.

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

The following piece of code fails to save that kind of information:

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 ，这种情况发生在ause let（ll，lr）只是 match 的伪装（请参见手册§2.2.3）。

The failure happens due to Coq's inability to remember that ll and lr come from split l and that happens because let (ll,lr) is just match in disguise (see the manual, §2.2.3).

回想一下，模式匹配的目的是（宽松地说）

Recall that the aims of pattern-matching is to (loosely speaking)

• 将归纳数据类型的某些值的组件拆包，然后将它们绑定到某些名称（我们在答案的第二部分中将需要使用此名称），并且


• 在相应的模式中将原始定义替换为其特殊情况匹配分支。

• unpack the components of some value of an inductive datatype and bind them to some names (we'll need this in the 2nd part of my answer) and
• replace the original definition with its special cases in the corresponding pattern-match branches.

现在，注意分割l 在我们进行模式匹配之前，在目标或上下文中的任何地方都不会发生。我们只是随意地将其引入定义中。这就是为什么模式匹配不能给我们任何东西-我们不能将 split l 替换为其特殊情况（（ll，lr ）），因为在任何地方都没有拆分l 。

Now, observe that split l does not occur anywhere in the goal or context before we pattern-match on it. We just arbitrarily introduce it into the definition. That's why pattern-matching doesn't give us anything -- we can't replace split l with its "special case" ((ll,lr)) in the goal or context, because there is no split l anywhere.

使用逻辑相等（ = ）还有另一种方法：

There is an alternative way of doing this by using logical equality (=):

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

这类似于使用记住策略。我们已经摆脱了 fst 和 snd ，但这是一个巨大的矫over过正，我不建议这样做。

This is analogous to using the remember tactic. We've got rid of fst and snd, but it is a huge overkill and I wouldn't recommend it.

2）我们需要证明的另一件事是 ll 2 <=长度l 和 lr 短于 l c $ c>。

2) Another thing we need to prove is the fact that ll and lr are shorter than l when 2 <= length l.

由于如果表达式是匹配也可以伪装（它适用于具有恰好两个构造函数的任何归纳数据类型），我们需要某种机制来记住 leb 2（length l）= true 然后然后分支。同样，由于我们在任何地方都没有 leb ，因此这些信息会丢失。

Since an if-expression is a match in disguise as well (it works for any inductive datatype with exactly two constructors), we need some mechanism to remember that leb 2 (length l) = true in the then branch. Again, since we don't have leb anywhere, this information gets lost.

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

There are at least two possible solutions to the problem:

• 我们还记得 leb 2（长度为l）为方程（就像我们在第1部分中所做的那样），或者


• 我们可以对结果类型使用某些比较函数，例如 bool （因此它可以代表两种选择），但它还应该记住我们需要的一些其他信息。然后，我们可以对比较结果进行模式匹配并提取信息，当然，在这种情况下，它必须是 2 <==长度l 的证明。 / li>
  

• either we remember leb 2 (length l) as an equation (just as we did in the 1st part), or
• we can use some comparison function with result type behaving like bool (so it can represent two alternatives), but it should also remember some additional information we need. Then we could pattern-match on the comparison result and extract the information, which, of course, in this case have to be a proof of 2 <= length l.

我们需要的是一种能够携带 m< = n 在 leb mn 返回 true 并证明 m> n 否则。
标准库中有一个类型可以做到这一点！它称为 sumbool ：

What we need is a type which is able to carry a proof of m <= n in the case when leb m n returns true and a proof of, say, m > n otherwise. There is a type in the standard library that does exactly that! It's called sumbool:

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

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

{A} + {B} is just a notation (syntactic sugar) for sumbool A B. Just as bool, it has two constructors, but in addition it remembers a proof of either of two propositions A and B. Its advantage over bool shows up when you do case analysis on it with if: you get a proof of A in the then branch and a proof of B in the else branch. In other words, you get to use context you saved beforehand, whereas bool doesn't carry any context (only in the mind of the programmer).

我们正是需要！好吧，不是在 else 分支中，而是我们希望在我们的<$中获得 2< =长度l c $ c>然后分支。因此，让我们问一下Coq是否已经具有比较函数，其返回类型如下：

And we need exactly that! Well, not in the else branch, but we would like to get 2 <= length l in our then branch. So, let us ask Coq if it already has a comparison function with the return type like that:

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}
*)

任何都可以，因为我们需要一个

Any of the five results would do, because we need a proof only in one case.

因此，如果leb 2（长度为l），我们可以替换，那么... 与如果le_lt_dec 2（长度l）... 并在证明上下文中获得 2< =长度让我们来完成证明。

Hence, we can replace if leb 2 (length l) then ... with if le_lt_dec 2 (length l) ... and get 2 <= length in the proof context, which will let us finish the proof.

这篇关于使用Fix或Program Fixpoint在Coq中编写有良好基础的程序的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！