我想证明，当接收二进制搜索树作为参数时，[inter]函数会生成另一个二进制搜索树。
插入功能：
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.
**
完成证明的最短方法可能是(就在最后一次**(：
** assert (k = k0) by auto with arith; subst.
inversion_clear H; now constructor.
Qed.
(第二行替换了我上一篇文章的引理BST_irrel(
事实上，你非常接近Qed！很多时候，如果某个结论看起来很难证明，那么看看上下文可能会很有用。如果你运气好的话，你可能会发现矛盾，并且已经解决了。否则，您可以尝试执行一些正向推理步骤(如在示例中推断k=k0，并在适当的情况下用k0替换k(。
Pierre
在您的最后一个目标中，您有k0 = k(由H0和H1组成(，并且您知道T t1 k0 v0 t2是一个搜索树。
H : BST (T t1 k0 v0 t2)
H0 : k >= k0
H1 : k0 >= k
============================
BST (T t1 k v t2)
因此，您可以在结论中将k替换为k0。如果你证明值v与T l k v r的搜索性无关(一个需要证明的小引理(，你的证明几乎完成了。
Lemma BST_irrel {V: Type} : forall l r k (v w:V),
BST (T l k v r) -> BST (T l k w r).
Proof. inversion 1; now constructor. Qed.