Определите дизъюнкции в виде проп

Question

Меня интересует, вероятно, ложная лемма:

Lemma decideOr : forall (P Q : Prop),
    (P \/ Q) -> {P} + {Q}.

, который утверждает, что мы можем алгоритмически решить любое доказательство or в виде Prop. Конечно, Coq не позволяет нам destruct вводить данные для его сортировки Set. Однако доказательство P \/ Q является лямбда-термином, который Coq принимает к печати, поэтому внешние инструменты могут его обрабатывать.

Первый вопрос: может ли этот лямбда-термин быть определен вне Coq (при условии, что этот термин не использует аксиомы, только простое Coq)? Возможно, потому что правила конструктивной логики требуют, чтобы все дизъюнкции были явно выбраны, без обмана путем доказательства от противоречия. Итак, можем ли мы закодировать парсер терминов доказательства Coq и попытаться решить, был ли доказан первый или второй операнд or? Если срок начинается с or_introl или or_intror, мы закончили. Таким образом, я думаю, что проблемы, когда термин является лямбда-приложением. Но затем термины Coq сильно нормализуются, поэтому мы приводим его к нормальной форме, и, похоже, он будет начинаться либо с or_introl, либо с or_intror.

Второй вопрос: если эта проблема может быть решена вне Coq, что мешает нам усвоить ее в Coq, то есть доказательство леммы decideOr выше?

Answer 1

Первый вопрос

Да, вы можете написать программу, которая принимает в качестве входных данных подтверждение Coq A \/ B и выводит true или false в зависимости от того, какая сторона использовалась для доказательства дизъюнкции.Действительно, если вы напишите

Compute P.

в Coq, где P : A \/ B, Coq нормализует доказательство P и выведет, какой конструктор был использован.Это не будет работать, если P использует доказательства, оканчивающиеся на Qed (потому что они не развернуты оценщиком), но в принципе можно заменить Qed на Defined везде и заставить его работать.

Второй вопрос

Что мешает нам доказать decideOr, так это то, что разработчики Coq хотели иметь тип предложений, который поддерживает исключенную середину (используя аксиому), в то же время позволяя программам выполняться.Если бы decideOr были теоремой и , мы хотели бы использовать исключенную середину (classical : forall A : Prop, A \/ ~ A), было бы невозможно выполнить программы, ответвляющиеся по результату decideOr (classical A).Это не означает, что decideOr является ложным: его вполне можно признать аксиомой.Существует разница между не доказуемостью («не существует доказательства A») и опровержимостью («существует доказательство ~ A»).