Coq Equality II

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?

Lemma neq_1_2 : 1 <> 2.
Proof.
  discriminate.
Defined.
Print neq_1_2.

(* neq_1_2 =
   fun H : 1 = 2 =>
   let H0 : False :=
     eq_ind 1
	   (fun e : nat =>
        match e with
        | 0 => False
        | S n => match n with
                 | 0 => True
                 | S _ => False
                 end
        end) I 2 H in
   False_ind False H0
        : 1 <> 2
 *)

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:

Check ((fun H: 1 = 2 =>
  eq_ind 1 (fun x =>
    match x with
    | 1 => True
    | _ => False
    end
  ) I 2 H) : 1 <> 2
).

(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.

Check eq_ind.
(* eq_ind
	 : forall (A : Type) (x : A) (P : A -> Prop),
       P x -> forall y : A, x = y -> P y
 *)

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:

Definition P := fun x =>
  match x with
  | 1 => True
  | _ => False
  end.

Compute (P 1).
(* = True : Prop *)

Compute (P 2).
(* = False : Prop *)

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

Check ((fun H: 1 = 2 => eq_ind 1 P I 2 H) : 1 <> 2).

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

Definition P := fun x =>
  match x with
  | a => True
  | _ => False
  end.

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:

Axiom proof_irrelevance: forall (P: Prop) (p1 p2: P), p1 = p2.

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:

Inductive foo : Prop :=
  | bar : foo
  | baz : foo.

Goal bar <> baz.

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

Fail discriminate.

(* The command has indeed failed with message:
   Not a discriminable equality.
 *)

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.

Fail Definition P' := fun x =>
  match x with
  | bar => True
  | baz => False
  end.

(* The command has indeed failed with message:
   Incorrect elimination of "x" in the inductive type "foo":
   the return type has sort "Type" while it should be "SProp" or "Prop".
   Elimination of an inductive object of sort Prop
   is not allowed on a predicate in sort Type
   because proofs can be eliminated only to build proofs.
 *)

Failure again! At least this error message is more informative…

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 Props that are allowed into Types and Sets 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.

It also means that we can’t prove an inequality on proof terms, even when it seems obvious by structural differences.

Next up in our series, we deal with rewriting.