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

[zh] Coq 中文
1 
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.

这种情况很普遍，常常需要化简假设的逻辑，假设可能是带量词的
当然，可以定义一个带量词的引理，这样 rewrite 会成功

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.*)
Admitted.

(*模式匹配失败是显然的，尝试定义更通用的引理！*)
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.
Admitted.

可以看到对于表达式嵌套的情况似乎是无力的
当然我们可以用 assert 创建新假设，在新的上下文中把将量词 intros 掉
但每次都写 assert(原式=新式).，是很麻烦的……

3

请在x ∧ 1 = 1外加括号：

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

对不起，可能提问的时候有一点误导，命题是(¬ ¬ x )∧ (1 = 1)，
棘手的是要代换的部分（双重否定）不是最外层表达式