coqcoq-extraction

What are background goals, shelved goals, and abandoned goals in Coq?

I am using Coq's ideslave (a.k.a. XML protocol). By calling <call val="Goal"><unit/></call>, a typical feedback looks like

<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>

I have formatted this feedback as an AST: enter image description here

As you can see (and as you know), there are four lists under the "goals" tag. The Coq document gave them four names (current goals, background goals, shelved goals, and abandoned goals).

My questions:

  1. What are the latter three goal categories: background goals, shelved goals, and abandoned goals? I cannot find docs on "shelved" and "abandoned" goals.

  2. In what ways are the three different? Their names are similar.

  3. Why shall we have pair under the background goals (i.e., the 2nd list), and then lists again under pair, and then the actually goals? Are there differences between the background goals under the first pair and the ones under the second pair?

Thanks for helping!

Solution

  • The proof representation you see is just a reification of the core Proof.t object that contains the information about the current proof.

    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.