Coq 中的背景目标、搁置目标和废弃目标是什么？
What are background goals, shelved goals, and abandoned goals in Coq?
我正在使用 Coq 的 ideslave（a.k.a。XML 协议）。通过调用 <call val="Goal"><unit/></call>，典型的反馈看起来像
<value val="good"><option val="some"><goals><list><goal><string>239</string><list><richpp><_><pp>P : <constr.reference>ProgrammingLanguage</constr.reference></pp></_></richpp><richpp><_><pp>iP : <constr.reference>ImperativeProgrammingLanguage</constr.reference> <constr.variable>P</constr.variable></pp></_></richpp><richpp><_><pp>state : <constr.type>Type</constr.type></pp></_></richpp><richpp><_><pp>state_R : <constr.reference>Relation</constr.reference> <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>BSS : <constr.reference>BigStepSemantics</constr.reference> <constr.variable>P</constr.variable> <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>iBSS : <constr.path>Total</constr.path>.<constr.reference>ImpBigStepSemantics</constr.reference> <constr.variable>P</constr.variable> <constr.variable>state</constr.variable> <constr.variable>BSS</constr.variable></pp></_></richpp><richpp><_><pp>b : <constr.reference>bool_expr</constr.reference></pp></_></richpp><richpp><_><pp>c : <constr.reference>cmd</constr.reference></pp></_></richpp><richpp><_><pp>s1 : <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>ms2, ms3 : <constr.reference>MetaState</constr.reference> <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>H : <constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference> <constr.variable>s1</constr.variable> <constr.variable>b</constr.variable></pp></_></richpp><richpp><_><pp>H0 : <constr.path>Total</constr.path>.<constr.reference>forward</constr.reference> (<constr.reference>Terminating</constr.reference> <constr.variable>s1</constr.variable>) <constr.variable>ms2</constr.variable></pp></_></richpp><richpp><_><pp>H1 : <constr.reference>lift_relation</constr.reference> (<constr.keyword>fun</constr.keyword> (s : <constr.variable>state</constr.variable>) (ms : <constr.reference>MetaState</constr.reference> <constr.variable>state</constr.variable>) => <constr.reference>access</constr.reference> <constr.variable>s</constr.variable> <constr.variable>c</constr.variable> <constr.variable>ms</constr.variable>)\n <constr.variable>ms2</constr.variable> <constr.variable>ms3</constr.variable></pp></_></richpp><richpp><_><pp>H2 : <constr.variable>ms3</constr.variable><constr.notation> =</constr.notation> <constr.reference>Error</constr.reference><constr.notation> \/</constr.notation> <constr.variable>ms3</constr.variable><constr.notation> =</constr.notation> <constr.reference>NonTerminating</constr.reference></pp></_></richpp></list><richpp><_><pp><constr.path>Partial</constr.path>.<constr.reference>loop_access_fin</constr.reference>\n (<constr.keyword>fun</constr.keyword> (s : <constr.variable>state</constr.variable>) (ms : <constr.reference>MetaState</constr.reference> <constr.variable>state</constr.variable>) => <constr.reference>access</constr.reference> <constr.variable>s</constr.variable> <constr.variable>c</constr.variable> <constr.variable>ms</constr.variable>)\n (<constr.keyword>fun</constr.keyword> s : <constr.variable>state</constr.variable> => <constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference> <constr.variable>s</constr.variable> <constr.variable>b</constr.variable>) <constr.variable>s1</constr.variable> <constr.variable>ms3</constr.variable></pp></_></richpp></goal></list><list><pair><list/><list><goal><string>250</string><list><richpp><_><pp>P : <constr.reference>ProgrammingLanguage</constr.reference></pp></_></richpp><richpp><_><pp>iP : <constr.reference>ImperativeProgrammingLanguage</constr.reference> <constr.variable>P</constr.variable></pp></_></richpp><richpp><_><pp>state : <constr.type>Type</constr.type></pp></_></richpp><richpp><_><pp>state_R : <constr.reference>Relation</constr.reference> <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>BSS : <constr.reference>BigStepSemantics</constr.reference> <constr.variable>P</constr.variable> <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>iBSS : <constr.path>Total</constr.path>.<constr.reference>ImpBigStepSemantics</constr.reference> <constr.variable>P</constr.variable> <constr.variable>state</constr.variable> <constr.variable>BSS</constr.variable></pp></_></richpp><richpp><_><pp>b : <constr.reference>bool_expr</constr.reference></pp></_></richpp><richpp><_><pp>c : <constr.reference>cmd</constr.reference></pp></_></richpp><richpp><_><pp>s1, s2, s3, s4 : <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>ms : <constr.reference>MetaState</constr.reference> <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>H : <constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference> <constr.variable>s1</constr.variable> <constr.variable>b</constr.variable></pp></_></richpp><richpp><_><pp>H0 : <constr.variable>s1</constr.variable><constr.notation> <=</constr.notation> <constr.variable>s2</constr.variable></pp></_></richpp><richpp><_><pp>H1 : <constr.reference>access</constr.reference> <constr.variable>s2</constr.variable> <constr.variable>c</constr.variable> (<constr.reference>Terminating</constr.reference> <constr.variable>s3</constr.variable>)</pp></_></richpp><richpp><_><pp>H2 : <constr.variable>s3</constr.variable><constr.notation> <=</constr.notation> <constr.variable>s4</constr.variable></pp></_></richpp><richpp><_><pp>H3 : <constr.path>Total</constr.path>.<constr.reference>loop_access_fin</constr.reference>\n (<constr.keyword>fun</constr.keyword> (s : <constr.variable>state</constr.variable>) (ms : <constr.reference>MetaState</constr.reference> <constr.variable>state</constr.variable>) => <constr.reference>access</constr.reference> <constr.variable>s</constr.variable> <constr.variable>c</constr.variable> <constr.variable>ms</constr.variable>)\n (<constr.keyword>fun</constr.keyword> s : <constr.variable>state</constr.variable> => <constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference> <constr.variable>s</constr.variable> <constr.variable>b</constr.variable>) <constr.variable>s4</constr.variable> <constr.variable>ms</constr.variable></pp></_></richpp><richpp><_><pp>IHloop_access_fin : <constr.path>Partial</constr.path>.<constr.reference>loop_access_fin</constr.reference>\n (<constr.keyword>fun</constr.keyword> (s : <constr.variable>state</constr.variable>) (ms : <constr.reference>MetaState</constr.reference> <constr.variable>state</constr.variable>) =>\n <constr.reference>access</constr.reference> <constr.variable>s</constr.variable> <constr.variable>c</constr.variable> <constr.variable>ms</constr.variable>) (<constr.keyword>fun</constr.keyword> s : <constr.variable>state</constr.variable> => <constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference> <constr.variable>s</constr.variable> <constr.variable>b</constr.variable>)\n <constr.variable>s4</constr.variable> <constr.variable>ms</constr.variable></pp></_></richpp></list><richpp><_><pp><constr.path>Partial</constr.path>.<constr.reference>loop_access_fin</constr.reference>\n (<constr.keyword>fun</constr.keyword> (s : <constr.variable>state</constr.variable>) (ms0 : <constr.reference>MetaState</constr.reference> <constr.variable>state</constr.variable>) => <constr.reference>access</constr.reference> <constr.variable>s</constr.variable> <constr.variable>c</constr.variable> <constr.variable>ms0</constr.variable>)\n (<constr.keyword>fun</constr.keyword> s : <constr.variable>state</constr.variable> => <constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference> <constr.variable>s</constr.variable> <constr.variable>b</constr.variable>) <constr.variable>s1</constr.variable> <constr.variable>ms</constr.variable></pp></_></richpp></goal></list></pair><pair><list/><list><goal><string>212</string><list><richpp><_><pp>P : <constr.reference>ProgrammingLanguage</constr.reference></pp></_></richpp><richpp><_><pp>iP : <constr.reference>ImperativeProgrammingLanguage</constr.reference> <constr.variable>P</constr.variable></pp></_></richpp><richpp><_><pp>state : <constr.type>Type</constr.type></pp></_></richpp><richpp><_><pp>state_R : <constr.reference>Relation</constr.reference> <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>BSS : <constr.reference>BigStepSemantics</constr.reference> <constr.variable>P</constr.variable> <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>iBSS : <constr.path>Total</constr.path>.<constr.reference>ImpBigStepSemantics</constr.reference> <constr.variable>P</constr.variable> <constr.variable>state</constr.variable> <constr.variable>BSS</constr.variable></pp></_></richpp><richpp><_><pp>b : <constr.reference>bool_expr</constr.reference></pp></_></richpp><richpp><_><pp>c : <constr.reference>cmd</constr.reference></pp></_></richpp><richpp><_><pp>s : <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>ms : <constr.reference>MetaState</constr.reference> <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>H : <constr.reference>access</constr.reference> <constr.variable>s</constr.variable> (<constr.reference>Swhile</constr.reference> <constr.variable>b</constr.variable> <constr.variable>c</constr.variable>) <constr.variable>ms</constr.variable></pp></_></richpp><richpp><_><pp>H0 : <constr.path>Total</constr.path>.<constr.reference>loop_access_inf</constr.reference>\n (<constr.keyword>fun</constr.keyword> (s : <constr.variable>state</constr.variable>) (ms : <constr.reference>MetaState</constr.reference> <constr.variable>state</constr.variable>) => <constr.reference>access</constr.reference> <constr.variable>s</constr.variable> <constr.variable>c</constr.variable> <constr.variable>ms</constr.variable>)\n (<constr.keyword>fun</constr.keyword> s : <constr.variable>state</constr.variable> => <constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference> <constr.variable>s</constr.variable> <constr.variable>b</constr.variable>) <constr.variable>s</constr.variable></pp></_></richpp><richpp><_><pp>H1 : <constr.variable>ms</constr.variable><constr.notation> =</constr.notation> <constr.reference>NonTerminating</constr.reference></pp></_></richpp></list><richpp><_><pp><constr.path>Partial</constr.path>.<constr.reference>loop_access_fin</constr.reference>\n (<constr.keyword>fun</constr.keyword> (s0 : <constr.variable>state</constr.variable>) (ms0 : <constr.reference>MetaState</constr.reference> <constr.variable>state</constr.variable>) => <constr.reference>access</constr.reference> <constr.variable>s0</constr.variable> <constr.variable>c</constr.variable> <constr.variable>ms0</constr.variable>)\n (<constr.keyword>fun</constr.keyword> s0 : <constr.variable>state</constr.variable> => <constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference> <constr.variable>s0</constr.variable> <constr.variable>b</constr.variable>) <constr.variable>s</constr.variable> <constr.variable>ms</constr.variable><constr.notation> \/</constr.notation>\n<constr.path>Partial</constr.path>.<constr.reference>loop_access_inf</constr.reference>\n (<constr.keyword>fun</constr.keyword> (s0 : <constr.variable>state</constr.variable>) (ms0 : <constr.reference>MetaState</constr.reference> <constr.variable>state</constr.variable>) => <constr.reference>access</constr.reference> <constr.variable>s0</constr.variable> <constr.variable>c</constr.variable> <constr.variable>ms0</constr.variable>)\n (<constr.keyword>fun</constr.keyword> s0 : <constr.variable>state</constr.variable> => <constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference> <constr.variable>s0</constr.variable> <constr.variable>b</constr.variable>) <constr.variable>s</constr.variable><constr.notation> /\</constr.notation> <constr.variable>ms</constr.variable><constr.notation> =</constr.notation> <constr.reference>NonTerminating</constr.reference></pp></_></richpp></goal></list></pair><pair><list/><list/></pair></list><list/><list/></goals></option></value>
我已将此反馈格式化为 AST：
如您所见（如您所知），"goals" 标签下有四个列表。 Coq document 给了他们四个名字（当前目标、背景目标、搁置目标和放弃目标）。
我的问题：
后三类目标是什么：背景目标、搁置目标和放弃目标？我找不到关于 "shelved" 和 "abandoned" 目标的文档。
三者有什么不同？他们的名字很相似。
为什么我们要在背景目标（即第 2 个列表）下有 pair，然后在 pair 下再次列出，然后才是实际目标？第一个pair下的背景目标和第二个pair下的背景目标有区别吗？
感谢您的帮助！
您看到的证明表示只是核心 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 *)
}
What are the latter three goal categories: background goals, shelved goals, and abandoned goals? I cannot find docs on "shelved" and "abandoned" goals.
背景目标表示不是"in focus"的目标。从 8.5 开始，Coq 有一个 "multi-goal focus" 的概念，这意味着一个策略可以对一组目标进行操作。这可以构造为堆栈，因此列表列表。关于这对，它用于 "unfocusing"，但它可能很快就会消失，请参阅此 Pull Request 中的讨论以获取更多信息。
搁置的目标 是在通常的交互式证明上下文中隐藏的目标。例如，这些是你可能只想通过 side-effect 来解决的目标 ─ 想想 exists x, P x，你可能想把 x 搁置，直接解决 P x ─或通过其他机制，例如 type-class 分辨率。
最终放弃目标是为用户承认的目标，因此被视为公理。
我正在使用 Coq 的 ideslave（a.k.a。XML 协议）。通过调用 <call val="Goal"><unit/></call>，典型的反馈看起来像
<value val="good"><option val="some"><goals><list><goal><string>239</string><list><richpp><_><pp>P : <constr.reference>ProgrammingLanguage</constr.reference></pp></_></richpp><richpp><_><pp>iP : <constr.reference>ImperativeProgrammingLanguage</constr.reference> <constr.variable>P</constr.variable></pp></_></richpp><richpp><_><pp>state : <constr.type>Type</constr.type></pp></_></richpp><richpp><_><pp>state_R : <constr.reference>Relation</constr.reference> <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>BSS : <constr.reference>BigStepSemantics</constr.reference> <constr.variable>P</constr.variable> <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>iBSS : <constr.path>Total</constr.path>.<constr.reference>ImpBigStepSemantics</constr.reference> <constr.variable>P</constr.variable> <constr.variable>state</constr.variable> <constr.variable>BSS</constr.variable></pp></_></richpp><richpp><_><pp>b : <constr.reference>bool_expr</constr.reference></pp></_></richpp><richpp><_><pp>c : <constr.reference>cmd</constr.reference></pp></_></richpp><richpp><_><pp>s1 : <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>ms2, ms3 : <constr.reference>MetaState</constr.reference> <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>H : <constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference> <constr.variable>s1</constr.variable> <constr.variable>b</constr.variable></pp></_></richpp><richpp><_><pp>H0 : <constr.path>Total</constr.path>.<constr.reference>forward</constr.reference> (<constr.reference>Terminating</constr.reference> <constr.variable>s1</constr.variable>) <constr.variable>ms2</constr.variable></pp></_></richpp><richpp><_><pp>H1 : <constr.reference>lift_relation</constr.reference> (<constr.keyword>fun</constr.keyword> (s : <constr.variable>state</constr.variable>) (ms : <constr.reference>MetaState</constr.reference> <constr.variable>state</constr.variable>) => <constr.reference>access</constr.reference> <constr.variable>s</constr.variable> <constr.variable>c</constr.variable> <constr.variable>ms</constr.variable>)\n <constr.variable>ms2</constr.variable> <constr.variable>ms3</constr.variable></pp></_></richpp><richpp><_><pp>H2 : <constr.variable>ms3</constr.variable><constr.notation> =</constr.notation> <constr.reference>Error</constr.reference><constr.notation> \/</constr.notation> <constr.variable>ms3</constr.variable><constr.notation> =</constr.notation> <constr.reference>NonTerminating</constr.reference></pp></_></richpp></list><richpp><_><pp><constr.path>Partial</constr.path>.<constr.reference>loop_access_fin</constr.reference>\n (<constr.keyword>fun</constr.keyword> (s : <constr.variable>state</constr.variable>) (ms : <constr.reference>MetaState</constr.reference> <constr.variable>state</constr.variable>) => <constr.reference>access</constr.reference> <constr.variable>s</constr.variable> <constr.variable>c</constr.variable> <constr.variable>ms</constr.variable>)\n (<constr.keyword>fun</constr.keyword> s : <constr.variable>state</constr.variable> => <constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference> <constr.variable>s</constr.variable> <constr.variable>b</constr.variable>) <constr.variable>s1</constr.variable> <constr.variable>ms3</constr.variable></pp></_></richpp></goal></list><list><pair><list/><list><goal><string>250</string><list><richpp><_><pp>P : <constr.reference>ProgrammingLanguage</constr.reference></pp></_></richpp><richpp><_><pp>iP : <constr.reference>ImperativeProgrammingLanguage</constr.reference> <constr.variable>P</constr.variable></pp></_></richpp><richpp><_><pp>state : <constr.type>Type</constr.type></pp></_></richpp><richpp><_><pp>state_R : <constr.reference>Relation</constr.reference> <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>BSS : <constr.reference>BigStepSemantics</constr.reference> <constr.variable>P</constr.variable> <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>iBSS : <constr.path>Total</constr.path>.<constr.reference>ImpBigStepSemantics</constr.reference> <constr.variable>P</constr.variable> <constr.variable>state</constr.variable> <constr.variable>BSS</constr.variable></pp></_></richpp><richpp><_><pp>b : <constr.reference>bool_expr</constr.reference></pp></_></richpp><richpp><_><pp>c : <constr.reference>cmd</constr.reference></pp></_></richpp><richpp><_><pp>s1, s2, s3, s4 : <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>ms : <constr.reference>MetaState</constr.reference> <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>H : <constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference> <constr.variable>s1</constr.variable> <constr.variable>b</constr.variable></pp></_></richpp><richpp><_><pp>H0 : <constr.variable>s1</constr.variable><constr.notation> <=</constr.notation> <constr.variable>s2</constr.variable></pp></_></richpp><richpp><_><pp>H1 : <constr.reference>access</constr.reference> <constr.variable>s2</constr.variable> <constr.variable>c</constr.variable> (<constr.reference>Terminating</constr.reference> <constr.variable>s3</constr.variable>)</pp></_></richpp><richpp><_><pp>H2 : <constr.variable>s3</constr.variable><constr.notation> <=</constr.notation> <constr.variable>s4</constr.variable></pp></_></richpp><richpp><_><pp>H3 : <constr.path>Total</constr.path>.<constr.reference>loop_access_fin</constr.reference>\n (<constr.keyword>fun</constr.keyword> (s : <constr.variable>state</constr.variable>) (ms : <constr.reference>MetaState</constr.reference> <constr.variable>state</constr.variable>) => <constr.reference>access</constr.reference> <constr.variable>s</constr.variable> <constr.variable>c</constr.variable> <constr.variable>ms</constr.variable>)\n (<constr.keyword>fun</constr.keyword> s : <constr.variable>state</constr.variable> => <constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference> <constr.variable>s</constr.variable> <constr.variable>b</constr.variable>) <constr.variable>s4</constr.variable> <constr.variable>ms</constr.variable></pp></_></richpp><richpp><_><pp>IHloop_access_fin : <constr.path>Partial</constr.path>.<constr.reference>loop_access_fin</constr.reference>\n (<constr.keyword>fun</constr.keyword> (s : <constr.variable>state</constr.variable>) (ms : <constr.reference>MetaState</constr.reference> <constr.variable>state</constr.variable>) =>\n <constr.reference>access</constr.reference> <constr.variable>s</constr.variable> <constr.variable>c</constr.variable> <constr.variable>ms</constr.variable>) (<constr.keyword>fun</constr.keyword> s : <constr.variable>state</constr.variable> => <constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference> <constr.variable>s</constr.variable> <constr.variable>b</constr.variable>)\n <constr.variable>s4</constr.variable> <constr.variable>ms</constr.variable></pp></_></richpp></list><richpp><_><pp><constr.path>Partial</constr.path>.<constr.reference>loop_access_fin</constr.reference>\n (<constr.keyword>fun</constr.keyword> (s : <constr.variable>state</constr.variable>) (ms0 : <constr.reference>MetaState</constr.reference> <constr.variable>state</constr.variable>) => <constr.reference>access</constr.reference> <constr.variable>s</constr.variable> <constr.variable>c</constr.variable> <constr.variable>ms0</constr.variable>)\n (<constr.keyword>fun</constr.keyword> s : <constr.variable>state</constr.variable> => <constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference> <constr.variable>s</constr.variable> <constr.variable>b</constr.variable>) <constr.variable>s1</constr.variable> <constr.variable>ms</constr.variable></pp></_></richpp></goal></list></pair><pair><list/><list><goal><string>212</string><list><richpp><_><pp>P : <constr.reference>ProgrammingLanguage</constr.reference></pp></_></richpp><richpp><_><pp>iP : <constr.reference>ImperativeProgrammingLanguage</constr.reference> <constr.variable>P</constr.variable></pp></_></richpp><richpp><_><pp>state : <constr.type>Type</constr.type></pp></_></richpp><richpp><_><pp>state_R : <constr.reference>Relation</constr.reference> <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>BSS : <constr.reference>BigStepSemantics</constr.reference> <constr.variable>P</constr.variable> <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>iBSS : <constr.path>Total</constr.path>.<constr.reference>ImpBigStepSemantics</constr.reference> <constr.variable>P</constr.variable> <constr.variable>state</constr.variable> <constr.variable>BSS</constr.variable></pp></_></richpp><richpp><_><pp>b : <constr.reference>bool_expr</constr.reference></pp></_></richpp><richpp><_><pp>c : <constr.reference>cmd</constr.reference></pp></_></richpp><richpp><_><pp>s : <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>ms : <constr.reference>MetaState</constr.reference> <constr.variable>state</constr.variable></pp></_></richpp><richpp><_><pp>H : <constr.reference>access</constr.reference> <constr.variable>s</constr.variable> (<constr.reference>Swhile</constr.reference> <constr.variable>b</constr.variable> <constr.variable>c</constr.variable>) <constr.variable>ms</constr.variable></pp></_></richpp><richpp><_><pp>H0 : <constr.path>Total</constr.path>.<constr.reference>loop_access_inf</constr.reference>\n (<constr.keyword>fun</constr.keyword> (s : <constr.variable>state</constr.variable>) (ms : <constr.reference>MetaState</constr.reference> <constr.variable>state</constr.variable>) => <constr.reference>access</constr.reference> <constr.variable>s</constr.variable> <constr.variable>c</constr.variable> <constr.variable>ms</constr.variable>)\n (<constr.keyword>fun</constr.keyword> s : <constr.variable>state</constr.variable> => <constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference> <constr.variable>s</constr.variable> <constr.variable>b</constr.variable>) <constr.variable>s</constr.variable></pp></_></richpp><richpp><_><pp>H1 : <constr.variable>ms</constr.variable><constr.notation> =</constr.notation> <constr.reference>NonTerminating</constr.reference></pp></_></richpp></list><richpp><_><pp><constr.path>Partial</constr.path>.<constr.reference>loop_access_fin</constr.reference>\n (<constr.keyword>fun</constr.keyword> (s0 : <constr.variable>state</constr.variable>) (ms0 : <constr.reference>MetaState</constr.reference> <constr.variable>state</constr.variable>) => <constr.reference>access</constr.reference> <constr.variable>s0</constr.variable> <constr.variable>c</constr.variable> <constr.variable>ms0</constr.variable>)\n (<constr.keyword>fun</constr.keyword> s0 : <constr.variable>state</constr.variable> => <constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference> <constr.variable>s0</constr.variable> <constr.variable>b</constr.variable>) <constr.variable>s</constr.variable> <constr.variable>ms</constr.variable><constr.notation> \/</constr.notation>\n<constr.path>Partial</constr.path>.<constr.reference>loop_access_inf</constr.reference>\n (<constr.keyword>fun</constr.keyword> (s0 : <constr.variable>state</constr.variable>) (ms0 : <constr.reference>MetaState</constr.reference> <constr.variable>state</constr.variable>) => <constr.reference>access</constr.reference> <constr.variable>s0</constr.variable> <constr.variable>c</constr.variable> <constr.variable>ms0</constr.variable>)\n (<constr.keyword>fun</constr.keyword> s0 : <constr.variable>state</constr.variable> => <constr.path>Total</constr.path>.<constr.reference>eval_bool</constr.reference> <constr.variable>s0</constr.variable> <constr.variable>b</constr.variable>) <constr.variable>s</constr.variable><constr.notation> /\</constr.notation> <constr.variable>ms</constr.variable><constr.notation> =</constr.notation> <constr.reference>NonTerminating</constr.reference></pp></_></richpp></goal></list></pair><pair><list/><list/></pair></list><list/><list/></goals></option></value>
我已将此反馈格式化为 AST：
如您所见（如您所知），"goals" 标签下有四个列表。 Coq document 给了他们四个名字（当前目标、背景目标、搁置目标和放弃目标）。
我的问题：
后三类目标是什么：背景目标、搁置目标和放弃目标？我找不到关于 "shelved" 和 "abandoned" 目标的文档。
三者有什么不同？他们的名字很相似。
为什么我们要在背景目标（即第 2 个列表）下有
pair，然后在pair下再次列出，然后才是实际目标？第一个pair下的背景目标和第二个pair下的背景目标有区别吗？
感谢您的帮助！
您看到的证明表示只是核心 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 *)
}
What are the latter three goal categories: background goals, shelved goals, and abandoned goals? I cannot find docs on "shelved" and "abandoned" goals.
背景目标表示不是"in focus"的目标。从 8.5 开始，Coq 有一个 "multi-goal focus" 的概念，这意味着一个策略可以对一组目标进行操作。这可以构造为堆栈，因此列表列表。关于这对，它用于 "unfocusing"，但它可能很快就会消失，请参阅此 Pull Request 中的讨论以获取更多信息。
搁置的目标 是在通常的交互式证明上下文中隐藏的目标。例如，这些是你可能只想通过 side-effect 来解决的目标 ─ 想想
exists x, P x，你可能想把x搁置，直接解决P x─或通过其他机制，例如 type-class 分辨率。最终放弃目标是为用户承认的目标，因此被视为公理。