用 John Major 的平等重写

Question

John Major 的等式带有以下重写引理：

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可以证明吗？

如果没有：

将其假设为公理是否安全？
是否可以将其简化为更简单安全的公理？

Answer 1

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

如果A * A = B * B蕴含A = B，这意味着对类型构造函数是单射的。一般而言，类型构造函数的单射性（即对于所有类型）与经典逻辑和单价性不一致。对于某些类型构造函数，单射性是可证明的，但对于对而言则不是。

Is it safe to assume it as an axiom?

如果您使用经典逻辑或单价，则不是。否则，它可能是，但我会尝试改写问题，以便不会出现类型构造函数的内射性。

用 John Major 的平等重写

Rewriting with John Major's equality

coq

dependent-type