1

我正在使用 Coq 的 ideslave（又名 XML 协议）。通过调用<call val="Goal"><unit/></call>，典型的反馈看起来像

<value val="good"><option val="some"><goals><list><goal><string>239</string><list><richpp><_><pp>P&nbsp;:&nbsp;<constr.reference>ProgrammingLanguage</constr.reference></pp></_></richpp><richpp><_><pp>iP&nbsp;:&nbsp;<constr.reference>ImperativeProgrammingLanguage</constr.reference>&nbsp;<constr.variable>P</constr.variable></pp></_></richpp><richpp><_><pp>state&nbsp;:&nbsp;<constr.type>Type</constr.type></pp></_></richpp><richpp><_><pp>state_R&nbsp;:&nbsp;<constr.reference>Relation</constr.reference>&nbsp;<constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>BSS&nbsp;:&nbsp;<constr.reference>BigStepSemantics</constr.reference>&nbsp;<constr.variable>P</constr.variable>&nbsp;<constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>iBSS&nbsp;:&nbsp;<constr.path>Total</constr.path>.<constr.reference>ImpBigStepSemantics</constr.reference>&nbsp;<constr.variable>P</constr.variable>&nbsp;<constr.variable>state</constr.variable>&nbsp;<constr.variable>BSS</constr.variable></pp></_></richpp><richpp><_><pp>b&nbsp;:&nbsp;<constr.reference>bool_expr</constr.reference></pp></_></richpp><richpp><_><pp>c&nbsp;:&nbsp;<constr.reference>cmd</constr.reference></pp></_></richpp><richpp><_><pp>s1&nbsp;:&nbsp;<constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>ms2,&nbsp;ms3&nbsp;:&nbsp;<constr.reference>MetaState</constr.reference>&nbsp;<constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>H&nbsp;:&nbsp;<constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference>&nbsp;<constr.variable>s1</constr.variable>&nbsp;<constr.variable>b</constr.variable></pp></_></richpp><richpp><_><pp>H0&nbsp;:&nbsp;<constr.path>Total</constr.path>.<constr.reference>forward</constr.reference>&nbsp;(<constr.reference>Terminating</constr.reference>&nbsp;<constr.variable>s1</constr.variable>)&nbsp;<constr.variable>ms2</constr.variable></pp></_></richpp><richpp><_><pp>H1&nbsp;:&nbsp;<constr.reference>lift_relation</constr.reference>&nbsp;(<constr.keyword>fun</constr.keyword>&nbsp;(s&nbsp;:&nbsp;<constr.variable>state</constr.variable>)&nbsp;(ms&nbsp;:&nbsp;<constr.reference>MetaState</constr.reference>&nbsp;<constr.variable>state</constr.variable>)&nbsp;=&gt;&nbsp;<constr.reference>access</constr.reference>&nbsp;<constr.variable>s</constr.variable>&nbsp;<constr.variable>c</constr.variable>&nbsp;<constr.variable>ms</constr.variable>)\n&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<constr.variable>ms2</constr.variable>&nbsp;<constr.variable>ms3</constr.variable></pp></_></richpp><richpp><_><pp>H2&nbsp;:&nbsp;<constr.variable>ms3</constr.variable><constr.notation>&nbsp;=</constr.notation>&nbsp;<constr.reference>Error</constr.reference><constr.notation>&nbsp;\\/</constr.notation>&nbsp;<constr.variable>ms3</constr.variable><constr.notation>&nbsp;=</constr.notation>&nbsp;<constr.reference>NonTerminating</constr.reference></pp></_></richpp></list><richpp><_><pp><constr.path>Partial</constr.path>.<constr.reference>loop_access_fin</constr.reference>\n&nbsp;&nbsp;(<constr.keyword>fun</constr.keyword>&nbsp;(s&nbsp;:&nbsp;<constr.variable>state</constr.variable>)&nbsp;(ms&nbsp;:&nbsp;<constr.reference>MetaState</constr.reference>&nbsp;<constr.variable>state</constr.variable>)&nbsp;=&gt;&nbsp;<constr.reference>access</constr.reference>&nbsp;<constr.variable>s</constr.variable>&nbsp;<constr.variable>c</constr.variable>&nbsp;<constr.variable>ms</constr.variable>)\n&nbsp;&nbsp;(<constr.keyword>fun</constr.keyword>&nbsp;s&nbsp;:&nbsp;<constr.variable>state</constr.variable>&nbsp;=&gt;&nbsp;<constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference>&nbsp;<constr.variable>s</constr.variable>&nbsp;<constr.variable>b</constr.variable>)&nbsp;<constr.variable>s1</constr.variable>&nbsp;<constr.variable>ms3</constr.variable></pp></_></richpp></goal></list><list><pair><list/><list><goal><string>250</string><list><richpp><_><pp>P&nbsp;:&nbsp;<constr.reference>ProgrammingLanguage</constr.reference></pp></_></richpp><richpp><_><pp>iP&nbsp;:&nbsp;<constr.reference>ImperativeProgrammingLanguage</constr.reference>&nbsp;<constr.variable>P</constr.variable></pp></_></richpp><richpp><_><pp>state&nbsp;:&nbsp;<constr.type>Type</constr.type></pp></_></richpp><richpp><_><pp>state_R&nbsp;:&nbsp;<constr.reference>Relation</constr.reference>&nbsp;<constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>BSS&nbsp;:&nbsp;<constr.reference>BigStepSemantics</constr.reference>&nbsp;<constr.variable>P</constr.variable>&nbsp;<constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>iBSS&nbsp;:&nbsp;<constr.path>Total</constr.path>.<constr.reference>ImpBigStepSemantics</constr.reference>&nbsp;<constr.variable>P</constr.variable>&nbsp;<constr.variable>state</constr.variable>&nbsp;<constr.variable>BSS</constr.variable></pp></_></richpp><richpp><_><pp>b&nbsp;:&nbsp;<constr.reference>bool_expr</constr.reference></pp></_></richpp><richpp><_><pp>c&nbsp;:&nbsp;<constr.reference>cmd</constr.reference></pp></_></richpp><richpp><_><pp>s1,&nbsp;s2,&nbsp;s3,&nbsp;s4&nbsp;:&nbsp;<constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>ms&nbsp;:&nbsp;<constr.reference>MetaState</constr.reference>&nbsp;<constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>H&nbsp;:&nbsp;<constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference>&nbsp;<constr.variable>s1</constr.variable>&nbsp;<constr.variable>b</constr.variable></pp></_></richpp><richpp><_><pp>H0&nbsp;:&nbsp;<constr.variable>s1</constr.variable><constr.notation>&nbsp;&lt;=</constr.notation>&nbsp;<constr.variable>s2</constr.variable></pp></_></richpp><richpp><_><pp>H1&nbsp;:&nbsp;<constr.reference>access</constr.reference>&nbsp;<constr.variable>s2</constr.variable>&nbsp;<constr.variable>c</constr.variable>&nbsp;(<constr.reference>Terminating</constr.reference>&nbsp;<constr.variable>s3</constr.variable>)</pp></_></richpp><richpp><_><pp>H2&nbsp;:&nbsp;<constr.variable>s3</constr.variable><constr.notation>&nbsp;&lt;=</constr.notation>&nbsp;<constr.variable>s4</constr.variable></pp></_></richpp><richpp><_><pp>H3&nbsp;:&nbsp;<constr.path>Total</constr.path>.<constr.reference>loop_access_fin</constr.reference>\n&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<constr.keyword>fun</constr.keyword>&nbsp;(s&nbsp;:&nbsp;<constr.variable>state</constr.variable>)&nbsp;(ms&nbsp;:&nbsp;<constr.reference>MetaState</constr.reference>&nbsp;<constr.variable>state</constr.variable>)&nbsp;=&gt;&nbsp;<constr.reference>access</constr.reference>&nbsp;<constr.variable>s</constr.variable>&nbsp;<constr.variable>c</constr.variable>&nbsp;<constr.variable>ms</constr.variable>)\n&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<constr.keyword>fun</constr.keyword>&nbsp;s&nbsp;:&nbsp;<constr.variable>state</constr.variable>&nbsp;=&gt;&nbsp;<constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference>&nbsp;<constr.variable>s</constr.variable>&nbsp;<constr.variable>b</constr.variable>)&nbsp;<constr.variable>s4</constr.variable>&nbsp;<constr.variable>ms</constr.variable></pp></_></richpp><richpp><_><pp>IHloop_access_fin&nbsp;:&nbsp;<constr.path>Partial</constr.path>.<constr.reference>loop_access_fin</constr.reference>\n&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<constr.keyword>fun</constr.keyword>&nbsp;(s&nbsp;:&nbsp;<constr.variable>state</constr.variable>)&nbsp;(ms&nbsp;:&nbsp;<constr.reference>MetaState</constr.reference>&nbsp;<constr.variable>state</constr.variable>)&nbsp;=&gt;\n&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<constr.reference>access</constr.reference>&nbsp;<constr.variable>s</constr.variable>&nbsp;<constr.variable>c</constr.variable>&nbsp;<constr.variable>ms</constr.variable>)&nbsp;(<constr.keyword>fun</constr.keyword>&nbsp;s&nbsp;:&nbsp;<constr.variable>state</constr.variable>&nbsp;=&gt;&nbsp;<constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference>&nbsp;<constr.variable>s</constr.variable>&nbsp;<constr.variable>b</constr.variable>)\n&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<constr.variable>s4</constr.variable>&nbsp;<constr.variable>ms</constr.variable></pp></_></richpp></list><richpp><_><pp><constr.path>Partial</constr.path>.<constr.reference>loop_access_fin</constr.reference>\n&nbsp;&nbsp;(<constr.keyword>fun</constr.keyword>&nbsp;(s&nbsp;:&nbsp;<constr.variable>state</constr.variable>)&nbsp;(ms0&nbsp;:&nbsp;<constr.reference>MetaState</constr.reference>&nbsp;<constr.variable>state</constr.variable>)&nbsp;=&gt;&nbsp;<constr.reference>access</constr.reference>&nbsp;<constr.variable>s</constr.variable>&nbsp;<constr.variable>c</constr.variable>&nbsp;<constr.variable>ms0</constr.variable>)\n&nbsp;&nbsp;(<constr.keyword>fun</constr.keyword>&nbsp;s&nbsp;:&nbsp;<constr.variable>state</constr.variable>&nbsp;=&gt;&nbsp;<constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference>&nbsp;<constr.variable>s</constr.variable>&nbsp;<constr.variable>b</constr.variable>)&nbsp;<constr.variable>s1</constr.variable>&nbsp;<constr.variable>ms</constr.variable></pp></_></richpp></goal></list></pair><pair><list/><list><goal><string>212</string><list><richpp><_><pp>P&nbsp;:&nbsp;<constr.reference>ProgrammingLanguage</constr.reference></pp></_></richpp><richpp><_><pp>iP&nbsp;:&nbsp;<constr.reference>ImperativeProgrammingLanguage</constr.reference>&nbsp;<constr.variable>P</constr.variable></pp></_></richpp><richpp><_><pp>state&nbsp;:&nbsp;<constr.type>Type</constr.type></pp></_></richpp><richpp><_><pp>state_R&nbsp;:&nbsp;<constr.reference>Relation</constr.reference>&nbsp;<constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>BSS&nbsp;:&nbsp;<constr.reference>BigStepSemantics</constr.reference>&nbsp;<constr.variable>P</constr.variable>&nbsp;<constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>iBSS&nbsp;:&nbsp;<constr.path>Total</constr.path>.<constr.reference>ImpBigStepSemantics</constr.reference>&nbsp;<constr.variable>P</constr.variable>&nbsp;<constr.variable>state</constr.variable>&nbsp;<constr.variable>BSS</constr.variable></pp></_></richpp><richpp><_><pp>b&nbsp;:&nbsp;<constr.reference>bool_expr</constr.reference></pp></_></richpp><richpp><_><pp>c&nbsp;:&nbsp;<constr.reference>cmd</constr.reference></pp></_></richpp><richpp><_><pp>s&nbsp;:&nbsp;<constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>ms&nbsp;:&nbsp;<constr.reference>MetaState</constr.reference>&nbsp;<constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>H&nbsp;:&nbsp;<constr.reference>access</constr.reference>&nbsp;<constr.variable>s</constr.variable>&nbsp;(<constr.reference>Swhile</constr.reference>&nbsp;<constr.variable>b</constr.variable>&nbsp;<constr.variable>c</constr.variable>)&nbsp;<constr.variable>ms</constr.variable></pp></_></richpp><richpp><_><pp>H0&nbsp;:&nbsp;<constr.path>Total</constr.path>.<constr.reference>loop_access_inf</constr.reference>\n&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<constr.keyword>fun</constr.keyword>&nbsp;(s&nbsp;:&nbsp;<constr.variable>state</constr.variable>)&nbsp;(ms&nbsp;:&nbsp;<constr.reference>MetaState</constr.reference>&nbsp;<constr.variable>state</constr.variable>)&nbsp;=&gt;&nbsp;<constr.reference>access</constr.reference>&nbsp;<constr.variable>s</constr.variable>&nbsp;<constr.variable>c</constr.variable>&nbsp;<constr.variable>ms</constr.variable>)\n&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<constr.keyword>fun</constr.keyword>&nbsp;s&nbsp;:&nbsp;<constr.variable>state</constr.variable>&nbsp;=&gt;&nbsp;<constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference>&nbsp;<constr.variable>s</constr.variable>&nbsp;<constr.variable>b</constr.variable>)&nbsp;<constr.variable>s</constr.variable></pp></_></richpp><richpp><_><pp>H1&nbsp;:&nbsp;<constr.variable>ms</constr.variable><constr.notation>&nbsp;=</constr.notation>&nbsp;<constr.reference>NonTerminating</constr.reference></pp></_></richpp></list><richpp><_><pp><constr.path>Partial</constr.path>.<constr.reference>loop_access_fin</constr.reference>\n&nbsp;&nbsp;(<constr.keyword>fun</constr.keyword>&nbsp;(s0&nbsp;:&nbsp;<constr.variable>state</constr.variable>)&nbsp;(ms0&nbsp;:&nbsp;<constr.reference>MetaState</constr.reference>&nbsp;<constr.variable>state</constr.variable>)&nbsp;=&gt;&nbsp;<constr.reference>access</constr.reference>&nbsp;<constr.variable>s0</constr.variable>&nbsp;<constr.variable>c</constr.variable>&nbsp;<constr.variable>ms0</constr.variable>)\n&nbsp;&nbsp;(<constr.keyword>fun</constr.keyword>&nbsp;s0&nbsp;:&nbsp;<constr.variable>state</constr.variable>&nbsp;=&gt;&nbsp;<constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference>&nbsp;<constr.variable>s0</constr.variable>&nbsp;<constr.variable>b</constr.variable>)&nbsp;<constr.variable>s</constr.variable>&nbsp;<constr.variable>ms</constr.variable><constr.notation>&nbsp;\\/</constr.notation>\n<constr.path>Partial</constr.path>.<constr.reference>loop_access_inf</constr.reference>\n&nbsp;&nbsp;(<constr.keyword>fun</constr.keyword>&nbsp;(s0&nbsp;:&nbsp;<constr.variable>state</constr.variable>)&nbsp;(ms0&nbsp;:&nbsp;<constr.reference>MetaState</constr.reference>&nbsp;<constr.variable>state</constr.variable>)&nbsp;=&gt;&nbsp;<constr.reference>access</constr.reference>&nbsp;<constr.variable>s0</constr.variable>&nbsp;<constr.variable>c</constr.variable>&nbsp;<constr.variable>ms0</constr.variable>)\n&nbsp;&nbsp;(<constr.keyword>fun</constr.keyword>&nbsp;s0&nbsp;:&nbsp;<constr.variable>state</constr.variable>&nbsp;=&gt;&nbsp;<constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference>&nbsp;<constr.variable>s0</constr.variable>&nbsp;<constr.variable>b</constr.variable>)&nbsp;<constr.variable>s</constr.variable><constr.notation>&nbsp;/\\</constr.notation>&nbsp;<constr.variable>ms</constr.variable><constr.notation>&nbsp;=</constr.notation>&nbsp;<constr.reference>NonTerminating</constr.reference></pp></_></richpp></goal></list></pair><pair><list/><list/></pair></list><list/><list/></goals></option></value>

