下面的章节给出的例子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.
问题是不可能用命令编写mergeSort函数,Fixpoint因为函数没有在结构上减少:
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
这个新定义对我来说听起来很神奇.所以我想知道:
很容易看出你需要进行两次更改才能获得A. Chlipala的解决方案.
1)在做某事时split你需要记住它ll并且lr来自分裂,否则它们将是一些任意列表,它们不可能比原始列表短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).
回想一下模式匹配的目的是(松散地说)
现在,观察在我们对其进行模式匹配之前,目标或上下文中的任何位置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-expression是一种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在证据方面,这将让我们完成了证明.