理解和使用 coq 中的嵌套归纳定义
Understanding and working with nested inductive definitons in coq
我正在尝试证明 insert_SearchTree，一个关于在插入关系之后保留二叉搜索树的定理，如下所示。我不确定如何使用依赖于嵌套 Inductive 定义的归纳假设，即 SearchTree 的单个构造函数调用 SearchTree'。但是，一旦我实例化并反转 IH，我们就会得到一个与 k 无法比拟的争论 hi0？
....
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.
开始时目标当前太弱 induction。在第二种情况的开始，目标是这样的：
H : SearchTree' lo l k
H0 : SearchTree' (S k) r hi
IHSearchTree'1 : forall (k : key) (v : V), SearchTree (insert k v l)
IHSearchTree'2 : forall (k : key) (v : V), SearchTree (insert k v r)
============================
forall (k0 : key) (v0 : V), SearchTree (insert k0 v0 (T l k v r))
继续的高级想法是组合 H 和 IHSearchTree'2，或 H0 和 IHSearchTree'1，具体取决于插入的哪一侧。但这是不可能的，因为两个 IH 假设中的 SearchTree 谓词不是 组合的 ：只知道 insert k0 v0 l 是搜索树无济于事知道包含它的树 T (insert k0 v0 l) k v r 是否也是搜索树。所以证明没有通过。
将搜索树放在一起时，我们不只是想知道某物是搜索树。我们还想知道键的一些界限（特别是这里，它们必须以 k 为界）。这就是辅助谓词 SearchTree' 提供的。组合性问题正是使用辅助归纳谓词 SearchTree' 定义 SearchTree 的原因，它是组合的（它可以并且是根据自身定义的）。
关于树上提到 SearchTree 的递归函数的属性应该首先使用 SearchTree' 概括为更多信息属性，以便归纳可以通过。它看起来像这样：
Lemma insert_SearchTree' :
forall t k0 v0 ??? ,
SearchTree' ??? t ??? -> SearchTree' ??? (insert k0 v0 t) ???.
有多种有效的方法可以填充这些“???”的空白。对于 reader 来说，想出新的是一个很好的锻炼。在这里和许多其他情况下应该运作良好的一种方法是为谓词的所有缺失参数放置变量，然后找出它们之间的一些合适的关系：
Lemma insert_SearchTree' :
forall t k0 v0 lo hi lo' hi',
??? (* find a suitable assumption *) ->
SearchTree' lo t hi -> SearchTree' lo' (insert k0 v0 t) hi'.
该关系应反映 insert 的行为。就这些边界而言，insert 所做的是将键 k0 添加到树中，因此除了树的其余部分之外，边界必须对其进行约束：
Lemma insert_SearchTree' :
forall t k0 v0 lo hi lo' hi',
lo' <= lo -> hi <= hi' ->
lo' <= k0 -> k0 < hi' ->
SearchTree' lo t hi -> SearchTree' lo' (insert k0 v0 t) hi'.
最后，由于我们要在SearchTree' lo t hi假设上使用induction，所以最好将它没有提及的大部分变量和假设向右移动，以加强归纳假设进一步（据我所知，这样做总是安全的）：
Lemma insert_SearchTree' :
forall t k0 v0 lo hi, (* k0 and v0 remain constant throughout the recursive applications of (insert k0 v0), so they can stay here (it would still be fine if they are moved with the rest). *)
SearchTree' lo t hi ->
forall lo' hi', (* The bounds are going to change at every step, so they move to the right of the inductive predicate. *)
lo' <= lo -> hi <= hi' ->
lo' <= k0 -> k0 < hi' ->
SearchTree' lo' (insert k0 v0 t) hi'.
证明这个引理并用它来证明 insert_SearchTree 留作 reader.
的练习
我正在尝试证明 insert_SearchTree，一个关于在插入关系之后保留二叉搜索树的定理，如下所示。我不确定如何使用依赖于嵌套 Inductive 定义的归纳假设，即 SearchTree 的单个构造函数调用 SearchTree'。但是，一旦我实例化并反转 IH，我们就会得到一个与 k 无法比拟的争论 hi0？
....
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.
开始时目标当前太弱 induction。在第二种情况的开始，目标是这样的：
H : SearchTree' lo l k
H0 : SearchTree' (S k) r hi
IHSearchTree'1 : forall (k : key) (v : V), SearchTree (insert k v l)
IHSearchTree'2 : forall (k : key) (v : V), SearchTree (insert k v r)
============================
forall (k0 : key) (v0 : V), SearchTree (insert k0 v0 (T l k v r))
继续的高级想法是组合 H 和 IHSearchTree'2，或 H0 和 IHSearchTree'1，具体取决于插入的哪一侧。但这是不可能的，因为两个 IH 假设中的 SearchTree 谓词不是 组合的 ：只知道 insert k0 v0 l 是搜索树无济于事知道包含它的树 T (insert k0 v0 l) k v r 是否也是搜索树。所以证明没有通过。
将搜索树放在一起时，我们不只是想知道某物是搜索树。我们还想知道键的一些界限（特别是这里，它们必须以 k 为界）。这就是辅助谓词 SearchTree' 提供的。组合性问题正是使用辅助归纳谓词 SearchTree' 定义 SearchTree 的原因，它是组合的（它可以并且是根据自身定义的）。
关于树上提到 SearchTree 的递归函数的属性应该首先使用 SearchTree' 概括为更多信息属性，以便归纳可以通过。它看起来像这样：
Lemma insert_SearchTree' :
forall t k0 v0 ??? ,
SearchTree' ??? t ??? -> SearchTree' ??? (insert k0 v0 t) ???.
有多种有效的方法可以填充这些“???”的空白。对于 reader 来说，想出新的是一个很好的锻炼。在这里和许多其他情况下应该运作良好的一种方法是为谓词的所有缺失参数放置变量，然后找出它们之间的一些合适的关系：
Lemma insert_SearchTree' :
forall t k0 v0 lo hi lo' hi',
??? (* find a suitable assumption *) ->
SearchTree' lo t hi -> SearchTree' lo' (insert k0 v0 t) hi'.
该关系应反映 insert 的行为。就这些边界而言，insert 所做的是将键 k0 添加到树中，因此除了树的其余部分之外，边界必须对其进行约束：
Lemma insert_SearchTree' :
forall t k0 v0 lo hi lo' hi',
lo' <= lo -> hi <= hi' ->
lo' <= k0 -> k0 < hi' ->
SearchTree' lo t hi -> SearchTree' lo' (insert k0 v0 t) hi'.
最后，由于我们要在SearchTree' lo t hi假设上使用induction，所以最好将它没有提及的大部分变量和假设向右移动，以加强归纳假设进一步（据我所知，这样做总是安全的）：
Lemma insert_SearchTree' :
forall t k0 v0 lo hi, (* k0 and v0 remain constant throughout the recursive applications of (insert k0 v0), so they can stay here (it would still be fine if they are moved with the rest). *)
SearchTree' lo t hi ->
forall lo' hi', (* The bounds are going to change at every step, so they move to the right of the inductive predicate. *)
lo' <= lo -> hi <= hi' ->
lo' <= k0 -> k0 < hi' ->
SearchTree' lo' (insert k0 v0 t) hi'.
证明这个引理并用它来证明 insert_SearchTree 留作 reader.