0

我试图证明一些 FOL 等价。我在使用德摩根定律作为量词时遇到了麻烦，特别是

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

我尝试从 Coq.Logic.Classical_Pred_Type. 应用 not_ex_all_not，并搜索 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".

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

4

1 回答 1

3

让我们观察一下我们可以从中得出什么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是一种相对低级的策略。有一个 高级 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.
于 2019-07-05T00:32:58.683 回答