如何解决我如何概括一个 iff 的 Coq 证明?
我必须做的一种常见的证明是这样的
Lemma my_lemma : forall y,(forall x x',Q x x' y) -> (forall x x',P x y <-> P x' y).
Proof.
intros y Q_y.
split.
+ <some proof using Q>
+ <the same proof using Q,but x and x' are swapped>
其中 Q
本身就是某种 iff 形状的谓词。
我的问题是P x y -> P x' y
和P x' y -> P x y
的证明往往基本相同,唯一的区别是x
和x'
的角色互换了.我可以要求 Coq 将目标转化为
forall x x',P x y -> P x' y
然后将其推广到 iff 情况,这样我就不需要在证明中重复自己?
我查看了标准库、战术索引和一些 SO 问题,但没有告诉我如何做到这一点。
解决方法
这是它的自定义策略:
Ltac sufficient_if :=
match goal with
| [ |- forall (x : ?t) (x' : ?t'),?T <-> ?U ] => (* If the goal looks like an equivalence (T <-> U) (hoping that T and U are sufficiently similar)... *)
assert (HHH : forall (x : t) (x' : t'),T -> U); (* Change the goal to (T -> U) *)
[ | split; apply HHH ] (* And prove the two directions of the old goal *)
end.
Parameter Q : nat -> nat -> nat -> Prop.
Parameter P : nat -> nat -> Prop.
Lemma my_lemma : forall y,(forall x x',Q x x' y) -> (forall x x',P x y <-> P x' y).
Proof.
intros y Q_y.
sufficient_if.
,
在数学中,人们经常可以做出“假设”“不失一般性” (WLOG) 来简化这种证明。在您的示例中,您可以说“假设 不失一般性 P x y
成立。要证明 P x y <-> P x' y
足以证明 P x' y.
”
如果您使用的是 ssreflect
,则您拥有 wlog
tactic。
您本质上cut
在另一个可以轻松解决您的目标的目标中。您也可以使用 assert
或 enough
等标准策略(类似于 assert
,但证明义务的顺序不同)。
一个例子来说明我的意思:下面我只想展示一个方向的蕴涵,因为它可以很容易地解决另一个方向的蕴涵(用firstorder
)。
Context (T:Type) (P:T->T->Prop).
Goal forall x y,P x y <-> P y x.
enough (forall x y,P x y -> P y x) by firstorder.
现在我只需要显示一个方向的目标,因为它暗示了真正目标的两个方向。
有关 WLOG 的更多信息,请参见例如 1
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。