如何或是否有可能证明或伪造`forall(PQ:Prop),(P - > Q) - >(Q - > P) - > P = Q.在Coq中？

Question

我想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.但是,如果是这样,为什么必须消除证据的内容？

没有上述命题,我无法证明以下或他们的否定.

Lemma True_neq_True2 : True = True2 -> False.

Theorem iff_eq : forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.

所以我的问题是:

1. 如何或可能forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.在Coq中证明或伪造？
2. 为什么inversion H没有; 这是因为coq的证明独立性,如果是这样,为什么Coq会浪费精力去做这件事.

Answer 1

1. 你提到的原则forall P Q : Prop, (P <-> Q) -> P = Q,通常被称为命题扩展性.这个原则在Coq的逻辑中是不可证明的,并且最初的逻辑被设计为可以作为公理添加而没有任何伤害.因此,在标准库(Coq.Logic.ClassicalFacts)中,人们可以找到关于这个原理的许多定理,将它与其他众所周知的经典推理逻辑原理联系起来.令人惊讶的是,最近发现Coq的逻辑与这个原则不相符,但是有一个非常微妙的原因.这被认为是一个错误,因为逻辑的设计使得这可以作为一个没有伤害的公理添加.他们想在新版本的Coq中修复这个问题,但我不知道它的当前状态是什么.从版本8.4开始,命题扩展性在Coq中是不一致的.

   在任何情况下,如果在将来的Coq版本中修复了这个错误,那么就不可能在Coq中证明或反驳这个原则.换句话说,Coq团队希望这个原则独立于Coq的逻辑.

2. inversion H因为关于证明的推理规则(类型为a的事物Prop)与推理非证明(类型为a的事物)的规则不同,所以没有做任何事情Type.您可能知道Coq中的证据只是条款.在引擎盖下,inversion基本上构建了以下术语:

   Definition true_not_false : true <> false :=
     fun H =>
       match H in _ = b
               return if b then True else False
       with
       | eq_refl => I
       end.
   

   如果您尝试对boolin 的版本执行相同操作Prop,则会收到更多信息:

   Inductive Pbool : Prop :=
   | Ptrue : Pbool
   | Pfalse : Pbool.
   
   Fail Definition Ptrue_not_Pfalse : Ptrue <> Pfalse :=
     fun H =>
       match H in _ = b
               return if b then True else False
       with
       | eq_refl => I
       end.
   
   (* The command has indeed failed with message: *)
   (* => Error: *)
   (*    Incorrect elimination of "b" in the inductive type "Pbool": *)
   (*    the return type has sort "Type" while it should be "Prop". *)
   (*    Elimination of an inductive object of sort Prop *)
   (*    is not allowed on a predicate in sort Type *)
   (*    because proofs can be eliminated only to build proofs. *)
   

   实际上,其中一个原因是Coq被设计为与另一个称为证明无关的原则兼容(我认为这就是"证明独立性"的意思).