如何证明相等是不可能的

Question

1 subgoal
a, b : Tipe
H : TApp a b = a
______________________________________(1/1)
False

（其中 TApp 是构造函数）

在 Idris 中，这可以用 \Refl => impossible 证明，但我还没有设法在 Coq 中为它写任何证明。

有没有简单的证明方法？

Answer 1

您可以通过induction a. 证明这一点。这个想法是Tipe 的归纳原理编码了它的值大小是有限的这一事实，而TApp a b = a 假设允许您构造一个无限值，但这些都是您所拥有的原始事实的间接结果，因此你需要为此付出一些努力。扩展 Coq 以自动派生和使用此类发生检查引理肯定是可能的。