教 coq 检查终止
Teach coq to check termination
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 并说服它接受定点定义？
您可以使用称为 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
你有多种选择，最后都归结为结构递归。
前言
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 相比，它可能会有所限制。您可以了解更多关于它们的差异 .
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 组合器
如果您点击 中关于 mergeSort 函数的链接，您可以了解有关此（手动）方法的更多信息。顺便说一句，如果您应用我之前提到的嵌套 fix 技巧，则可以在不使用 Fix 的情况下定义 mergeSort 函数。这是一个使用 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 引理，最后一次检查会发生什么情况？
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 并说服它接受定点定义？
您可以使用称为 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
你有多种选择，最后都归结为结构递归。
前言
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 相比，它可能会有所限制。您可以了解更多关于它们的差异
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 组合器
如果您点击 mergeSort 函数的链接，您可以了解有关此（手动）方法的更多信息。顺便说一句，如果您应用我之前提到的嵌套 fix 技巧，则可以在不使用 Fix 的情况下定义 mergeSort 函数。这是一个使用 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 引理，最后一次检查会发生什么情况？