如何在 Coq 中证明 insert_BST

Question

我想证明，当接收二叉搜索树作为参数时， [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 kv 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.
       **

Answer 1

完成证明的最短方法可能是（就在您的最后一个 ** 处）：（

** assert (k = k0) by auto with arith; subst.
   inversion_clear H; now constructor.
Qed.

第二行替换了我上一篇文章的引理 BST_irrel）

确实，您非常接近Qed！很多时候，如果某个结论看起来难以证明，那么查看上下文可能会有所帮助。如果你幸运的话，你可能会发现一个矛盾，然后就完成了。否则，您可以尝试执行一些前向推理步骤（例如在示例中推断 k=k0 ，并在示例中将 k 替换为 k0适当的事件）。

皮埃尔

Answer 2

在您的上一个目标中，您有 k0 = k（通过 H0 和 H1），并且您知道 T t1 k0 v0 t2< /code> 是一个搜索树。

  H : BST (T t1 k0 v0 t2)
  H0 : k >= k0
  H1 : k0 >= k
  ============================
  BST (T t1 k v t2)

因此，您可以在结论中将 k 替换为 k0 。如果你证明
如果值 v 与 T lkv 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.