proof - 使用 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.