Sometimes you just want to prove that nasty
~ T = U for some types
U. Well, while in general it is not decidable (nor provable), sometimes there is a relatively easy way to do it, when
U are not both infinite. In other words, either
U, or both of them should be finite.
Simple example: bool is not unit
The idea is simple: if types are equal, there exists a bijection between their elements. Let us prove a simple lemma
The proof was a piece of cake. Now to battle!
You remember, that
unit is a type, inhabited by only one element
f true and
f false are evaluated to
tt. There is not much choice here. However we know, that . By instantiating
false we get and . Since both and are equal, we deduce and , contradiction.
Here is a little diagram to help:
Now the code:
So, the key idea is to enumerate possible bijections. As at least one of sets is finite, you will eventually enumerate all the candidates, and when the sets are of different size, you will get contradictions because you will run out of distinct functions trying to enumerate all bijections.
Example: nat is not bool
Let us apply the same principle to prove
~ nat = bool.
We are going to use a bit of semicolons because otherwise the proof will become very repetitive. Basically where you see an exclamation mark we got 8 goals which contexts include:
z all range over . There will always be at least two of three boolean values equal to each other (which should follow from Dirichlet principle), which will feed us with nice contradiction to do a rewrite and inversion.
An interesting question (the answer to which I do not know) is whether we could automate it inside Coq somehow without writing plugins for it.