recursion - 嵌套递归和 `Program Fixpoint` 或 `Function`

Question

我想使用 Program Fixpoint 定义以下函数或Function在 Coq 中:

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 中使用 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命令用来查明终止证明只需要考虑t ∈ set ts ..

如果这样的引理不可用，例如因为我定义了

definition "map' = map"

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

declare map_cong[folded map'_def,fundef_cong]

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.