I want to prove that when receiving a binary search tree as an argument, the [insert] function generates another binary search tree.
Insert Function:
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.
I have written the following proof. However I am stuck in the middle of the proof.
I can see what I have to proove BST (T t1 k v t2), but I am unable to proceed by applying the hypothesis H : BST (T t1 k0 v0 t2)...
What can I do next in order to proove that
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.
The whole code is here down below:
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.
**
The shortest way to complete your proof may be (just at your last **):
** assert (k = k0) by auto with arith; subst.
inversion_clear H; now constructor.
Qed.
(the second line replaces the lemma BST_irrel of my previous post)
Indeed, you were very close to the Qed! Quite often, if some conclusion looks difficult to prove, it may be useful to look at the context. If you are lucky, you may find a contradiction and it's done. Otherwise, you can try to do a few forward-reasoning steps (like infering k=k0 in your example, and replace k with k0in appropriate occurrences).
Pierre