Новая область в Coq

Question

Я бы хотел, чтобы моя собственная область, чтобы играть с длинными distfixes.

Declare Scope my_scope. 
Delimit Scope my_scope with my. 
Open Scope my_scope. 

Definition f (x y a b : nat) : nat := x+y+a+b. 
Notation "x < y * a = b" := (f x y a b) 
(at level 100, no associativity) : my_scope. 

Check (1 < 2 * 3 = 4)%my. 

Как вы создаете новую область?

EDIT: Я выбрал «x < y * a = b» для переопределения операторов Coq (каждый с другим приоритетом).  

Answer 1

Команда Declare Scope не существует. Различные команды о областях описаны в section 12.2 of the Coq manual.

Ваш выбор примерной нотации имеет неотъемлемые проблемы, поскольку он сталкивается с предопределенными обозначениями, которые, по-видимому, используются перед вашими обозначениями.

При взгляде на первые компонентах анализатор видит _ < _ и думает, что вы на самом деле говорите о сравнении целых чисел, то он видит вторую часть как экземпляр записи _ * _, то он видит, что все, что левый стороны равенства. И все вместе парсер счастлив, он строит выражение вида:

(1 < (2 * 3)) = 4 

Это строится парсером, и тип системы еще не, запрошенные. Контроллер типа видит естественное число в качестве первого ребенка (_ < _) и счастлив. Он видит (_ * _) в качестве второго ребенка, и он счастлив, теперь он знает, что первый ребенок этого продукта должен быть nat-номером, и он по-прежнему счастлив; в конце он имеет равенство, а первый компонент этого равенства относится к типу Prop, но второй компонент относится к типу nat.

Если вы наберете Locate "_ < _ * _ = _"., ответ подскажет вам, что вы определили новую нотацию. Проблема в том, что эта нотация никогда не используется, потому что парсер всегда находит другую нотацию, которую он может использовать раньше. Понимание того, почему нотация предпочтительнее другой, требует больше знаний о технологии разбора, о чем упоминается в главе 12 Кока в предложении (неясное для меня):

Расширяемый анализ Coq выполняется Camlp5, который по существу анализатор LL1.

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

Notation "<< x < y * a = b >>" := (f x y a b) 
(x at level 59, y at level 39, a at level 59) : my_scope. 

Уровень x выбирается так, чтобы быть ниже, чем уровень =, уровень у выбирается так, чтобы быть ниже, чем уровень *, уровень a выбирается так, чтобы быть ниже, чем =. Уровни были получены путем считывания ответа команды Print Grammar constr. Кажется, что это работает, поскольку принята следующая команда.

Check << 1 < 2 * 3 = 4 >>. 

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

Answer 2

Чтобы ответить на этот актуальный вопрос в заголовке:

Новая область будет создаваться при объявлении нотации, которая использует его. То есть вы не объявляете новую область my_scope отдельно. Вы просто пишете

Notation "x <<< y" := (f x y) (at level 100, no associativity) : my_scope. 

и объявляет о новой сфере применения my_scope.