Как оставить гол незавершенным в Coq - PullRequest
Новая
       4

Как оставить гол незавершенным в Coq

1 голос
/ 01 февраля 2020

В Изабель вы можете оставить цель незавершенной двумя способами:

  • извините: вы оставите свое доказательство, и этот факт можно будет использовать в последующих доказательствах.
  • упс: оставим доказательство, но этот факт нельзя использовать в более поздних доказательствах.

Есть ли подобная функциональность в Coq, которая позволила бы мне оставить цель незавершенной, чтобы вернуться к ней позже? Это полезно, чтобы набросать структуру доказательства, не заполняя все детали. Обратите внимание, что подход в Как переключить текущую цель в Coq? изменяет структуру доказательства. Это не то, что я ищу.

1 Ответ

3 голосов
/ 01 февраля 2020

У вас есть несколько способов прекратить доказательство в Coq. Вы, наверное, знаете Qed, который утверждает, что доказательство завершено. Существует также Defined, когда вы хотите, чтобы доказательство имело вычислительный контент.

Вещи, которые вы ищете:

  • Admitted, которое допускает доказательство, так что можно использовать позже;
  • Abort, который прекращает доказательство леммы.

Их можно использовать таким образом: 

Lemma foo : forall n, n = 0.
Proof.
  intro n. destruct n.
  - reflexivity.
  -
Abort.

Lemma bar : forall n, n = n.
Admitted.

В обоих случаях вы можете иметь сценарий частичного доказательства до Admitted / Abort или вообще без него.

Как указывает @HTNW, вы также можете использовать эквивалентные тактики admit и give_up внутри подзадач доказательства. Используя их, однако, имеет , который должен быть заключен с использованием Admitted или Abort. 

Lemma lem : forall A, A + A -> A.
Proof.
  intros A h.
  destruct h.
  - admit.
  - give_up.
Admitted.

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

Axiom cheating : forall A, A.

Tactic Notation "cheat" := apply cheating.

Lemma lem : forall A, A + A -> A.
Proof.
  intros A h.
  destruct h.
  - cheat.
  - cheat.
Defined. (* This is now ok *)

Вы должны быть осторожны, используя этот трюк. Вы можете проверить, что лемма была доказана без аксиом, используя Print Assumptions lem. Если он говорит «закрыто в контексте», то вы хороши, иначе он перечислит аксиомы, от которых он зависит, и если появится cheating, вы знаете, что это не полностью доказано.

...