Доказательство контрпримером в Coq

После доказательства десятков лемм в исчислении высказываний и предикатов (некоторые более сложные, чем другие, но, как правило, все же доказуемые на intro-apply-destruct автопилоте), я наткнулся на одну, начинающуюся с ~forall, и тут же попался. Очевидно, мне не хватало понимания и знаний Coq. Итак, я прошу низкоуровневую технику Coq для доказательства утверждений общего вида

~forall A [B].., C -> D.  
exists A [B].., ~(C -> D).

На словах, я надеюсь на общий рецепт Coq для настройки и запуска контрпримеров. (Основная причина количественной оценки вышеперечисленных функций заключается в том, что это (или) примитивная связка в Coq.) Если вам нужны примеры, я предлагаю, например.

~forall P Q: Prop, P -> Q.
~forall P: Prop, P -> ~P.

Существует связанный вопрос, который не ставил и не отвечал на мой, поэтому я полагаю, что это не дубликат.


quantifiers coq negation proof
person jaam    schedule 01.03.2016    source источник

Ответы (1)


arrow_upward
5
arrow_downward

Напомним, что ~ P определяется как P -> False. Другими словами, чтобы показать такое утверждение, достаточно предположить P и получить противоречие. Важным моментом является то, что вам разрешено использовать P в качестве гипотезы любым удобным для вас способом. В частном случае универсально квантифицируемых утверждений может пригодиться тактика specialize. Эта тактика позволяет нам создать экземпляр универсальной количественной переменной с конкретным значением. Например,

Goal ~ forall P Q, P -> Q.
Proof.
  intros contra.
  specialize (contra True False). (* replace the hypothesis 
                                     by [True -> False] *)
  apply contra. (* At this point the goal becomes [True] *)
  trivial.
Qed.
person Arthur Azevedo De Amorim    schedule 01.03.2016
comment
Спасибо, specialize это было (также решил мою первоначальную проблему). Существуют ли другие, менее распространенные (чем intro, apply, destruct..) тактики, часто используемые в доказательствах контрпримерами? - person jaam; 01.03.2016
comment
Вам не нужен specialize в том смысле, что он делает что-то особенное, чего вы уже не могли сделать. В приведенном выше решении contra является функцией трех аргументов типа forall P Q, P->Q. Вы можете просто использовать его для создания значения, которое вы можете применить. Таким образом, в этом случае вы можете решить все это с помощью intro C; apply (C True False I). или даже (используя вывод типа Coq) intro C; apply (C _ _ I)., где I — конструктор для True. - person larsr; 02.03.2016
comment
@jaam базовый набор тактик, который поставляется с Coq, не очень ортогонален, и есть много тактик, которые могут быть полезны в доказательствах с помощью контрпримера, например contradiction, discriminate... Но обратите внимание, что в принципе вы можете решить все эти используя очень мало тактик. Как указал larsr, например, вы могли просто использовать apply. Вы также можете использовать assert для создания промежуточных результатов с помощью сценариев проверки, не создавая объект проверки вручную. - person Arthur Azevedo De Amorim; 02.03.2016
comment
Спасибо. Итак, ссылаясь на @larsr выше, с целью C : forall P Q : Prop, P -> Q ├ False, 1-й _ выводится из I, а второй из вывода False? - person jaam; 03.03.2016
comment
@jaam Когда я начал использовать Coq, я часто использовал exfalso, чтобы заставить текущую цель быть False, затем apply H, где H — это гипотеза формы ~ P, то есть P -> False. Он соответствует прямолинейному, традиционному стилю с защитой от обратного. Это не обязательно, но может быть легче следовать. - person anol; 07.03.2016