Блог

Я следую этому руководству: 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]).
Я не понимаю, что я делаю не так?
Кроме того, где лучше всего получить документацию? Я имею в виду документацию, удобную для начинающих.

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

 Require Import Utf8.

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

Эквивалентами этих обозначений в формате ASCII являются forall for ∀ (как вы поняли) и -> for → . Если у вас есть импортированные обозначения, вы можете увидеть, что они означают при использовании 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
  

в котором используется -> обозначение.