Теорема о вставке в BST в coq

Question

Я создал дерево BST в coq, затем я создаю определение правильности BST. Теперь я должен продемонстрировать, что вставка в правильный BST создает правильный BST, но я не могу закрыть эту демонстрацию.

Inductive BST : Type :=
  | Empty : BST
  | Node : BST -> nat -> BST -> BST.

Fixpoint insert (El : nat) (bst : BST) : BST :=
  match bst with
    | Empty => Node Empty El Empty
    | Node l el r =>
        match el ?= El with
          | Eq => bst
          | Lt => Node l el (insert El r)
          | Gt => Node (insert El l) el r
        end
  end.

Fixpoint toList (bst : BST) : list nat := 
  match bst with
    | Empty => nil
    | Node l el r => toList(l) ++ (el :: nil) ++ toList(r)
  end.

Definition correct_on_l(root : nat)(l : BST) : bool :=
  forallb (fun el => el <? root)(toList l).

Definition correct_on_r(root : nat)(r : BST) : bool :=
  forallb (fun el => root <? el)(toList r).

Inductive correct : BST -> Prop :=
  | cor_empty : correct Empty
  | cor_node : 
      forall l e r,
        correct_on_l e l = true ->
        correct l ->
        correct_on_r e r = true ->
        correct r ->
        correct (Node l e r).

Это теорема:

Theorem insert_correct :
  forall a bst,
    correct bst -> correct(insert a bst).
Proof.
  intros.
  induction H; simpl in *.
  - constructor; trivial; try constructor.
  - destruct (e ?= a) eqn:D.
    + constructor; assumption.
    + constructor; try assumption.
      apply nat_compare_lt in D.
      admit.
    + constructor; try assumption. apply nat_compare_gt in D.
      admit.
Admitted.

Answer 1

Можно доказать вспомогательную лемму, показывающую, что варианты correct_on_* сохраняются при вставке. Естественно, вам нужно добавить гипотезу, которая говорит, что root дерева e меньше (или больше) вставленного элемента.