使用coq，試圖證明樹上的簡單引理

Question

試圖證明元素插入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相信我。我該如何繼續？

Answer 1

您必須使用le_trans定理：

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

是來自Le包。 它MEAS，你必須導入Le或更一般Arith有：在你的文件的開頭

Require Import Arith. 

。然後，你可以這樣做：

eapply le_trans. 
eapply H0; trivial. 
trivial.