Каковы исходные цели, отложенные цели и заброшенные цели в Coq?
Я использую ideslave Coq (он же протокол 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: 
Как вы можете видеть (и как вы знаете), под тегом "цели" есть четыре списка. Документ Coq дал им четыре названия (текущие цели, исходные цели, отложенные цели и оставленные цели).
Мои вопросы:
Каковы последние три категории целей: исходные цели, отложенные цели и заброшенные цели? Я не могу найти документы по "отложенным" и "заброшенным" целям.
Чем они отличаются? Их имена похожи.
Почему у нас
pairпод фоновые цели (то есть, 2-й список), а затем списки снова подpair, а потом собственно цели? Есть ли различия между фоновыми целями по первомуpairа те, что под вторымpair?
Спасибо за помощь!
1 ответ
Решение
Доказательное представление, которое вы видите, - это всего лишь воплощение ядра 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 имеет понятие "многоцелевого фокуса", что означает, что тактика может работать над набором целей. Это может быть структурировано как стек, поэтому список списков. Что касается пары, она используется для "расфокусировки", но она может скоро уйти, см. Обсуждение в этом запросе на получение дополнительной информации.
отложенные цели - это цели, которые скрыты от обычного интерактивного контекста доказательства. Например, это цели, которые вы можете решить только побочным эффектом - подумайте о
exists x, P xвы можете поставитьxв полку и прямо решитьP x─ или другим механизмом, таким как разрешение класса типов.и, наконец, отказ от целей - это цели, которые были приняты пользователем и, таким образом, приняты в качестве аксиом.