coq - 从 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(身份证明的唯一性)结果。 .