Coq中量词的德摩根定律

Question

我试图证明一些for等效。我在使用demorgan的法律方面遇到困难，特别是

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

我尝试从coq.logic.classical_pred_type。和搜查stackoverflow应用于not_ex_all_not(coq convert to for forall语句，将〜转换为假设中的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".

我希望Demorgan定律适用于目标，从而导致否定的存在。

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是一种相对较低的战术。

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的自动化策略，该策略(如您所知(解决了一阶直觉逻辑。请注意，由于firstorder无法处理经典逻辑，因此仍然需要NNPP。

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.