Проверка на evars в тактике, которая возвращает значение

Существует изящный (или неприятный) маленький трюк, который вы можете использовать, чтобы вставить выполнение тактики в конструкцию конструкции в Coq >= 8.5: оберните его в match goal.

Ltac reify_wrt values ls :=
  match ls with
  | nil => constr:(@nil nat)
  | ?a :: ?ls' => let i := lookup a values in
                 let idx := reify_wrt values ls' in
                 constr:(i :: idx)
  | ?e :: ?ls' => let check := match goal with _ => is_evar e end in
                  let i := constr:(100) in 
                  let idx := reify_wrt values ls' in
                  constr:(i :: idx)
  end.

Поскольку меня завораживают тайны языков программирования, я расскажу вам больше, чем вы, вероятно, когда-либо хотели узнать о настоящих и прошлых моделях выполнения Ltac.

Есть две фазы тактической оценки: тактическая оценка экспрессии и тактический бег. Во время выполнения тактики выполняется упорядочивание, уточнение, перезапись и т. д. Во время оценки тактического выражения оцениваются следующие конструкции, если они находятся в позиции головы тактического выражения:

• тактические призывы разрешены/отслеживаются/встраиваются/разворачиваются
• let ... in ... связывает оценку выражения своего аргумента с именем и выполняет замену
• constr:(...) оценивается и проверяется тип
• lazymaytch ... with ... end оценивается (с обратным отслеживанием) и возвращает первую совпадающую ветвь, которая успешно оценивает выражение
• match ... with ... end оценивается (с возвратом) и ветвь с готовностью выполняется. Обратите внимание, что на этой картинке match выглядит странно, потому что заставляет выполнять тактику раньше. Если вы когда-либо видели «тактику немедленного создания матчей, не разрешенную в локальных определениях» в Coq ‹ 8.5, это сообщение об ошибке явно запрещает поведение, которое я использую выше. Я предполагаю, что это потому, что это странное поведение match является бородавкой, которую оригинальные разработчики, реализующие Ltac, хотели скрыть. Таким образом, единственное место, где вы можете заметить это в Coq 8.4, это если вы вставите match внутри lazymatch и поиграете с уровнями отказов, и заметите, что lazymatch будет возвращаться назад при неудачах выполнения тактики во внутреннем match, когда вы обычно ожидаете, что он потерпит неудачу.

В Coq 8.5 тактический движок был переписан для обработки зависимых подцелей. Это вызвало тонкие изменения в семантике ;, которые можно наблюдать только при использовании evars, которые являются общими для нескольких целей. В переписывании разработчики изменили семантику lazymatch на «match без возврата» и сняли ограничение на «тактику немедленного создания матчей». Следовательно, вы можете делать странные вещи, например:

let dummy := match goal with _ => rewrite H end in
constr:(true)

и иметь тактику создания конструкций с побочными эффектами. Однако вы больше не можете делать:

let tac := lazymatch b with
                | true => tac1
                | false => tac2
                end in
tac long args.

потому что в Coq >= 8.5 lazymatch также жадно оценивает свои ветки.

Это известное ограничение Ltac: нельзя написать тактику, которая иногда возвращает значение, а иногда возвращает другую тактику. Решение состоит в том, чтобы переписать свою тактику в стиле продолжения передачи. К сожалению, я не могу дать вам подробное объяснение, как это сделать, но CDPT Адама Члипалы имеет глава Ltac, описывающая проблему; просто ищите "продолжение" в тексте.