Joonazan
Joonazan

Reputation: 1416

How to prove equality impossible

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

Answers (1)

Li-yao Xia
Li-yao Xia

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

Related Questions