Как правило, когда вы анализируете кейс в программе проверки теорем, многие случаи сводятся к «не может быть». Например, если вы доказываете некоторый факт о целых числах, вам может потребоваться выполнить анализ случая того, является ли целое число 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 - «никогда не случится». Но вы не можете просто заявить о себе в Coq. На самом деле вы должны записать проверочный термин.
Итак, выше, вы должны доказать нелепую цель false = true. И единственное, с чем вам нужно работать - это гипотеза H: andb false c = true. Мгновенная мысль покажет вам, что на самом деле это абсурдная гипотеза (потому что andb false y сводится к ложному для любого 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, так что теперь вы можете доказать любую цель, какую пожелаете.
Тактика - это в основном механизм, который строит термин доказательства.