Coq: О "%" и "мод" как символ записи - PullRequest
Новая
       12

Coq: О "%" и "мод" как символ записи

2 голосов
/ 15 мая 2019

Я пытаюсь определить нотацию для отношения эквивалентности по модулю: 

Inductive mod_equiv : nat -> nat -> nat -> Prop :=
  | mod_intro_same : forall m n, mod_equiv m n n
  | mod_intro_plus_l : forall m n1 n2, mod_equiv m n1 n2 -> mod_equiv m (m + n1) n2
  | mod_intro_plus_r : forall m n1 n2, mod_equiv m n1 n2 -> mod_equiv m n1 (m + n2).

(* 1 *) Notation "x == y 'mod' z" := (mod_equiv z x y) (at level 70).
(* 2 *) Notation "x == y % z" := (mod_equiv z x y) (at level 70).
(* 3 *) Notation "x == y %% z" := (mod_equiv z x y) (at level 70).

Все три нотации принимаются Coq.Однако в некоторых случаях я не могу использовать обозначение для формулировки теоремы: 

(* 1 *)
Theorem mod_equiv_sym : forall (m n p : nat), n == p mod m -> p == n mod m.
(* Works fine as-is, but gives error if `Arith` is imported before:
   Syntax error: 'mod' expected after [constr:operconstr level 200] (in [constr:operconstr]).
*)

(*************************************)

(* 2 *)
Theorem mod_equiv_sym : forall (m n p : nat), n == p % m -> p == n % m.
(* Gives the following error:
   Syntax error: '%' expected after [constr:operconstr level 200] (in [constr:operconstr]).
*)

(*************************************)

(* 3 *)
Theorem mod_equiv_sym : forall (m n p : nat), n == p %% m -> p == n %% m.
(* Works just fine. *)

  1. Обозначение mod определено как Coq.Init.Nat, так и Coq.Arith.PeanoNat сверхууровень.Почему новая нотация x == y 'mod' z хороша в одной среде, но не в другой?

  2. Нотация %, кажется, конфликтует со встроенной нотацией %, ноПарсер Coq выдает почти то же сообщение об ошибке, что и mod, и в обоих случаях это сообщение не очень полезно.Это намеренное поведение?IMO, если синтаксический анализатор не может понять нотацию в таком тривиальном контексте, нотация не должна была быть принята во-первых.

1 Ответ

2 голосов
/ 01 июля 2019

Ваш первый вопрос имеет простой ответ. Начальное состояние Coq (частично) определяется как Coq.Init.Prelude , которое ( на этот ответ ) содержит строку 

Require Coq.Init.Nat.

То есть Coq.Init.Prelude не импортируется, а доступно только с Require. Обозначения активны, только если модуль, содержащий их, импортирован. Если нотация объявлена ​​локальной (Local Notation ...), то даже импорт модуля не активирует нотацию.

Второй вопрос сложнее и углубляется в то, как Coq анализирует записи. Давайте начнем с примера, который работает. В Coq.Init.Notations (которая фактически импортируется в Coq.Init.Prelude), запись "x <= y <z" зарезервирована. </p> 

Reserved Notation "x <= y < z" (at level 70, y at next level).

В Coq.Init.Peano (который также импортируется) значение дается обозначению. Мы не будем особо беспокоиться об этой части, так как в основном мы занимаемся синтаксическим анализом.

Чтобы увидеть, какой эффект имеет резервирование нотации, вы можете использовать местную команду Print Grammar constr.. Это отобразит длинный список всего, что входит в разбор constr (основной единицы грамматики Coq). Запись для этой записи найдена в списке. 

| "70" RIGHTA
  [ SELF;  "?="; NEXT
  [...]
  | SELF;  "<="; NEXT;  "<"; NEXT
  [...]
  | SELF;  "="; NEXT ]

Мы видим, что нотация является ассоциативной справа (RIGHTA) 1 и живет на уровне 70. Мы также видим, что три переменные в нотации x, y и z анализируются на уровне 70 (SELF), уровне 71 (NEXT) и уровне 71 (NEXT) соответственно. 2

Во время синтаксического анализа Coq начинается с уровня 0 и смотрит на следующий токен. Пока нет токена, который должен быть проанализирован на текущем уровне, уровень увеличивается. Поэтому нотации с более низкими уровнями имеют приоритет над нотациями с более высокими уровнями. (Это концептуально, как это работает - это, вероятно, немного оптимизировано).

