示教coq检查终止

Question

与其他许多不同的是，Coq接受一个可选的显式参数，该参数可用于指示固定点定义的递减结构。

来自Gallina规范，1.3.4，

Fixpoint ident params {struct ident0 } : type0 := term0

定义语法。但是通过它，我们知道它必须是一个标识符，而不是一个通用的度量。

然而，一般来说，有一些递归函数，其终止并不是很明显，或者实际上是，但对于终止检查器来说，只是很难找到递减结构。例如，下面的程序交错了两个列表，

Fixpoint interleave (A : Set) (l1 l2 : list A) : list A :=
  match l1 with
  | [] => []
  | h :: t => h :: interleave l2 t
  end

这个函数显然是终止了，而Coq就是不能弄清楚。原因是l1和l2在每个周期都不会下降。但是，如果我们考虑一个定义为length l1 + length l2的度量呢？那么这个度量显然减少了每一次递归。

因此，我的问题是，在复杂的情况下，代码不能直接以可终止检查的方式组织，您如何教育coq并说服它接受固定点定义？

Answer 1

您有多个选项，所有这些选项最终都归结为结构递归。

前言

From Coq Require Import List.
Import ListNotations.
Set Implicit Arguments.

结构递归

有时你可以用结构递归的方式重新制定你的算法：

Fixpoint interleave1 {A} (l1 l2 : list A) {struct l1} : list A :=
  match l1, l2 with
  | [], _ => l2
  | _, [] => l1
  | h1 :: t1, h2 :: t2 => h1 :: h2 :: interleave1 t1 t2
  end.

顺便说一句，在某些情况下，您可以使用嵌套fixes的技巧--参见this definition of Ackermann function (它不适用于Fixpoint)。

Program Fixpoint

你可以使用Program Fixpoint机制，它可以让你自然地编写程序，然后证明它总是会终止。

From Coq Require Import Program Arith.

Program Fixpoint interleave2 {A} (l1 l2 : list A) 
  {measure (length l1 + length l2)} : list A :=
  match l1 with
  | [] => l2
  | h :: t => h :: interleave2 l2 t
  end.
Next Obligation. simpl; rewrite Nat.add_comm; trivial with arith. Qed.

Function

另一种选择是使用Function命令，与Program Fixpoint相比，该命令可能有一定的限制。你可以找到更多关于他们的不同之处here。

From Coq Require Recdef.

Definition sum_len {A} (ls : (list A * list A)) : nat :=
  length (fst ls) + length (snd ls).

Function interleave3 {A} (ls : (list A * list A))
  {measure sum_len ls} : list A :=
  match ls with
  | ([], _) => []
  | (h :: t, l2) => h :: interleave3 (l2, t)
  end.
Proof.
  intros A ls l1 l2 h t -> ->; unfold sum_len; simpl; rewrite Nat.add_comm; trivial with arith.
Defined.

Equations插件

这是一个外部插件，解决了在Coq中定义函数的许多问题，包括依赖类型和终止。

From Equations Require Import Equations.

Equations interleave4 {A} (l1 l2 : list A) : list A :=
interleave4 l1 l2 by rec (length l1 + length l2) lt :=
interleave4 nil l2 := l2;
interleave4 (cons h t) l2 := cons h (interleave4 l2 t).
Next Obligation. rewrite Nat.add_comm; trivial with arith. Qed.

如果您应用this fix，则上面的代码可以正常工作。

Fix / Fix_F_2组合器

如果您遵循this question中关于mergeSort函数的链接，您可以了解有关此(手动)方法的更多信息。顺便说一句，如果应用我前面提到的嵌套mergeSort技巧，就可以在不使用Fix的情况下定义fix函数。下面是一个使用Fix_F_2组合器的解决方案，因为我们有两个参数，而不是像mergeSort这样的参数

Definition ordering {A} (l1 l2 : list A * list A) : Prop :=
  length (fst l1) + length (snd l1) < length (fst l2) + length (snd l2).

Lemma ordering_wf' {A} : forall (m : nat) (p : list A * list A),
    length (fst p) + length (snd p) <= m -> Acc (@ordering A) p.
Proof.
  unfold ordering; induction m; intros p H; constructor; intros p'.
  - apply Nat.le_0_r, Nat.eq_add_0 in H as [-> ->].
    intros contra%Nat.nlt_0_r; contradiction.
  - intros H'; eapply IHm, Nat.lt_succ_r, Nat.lt_le_trans; eauto.
Defined.

Lemma ordering_wf {A} : well_founded (@ordering A).
Proof. now red; intro ; eapply ordering_wf'. Defined.

(* it's in the stdlib but unfortunately opaque -- this blocks evaluation *)
Lemma destruct_list {A} (l : list A) :
  { x:A & {tl:list A | l = x::tl} } + { l = [] }.
Proof.
  induction l as [|h tl]; [right | left]; trivial.
  exists h, tl; reflexivity.
Defined.

Definition interleave5 {A} (xs ys : list A) : list A.
  refine (Fix_F_2 (fun _ _ => list A)
    (fun (l1 l2 : list A)
       (interleave : (forall l1' l2', ordering (l1', l2') (l1, l2) -> list A)) =>
       match destruct_list l1 with
       | inright _ => l2
       | inleft pf => let '(existT _ h (exist _ tl eq)) := pf in
                     h :: interleave l2 tl _
       end) (ordering_wf (xs,ys))).
Proof. unfold ordering; rewrite eq, Nat.add_comm; auto.
Defined.

评估测试

Check eq_refl : interleave1 [1;2;3] [4;5;6] = [1;4;2;5;3;6].
Check eq_refl : interleave2 [1;2;3] [4;5;6] = [1;4;2;5;3;6].
Check eq_refl : interleave3 ([1;2;3], [4;5;6]) = [1;4;2;5;3;6].
Fail Check eq_refl : interleave4 [1;2;3] [4;5;6] = [1;4;2;5;3;6]. (* Equations plugin *)
Check eq_refl : interleave5 [1;2;3] [4;5;6] = [1;4;2;5;3;6].

练习:如果注释掉destruct_list引理，最后一次检查会发生什么？

Answer 2

您可以使用称为measure的东西来代替结构参数进行终止。为此，我相信您必须使用Program Fixpoint机制，该机制有点复杂，会使您的证明看起来更丑陋(因为它会根据您提供的证明生成一个结构递归，因此您实际使用的函数并不完全是您编写的函数)。

详情请访问：https://coq.inria.fr/refman/program.html

看起来Equations也可以处理度量？请参阅http://mattam82.github.io/Coq-Equations/examples/RoseTree.html https://www.irif.fr/~sozeau/research/coq/equations.en.html