用约翰·梅杰的同等重写

问题描述 投票:2回答:1

约翰·梅杰的平等带有以下重写的引理:

Check JMeq_ind_r.
(*
JMeq_ind_r
     : forall (A : Type) (x : A) (P : A -> Prop),
       P x -> forall y : A, JMeq y x -> P y
*)

很容易这样概括:

Lemma JMeq_ind2_r
     : forall (A:Type)(x:A)(P:forall C,C->Prop),
       P A x -> forall (B:Type)(y:B), @JMeq B y A x -> P B y.
Proof.
intros.
destruct H0.
assumption.
Qed.

但是我需要一些不同的东西:

Lemma JMeq_ind3_r
     : forall (A:Type)(x:A*A) (P:forall C,C*C->Prop),
       P A x -> forall (B:Type)(y:B*B), @JMeq (B*B) y (A*A) x -> P B y.
Proof.
intros.
Fail destruct H0.
Abort.

JMeq_ind3_r是否可证明?

如果不是:

  • 将其假定为公理是否安全?
  • 是否可以简化为更简单,更安全的公理?
coq dependent-type
1个回答
1
投票

这是不可证明的。 JMeq本质上是捆绑在一起的两个相等证明,一个用于类型,另一个用于值。在这种情况下,我们从A * A = B * B的假设中得出。由此无法证明A = B,因此我们无法将P A x转换为P B y

如果A * A = B * B暗含A * B,则表示对类型构造函数是单射的。通常(对于所有类型)类型构造函数的整体性与经典逻辑以及单义性不一致。对于某些类型的构造函数,可证明内射性,但对对则不可。

将其假定为公理是否安全?

如果您使用经典逻辑或单调逻辑,则不是。否则,可能是这样,但是我将尝试改述该问题,以使类型构造函数不可插入性出现。

© www.soinside.com 2019 - 2024. All rights reserved.