1

ここで言及されているツリーには、すべてのサブツリー (ツリー全体を含む) で、ルートの内容が最も優先されるという特性があります。ただし、兄弟ノードの順序は指定されていません。

ツリーの定義は次のとおりです。

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

coq を使用して 2 つのツリーをマージしたいと考えています。2 つのツリーが (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 では fixpoint の引き数が減少する必要があることは知っています。しかし、2 つの減少する引数を持つ関数をどのように扱うのでしょうか?

補題 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を返す関数と比較し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

最初のツリーから 2 番目のツリーに要素を 1 つずつ挿入することを検討してください。したがって、2 つの再帰関数を使用して 2 つのツリーをマージできます。

于 2012-12-06T12:00:39.727 に答える