# 如何对含量词的命题进行代换操作？

``````Set Universe Polymorphism.
Require Import Coq.Unicode.Utf8_core.
(*假设我有一些公理……*)
Axiom 逻辑外延 :
forall P Q: Prop, (P<->Q)=(P=Q).

Axiom 排中 :
forall P : Prop, P \/ ~ P.

Lemma 双重否定 : forall P, (~ ~P) = P.
Proof.
intros.
rewrite <- 逻辑外延.
split. {
intros. pose proof (排中 P).
destruct H0. { auto. } { exfalso. auto. }
} {
intros. pose proof (排中 (~ P)).
destruct H0. { auto. } { auto. }
}
Qed.

(*假设我有一个目标*)
Theorem 目标 :(forall x:nat, ~(~(x = x)))=(forall x:nat, x = x) .
Proof.
intros.
(*尝试证明……*)
rewrite -> 双重否定.
Qed.
``````

``````Theorem 全称双否 :forall{A:Type}{P:A→Prop},
(forall x:A, ¬(¬(P x))) =
(forall x:A, (P x)).
Proof.
intros.
rewrite <- 逻辑外延.
firstorder. pose proof (排中 (P x)). firstorder.
Qed.

(*对于简单目标……*)
Theorem 简单目标 :(forall x:nat, ~(~(x = x)))=(forall x:nat, x = x) .
Proof.
intros.
(*证明成功！*)
rewrite -> 全称双否. auto.
Qed.

(*对于复杂目标……*)
Theorem 复杂目标 :(∀ x : Prop, ¬ ¬ x ∧ 1 = 1) = (∀ x : Prop, x ∧ 1 = 1).
Proof.
intros.
(*证明失败！*)
(*rewrite -> 全称双否. auto.*)

(*模式匹配失败是显然的，尝试定义更通用的引理！*)
Theorem 通用引理 :forall{A:Type}{P:A→Prop}{M:Prop→Prop},
(∀ x : A, M (¬ ¬ P x)) = (∀ x : A, M (P x)).
Proof.
intros.
rewrite <- 逻辑外延.
firstorder; pose proof (排中 (P x)). {
pose proof (H x). rewrite -> 双重否定 in H1. auto.
}{
pose proof (H x). rewrite -> 双重否定. auto.
}
Qed.

Theorem 二次尝试 :(∀ x : Prop, ¬ ¬ x ∧ 1 = 1) = (∀ x : Prop, x ∧ 1 = 1).
Proof.
intros.
(*证明依然失败！*)
rewrite -> 通用引理. auto.
``````

``````Theorem 复杂目标 :(∀ x : Prop, ¬ ¬ (x ∧ 1 = 1)) = (∀ x : Prop, x ∧ 1 = 1).
Proof.
intros.
rewrite -> 全称双否. auto.
Qed.
``````