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을 할 수없는 것 나를 믿는다. 계속하려면 어떻게해야합니까?

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

Le 패키지에서 제공 :

Answer 1

당신은 le_trans 정리를 사용해야합니다. 그것은 당신과 함께 Le 또는 더 일반적으로 Arith 가져올 수 있다고 MEAS : 파일의 시작 부분에

Require Import Arith. 

합니다. 그런 다음 수행 할 수 있습니다.

eapply le_trans. 
eapply H0; trivial. 
trivial.