了解并处理coq中的嵌套归纳定义

Question

我试图证明insert_SearchTree，这是一个有关在插入关系后保留二叉搜索树的定理，如下。我不确定如何使用依赖于嵌套归纳定义的归纳假设，即SearchTree对SearchTree'的单个构造函数调用。但是，一旦实例化并反转了IH，我们就会得到与hi0无可比拟的争论k？

  ....
  H1 : SearchTree' 0 (insert k0 v0 l) hi0
  H2 : k0 < k
  ============================
  SearchTree' 0 (insert k0 v0 l) k

我对此证明的方法是否有缺陷，或者是否有使它们具有可比性的技巧？我曾想过尝试证明类似>>的东西

 Theorem insert_SearchTree'':
  forall k v t hi,
   SearchTree' 0 t hi -> SearchTree' 0 (insert k v t) hi .
Proof.
但是经过尝试后，我意识到这并不等效（尽管不确定，我认为这是无法证明的）……欢迎提出任何建议。大多数代码是辅助代码，我根据有关问题独立的建议将其包括在内。 

Require Export Coq.Arith.Arith.
Require Export Coq.Arith.EqNat.
Require Export Coq.omega.Omega.

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

Print reflect.

Lemma beq_reflect : forall x y, reflect (x = y) (x =? y).
Proof.
  intros x y.
  apply iff_reflect. symmetry.  apply beq_nat_true_iff.
Qed.

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

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

Hint Resolve blt_reflect ble_reflect beq_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]]].

Section TREES.
Variable V : Type.
Variable default: V.

Definition key := nat.

Inductive tree : Type :=
 | E : tree
 | T: tree -> key -> V -> tree -> tree.

Inductive SearchTree' : key -> tree -> key -> Prop :=
| ST_E : forall lo hi, lo <= hi -> SearchTree' lo E hi
| ST_T: forall lo l k v r hi,
    SearchTree' lo l k ->
    SearchTree' (S k) r hi ->
    SearchTree' lo (T l k v r) hi.

Inductive SearchTree: tree -> Prop :=
| ST_intro: forall t hi, SearchTree' 0 t hi -> SearchTree t.

Fixpoint insert (x: key) (v: V) (s: tree) : tree :=
 match s with
 | E => T E x v E
 | T a y v' b => if  x <? y then T (insert x v a) y v' b
                        else if y <? x then T a y v' (insert x v b)
                        else T a x v b
 end.

Theorem insert_SearchTree:
  forall k v t,
   SearchTree t -> SearchTree (insert k v t).
Proof.
  clear default.
  intros.
  generalize dependent v.
  generalize dependent k.
  induction H.
  induction H.
  - admit.
  - intros.
    specialize (IHSearchTree'1 k0 v0).
    inversion IHSearchTree'1. 
    subst.
    simpl.
    bdestruct (k0 <? k).
    apply (ST_intro _ hi0 ).
    constructor.
    admit.

End TREES.

我正在尝试证明insert_SearchTree，这是一个有关在插入关系后保留二进制搜索树的定理，如下。我不确定如何使用依赖...

Answer 1

启动induction时，目标目前太弱。在第二种情况的开始，目标看起来像这样：