Почему эта программа coq не запускается? - PullRequest
Новая
       2

Почему эта программа coq не запускается?

0 голосов
/ 18 марта 2020

Я новичок в Coq и изучаю, как создавать коды с видео https://www.youtube.com/watch?v=oJm5TH0GdSo&list=PLt7hcIEdZLAnCoZePG60qgVP4ddP0s3WZ&index=2.

Я создал программу после этого видео (которая начинается почти с 29 минут видео) но он не работает, как я ожидал. Не могли бы вы сказать мне, почему это происходит? Я всегда застреваю в случае.

Программа, которую я сделал, дана ниже: 

Theorem shugouonajidesho : 
  forall P Q : Prop,
    P/\Q->Q/\P.
Proof. 
  intros P Q H. split.
  Case "Q".
  inversion H as [HP HQ]. imply HQ.
  Case "P".  inversion H as {HP HQ]. imply HP. 
Qed.

1 Ответ

0 голосов
/ 18 марта 2020

В вашем доказательстве есть три проблемы, но в основном это синтаксис c.

Синтаксис Case "Q" и Case "P" исходит из Фондов программного обеспечения. Вам нужно будет импортировать некоторую конкретную библиотеку , чтобы иметь возможность использовать ее. Если вы не хотите этого делать, это не обязательно. Чтобы сфокусировать цели, вы можете использовать маркеры (обычно -, + или *). Есть и другие способы, но это наиболее типичный.

imply tacti c не существует (по крайней мере, в стандартной библиотеке). Однако то, как вы его используете, заставляет меня думать, что вы имели в виду apply.

В inversion H as {HP HQ]. обе скобки должны быть квадратными скобками.

Внесение этих изменений позволяет теореме работать, но я бы также предложил несколько изменений для идиоматичности.

Использование inversion, вероятно, здесь излишне. Все, что вы делаете, это уничтожаете соединение на его части, поэтому destruct H as [HP HQ]. будет работать так же хорошо.

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

Наконец, второстепенный: я бы предложил поставить пробелы вокруг ->. Это немного облегчает чтение. 

Theorem shugouonajidesho: forall P Q : Prop, P/\Q -> Q/\P.
Proof.
  intros P Q H.
  split.
  - inversion H as [HP HQ].
    apply HQ.
  - inversion H as [HP HQ].
    apply HP.
Qed.
...