How does the discriminate tactic work?

Question

I was curious about how the discriminate tactic works behind the curtain. Therefore I did some experiments.

First a simple Inductive definition:

Inductive AB:=A|B.

Then a simple lemma which can be proved by the discriminate tactic:

Lemma l1: A=B -> False.
intro.
discriminate.
Defined.

Let's see what the proof looks like:

Print l1.

l1 = 
fun H : A = B =>
(fun H0 : False => False_ind False H0)
  (eq_ind A
     (fun e : AB => match e with
                    | A => True
                    | B => False
                    end) I B H)
     : A = B -> False

This looks rather complicated and I do not understand what is happening here. Therefore I tried to prove the same lemma more explicitly:

Lemma l2: A=B -> False.
apply (fun e:(A=B) => match e with end).
Defined.

Let's again see what Coq has made with this:

Print l2.

l2 = 
fun e : A = B =>
match
  e as e0 in (_ = a)
  return
    (match a as x return (A = x -> Type) with
     | A => fun _ : A = A => IDProp
     | B => fun _ : A = B => False
     end e0)
with
| eq_refl => idProp
end
     : A = B -> False

Now I am totally confused. This is still more complicated. Can anyone explain what is going on here?

Answer 1

Let's go over this l1 term and describe every part of it.

l1 : A = B -> False

l1 is an implication, hence by Curry-Howard correspondence it's an abstraction (function):

fun H : A = B =>

Now we need to construct the body of our abstraction, which must have type False. The discriminate tactic chooses to implement the body as an application f x, where f = fun H0 : False => False_ind False H0 and it's just a wrapper around the induction principle for False, which says that if you have a proof of False, you can get a proof of any proposition you want (False_ind : forall P : Prop, False -> P):

(fun H0 : False => False_ind False H0)
  (eq_ind A
     (fun e : AB => match e with
                    | A => True
                    | B => False
                    end) I B H)

If we perform one step of beta-reduction, we'll simplify the above into

False_ind False
          (eq_ind A
             (fun e : AB => match e with
                            | A => True
                            | B => False
                           end) I B H)

The first argument to False_ind is the type of the term we are building. If you were to prove A = B -> True, it would have been False_ind True (eq_ind A ...).

By the way, it's easy to see that we can simplify our body further - for False_ind to work it needs to be provided with a proof of False, but that's exactly what we are trying to construct here! Thus, we can get rid of False_ind completely, getting the following:

eq_ind A
  (fun e : AB => match e with
                 | A => True
                 | B => False
                 end) I B H

eq_ind is the induction principle for equality, saying that equals can be substituted for equals:

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

In other words, if one has a proof of P x, then for all y equal to x, P y holds.

Now, let's create step-by-step a proof of False using eq_ind (in the end we should obtain the eq_ind A (fun e : AB ...) term).

We start, of course, with eq_ind, then we apply it to some x - let's use A for that purpose. Next, we need the predicate P. One important thing to keep in mind while writing P down is that we must be able to prove P x. This goal is easy to achieve - we are going to use the True proposition, which has a trivial proof. Another thing to remember is the proposition we are trying to prove (False) - we should be returning it if the input parameter is not A. With all the above the predicate almost writes itself:

fun x : AB => match x with
              | A => True
              | B => False
              end

We have the first two arguments for eq_ind and we need three more: the proof for the branch where x is A, which is the proof of True, i.e. I. Some y, which will lead us to the proposition we want to get proof of, i.e. B, and a proof that A = B, which is called H at the very beginning of this answer. Stacking these upon each other we get

eq_ind A
       (fun x : AB => match x with
                  | A => True
                  | B => False
                  end)
       I
       B
       H

And this is exactly what discriminate gave us (modulo some wrapping).