Coq中量词的德摩根定律

Question

我正在尝试证明一些 FOL 等价性。我无法将德摩根定律用于量词，尤其是

~ (exists x. P(x)) <-> forall x. ~P(x)

我尝试从 Coq.Logic.Classical_Pred_Type. 应用 not_ex_all_not，并搜索 StackOverflow（Coq convert non exist to forall statement、Convert ~exists to forall in hypothesis），但都没有接近解决问题。

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".

我希望将德摩根定律应用于导致否定存在主义的目标。

Answer 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 来剥离它，我们就完成了。

这是等效的 Coq 证明：

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 是一种相对低级的策略。 an advanced Coq feature 允许将命题引理应用于子项。）

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.