2

要素の bst への挿入関数の正しさを証明しようとして、一見些細な補題を証明しようとして立ち往生しました。これまでの私の試み：

Inductive tree : Set :=
| leaf : tree
| node : tree -> nat -> tree -> tree.    

Fixpoint In (n : nat) (T : tree) {struct T} : Prop :=
  match T with
  | leaf => False
  | node l v r => In n l \/ v = n \/ In n r
  end.

(* all_lte is the proposition that all nodes in tree t 
   have value at most n *)  
Definition all_lte (n : nat) (t : tree) : Prop :=
  forall x, In x t -> (x <= n).

Lemma all_lte_trans: forall n m t, n <= m /\ all_lte n t -> all_lte m t.
Proof.
intros.
destruct H.
unfold all_lte in H0.
unfold all_lte.
intros.

ツリー内のすべてが よりも小さくn、n <= mすべてが よりも小さい場合は明らかですmが、coq に私を信じさせることはできないようです。どうすれば続行できますか?

4

1 に答える 1

3

le_trans定理を使用する必要があります：

le_trans: forall n m p : nat, n <= m -> m <= p -> n <= p

それはLeパッケージから来ています。Leより一般的には、次のようにインポートする必要があることを意味しますArith。

Require Import Arith.

ファイルの先頭に。次に、次のことができます。

eapply le_trans.
eapply H0; trivial.
trivial.
于 2012-06-26T10:25:53.383 に答える