Есть ли способ доказать следующую теорему в Coq?
Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2.
РЕДАКТИРОВАТЬ : Попытка дать краткое объяснение «что такое доказательство неуместности» (поправьте меня, если я ошибаюсь или неточен)
Основная идея заключается в том, что в мире предложений (или Prop
в Coq), что вас (и вы должны) действительно волнует, - это доказуемость предложения, а не его доказательства, их может быть много (или их нет). Если у вас есть несколько доказательств, с точки зрения доказуемости, они равны в том смысле, что они доказывают одно и то же утверждение . Так что их различие просто не имеет значения. Это отличается от вычислительной точки зрения, где вы действительно заботитесь о различии двух терминов, например, в принципе, вы не хотите, чтобы два обитателя bool
типа (или, Set
по словам Кока), а именно true
и false
были равны. Но если вы вставите их Prop
, они будут равны.
Ответы:
Доказательство неуместности в целом не подразумевается теорией, стоящей за Coq. Даже доказательство несоответствия равенству не подразумевается; это эквивалентно аксиоме К STREICHER в . Оба могут быть добавлены в качестве аксиом .
Существуют разработки, в которых полезно рассуждать об объектах доказательства, и несоответствие доказательства делает это почти невозможным. Можно утверждать, что в этих разработках должны быть все объекты, структура которых имеет значение
Set
, но с базовой теорией Coq такая возможность есть.Существует важная часть доказательства несоответствия, которая всегда имеет место. Аксиома Штрейхера K всегда выполняется в разрешимых областях, т. Е. Доказательства равенства на разрешимых множествах единственны. Общее доказательство находится в
Eqdep_dec
модуле в стандартной библиотеке Coq. Вот ваша теорема как следствие (мое доказательство здесь не обязательно самое элегантное):Для этого особого случая вот прямое доказательство (вдохновленное общим доказательством в
Eqdep_dec.v
). Во-первых, определим, что мы определяем каноническое доказательствоtrue=b
(как обычно в Coq, проще сначала иметь константу). Затем мы показываем, что любое доказательствоtrue=b
должно бытьrefl_equal true
.Если вы добавите классическую логику в Coq, вы получите доказательство неуместности. Говоря интуитивно, классическая логика дает вам оракул решения для предложений, и этого достаточно для аксиомы K. В модуле стандартной библиотеки Coq есть доказательство
Classical_Prop
.источник