Coq 中量词的 DeMorgan 定律

Question

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

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

我尝试从 Coq.Logic.Classical_Pred_Type 应用 not_ex_all_not，并搜索 Whosebug (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 是一种相对 low-level 的策略。是 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 的自动化策略，它（如您所猜）解决了 first-order 直觉逻辑。请注意，仍然需要 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.

Coq 中量词的 DeMorgan 定律

DeMorgan's law for quantifiers in Coq

coq

quantifiers

first-order-logic

demorgans-law