Если вы видите невозможную цель, есть две возможности: либо вы допустили ошибку в своей стратегии доказательства (возможно, ваша лемма ошибочна), либо гипотезы противоречивы.
Если вы считаете, что гипотезыпротиворечиво, вы можете установить цель на False, чтобы немного усложнить ситуацию.elimtype False достигает этого.Часто вы доказываете False, доказывая предложение P и его отрицание ~P;Тактика absurd P выводит любую цель из P и ~P.Если есть конкретная гипотеза, которая является противоречивой, contradict H установит цель на ~H, или если гипотеза будет отрицанием ~A, тогда цель будет A (сильнее ~ ~A, но обычно более удобной),Если одна конкретная гипотеза явно противоречива, contradiction H или просто contradiction докажут какую-либо цель.
Существует множество тактик, включающих гипотезы индуктивных типов.Выяснение того, какой из них использовать, в основном зависит от опыта.Вот основные из них (но вы столкнетесь с случаями, которые здесь не рассматриваются в ближайшее время):
destruct просто разбивает гипотезу на несколько частей.Он теряет информацию о зависимостях и рекурсии.Типичным примером является destruct H, где H - это соединение H : A /\ B, которое разбивает H на две независимые гипотезы типов A и B;или дважды destruct H, где H - это дизъюнкция H : A \/ B, которая разбивает доказательство на две разные подпространства: одно с гипотезой A и одно с гипотезой B. case_eqаналогично destruct, но сохраняет связи, которые гипотеза имеет с другими гипотезами.Например, destruct n, где n : nat разбивает доказательство на два подкрепления, одно для n = 0 и одно для n = S m.Если n используется в других гипотезах (т. Е. У вас есть H : P n), вам может потребоваться помнить, что уничтоженный вами n - это то же самое, что n, использованное в этих гипотезах: case_eq n делает это.inversion выполняет анализ случая по типу гипотезы.Это особенно полезно, когда в типе гипотезы есть зависимости, которые destruct забудет.Обычно вы используете case_eq для гипотез в Set (где имеет место равенство) и inversion для гипотез в Prop (которые имеют очень зависимые типы).Тактика inversion оставляет много равных, и за ней часто следует subst для упрощения гипотез.Тактика inversion_clear - это простая альтернатива inversion; subst, но она теряет немного информации. induction означает, что вы собираетесь доказать цель по индукции (= рекурсия) по данной гипотезе.Например, induction n, где n : nat означает, что вы выполните целочисленную индукцию и докажете базовый случай (n заменен на 0) и индуктивный случай (n заменен на m+1).
Ваш пример настолько прост, что вы можете доказать его как «очевидный по анализу кейсов на a».
Lemma has2b2: forall a:three, a<>zero/\a<>one ->a=two.
Proof. destruct a; tauto. Qed.
Но давайте посмотрим на кейсы, сгенерированные destructтактика, т.е. только после intros; destruct a..(Случай, когда a равен one, является симметричным; последний случай, когда a равен two, очевиден по рефлексивности.)
H : zero <> zero /\ zero <> one
============================
zero = two
Цель выглядит невозможной.Мы можем сказать это Coq, и здесь он может обнаружить противоречие автоматически (zero=zero очевидно, а остальное - тавтология первого порядка, обработанная тактикой tauto).
elimtype False. tauto.
Inфакт tauto работает, даже если вы не начнете с того, что говорите Coq, чтобы он не беспокоился о цели, и написали tauto без elimtype False первым (IIRC это не делало в более старых версиях Coq).Вы можете увидеть, что делает Coq с тактикой tauto, написав info tauto.Coq скажет вам, какой сценарий доказательства генерирует тактика tauto.Это не очень легко понять, поэтому давайте посмотрим на ручное доказательство этого случая.Во-первых, давайте разделим гипотезу (которая является соединением) на две части.
destruct H as [H0 H1].
Теперь у нас есть две гипотезы, одна из которых zero <> zero.Это явно неверно, потому что это отрицание zero = zero, что совершенно верно.
contradiction H0. reflexivity.
Мы можем взглянуть еще более подробно на то, что делает тактика contradiction.(info contradiction покажет, что происходит под сценой, но опять же это не для новичков).Мы утверждаем, что цель верна, потому что гипотезы противоречивы, поэтому мы можем доказать что угодно.Итак, давайте установим промежуточную цель на False.
assert (F : False).
Запустите red in H0., чтобы увидеть, что zero <> zero действительно обозначение для ~(zero=zero), которое, в свою очередь, определяется как значение zero=zero -> False.Итак, False является выводом H0:
apply H0.
И теперь нам нужно доказать, что zero=zero, то есть
reflexivity.
Теперь мы доказали наше утверждениеFalse.Осталось доказать, что False подразумевает нашу цель.Ну, False подразумевает любую цель, это ее определение (False определяется как индуктивный тип с 0 регистром).
destruct F.