如何证明平等是不可能的

Question

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

（其中TApp是构造函数）

在伊德里斯这可以用\Refl => impossible证明，但我没有设法在Coq中写出任何证据。

有一种简单的方法可以证明吗？

Answer 1

你可以通过induction a.来证明这一点。这个想法是Tipe的归纳原理编码这样一个事实，即它的值在大小上是有限的，而TApp a b = a假设允许你构造一个无限值，但这些是你原始事实的某种间接后果，因此你需要工作有点儿。 Coq的扩展可以自动导出和使用这种发生检查的引理。