Что означает "true = false" в Coq?

Ответ 1

Как правило, когда вы делаете анализ случая в доказательстве теоремы, многие дела сводятся к "не может случиться". Например, если вы доказываете некоторый факт о целых числах, вам может потребоваться провести анализ случая, является ли целое число i положительным, нулевым или отрицательным. Но могут быть другие гипотезы, лежащие в вашем контексте или, возможно, часть вашей цели, что противоречит одному из случаев. Вы можете узнать из предыдущего утверждения, например, что i никогда не может быть отрицательным.

Однако Coq не настолько умный. Поэтому вам все равно придется пройти через механику, фактически демонстрируя, что две противоречивые гипотезы могут быть склеены в доказательство абсурда и, следовательно, доказательство вашей теоремы.

Подумайте об этом, как в компьютерной программе:

switch (k) {
  case X:
    /* do stuff */
    break;
  case Y:
    /* do other stuff */
    break;
  default:
    assert(false, "can't ever happen");
}

Цель false = true - "никогда не случится". Но вы не можете просто утверждать свой выход в Кок. Вам действительно нужно указать срок действия.

Итак, вы должны доказать абсурдную цель false = true. И единственное, с чем вам нужно работать, - это hyothesis H: andb false c = true. Момент подумает, что на самом деле это абсурдная гипотеза (потому что andb false y сводится к false для любого y и, следовательно, не может быть правдой). Таким образом, вы натыкаетесь на цель единственной вещью в вашем распоряжении (а именно H), и ваша новая цель - false = andb false c.

Итак, вы применяете абсурдную гипотезу, пытающуюся достичь абсурдной цели. И вот, вот и получилось, что вы можете показать что-то, что вы можете показать рефлексивностью. QED.

ОБНОВЛЕНИЕ Формально, вот что происходит.

Напомним, что каждое индуктивное определение в Coq имеет индукционный принцип. Ниже приведены типы принципов индукции для равенства и предложения False (в отличие от термина False типа bool):

Check eq_ind.
eq_ind
  : forall (A : Type) (x : A) (P : A -> Prop),
    P x -> forall y : A, x = y -> P y
Check False_ind.
False_ind
 : forall P : Prop, False -> P

Этот принцип индукции для False говорит, что если вы дадите мне доказательство False, я могу дать вам доказательство любого предложения P.

Принцип индукции для eq более сложен. Пусть оно ограничивается bool. И конкретно к False. В нем говорится:

Check eq_ind false.
eq_ind false
 : forall P : bool -> Prop, P false -> forall y : bool, false = y -> P y

Итак, если вы начнете с предложения P(b), которое зависит от булевого b, и у вас есть доказательство P(false), то для любого другого булева y, равного False, вы имеете доказательство P(y).

Это не звучит ужасно, но мы можем применить его к любому предложению P, которое мы хотим. И мы хотим особо неприятного.

Check eq_ind false (fun b : bool => if b then False else True).
eq_ind false (fun b : bool => if b then False else True)
 : (fun b : bool => if b then False else True) false ->
   forall y : bool,
   false = y -> (fun b : bool => if b then False else True) y

Упрощение немного, что говорит True -> forall y : bool, false = y -> (if y then False else True).

Таким образом, это требует доказательства True, а затем некоторого логического y, который мы можем выбрать. Так что сделайте это.

Check eq_ind false (fun b : bool => if b then False else True) I true.
eq_ind false (fun b : bool => if b then False else True) I true
 : false = true -> (fun b : bool => if b then False else True) true

И вот мы: false = true -> False.

В сочетании с тем, что мы знаем о принципе индукции для False, мы имеем: если вы дадите мне доказательство false = true, я могу доказать любое предложение.

Итак, вернитесь к andb_true_elim1. Мы имеем гипотезу H, которая false = true. И мы хотим доказать какую-то цель. Как я показал выше, существует доказательство, которое превращает доказательства false = true в доказательства всего, что вы хотите. Поэтому, в частности, H является доказательством false = true, поэтому теперь вы можете доказать любую цель, которую вы хотите.

Тактика - это в основном техника, которая строит доказательство.

Ответ 2

true = false - это оператор, приравнивающий два разных булевых значения. Поскольку эти значения различны, это утверждение явно не доказуемо (в пустом контексте).

Учитывая ваше доказательство: вы попадаете на стадию, где цель false = true, так что вы не сможете это доказать... но дело в том, что ваш контекст (предположения) также противоречивы. Это часто случается, например, когда вы делаете анализ случаев, и один из случаев противоречит вашим другим предположениям.

Ответ 3

Я понимаю, что это старо, но я хочу прояснить некоторые интуиции за ответом Lambdageek (если кто-то найдет это)

Я заметил, что ключевым моментом является то, что мы определяем функцию F:bool->Prop с разными значениями в каждой точке (т.е. true => True и false => False). Однако из принципа индукции легко убедиться в равенстве eq_ind интуитивной идеи о том, что

forall A:Type, forall P:A->Prop, forall x y:A, (x=y) -> (P x = P y),

Но это тогда означало бы, что если true=false имеем true=false, но, поскольку мы знаем True, получаем False.

Это означает, что основное свойство, которое мы используем, это способность определять F, который задается принципом рекурсии для bool, bool_rect:

forall P:bool -> Type, P true -> P false -> (forall b:bool, P b)

установив P (b:bool) := b=>Prop, то это то же самое, что и

Prop -> Prop -> (forall b:bool, Prop),

где мы вводим True и False, чтобы получить нашу функцию F.