Закон Де Моргана для кванторов в Coq
Я пытаюсь доказать некоторые эквивалентности FOL. У меня возникли проблемы с использованием законов ДеМоргана для квантификаторов, в частности
~ (exists x. P(x)) <-> forall x. ~P(x)
Я попытался применить not_ex_all_not из Coq.Logic.Classical_Pred_Type. и просмотрел StackOverflow (Coq преобразовать несуществующий оператор в forall, Преобразовать ~exists в forall в гипотезе), но ни один из них не приблизился к решению проблемы.
Theorem t3: forall (T: Type), forall p q: T -> Prop, forall r: T -> T -> Prop,
~(exists (x: T), ((p x) /\ (exists (y: T), ((q y) /\ ~(r x y)))))
<-> forall (x y: T), ((p x) -> (((q y) -> (r x y)))).
Proof.
intros T p q r.
split.
- intros H.
apply not_ex_all_not.
Я получаю эту ошибку:
In environment
T : Type
p, q : T → Prop
r : T → T → Prop
H : ¬ (∃ x : T, p x ∧ (∃ y : T, q y ∧ ¬ r x y))
Unable to unify
"∀ (U : Type) (P : U → Prop), ¬ (∃ n : U, P n) → ∀ n : U, ¬ P n"
with "∀ x y : T, p x → q y → r x y".
Я ожидал, что закон ДеМоргана будет применен к цели, приводящей к отрицанию экзистенциального.
Ответы 1
Давайте посмотрим, что мы можем получить из H:
~ (exists x : T, p x /\ (exists y : T, q y /\ ~ r x y))
=> (not exists <-> forall not)
forall x : T, ~ (p x /\ (exists y : T, q y /\ ~ r x y))
=> (not (A and B) <-> A implies not B)
forall x : T, p x -> ~ (exists y : T, q y /\ ~ r x y)
=>
forall x : T, p x -> forall y : T, ~ (q y /\ ~ r x y)
=>
forall x : T, p x -> forall y : T, q y -> ~ (~ r x y)
В конце мы получаем двойное отрицание. Если вы не возражаете против использования классической аксиомы, мы можем применить NNPP, чтобы удалить ее, и все готово.
Вот эквивалентное доказательство Кока:
Require Import Classical.
(* I couldn't find this lemma in the stdlib, so here is a quick proof. *)
Lemma not_and_impl_not : forall P Q : Prop, ~ (P /\ Q) <-> (P -> ~ Q).
Proof. tauto. Qed.
Theorem t3: forall (T: Type), forall p q: T -> Prop, forall r: T -> T -> Prop,
~(exists (x: T), ((p x) /\ (exists (y: T), ((q y) /\ ~(r x y)))))
<-> forall (x y: T), ((p x) -> (((q y) -> (r x y)))).
Proof.
intros T p q r.
split.
- intros H x y Hp Hq.
apply not_ex_all_not with (n := x) in H.
apply (not_and_impl_not (p x)) in H; try assumption.
apply not_ex_all_not with (n := y) in H.
apply (not_and_impl_not (q y)) in H; try assumption.
apply NNPP in H. assumption.
Вышеизложенное было предварительным рассуждением. Если вы хотите вернуться назад (применяя леммы к цели вместо гипотез), все становится немного сложнее, потому что вам нужно построить точные формы, прежде чем вы сможете применить леммы к цели. Вот почему ваш apply терпит неудачу. Coq не находит автоматически, где и как применить лемму из коробки.
(А apply — тактика относительно низкого уровня. Есть являетсярасширенная функция Coq, что позволяет применить пропозициональную лемму к подтерминам.)
Require Import Classical.
Lemma not_and_impl_not : forall P Q : Prop, ~ (P /\ Q) <-> (P -> ~ Q).
Proof. tauto. Qed.
Theorem t3: forall (T: Type), forall p q: T -> Prop, forall r: T -> T -> Prop,
~(exists (x: T), ((p x) /\ (exists (y: T), ((q y) /\ ~(r x y)))))
<-> forall (x y: T), ((p x) -> (((q y) -> (r x y)))).
Proof.
intros T p q r.
split.
- intros H x y Hp Hq.
apply NNPP. revert dependent Hq. apply not_and_impl_not.
revert dependent y. apply not_ex_all_not.
revert dependent Hp. apply not_and_impl_not.
revert dependent x. apply not_ex_all_not. apply H.
На самом деле существует тактика автоматизации под названием firstorder, которая (как вы уже догадались) решает интуиционистскую логику первого порядка. Обратите внимание, что NNPP по-прежнему необходим, поскольку firstorder не поддерживает классическую логику.
Theorem t3: forall (T: Type), forall p q: T -> Prop, forall r: T -> T -> Prop,
~(exists (x: T), ((p x) /\ (exists (y: T), ((q y) /\ ~(r x y)))))
<-> forall (x y: T), ((p x) -> (((q y) -> (r x y)))).
Proof.
intros T p q r.
split.
- intros H x y Hp Hq. apply NNPP. firstorder.
- firstorder. Qed.