我已将此反馈格式化为 AST： 在此处输入图像描述

如您所见（如您所知），“目标”标签下有四个列表。Coq 文档给了它们四个名称（当前目标、背景目标、搁置目标和废弃目标）。

我的问题：

  1. 后三个目标类别是什么：背景目标、搁置目标和废弃目标？我找不到关于“搁置”和“放弃”目标的文档。

  2. 三者在哪些方面有所不同？他们的名字很相似。

  3. 为什么我们要pair在背景下列出目标（即第二个列表），然后在 下再次列出，pair然后才是实际目标？pair第一个和第二个下的背景目标之间有区别pair吗？

感谢您的帮助！

4

1 回答 1

4

您看到的证明表示只是包含有关当前证明的信息的核心Proof.t对象的具体化。

type 'a pre_goals = {
  fg_goals : 'a list;
  (** List of the focussed goals *)
  bg_goals : ('a list * 'a list) list;
  (** Zipper representing the unfocussed background goals *)
  shelved_goals : 'a list;
  (** List of the goals on the shelf. *)
  given_up_goals : 'a list;
  (** List of the goals that have been given up *)
}

后三个目标类别是什么：背景目标、搁置目标和废弃目标？我找不到关于“搁置”和“放弃”目标的文档。

  • 背景目标代表不“焦点”的目标。从 8.5 开始，Coq 有了“多目标关注”的概念，这意味着一种策略可以针对一组目标进行操作。这可以构造为堆栈，因此是列表列表。关于这对，它用于“不聚焦”，但它可能很快就会消失，请参阅此Pull Request中的讨论以获取更多信息。

  • 搁置的目标是隐藏在通常的交互式证明上下文中的目标。例如，这些是您可能只想通过副作用来解决的目标——想想exists x, P x，你可能想x搁置并直接解决P x——或通过其他机制（如类型类解析）。

  • 最后放弃的目标是用户承认的目标，因此被视为公理。

于 2018-03-11T06:49:20.580 回答