如何在 Coq 中证明 insert_BST
How to prove insert_BST in 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.
**
在你的最后一个目标中，你有 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.
完成证明的最短方法可能是（就在你最后**）：
** assert (k = k0) by auto with arith; subst.
inversion_clear H; now constructor.
Qed.
（第二行替换我之前post的引理BST_irrel）
确实，你离 Qed 很近了！很多时候，如果某些结论看起来难以证明，那么查看上下文可能会有用。运气好的话，可能会发现一个矛盾，就搞定了。否则，您可以尝试执行一些 forward-reasoning 步骤（例如在您的示例中推断 k=k0，并在适当的情况下将 k 替换为 k0）。
皮埃尔
我想证明当接收到二叉搜索树作为参数时，[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.
**
在你的最后一个目标中，你有 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.
完成证明的最短方法可能是（就在你最后**）：
** assert (k = k0) by auto with arith; subst.
inversion_clear H; now constructor.
Qed.
（第二行替换我之前post的引理BST_irrel）
确实，你离 Qed 很近了！很多时候，如果某些结论看起来难以证明，那么查看上下文可能会有用。运气好的话，可能会发现一个矛盾，就搞定了。否则，您可以尝试执行一些 forward-reasoning 步骤（例如在您的示例中推断 k=k0，并在适当的情况下将 k 替换为 k0）。
皮埃尔