Предполагает ли ssreflect исключенную середину?
Я читаю учебник ssreflect, который гласит:
Ниже мы докажем..., переведя высказывание в его логический аналог, что легко доказать с помощью грубой силы. Этот метод доказательства называется отражением. Дизайн Ssreflect учитывает, и дух ssreflect рекомендует широко использовать такую технику.
Означает ли это (отражение), что ssreflect предполагает исключенную середину (forall A:Prop, A \/ ~A)?
Похоже, что это так, потому что все логические значения удовлетворяют EM. Если это так, это будет большим предположением для следования стилю ssreflect.
Кроме того, я не совсем понимаю "местную" или "мелкую" часть этого, которая следует:
Поскольку он обычно используется локально для эффективной обработки небольших частей доказательств (вместо использования в общей структуре доказательств), это называется мелкомасштабным отражением, отсюда и название ssreflect.
Что это означает, мелкие детали против общей структуры доказательства. Означает ли это, что мы можем иногда принимать EM локально без вреда и вообще не использовать EM, или локальное здесь означает что-то еще?
Кроме того, я не достаточно опытен в Coq, и не совсем понимаю, как этот стиль "грубой силы" на "логических аналогах" (в основном на основе case анализ из того, что я читал до сих пор) более эффективен, чем ванильный способ Coq. Для меня грубая сила не очень интуитивна и ее нелегко угадать, пока не увидишь результат.
Какие-нибудь конкретные примеры, чтобы проиллюстрировать эффективность здесь?
2 ответа
Ssreflect не предполагает исключенную середину, но большие части библиотеки построены на булевых предложениях, то есть типа boolдля которого это действительно держит это
forall b : bool, b = true \/ b = false
Эквивалентная версия вышеупомянутого обычно пишется с использованием неявного is_true кастинг, как:
forall b : bool, b \/ ~ b.
"Отражаемые" предикаты - это те, которые имеют версию в bool; хорошим примером является отношение "меньше или равно" между натуральными числами.
В стандартном Coq, le кодируется как индуктивный тип, тогда как в ssreflect это вычислительная функция leq: nat -> nat -> bool,
С использованием leq Функция доказательства более "эффективна" по следующей причине: представьте, что вы хотите доказать, что 102 < 203, Используя стандартное определение Coq, вам нужно будет построить большой термин доказательства, вы должны явно закодировать каждый шаг доказательства.
Однако, с его вычислительным аналогом, доказательство является просто термином erefl, засвидетельствовав, что алгоритм вернулся true, Это важно в больших доказательствах, помимо многих других преимуществ IMO.
В заключение я должен не согласиться с утверждением, что "ssreflect касается только разрешимых типов". Хотя большая часть библиотек основана на разрешимых (логических) предикатах, во многих других это предположение не делается или может быть очень полезным при наличии некоторых аксиом.
Ssreflect не предполагает исключенную середину в общем, вы не сможете доказать, что
forall A: Prop, A \/ ~A
Тем не менее, ssreflect касается только разрешимых типов: типов, в которых может быть принято решение о равенстве, обычно обозначаемых как
Definition decidable (T:Type) := forall x y:T, {x = y}+{x <> y}.
в Coq. Это означает, что для любых двух элементов типа TВы можете получить конструктивный (в Set, не в Prop как исключенное среднее) доказательство того, что они либо равны, либо различны. Поэтому большинство рассуждений можно сделать в bool и не в Prop, так что у вас есть какая-то ограниченная форма исключенного среднего, только для логических выражений.