嵌套递归和“程序修复点”或“函数”

Question

我想使用 Coq 中的 Program Fixpoint 或 Function 来定义以下函数：

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

Inductive Tree := Node : nat -> list Tree -> Tree.

Fixpoint height (t : Tree) : nat :=
  match t with
   | Node x ts => S (fold_right Nat.max 0 (map height ts))
  end.

Program Fixpoint mapTree (f : nat -> nat) (t : Tree)  {measure (height t)} : Tree :=
  match t with 
    Node x ts => Node (f x) (map (fun t => mapTree f t) ts)
  end.
Next Obligation.

不幸的是，此时我有一个证明义务：height t < height (Node x ts)，但不知道t是否是ts的成员。

类似地，如果使用Function而不是Program Fixpoint，只是Function会检测到问题并中止定义：

Error:
the term fun t : Tree => mapTree f t can not contain a recursive call to mapTree

我期望得到一个证明义务，其形式为In t ts → height t < height (Node x ts)。

有没有一种方法可以不重构函数定义来实现这一点？（例如，我知道需要在此处内联map的定义的解决方法 - 我想避免这种情况。）

Isabelle 为了证明这个期望，让我展示一下在Isabelle中执行相同操作时会发生什么，使用的是function命令，它与Coq的Function命令相关（据我所知）。

theory Tree imports Main begin

datatype Tree = Node nat "Tree list"

fun height where
  "height (Node _ ts) = Suc (foldr max (map height ts) 0)"

function mapTree where
  "mapTree f (Node x ts) = Node (f x) (map (λ t. mapTree f t) ts)"
by pat_completeness auto

termination
proof (relation "measure (λ(f,t). height t)")
  show "wf (measure (λ(f, t). height t))" by auto
next
  fix f :: "nat ⇒ nat" and x :: nat  and ts :: "Tree list" and t
  assume "t ∈ set ts"
  thus "((f, t), (f, Node x ts))  ∈ measure (λ(f, t). height t)"
    by (induction ts) auto
qed

在终止证明中，我得到假设 t ∈ set ts。

请注意，Isabelle 在这里不需要手动终止证明，以下定义也可以正常工作：

fun mapTree where
  "mapTree f (Node x ts) = Node (f x) (map (λ t. mapTree f t) ts)"

这是因为map函数具有形式为“同余引理”的特性。

xs = ys ⟹ (⋀x. x ∈ set ys ⟹ f x = g x) ⟹ map f xs = map g ys

“function”命令使用的是“set ts”集合中的“t”，以确定终止证明只需要考虑这个部分。如果没有这样的引理可用，例如因为我定义了…

definition "map' = map"

“并在`mapTree`中使用它，我得到了与Coq中相同的无法证明的证明义务。我可以通过声明`map'`的同余引理来使其再次工作，例如使用…”

declare map_cong[folded map'_def,fundef_cong]

- Joachim Breitner

Answer 1

在这种情况下，实际上您不需要完全具备良好基础递归的普遍性：

Require Import Coq.Lists.List.

Set Implicit Arguments.

Inductive tree := Node : nat -> list tree -> tree.

Fixpoint map_tree (f : nat -> nat) (t : tree) : tree :=
  match t with
  | Node x ts => Node (f x) (map (fun t => map_tree f t) ts)
  end.

Coq 能够自动推断出递归调用 map_tree 是在严格的子项上进行的。然而，证明有关这个函数的任何事情都很困难，因为为 tree 生成的归纳原理是没有用处的：

tree_ind : 
  forall P : tree -> Prop, 
    (forall (n : nat) (l : list tree), P (Node n l)) ->
    forall t : tree, P t

这其实是你之前描述的同一个问题。幸运的是，我们可以通过提供自己的归纳原理与证明项来解决该问题。

Require Import Coq.Lists.List.
Import ListNotations.

Unset Elimination Schemes.
Inductive tree := Node : nat -> list tree -> tree.
Set Elimination Schemes.

Fixpoint tree_ind
  (P : tree -> Prop)
  (IH : forall (n : nat) (ts : list tree),
          fold_right (fun t => and (P t)) True ts ->
          P (Node n ts))
  (t : tree) : P t :=
  match t with
  | Node n ts =>
    let fix loop ts :=
      match ts return fold_right (fun t' => and (P t')) True ts with
      | [] => I
      | t' :: ts' => conj (tree_ind P IH t') (loop ts')
      end in
    IH n ts (loop ts)
  end.

