教coq检查终止 [英] Teach coq to check termination

问题描述

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

Coq, unlike many others, accepts an optional explicit parameter,which can be used to indicate the decreasing structure of a fixpoint definition.

根据Gallina规范1.3.4，

From Gallina specification, 1.3.4,

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

定义语法.但是从中我们知道它必须是一个标识符，而不是一般的度量.

defines the syntax. but from it, we've known that it must be an identifier, instead of a general measure.

但是，总的来说，存在递归函数，终止不是很明显，或者实际上是终止，但是对于终止检查器来说，找到递减结构是很困难的.例如，以下程序交错两个列表，

However, in general, there are recursive functions, that the termination is not quite obvious,or it in fact is, but just difficult for the termination checker to find a decreasing structure. For example, following program interleaves two lists,

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的度量，该怎么办?然后，此措施显然会减少每次递归.

This function clearly terminates, while Coq just couldn't figure it out. The reason is neither l1 nor l2 are decreasing every cycle. But what if we consider a measure, defined to be length l1 + length l2? Then this measure clearly decreases every recursion.

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

So my question is, in the case of sophisticated situation, where code is not straightforward to be organized in a termination checkable way, how do you educate coq and convince it to accept the fixpoint definition?

推荐答案

您有多个选择，所有这些最终都归结为结构性递归.

You have multiple options and all of them boil down to structural recursion in the end.

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

结构递归

有时候，您可以以结构上递归的方式重新构造算法:

Structural recursion

Sometimes you can reformulate your algorithm in a structurally recursive way:

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.

偶然地，在某些情况下，您可以使用嵌套fix es的技巧-请参阅此Ackermann函数的定义(仅Fixpoint不能使用.)

Incidentally, in some cases you can use a trick with nested fixes -- see this definition of Ackermann function (it wouldn't work with just Fixpoint).

您可以使用Program Fixpoint机制，让您自然地编写程序，并在以后证明它总是终止.

You can use Program Fixpoint mechanism which lets you write your program naturally and later prove that it always terminates.

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相比，该命令可能会受到一些限制.您可以在此处中找到有关它们之间差异的更多信息.

Function

Another option is to use the Function command which can be somewhat limited compared to Program Fixpoint. You can find out more about their differences 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.

方程插件

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

Equations plugin

This is an external plugin which addresses many issues with defining functions in Coq, including dependent types and termination.

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.

如果您应用此修复程序，则上述代码将起作用.

The code above works if you apply this fix.

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

You can learn more about this (manual) approach if you follow the links from this question about mergeSort function. By the way, the mergeSort function can be defined without using Fix if you apply the nested fix trick I mentioned earlier. Here is a solution which uses Fix_F_2 combinator since we have two arguments and not one like 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引理，最后一次检查会发生什么?

Exercise: what happens with this last check if you comment out destruct_list lemma?

这篇关于教coq检查终止的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！