## Inequality

Last time we learned how to prove an equality without using `reflexivity`. On the other side of the coin, how do we prove inequality without `discriminate`?

Let’s start with a simple inequality: `1 <> 2`. What sort of proof term would `discriminate` generate?

Well, this wasn’t as simple as we might have hoped. After trimming it down a bit, it starts to become a little more digestible:

(We could in fact further reduce the term by η-reduction, but I’m not sure that enhances readability here).

Recall that the type `1 <> 2` is equivalent to `1 = 2 -> False`. It should be no suprise then that our proof term is a function taking a proof term of `1 = 2`, and constructing a term of type `False`.

The crux of our proof is the leading `eq_ind` function. This is the induction principle generated for `eq`. Let’s try to understand it by checking its type.

In english, this takes a dependent prop `P`, a proof of said proposition for term `x`, and finally a proof that `x = y`, before producing a proof of the proposition over `y`.

Hopefully this is intuitive. If `x` and `y` are equal, then they should be interchangeable. Informally, what is true of `x` should be true of `y` by substitution.

To prove then that `1` and `2` are unequal, we start with their assumed equality, then use `eq_ind` to construct a contradiction. We choose the dependent proposition `P` supplied to `eq_ind` such that `P` obviously holds for `1`, and obviously doesn’t for `2`. With this goal in mind, we reach the following definition:

Now we just give `P` to `eq_ind`, and fill in the other necessary arguments:

This method we used here can be generalized to any structural inequality. To prove `a <> b`, we would want to construct a similar `P` with a revised match statement

So long as `a` and `b` are structurally unequal, the match statment will take one to `True` and the other to `False`, setting the stage for our contradiction.

And so, we have reached the heart of the discriminate tactic. `discriminate` will construct such a dependent proposition, and use `eq_ind` to construct a contradiction Once it has proved `False`, it can prove any goal.

# Bonus: Proof (Ir)relevance

That’s it for the main topic, but for the interested reader, now is also a good time for a digression on Props and (in)equality.

While not directly derivable in Coq, many users decided to introduce the concept of proof irrelevance axiomatically:

That is, we permit any two proofs terms of some proposition to be considered equal.

Anytime you add an axiom to Coq, you must ensure that it is consistent. That is, that the axiom does not admit a proof of `False`.

Proof irrelevance would be inconsistent if we could come up with some `p1` and `p2` of a shared proposition which we could prove unequal, in direct contradiction with the axiom.

Thinking about what we just learned about inequalities, shouldn’t such a proof be rather trivial?

Consider the following silly `Prop`:

Why reinvent the wheel? Let’s just knock this out with `discriminate`:

Uh oh. Perhaps we were overconfident. Unfortunately `discriminate` doesn’t provide a very informative error message, so let’s just try building a manual proof like the one we did earlier.

Coq tells us that our elimination of `x` (our match term) is invalid, because a proof term (a term whose type has type `Prop`) cannot be eliminated to produce a term whose type has type `Type`.
What we have encountered is Coq’s elimination restriction on proof terms. Proof terms are only allowed to be eliminated to construct further proof terms. Therefore, we prevent information flow out of the `Prop` universe.
There are many reasons for this restriction, and in fact we should be thankful for it. Perhaps the most obvious is in terms of code extraction. Because the computational components of a Coq spec (the `Set` and `Type` sorted terms) are independent of proof terms, we can completely erase them during extraction!
The only information from `Prop`s that are allowed into `Type`s and `Set`s exist at the type-level. So once we confirm that our spec type-checks within Coq, we are safe to erase all proof terms in the extracted code.