用约翰·梅杰的等式重写

约翰·梅杰的等式带有以下重写引理：

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.

Is JMeq_ind3_r可证明吗？

If not:

• 将其视为公理是否安全？
• 它可以简化为更简单且安全的公理吗？

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

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

将其视为公理是否安全？

如果您使用经典逻辑或单价性，那么事实并非如此。否则，可能是这样，但我会尝试重新表述问题，以便类型构造函数单射性不会出现。