Search code examples
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.

    • background goals represents the goals that are not "in focus". Since 8.5, Coq has a notion of "multi-goal focus" which means that a tactic can operate over a set of goals. This can structured as a stack so hence the list of lists. Regarding the pair, it is used for "unfocusing", but it may go away soon, see the discussion in this Pull Request for more information.

    • shelved goals are goals that are hidden from the usual interactive proof context. For example, these are goals that you may want to solve only by side-effect ─ think of exists x, P x, you may want to put x in the shelve and directly solve P x ─ or by other mechanism such as type-class resolution.

    • and finally given up goals are goals that were admitted for the user and thus taken as axioms.