Как доказать вставку_BST в Coq

Я хочу доказать, что при получении в качестве аргумента бинарного дерева поиска функция [insert] генерирует другое бинарное дерево поиска.

Вставить функцию:

Fixpoint insert {V : Type} (x : key) (v : V) (t : tree V) : tree V :=
  match t with
  | E => T E x v E
  | T l y v' r => if x <? y then T (insert x v l) y v' r
                 else if x >? y then T l y v' (insert x v r)
                      else T l x v r
  end.

Я написал следующее доказательство. Однако я застрял в середине доказательства.

Я вижу, что мне нужно доказать BST (T t1 k v t2), но я не могу продолжить, применяя гипотезу H : BST (T t1 k0 v0 t2)... Что я могу сделать дальше, чтобы доказать, что

Theorem insert_BST : forall (V : Type) (k : key) (v : V) (t : tree V),
    BST t -> BST (insert k v t).
Proof.
  intros V k v t.
  induction t; intros H.
  - simpl. apply BST_T.
    + simpl. constructor.
    + simpl. constructor.
    + constructor.
    + constructor.
  - inversion H; subst.
    simpl in *.
    bdestruct (k0 >? k).
    + apply BST_T.
      * apply ForallT_insert.
          apply H4.
          apply H0.
      * apply H5.
      * apply IHt1.
        apply H6.
      * apply H7.
      + bdall.
       ** constructor. apply H4.
       * apply ForallT_insert.
       assumption.
       assumption.
      *apply H6.
      *  apply IHt2 in H7.
         apply H7.
       ** constructor; apply H.

Весь код ниже:

From Coq Require Import String.
From Coq Require Export Arith.
From Coq Require Export Lia.

Notation  "a >=? b" := (Nat.leb b a) (at level 70) : nat_scope.
Notation  "a >? b"  := (Nat.ltb b a) (at level 70) : nat_scope.


Definition key := nat.

Inductive tree (V : Type) : Type :=
| E
| T (l : tree V) (k : key) (v : V) (r : tree V).

Arguments E {V}.
Arguments T {V}.


Definition empty_tree {V : Type} : tree V := E. 

Fixpoint bound {V : Type} (x : key) (t : tree V) :=
  match t with
  | E => false
  | T l y v r => if x <? y then bound x l
                else if x >? y then bound x r
                     else true
  end.

Fixpoint lookup {V : Type} (d : V) (x : key) (t : tree V) : V :=
  match t with
  | E => d
  | T l y v r => if x <? y then lookup d x l
                else if x >? y then lookup d x r
                     else v
  end.

Fixpoint insert {V : Type} (x : key) (v : V) (t : tree V) : tree V :=
  match t with
  | E => T E x v E
  | T l y v' r => if x <? y then T (insert x v l) y v' r
                 else if x >? y then T l y v' (insert x v r)
                      else T l x v r
  end.

(** Nossa primeira tarefa será mostrar que a função [insert] de fato preserva esta invariante. Vamos então formalizar a invariante de uma árvore binária de busca. Faremos isto com a ajuda da função [ForallT]: *)

Fixpoint ForallT {V : Type} (P: key -> V -> Prop) (t: tree V) : Prop :=
  match t with
  | E => True
  | T l k v r => P k v /\ ForallT P l /\ ForallT P r
  end.

Inductive BST {V : Type} : tree V -> Prop :=
| BST_E : BST E
| BST_T : forall l x v r,
    ForallT (fun y _ => y < x) l ->
    ForallT (fun y _ => y > x) r ->
    BST l ->
    BST r ->
    BST (T l x v r).

Hint Constructors BST.
Ltac inv H := inversion H; clear H; subst.

Inductive reflect (P : Prop) : bool -> Set :=
  | ReflectT :   P -> reflect P true
  | ReflectF : ~ P -> reflect P false.

Theorem iff_reflect : forall P b, (P <-> b = true) -> reflect P b.
Proof.
  intros P b H. destruct b.
  - apply ReflectT. rewrite H. reflexivity.
  - apply ReflectF. rewrite H. intros H'. inversion H'.
Qed.

Theorem reflect_iff : forall P b, reflect P b -> (P <-> b = true).
Proof.
  intros P b H; split.
  - intro H'.
    inv H.
    + reflexivity.
    + contradiction.
  - intro H'; subst.
    inv H; assumption.
Qed.

Lemma eqb_reflect : forall x y, reflect (x = y) (x =? y).
Proof.
  intros x y. apply iff_reflect. symmetry.
  apply Nat.eqb_eq.
Qed.

Lemma ltb_reflect : forall x y, reflect (x < y) (x <? y).
Proof.
  intros x y. apply iff_reflect. symmetry.
  apply Nat.ltb_lt.
Qed.

Lemma leb_reflect : forall x y, reflect (x <= y) (x <=? y).
Proof.
  intros x y. apply iff_reflect. symmetry.
  apply Nat.leb_le.
Qed.

Hint Resolve ltb_reflect leb_reflect eqb_reflect : bdestruct.

Ltac bdestruct X :=
  let H := fresh in let e := fresh "e" in
   evar (e: Prop);
   assert (H: reflect e X); subst e;
    [eauto with bdestruct
    | destruct H as [H|H];
       [ | try first [apply not_lt in H | apply not_le in H]]].


Theorem empty_tree_BST : forall (V : Type),
    BST (@empty_tree V).
Proof.
 unfold empty_tree.
 constructor;try lia.
Qed.

Lemma ForallT_insert : forall (V : Type) (P : key -> V -> Prop) (t : tree V),
    ForallT P t -> forall (k : key) (v : V),
      P k v -> ForallT P (insert k v t).
Proof.
  intros V P t.
  induction t; intros H k' v' Pkv.
  - simpl. auto.
  - simpl in *.
    destruct H as [H1 [H2 H3]].
    bdestruct (k >? k').
    + simpl. repeat split.
      * assumption.
      * apply (IHt1 H2 k' v' Pkv).
      * assumption.
    + bdestruct (k' >? k).
      ++ simpl. repeat split.
         * assumption.
         * assumption.
         * apply (IHt2 H3 k' v' Pkv).
      ++ simpl. repeat split.
         * assumption.
         * assumption.
         * assumption.
Qed.

Ltac bdestruct_guard :=
  match goal with
  | |- context [ if ?X =? ?Y then _ else _ ] => bdestruct (X =? Y)
  | |- context [ if ?X <=? ?Y then _ else _ ] => bdestruct (X <=? Y)
  | |- context [ if ?X <? ?Y then _ else _ ] => bdestruct (X <? Y)
  end.
Ltac bdall :=
  repeat (simpl; bdestruct_guard; try lia; auto).

Theorem insert_BST : forall (V : Type) (k : key) (v : V) (t : tree V),
    BST t -> BST (insert k v t).
Proof.
  intros V k v t.
  induction t; intros H.
  - simpl. apply BST_T.
    + simpl. constructor.
    + simpl. constructor.
    + constructor.
    + constructor.
  - inversion H; subst.
    simpl in *.
    bdestruct (k0 >? k).
    + apply BST_T.
      * apply ForallT_insert.
          apply H4.
          apply H0.
      * apply H5.
      * apply IHt1.
        apply H6.
      * apply H7.
      + bdall.
       ** constructor. apply H4.
       * apply ForallT_insert.
       assumption.
       assumption.
      *apply H6.
      *  apply IHt2 in H7.
         apply H7.
       **