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

**URL:** <https://discourse.rocq-prover.org/t/topic/2120>\
**Category:** \[zh\] Rocq 中文\
**Created:** [December 9, 2023, 10:40am UTC](https://discourse.rocq-prover.org/t/topic/2120 "2023-12-09T10:40:57Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![hhiim](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/hhiim/32/394_2.png) [@hhiim](https://discourse.rocq-prover.org/u/hhiim)\
**Post date:** [December 9, 2023, 10:40am UTC](https://discourse.rocq-prover.org/t/topic/2120/1 "2023-12-09T10:40:57Z")

</div>

```Coq
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` 会成功

```Coq
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(原式=新式).`，是很麻烦的……

---

<div class="post-metadata">

**Author:** ![Lys](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lys/32/48_2.png) [@Lys](https://discourse.rocq-prover.org/u/Lys)\
**Post date:** [December 10, 2023, 6:43pm UTC](https://discourse.rocq-prover.org/t/topic/2120/3 "2023-12-10T18:43:52Z")

</div>

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

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

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

```

---

<div class="post-metadata">

**Author:** ![hhiim](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/hhiim/32/394_2.png) [@hhiim](https://discourse.rocq-prover.org/u/hhiim)\
**Post date:** [December 11, 2023, 10:30am UTC](https://discourse.rocq-prover.org/t/topic/2120/4 "2023-12-11T10:30:04Z")

</div>

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