Coq 中的递归偏函数

Question

我想知道在 Coq 中定义偏递归函数的最佳方式是什么。

假设我想定义一个returns 自然数列表的最大元素的函数。但是，我们希望只为非空列表定义此函数。

我一直在尝试以下方法：

Fixpoint MaxValueList (l : list nat | l <> []) : nat :=
match l with
|[n] => n
|n::l' => (max n (MaxValueList l'))
end.

但是，这是行不通的，因为 :: 是列表的构造函数，而不是 {l : list nat | l <> []}。

我的另一个尝试是使用 option。在这种情况下，我尝试了以下方法：

Fixpoint MaxValueList (l : list nat | l <> []) : option nat :=
match l with
|[] => None
|[n] => n
|n::l' => (max n (MaxValueList l'))
end.

这也不起作用，因为 max : nat -> nat -> nat 和 MaxValueList l' : option nat。

Answer 1

一种替代方法是使用 refine 策略来构造使用类似定理证明风格的函数。

每当我需要构建带有证明的术语（比如你的函数）时，我更喜欢使用定义和优化策略，因为它提供了一种更清晰、更简单的方法来自动证明关于命题的证明。

下面是我在简单形式化中定义的类似函数。您可以轻松修改它以强制执行非空列表输入要求。思路是使用refine tactic来提供函数的结构，函数属性的证明项标有空洞“_”，后面填上tactics。

Definition max_list : forall (l : list nat), {n | forall n', In n' l -> n > n'}.
  refine (fix max_list (l : list nat) : {n | forall n', In n' l -> n > n'} :=
        match l with
          | nil => exist _ 0 _
          | x :: l' =>
            match max_list l' with
              exist x' _ =>
                match le_gt_dec x x' with
                  | left _ => exist _ (S x') _
                  | right _ => exist _ (S x) _
                end
            end
        end) ; clear max_list  ; simpl in * ; intuition ;
               try (match goal with
                      | [H : context[In _ _ -> _],
                         H1 : In _ _ |- _] => apply H in H1 ; try omega
                    end).
Defined.

所谓的 Program 功能可以简化使用依赖类型编写函数。也许值得检查一下。我的经验是它会产生一些复杂的假设，因此，我更喜欢使用 refine.

Answer 2

以下是您的问题的可能解决方案：

Require Import Coq.Lists.List.
Import ListNotations.

Definition MaxValueListAux (n : nat) (l : list nat) : nat :=
  fold_left max l n.

Definition MaxValueListNE (l : list nat) : l <> [] -> nat :=
  match l with
  | []      => fun H => match H eq_refl with end
  | n :: l' => fun _ => MaxValueListAux n l'
  end.

在这里，我将原来的 MaxValueList 分成两部分：MaxValueListAux 函数计算给定默认值的列表的最大元素，以及 MaxValueListNE，它是第一个函数的包装器并接受一个证明参数。第二个函数只是排除了不可能的情况，并用适当的参数调用第一个函数；我将很快解释这究竟是如何工作的。由于这种分裂，我们不运行讨论在 MaxValueListNE 的非空分支中构建证明参数的问题；我们唯一要做的证明工作就是去掉空盒子。

请注意，第二个函数的编写方式很奇怪：我没有将 l <> [] 声明为 MaxValueListNE 的另一个参数，而是将其置于 return 类型中功能。这是因为依赖模式匹配在 Coq 中的工作方式；粗略地说，每当您需要将在 match 上获得的信息（例如 l 在 [] 分支上为空的事实）与来自 [=66 的信息结合起来时=]匹配（比如l <> []的证明），你需要让你的match语句return成为一个函数。这导致 Adam Chlipala 称之为 convoy pattern 的技巧，您可以了解有关 here 的更多信息。将该参数作为 return 类型的一部分允许 Coq 推断 match 语句所需的类型注释。

那么，MaxValueListNE 究竟是如何运作的呢？要理解这一点，我们必须稍微谈谈依赖模式匹配在 Coq 中是如何工作的。正如我之前提到的，我们以这种特殊方式编写这个函数，以便 Coq 可以推断出一些缺失的类型注释。但我们也可以手动添加：

Definition MaxValueListNE (l : list nat) : l <> [] -> nat :=
  match l return l <> [] -> nat with
  | []      => fun (H : [] <> [])      => match H eq_refl with end
  | n :: l' => fun (_ : n :: l' <> []) => MaxValueListAux n l'
  end.

当 Coq 读取这个定义时，它会尝试对函数进行类型检查，特别是确保 match return 的每个分支都是它承诺的类型的元素return。但是这样做时，允许用对应于该分支的任何值替换每次出现的判别项（在这种情况下，l）。在上面的第一个分支中，这意味着用 [] 替换 l，这反过来意味着 returned 函数接受类型 [] <> [] 的参数。回想一下，在 Coq 中，[] <> [] 与 [] = [] -> False 是一样的。由于 False 没有构造函数，我们可以通过 H eq_refl 上的模式匹配来摆脱那个矛盾的分支，其中 eq_refl 是唯一的相等类型的构造函数，并且被认为具有类型[] = [] 在这种情况下。

现在，值得注意的是，添加更多的类型信息并不一定是好的。对于您的函数，我更愿意省略证明参数并简单地写 Definition MaxValueList l := fold_left max l 0。请注意，0 是 max 的中性元素，因此 return 该值在空情况下是有意义的。例如，它允许我们证明像

这样的结果

forall l1 l2, MaxValueList (l1 ++ l2) = max (MaxValueList l1) (MaxValueList l2)

当然，这并不适用于所有情况：如果我们将 max 替换为 min，则上述定理将不再成立。不过，我认为使用适用于任意列表的 MinValueList 函数进行编程和推理仍然会更容易：如果有关该函数的某些结果仅适用于非空元素，我们可以将这些假设添加到我们的定理中：

forall l1 l2, l1 <> [] -> 
  MinValueList (l1 ++ l2) = min (MinValueList l1) (MinValueList l2).

这就是人们通常在 Coq 中定义除法的方式。我们没有使用部分函数 div : forall (n1 n2 : nat), n2 <> 0 -> nat，而是编写了总函数 div : nat -> nat -> nat，并证明了关于该函数的定理假设其第二个参数不为零。

Answer 3

convoy 模式是必须要理解的，但是使用 Program 可以避免其中的一些推理。 Program 还可以让您编写外观更正常的程序。我还没有真正使用过它，所以我会借此机会尝试一下。

Require Import Coq.Lists.List.
Import ListNotations.
Require Import Coq.Program.Wf.

您可以从 false 派生出您需要的任何类型的值。在匹配语句中的不可能分支中很有用。

Definition IMPOSSIBLE {T} (f:False):T := match f with end.

Program Fixpoint maxval (l:list nat) (H:l<>nil) {measure (length l)} : nat :=
  match l with
    | []       => IMPOSSIBLE _
    | [a]      => a
    | a::b::l' => max a (maxval (b::l') _)
  end.

编辑：正如eponier指出的那样，如果我们在定义maxval之前包含Require Import Arith.，我们将在这里完成。否则我们将不得不证明剩余的义务，如下所示：(END EDIT)

Next Obligation.

现在我们只需要证明递归终止即可。目标是

============================
 well_founded
   (MR lt (fun recarg : {l : list nat & l <> []} => length (projT1 recarg)))

编辑：eponier 指出这很容易被 apply measure_wf, PeanoNat.Nat.lt_wf_0.

证明

Coq 中的递归偏函数

Recursive partial functions in Coq

recursion

coq