Если вы видите невозможную цель, есть две возможности: либо вы допустили ошибку в своей стратегии доказательства (возможно, ваша лемма неверна), либо гипотезы противоречат друг другу.
Если вы думаете, что гипотезы противоречат друг другу, вы можете установить цель 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.
На самом деле 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 определяется как индуктивный тип с нулевым регистром).
destruct F.
person
Gilles 'SO- stop being evil'
schedule
26.07.2011
