Coq：“饱和”是什么意思？证明的上下文？
正如 MPI-SWS 的 std++：
(** The class [TCUnless] can be used to check that search for [P]
fails. This is useful as a guard for certain instances together with
classes like [TCFastDone] (see [tactics.v]) to prevent infinite loops
(e.g. when saturating the context). *)
Notation TCUnless P := (TCIf P TCFalse TCTrue).
As found in MPI-SWS' std++:
(** The class [TCUnless] can be used to check that search for [P]
fails. This is useful as a guard for certain instances together with
classes like [TCFastDone] (see [tactics.v]) to prevent infinite loops
(e.g. when saturating the context). *)
Notation TCUnless P := (TCIf P TCFalse TCTrue).
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
给定一组起始假设以及将它们组合成新假设的方法，“饱和上下文”意味着从起始组创建尽可能多的假设。这用于证明自动化以暴力破解解决方案。
让我们举一个愚蠢的例子：假设我们试图证明
3 <= 7，从以下假设开始：然后为了使上下文饱和，我们将重复组合这三个假设，获得数千个证明诸如
99 <= 100、99 <= 99、98 <= 100等命题，等等。这些命题之一是3 <= 7，因此您可以通过调用策略假设来得出结论。Given a set of starting hypotheses and a way to combine them into new hypotheses, "saturating the context" means to create as many hypotheses as possible from the starting set. This is used in proof automation to brute-force a solution.
Let's give a silly example: assume we're trying to prove that
3 <= 7, starting from the following hypotheses:Then to saturate the context we would combine these three hypotheses repeatedly, obtaining proofs for thousands of propositions such as
99 <= 100,99 <= 99,98 <= 100, etc. One of these propositions would be3 <= 7, so you could just conclude by calling the tacticassumption.