嵌套递归和“程序固定点"或“功能" [英] Nested recursion and `Program Fixpoint` or `Function`

问题描述

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

I’d like to define the following function using Program Fixpoint or Function in 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的成员.

Unfortunately, at this point I have a proof obligation height t < height (Node x ts) without knowing that t is a member of ts.

与Function而不是Program Fixpoint类似，只有Function会检测到问题并中止定义:

Similarly with Function instead of Program Fixpoint, only that Function detects the problem and aborts the definition:

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).

I would expect to get a proof obligation of In t ts → height t < height (Node x ts).

有没有一种方法不涉及重构函数定义? (例如，我知道一些变通方法需要在这里内嵌map的定义–我想避免这些.)

Is there a way of getting that that does not involve restructuring the function definition? (I know work-arounds that require inlining the definition of map here, for example – I’d like to avoid these.)

为了证明这一期望，让我展示使用function命令在Isabelle中执行相同操作时发生的情况，该命令与Coq的Function命令相关(AFAIK):

To justify that expectation, let me show what happens when I do the same in Isabelle, using the function command, which is (AFAIK) related to Coq’s Function command:

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.

In the termination proof, I get the assumption t ∈ set ts.

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

Note that Isabelle does not require a manual termination proof here, and the following definition works just fine:

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

之所以可行，是因为map函数具有以下形式的同余引理"

This works because the map function has a "congruence lemma" of the form

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

function命令用来发现终止证明只需要考虑t ∈ set ts的

.

that the function command uses to find out that the termination proof only needs to consider t ∈ set ts..

如果没有这样的引理，例如因为我定义了

If such a lemma is not available, e.g. because I define

definition "map' = map"

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

and use that in mapTree, I get the same unprovable proof obligation as in Coq. I can make it work again by declaring a congruence lemma for map', e.g. using

declare map_cong[folded map'_def,fundef_cong]

推荐答案

通常，建议避免该问题.但是，如果您真的想获得Isabelle赋予您的证明义务，可以采用以下方法:

In general, it might be advisable to avoid this problem. But if one really wants to obtain the proof obligation that Isabelle gives you, here is a way:

在Isabelle中，我们可以给出一个外部引理，说明map仅将其参数应用于给定列表的成员.在Coq中，我们无法在外部引理中执行此操作，但可以在类型中执行此操作.所以不是正常的地图类型

In Isabelle, we can give an external lemma that stats that map applies its arguments only to members of the given list. In Coq, we cannot do this in an external lemma, but we can do it in the type. So instead of the normal type of map

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

我们希望类型说"f仅应用于列表的元素:

we want the type to say "f is only ever applied to elements of the list:

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

(它需要对参数进行重新排序，以便f的类型可以提及xs).

(It requires reordering the argument so that the type of f can mention xs).

编写此功能并非易事，我发现使用证明脚本更容易:

Writing this function is not trivial, and I found it easier to use a proof script:

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.

但是您也可以手工"编写它:

But you can also write it "by hand":

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中使用此功能，即

In either case, the result is nice: I can use this function in mapTree, i.e.

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:

and I don’t have to do anything with the new argument to f, but it shows up in the the termination proof obligation, as In t ts → height t < height (Node x ts) as desired. So I can prove that and define 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.

It only works with Program Fixpoint, not with Function, unfortunately.

这篇关于嵌套递归和“程序固定点"或“功能"的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！