如何在coq中合并两棵树？

Question

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

树的定义如下：

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

我想使用 coq 合并两棵树。假设两棵树是 (cons l1 n1 r1) 和 (cons l2 n2 r2)，如果 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.

fixpoint的错误信息是：

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

Answer 1

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

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 更偏向于逻辑方面。为什么不将n1 和n2 与返回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.，并证明一些东西。

Answer 2

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