coq синтаксис теоремы импликации - PullRequest
Новая
       6

coq синтаксис теоремы импликации

0 голосов
/ 15 марта 2019

Я следую этому руководству: https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html
Раздел «Доказательство путем перезаписи»:
Код 

Theorem plus_id_example : forall n m : nat,
  n = m =>
  n + n = m + m.

Создает ошибку:
Синтаксическая ошибка: '.'ожидается после [vernac: gallina] (в [vernac_aux]).
Я не понимаю, что я делаю не так?
Кроме того, как лучше всего получить документацию?Я имею в виду документацию, удобную для начинающих.

1 Ответ

1 голос
/ 15 марта 2019

Чтобы использовать текст в том виде, в котором он написан на странице, на которую вы ссылаетесь, вам необходимо импортировать некоторые записи. В частности, ∀ и → не существуют по умолчанию. Для импорта этих обозначений используйте Require Import Utf8.

Require Import Utf8.

Theorem plus_id_example : ∀n m:nat,
  n = m →
  n + n = m + m.

ASCII-эквивалентами этих обозначений являются forall для ∀ (как вы выяснили) и -> для →. Если у вас есть импортированные нотации, вы можете увидеть, что они обозначают Locate. Locate "→". будет иметь выход 

Notation
"x → y" := forall _ : x, y : type_scope
(default interpretation)

Конечно, это не дает нам ->, поскольку -> само по себе является обозначением для того же самого. Coq отобразит эту запись по умолчанию, поэтому, если вы введете 

Theorem plus_id_example : forall n m : nat,
  forall _ : n = m,
  n + n = m + m.

(без импорта Utf8), вывод 

1 subgoal
______________________________________(1/1)
forall n m : nat, n = m -> n + n = m + m

, который использует обозначение ->.

...