Блог

Я использую Coq 8.10.0. Следующий сценарий проверки, похоже, работает на Mac (игнорируя предупреждение):

 Lemma plus_comm : forall (n m : nat), n   m = m   n.
Proof.
  intros.
  - admit.
Qed.
 

Но один и тот же сценарий проверки не принимается в Linux (Ubuntu) и Windows. Он выдает следующую ошибку:

(в proof plus_comm): попытка сохранить доказательство с отказом от целей. Если это действительно то, что вы хотите сделать, используйте Допущенный вместо Qed .

Есть какие-нибудь идеи, что здесь происходит?

PS: Я знаю, что в идеале доказательства с допусками должны заканчиваться Допущенными вместо Qed / Defined . Я пытаюсь отладить сценарий проверки.

Вы уверены, что используете одну и ту же версию Coq на macOS и на Windows / Linux? Я точно не помню, какая версия внесла изменения в поведение, но теперь по умолчанию запрещено Qed использовать неполное доказательство.

Если вы все еще хотите отладить доказательство и вам нужно использовать Qed , я бы предложил использовать временную аксиому:

 Axiom todo : forall {A}, A.
Tactic Notation "todo" := (exact todo).
 

Теперь вы можете использовать todo в качестве тактики вместо admit и это позволит вам использовать Qed .

Я только что понял, что это не из-за операционной системы. Это из-за LibTactics от Software Foundations (https://softwarefoundations.cis.upenn.edu/plf-current/LibTactics.html ). Если у нас есть LibTactics, импортированные в Coq proof script, это позволяет нам поместить Qed в конец леммы с допусками.