代码之家 › 专栏 › 技术社区 › Jian Wang

Coq中的背景目标、搁置目标和放弃目标是什么?

coq-extraction coq

Jian Wang · 技术社区 · 6 年前

我正在使用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 document 给他们四个名字(当前目标、背景目标、搁置目标和放弃目标)。

我的问题:

后三种目标类别是什么:背景目标、搁置目标和放弃目标?我找不到关于“搁置”和“放弃”目标的文档。
这三种方法有哪些不同?他们的名字很相似。
我们为什么要 pair 在背景目标下(即第二个列表),然后再次在下面列出 一对 ,然后是实际目标?第一项下的背景目标之间是否存在差异 一对 第二个下面的 一对 ?

谢谢你的帮助!

1 回复 | 直到 6 年前

ejgallego 6 年前

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

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 或通过其他机制,如类型类解析。
最后放弃目标是用户认可的目标,因此被视为公理。