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.