Когда обнаруживается сложная запись, например, после «5 <=», анализатор запоминает грамматику этой записи <sup>3 : SELF; "<="; NEXT; "<"; NEXT. После «5 <=» мы анализируем <code>y на уровне 71, а это означает, что если ничто не работает на уровне ниже 71, мы прекращаем пытаться проанализировать y и двигаться дальше.

После этого следующий токен должен быть "<", тогда мы анализируем z на уровне 71, если это так. </p>

Отличительной особенностью уровней является то, что они позволяют взаимодействовать с другими нотациями без использования скобок. Например, в коде 1 * 2 < 3 + 4 <= 5 * 6 нам не нужны скобки, поскольку * и + объявлены на более низких уровнях (40 и 50 соответственно). Поэтому, когда мы анализируем y (на уровне 71), мы можем проанализировать все 3 + 4, прежде чем перейти к <= z. Кроме того, когда мы анализируем z, мы можем захватить 5 * 6, потому что * анализирует на более низком уровне, чем уровень синтаксического анализа для z.

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

Когда импортируются Arith (или Nat), mod становится нотацией. В частности, мы имеем левую ассоциативную нотацию на уровне 40, грамматика которой SELF; "mod"; NEXT (используйте Print Grammar constr. для проверки). Когда вы определяете нотацию mod, запись ассоциируется справа на уровне 70 с грамматикой SELF; "=="; constr:operconstr LEVEL "200"; "mod"; NEXT. Средняя часть просто означает, что y анализируется на уровне 200 (как constr - как и все, о чем мы говорили).

Таким образом, при синтаксическом анализе n == p mod m мы анализируем n == в порядке, затем начинаем синтаксический анализ y на уровне 200. Так как mod у Арит только на 40-м уровне, мы будем анализировать p mod m. Но тогда наша запись x == y mod z остается без изменений. Мы находимся в конце заявления, и mod z до сих пор не проанализирован. 

Syntax error: 'mod' expected after [constr:operconstr level 200] (in [constr:operconstr]).

(теперь ошибка имеет смысл?)

Если вы действительно хотите использовать нотацию mod, все еще используя нотацию Арит mod, вам нужно проанализировать y на более низком уровне. Так как x mod y находится на уровне 40, мы можем сделать y уровнем 39 с 

Notation "x == y 'mod' z" := (mod_equiv z x y) (at level 70, y at level 39).

Поскольку арифметические операции выполняются на уровнях 40 и выше, это означает, что нам нужно написать 5 == (3 * 4) mod 7, используя скобки.

Для вашей записи "%" это будет сложно. «%» обычно используется для разграничения области (например, (x + y)%nat) и очень тесно связывается на уровне 1. Вы можете сделать y синтаксический анализ на уровне 0, но это означает, что нотации вообще не могут использоваться для y без скобок. Если это приемлемо, продолжайте.

Поскольку «%%» не конфликтует ни с чем (в стандартной библиотеке), вы можете использовать его здесь на любом удобном для вас уровне. Возможно, вы захотите сделать y анализ на более низком уровне (y at next level довольно стандартно), но это не обязательно.

  1. Правая ассоциативность является значением по умолчанию. Судя по всему, парсер Coq не имеет опции «без ассоциативности», поэтому даже если вы явно скажете «без ассоциативности», он все равно будет зарегистрирован как правоассоциативный. На практике это не часто вызывает проблемы.

  2. Вот почему запись зарезервирована с "y на следующем уровне". По умолчанию переменные в середине нотации анализируются на уровне 200, что можно увидеть, сохранив аналогичную нотацию, такую ​​как Reserved Notation "x ^ y ^ z" (at level 70). и используя Print Grammar constr., чтобы увидеть уровни синтаксического анализа. Как мы увидим, это то, что происходит с x == y mod z.

  3. Что произойдет, если несколько обозначений начинаются с "5 <="? Очевидно, что будет взят тот, который имеет более низкий уровень, но если они имеют один и тот же уровень, он пробует оба и возвращается, если не анализирует. Однако, если одна нотация заканчивается, она не возвращается, даже если этот выбор вызовет проблемы позже. Я не уверен в точных правилах, но подозреваю, что это зависит от того, какая нотация объявлена ​​первой. </p>

...