Reputation: 1416
1 subgoal
a, b : Tipe
H : TApp a b = a
______________________________________(1/1)
False
(where TApp is a constructor)
In Idris this can be proved with \Refl => impossible
but I haven't managed to write any proof for it in Coq.
Is there an easy way to prove it?
Upvotes: 1
Views: 184
Reputation: 33389
You can prove it by induction a.
. The idea is that the induction principle for Tipe
encodes the fact that its values are finite in size, while the TApp a b = a
assumption allows you to construct an infinite value, but these are somewhat indirect consequences from the raw facts you have, hence you need to work a bit for it. An extension of Coq to derive and use such occurs-check lemmas automatically would definitely be possible.
Upvotes: 3