Используя 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 пакета. Это тез, что вы должны импортировать Le или в более общем Arith с:

Require Import Arith. 

в начале файла. Затем вы можете сделать:

eapply le_trans. 
eapply H0; trivial. 
trivial.