я могу заставить Coq печатать круглые скобки?

Я новичок в Coq, работаю над написанием теоретико-множественных доказательств.

Я понял, что скобки опущены, и мне трудно читать формулу. Например,

1 subgoal
A, B : {set T}
H : B \subset A
______________________________________(1/1)
A :\: A :|: A :&: B = B

Но я бы хотел, чтобы Coq напечатал (A :\: A) :|: (A :&: B) = B. Этот вывод выше получен с помощью следующего кода.

Require Import ssreflect ssrbool ssrnat fintype finset.
Theorem a_a_b__b' (A B : {set T}) : B \subset A -> (A :\: (A :\: B)) = B.
Proof.
  move=> H.
  rewrite setDDr.

К моему удивлению, если я увижу исходную кодировку setDDr в finset.v, в нем есть следующие круглые скобки

Lemma setDDr A B C : A :\: (B :\: C) = (A :\: B) :|: (A :&: C).
Proof. by rewrite !setDE setCI setIUr setCK. Qed.

Поэтому мне интересно, почему скобки исчезают и как заставить Coq явно печатать скобки в CoqIde.


coq coqide
person Pengin    schedule 04.10.2016    source источник

Ответы (3)


arrow_upward
3
arrow_downward

Вы можете отключить все обозначения с помощью этой команды:

Unset Printing Notations.

Printing Notations - это флаг, Unset его выключает. Дополнительную информацию об обозначениях можно найти здесь: https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#syntax-extensions-and-interpretation-scopes.

Например,

(n + m) * 0 = n * 0 + m * 0

будет напечатан как

eq (Nat.mul (Nat.add n m) O) (Nat.add (Nat.mul n O) (Nat.mul m O))

Я знаю, это не очень хорошее решение.

person Khoa Vo    schedule 26.09.2019
comment
Было бы здорово, если бы был промежуточный флаг, добавляющий только неявные круглые скобки. Возможно, что-то вроде «Установить круглые скобки для печати». - person Ricardo; 05.01.2020

arrow_upward
2
arrow_downward

В последних версиях Coq Set Printing Parentheses должно работать.

person Rincewind    schedule 04.01.2021

arrow_upward
1
arrow_downward

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

Предполагается, что Coq вставляет круглые скобки в зависимости от приоритета операторов, это означает, что вам придется переопределить приоритет :|: для достижения желаемого. Это нелегко сделать, и большинству людей это не понравится. Текущий приоритет :|: - это то, что ожидают математики.

Возможный обходной путь - определить другую локальную нотацию для собственного использования:

From mathcomp
Require Import ssreflect ssrbool eqtype ssrnat seq choice fintype finset.

Section U.

Variable (T: finType).

Local Notation "A :||: B" := (@setU T A B) (at level 48, left associativity).

Theorem a_a_b__b' (A B : {set T}) : B \subset A -> (A :\: (A :\: B)) = B.
Proof.
move=> H; rewrite setDDr.

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

person ejgallego    schedule 04.10.2016
comment
Хм, вот безумная идея: можно ли включить скобки в нотацию "'(' A :||: B ')'" и отправить ее на уровень 0? Я пробовал это на nat +: например, 1 + 2 * 3 анализирует правильно, и (1 + 2) + (3 + 4) печатается со всеми скобками, в том числе, к сожалению, верхнего уровня. Мне интересно, каковы будут недостатки этого подхода. - person Anton Trunov; 04.10.2016
comment
Вы действительно можете это сделать, но разве это не нарушает нормальный синтаксический анализ скобок? - person ejgallego; 04.10.2016
comment
Я пробовал несколько примеров, но не обнаружил, что это каким-то образом ломает парсинг. Может, мне просто не повезло. - person Anton Trunov; 04.10.2016
comment
Вы можете опубликовать полный пример? - person ejgallego; 04.10.2016
comment
Я понимаю. Однако вам нужно объявить его на уровне 0, это напечатает `(A: \: A: ||: A: &: B)` вместо `(A: \: A): ||: (A: & : B) `, да? - person ejgallego; 04.10.2016
comment
Ты прав. Я имел в виду, что таким образом мы можем переопределить (A :\: A) и (A :&: B). Не могу сейчас попробовать, похоже, я как-то сломал установку ssreflect. - person Anton Trunov; 04.10.2016
comment
Я попробовал и получил неоднозначные результаты: (A :&: A) :|: A :&: B = B - person ejgallego; 04.10.2016
comment
Интересно, так что в этом выражении упала вторая пара скобок (A :&: A) :|: (A :&: B) = B? Я попробовал нечто подобное с nats: Notation "'(' x * y ')'" := (Nat.mul x y) (at level 0, left associativity)., и, похоже, он сохранил скобки: Goal (1 * 1) + (1 * 2) = 3. дает как (1 * 1) + (1 * 2) = 3 в качестве цели. - person Anton Trunov; 04.10.2016
comment
Я сделал ошибку, извините, моя ошибка. Вроде теперь нормально работает. - person ejgallego; 04.10.2016
comment
Спасибо за ответ и информативные комментарии. В самом деле, работа намного сложнее (и неприятна), чем я ожидал ... Я предполагал, что у Coq может быть такая команда, как Set Print Parentheses Level 4. Я должен узнать приоритет операторов, а не вводить Local Notations. Есть ли ссылка, объясняющая приоритет? Например, почему вы можете сказать мне, что :\: и :&: выше, чем :|:? Где в исходном коде Coq их определяет? - person Pengin; 04.10.2016
comment
Позвольте мне подробнее объяснить мою озабоченность ... Вы написали Текущий приоритет: |: - это то, что ожидают математики. Но я полагаю, что математикам не нравятся плохо определенные формулы, такие как $ A \ cup B \ cap C $, если не указан приоритет. Поэтому я предполагаю, что Coq (или связанные библиотеки) строго определяют приоритет. Я хотел бы знать приоритет в Coq. - person Pengin; 04.10.2016
comment
@Pengin Я не знаю ни одной простой команды для этого, но (1) вы можете искать уровни приоритета в источнике (но это не всегда). Вам нужен Notation ... (at level ...). Но это может быть Reserved Notation определено в другом месте. (2) Таким образом, вы можете просто загрузить свои модули, ввести команду Print Grammar constr. и выполнить поиск по выходным данным. Обратные косые черты удваиваются из-за экранирования. Вам нужно искать :\\:, если вы хотите узнать уровень :\: (кстати, это уровень 50 и левоассоциативный). P.S. На всякий случай: уровень 0 означает самую сильную привязку. HTH - person Anton Trunov; 04.10.2016
comment
В дополнение к очень хорошим предложениям Антона, здесь приводится конкретное определение обозначений множества: github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/. - person ejgallego; 05.10.2016