从a到b，然后b到a的铸造是身份？

Question

给出定义：

Definition cast (a b:Type) (p:a = b) (x:a) : b :=
    match p with
    | eq_refl _  => x
    end.

我希望可以证明以下引理：

Lemma cast_cast_is_id : forall (a b:Type) (x:a) (p:a = b) (q:b = a),
    cast b a q (cast a b p x) = x.

但是，我似乎无法对此进行证明。我可以成功销毁p，但此后无法销毁q。似乎用eq_sym p而不是任意q代替引理的陈述对我似乎没有帮助。

[我担心我不知不觉中偶然发现了HoTT的一些细微之处。

任何人都可以证明这个引理，或者如果没有进一步的公理，它是不可证明的吗？

Answer 1

我不确定，但是在我看来，您要证明的内容与forall a (p:a=a), p = eq_refl没什么不同。如果是这样，您将无法在Coq中证明这一点，除非您对a有所了解，例如可判定的相等性。在这种情况下，您可以使用standard library中UIP（身份证明的唯一性）上的结果。