Fixpoint map_tree (f : nat -> nat) (t : tree) : tree :=
  match t with
  | Node x ts => Node (f x) (map (fun t => map_tree f t) ts)
  end.

Unset Elimination Schemes命令可以防止Coq为tree生成其默认的（且无用的）归纳原理。在归纳假设中出现的fold_right只是表达谓词P适用于出现在ts中的每个树t'。

以下是您可以使用此归纳原理证明的语句:

Lemma map_tree_comp f g t :
  map_tree f (map_tree g t) = map_tree (fun n => f (g n)) t.
Proof.
  induction t as [n ts IH]; simpl; f_equal.
  induction ts as [|t' ts' IHts]; try easy.
  simpl in *.
  destruct IH as [IHt' IHts'].
  specialize (IHts IHts').
  now rewrite IHt', <- IHts.
Qed.

- Arthur Azevedo De Amorim

---

在这种情况下，您实际上不需要完全递归基础。我猜我把例子简化得太多了。它之所以有效，是因为map使用本地不动点进行了精确定义，并且终止检查器可以穿透其内部。如果我在不那么规范的情况下递归，而我确实需要良好基础的递归，该怎么办？ - Joachim Breitner

另外，感谢“Unset Elimination Schemes” - 这是否会使 Coq 在执行“induction t”时选择“tree_ind”？ - Joachim Breitner

Coq总是选择foo_ind作为对名为foo的归纳类型进行归纳的方式。 - Arthur Azevedo De Amorim

哈，这很有趣，也很好知道。是否有混淆的 Coq 证明比赛？ - Joachim Breitner

Answer 2

现在，您可以使用方程式并自动获得正确的消元原理，使用结构嵌套递归或良基递归。

- Matthieu Sozeau

---

我喜欢map_In的定义方式，因为它不需要像我的答案那样进行证明！尽管我不理解为什么——递归调用map_In中参数中的_是如何解析的？（可能是到术语or_intror H。） - Joachim Breitner

使用“program_simpl”策略自动填充漏洞，它在这里调用了“auto”。我猜这足以解决它们。否则你会得到证明义务，没有魔术，证明仍然存在！ - Matthieu Sozeau

Answer 3

一般而言，避免这个问题可能是明智的选择。但是如果确实想要获得 Isabelle 给出的证明义务，可以通过以下方式实现：

在 Isabelle 中，我们可以给出一个外部引理，它说明 map 只将其参数应用于给定列表的成员。在 Coq 中，我们无法在外部引理中这样做，但可以在类型中这样做。因此，我们使用不同于 map 的常规类型。

forall A B, (A -> B) -> list A -> list B

我们希望这个类型表示“f 只能应用于列表中的元素”：

forall A B (xs : list A), (forall x : A, In x xs -> B) -> list B

需要重新排列参数，以便 f 的类型可以提到 xs。

编写这个函数并不容易，我发现使用证明脚本更容易:

Definition map {A B} (xs : list A) (f : forall (x:A), In x xs -> B) : list B.
Proof.
  induction xs.
  * exact [].
  * refine (f a _ :: IHxs _).
    - left. reflexivity.
    - intros. eapply f. right. eassumption.
Defined.

但你也可以“手写”它：

Fixpoint map {A B} (xs : list A) : forall (f : forall (x:A), In x xs -> B), list B :=
  match xs with
   | [] => fun _ => []
   | x :: xs => fun f => f x (or_introl eq_refl) :: map xs (fun y h => f y (or_intror h))
  end.

无论哪种情况，结果都很好：我可以在mapTree中使用此函数。

Program Fixpoint mapTree (f : nat -> nat) (t : Tree)  {measure (height t)} : Tree :=
  match t with 
    Node x ts => Node (f x) (map ts (fun t _ => mapTree f t))
  end.
Next Obligation.

我不需要对f的新参数做任何事情，但它出现在终止证明义务中，如所需的In t ts → height t < height (Node x ts)。因此，我可以证明并定义mapTree：

  simpl.
  apply Lt.le_lt_n_Sm.
  induction ts; inversion_clear H.
  - subst. apply PeanoNat.Nat.le_max_l.
  - rewrite IHts by assumption.
    apply PeanoNat.Nat.le_max_r.
Qed.

不幸的是，它只能与Program Fixpoint一起使用，而不能与Function一起使用。

- Joachim Breitner