Используя coq, пытаюсь доказать простую лемму о деревьях

Пытаясь доказать корректность функции вставки элементов в 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 поверить мне. Как мне продолжить?


coq proof transitivity
person David Miller    schedule 26.06.2012    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Вы должны использовать теорему 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.
person Anne    schedule 26.06.2012