При реализации сложной тактики в Ltac есть некоторые команды Ltac или вызов тактики, которые, как я ожидаю, потерпят неудачу и где это ожидается (например, чтобы завершить repeat или вызвать обратное отслеживание). Эти сбои обычно возникают на...

Допустим, у меня есть причудливая тактика, позволяющая решать леммы определенного типа: Ltac solveFancy := some_preparation; repeat (first [important_step1 | important_step2]; some_cleanup); solve_basecase. Теперь я использую...

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

Этот вопрос касается проекта, которым я занимаюсь, а именно кодирования Principia Mathematica на Coq. Principia разработал правила вывода, одним из которых является Syll: ∀ P Q R: Опора, P → Q, Q → R: P → R Я пытаюсь создать сценарий Ltac,...