我想forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.
在 Coq 中证明或证伪。这是我的方法。
Inductive True2 : Prop :=
| One : True2
| Two : True2.
Lemma True_has_one : forall (t0 t1 : True), t0 = t1.
Proof.
intros.
destruct t0. destruct t1.
reflexivity.
Qed.
Lemma not_True2_has_one : (forall (t0 t1 : True2), t0 = t1) -> False.
Proof.
intros.
specialize (H One Two).
inversion H.
但是,inversion H
什么都不做。我想可能是因为 coq 的证明独立性(我不是以英语为母语的人,我不知道确切的单词,请原谅我的无知),并且 coq 无法证明 One = Two -> False。但如果是这样,为什么必须 coq 消除证明的内容?
没有上述命题,我就无法证明以下命题或它们的否定。
Lemma True_neq_True2 : True = True2 -> False.
Theorem iff_eq : forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.
所以我的问题是:
- 如何或有可能
forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.
在 Coq 中证明或证伪? - 为什么
inversion H
什么都不做;是不是因为 coq 的证明独立性,如果是这样,为什么 Coq 这样做会浪费精力。