嵌套递归和`程序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命令相关的命令(AFAIK)时也会发生的事情:

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所有树上的果子持有t'出现ts.

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

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.

Answer 2

您现在可以使用方程式执行此操作，并使用结构嵌套递归或有根据的递归自动获得正确的消除原理

Answer 3

一般来说，建议避免此问题。但如果真想获得Isabelle给你的举证义务，这里有一个方法：

\n\n

在伊莎贝尔中，我们可以给出一个外部引理来统计map仅将其参数应用于给定列表的成员。在 Coq 中，我们不能在外部引理中做到这一点，但我们可以在类型中做到这一点。所以而不是普通类型的地图

\n\n

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

\n\n

我们希望类型为 \xe2\x80\x9cf只应用于列表的元素：

\n\n

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

\n\n

（它需要重新排序参数，以便类型f可以提及xs）。

\n\n

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

\n\n

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

\n\n

但你也可以手写\xe2\x80\x9c\xe2\x80\x9d：

\n\n

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

\n\n

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

\n\n

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

\n\n

我不需要对 的新参数做任何事情f，但它会根据需要显示在终止证明义务中In t ts \xe2\x86\x92 height t < height (Node x ts)。所以我可以证明并定义mapTree：

\n\n

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

\n\n

不幸的是，它仅适用于Program Fixpoint，不适用于Function。

\n