1

这里提到的树有这样的性质，即在所有子树（包括整棵树）上，根的内容具有最高优先级；但没有在兄弟节点上指定顺序。

树的定义如下：

Inductive tree : Set :=
| nil : tree
| cons : tree->nat->tree->tree.

我想使用 coq 合并两棵树。假设两棵树是 (cons l1 n1 r1) 和 (cons l2 n2 r2)，如果 n1 <= n2 则我将 l1 和 r1 合并为子树并创建新树 ((merge l1 r1) n1 (cons l2 n2 r2) ）。当 n2 <= n1 时可以使用类似的处理。

下面是合并的定义：

Fixpoint merge (t1 t2 : tree) : tree.
  destruct t1 as [ | l1 n1 r1].
  apply t2.
  destruct t2 as [ | l2 n2 r2].
    apply (cons l1 n1 r1).
    destruct (le_le_dec n1 n2).
      apply (cons (merge l1 r1) n1 (cons l2 n2 r2)).
      apply (cons (cons l1 n1 r1) n2 (merge l2 r2)).
Defined.

问题是 coq 认为上面的定义是错误的。但实际上合并功能最终可以终止。

我知道 coq 需要一个递减的定点参数。但是如何处理具有两个递减参数的函数呢？

引理 le_le_dec 只是为案例分析定义的：

Lemma le_le_dec : forall x y, {x <= y}+{y <= x}.
Proof.
  intros x y.
  destruct (nat_delta x y) as [xy | yx].
    destruct xy as [n e]. left. apply le_delta. exists n. assumption.
    destruct yx as [n e]. right. apply le_delta. exists n. assumption.
Qed.

引理 le_delta 和 nat_delta 如下：

Lemma le_delta: forall n m, n <= m <-> exists x, (x + n = m).
Proof.
  intros n m.
  split.
  intros e. induction e as [ |m les IHe].
    exists 0. simpl. reflexivity.
    destruct IHe as [x  e]. exists (S x). simpl. rewrite e. reflexivity.
  intros e. destruct e as [x e]. revert e. revert m.
  induction x as [ | x IHx].
    intros m e. simpl in e. rewrite e. apply le_n.
    intros m e. destruct m as [ | m].
      discriminate e.
      apply (le_S n m).
      apply (IHx m).
      inversion e. reflexivity.
Qed.

Lemma nat_delta : forall x y, {n | n+x=y} + {n | n+y=x}.
Proof.
  intros x y. induction x as [ | x IHx].
    left. exists y. simpl. rewrite <- (plus_n_O y). reflexivity.
    destruct IHx as [xy | yx].
    destruct xy as [n e]. destruct n as [ | n].
      right. exists (S 0). rewrite <- e. simpl. reflexivity.
      left. exists n. rewrite <- plus_n_Sm. rewrite <- e. simpl. reflexivity.
    destruct yx as [n e].    
    right. exists (S n). simpl. rewrite e. reflexivity.
Qed.

固定点的错误消息是：

Error:
Recursive definition of merge is ill-formed.
In environment
merge : tree -> tree -> tree
t1 : tree
t2 : tree
l1 : tree
n1 : nat
r1 : tree
l2 : tree
n2 : nat
r2 : tree
l : n2 <= n1
Recursive call to merge has principal argument equal to "l2" instead of
one of the following variables: "l1" "r1".
Recursive definition is:
"fun t1 t2 : tree =>
 match t1 with
| nil => t2
| cons l1 n1 r1 =>
     match t2 with
     | nil => cons l1 n1 r1
     | cons l2 n2 r2 =>
         let s := le_le_dec n1 n2 in
         if s
         then cons (merge l1 r1) n1 (cons l2 n2 r2)
         else cons (cons l1 n1 r1) n2 (merge l2 r2)
     end
 end".
4

2 回答 2

2

您必须在任何递归调用上使用相同的唯一递减参数。尝试这个：

Fixpoint merge (t1 t2 : tree) : tree.
  destruct t1 as [ | l1 n1 r1].
  apply t2.
  destruct t2 as [ | l2 n2 r2].
    apply (cons l1 n1 r1).
    destruct (le_le_dec n1 n2).
      apply (cons (cons l2 n2 r2) n1 (merge l1 r1)).
      apply (cons (merge l1 r1) n2 (cons l2 n1 r2)).
Defined.

我不确定这种方式是否保留了您程序的属性，但如果您不确定，您可以尝试证明它们是。

如果不是证明你的函数存在，你只是简单地编写了它，你可以使用Function而不是Fixpoint证明你的函数终止而不改变它的结构。

此外，我在尝试提取le_le_dec. 我认为那是因为le_le_dec更多的是在逻辑方面。为什么不比较n1andn2与返回 a 的函数bool并对结果进行案例分析？

你也可以试试这个：

Fixpoint meas (t1: tree): nat :=
  match t1 with
  | nil => O
  | cons t2 _ t3 => S ((meas t2) + (meas t3))
  end.

Fixpoint less_eq (n1 n2: nat): bool :=
  match n1, n2 with
  | O, O => true
  | O, S _ => true
  | S _, O => false
  | S n3, S n4 => less_eq n3 n4
  end.

Program Fixpoint merge (t1 t2: tree) {measure ((meas t1) + (meas t2))}: tree :=
  match t1 with
  | nil => t2
  | cons l1 n1 r1 =>
    match t2 with
    | nil => cons l1 n1 r1
    | cons l2 n2 r2 =>
      match less_eq n1 n2 with
      | false => cons (cons l1 n1 r1) n2 (merge l2 r2)
      | true => cons (merge l1 r1) n1 (cons l2 n2 r2)
      end
    end
  end.

然后你需要输入Next Obligation.，并证明一些东西。

于 2012-12-02T13:33:47.140 回答
0

您可能需要考虑将第一棵树中的元素一个一个地插入到第二棵树中。因此，您可以使用两个递归函数合并两棵树。

于 2012-12-06T12:00:39.727 回答