Почему Coq.Init.Logic определяет обозначение «A -> B»? - PullRequest
Новая
       10

Почему Coq.Init.Logic определяет обозначение «A -> B»?

0 голосов
/ 09 сентября 2018

Файл Coq Standard Library Coq.Init.Logic, который можно найти здесь , содержит оператор

Notation "A -> B" := (forall (_ : A), B) : type_scope.

Я не понимаю, как это возможно, учитывая, что символ -> уже имеет встроенное значение. -> перезаписывается ли это?

Если я введу A -> B, как Coq узнает, имею ли я в виду A -> B или forall (x : A), B?

Да, я знаю, что два предложения логически эквивалентны, но разве это не должно быть теоремой, а не обозначением?

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

1 Ответ

0 голосов
/ 09 сентября 2018

Символ -> на самом деле определяется обозначением, которое вы нашли в Coq.Init.Logic! Пока forall является встроенным, -> определяется с использованием системы обозначений. Модуль Coq.Init.Logic автоматически загружается в Coq, поскольку он экспортируется с помощью Coq.Init.Prelude , поэтому у вас сразу есть к нему доступ.

Когда вы пишете A -> B, это интерпретируется с использованием записи, которая является forall (_:A), B; это синтаксически похоже на forall (x:A), B, за исключением того, что выражение B не может зависеть от x. Нет никакой двусмысленности - это единственное определение для A -> B, и действительно, если вы загрузите Coq без прелюдии (например, передавая флаг -noinit) A -> B не будет анализироваться.

Одним из аспектов Coq, который делает -> кажущимся встроенным, является то, что нотация двунаправленная - она ​​применяется как для анализа, так и для печати. Вот почему вы видите -> в своих целях и когда вы используете Check и Search. Здесь есть реальная двусмысленность; в этом случае, если forall (x:A), B имеет B, который не зависит от x, Coq предпочитает печатать его, используя нотацию, а не встроенный синтаксис. Если вы отключите печать примечаний (Unset Printing Notation.), вы увидите forall (_:A), B везде, где вы видели A -> B. Конечно, если у вас есть тип функции с реальной зависимостью, то Coq должен использовать forall (x:A), B, поскольку B должен ссылаться на переменную x.

...