Ответ 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, поэтому теперь вы можете доказать любую цель, которую вы хотите.
Тактика - это в основном техника, которая строит доказательство.