How does discriminatory tactics work?

I was curious how this tactic works behind the curtain. So I did some experiments.

First, a simple inductive definition:

Inductive AB:=A|B.


Then a simple lemma that can be proved by tactics discriminate


Lemma l1: A=B -> False.


Let's see what this 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


It looks pretty complicated and I don't understand what's going on here. Therefore, I tried to more accurately prove the same lemma:

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


Let's take another look at what Coq did with this:

Print l2.

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


Now I am completely confused. This is even more difficult. Can anyone explain what is going on here?


source to share

2 answers

We go over this term l1

and describe each part of it.

l1 : A = B -> False



is an implication, therefore, in relation to Curry-Howard, this is an abstraction (function):

fun H : A = B =>


Now we need to build the body of our abstraction, which should be of a type False

. The tactic is discriminate

deciding to implement the body as an application f x

, where f = fun H0 : False => False_ind False H0

and this is just a wrapper around the induction principle for False

, which says that if you have proof False

, you can get proof of any sentence 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 do one step of beta reduction, we simplify it to

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


The first argument False_ind

is the type of term to create. If you had to prove it A = B -> True

, it would be False_ind True (eq_ind A ...)


By the way, it's easy to see that we can simplify our body further - in order False_ind

to work it needs to be equipped with a proof False

, but that's exactly what we're trying to build here! Thus, we can get rid of completely by False_ind

getting the following:

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



- the principle of induction for equality, saying that equalities can be replaced by equal:

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


In other words, if we have a proof P x

, then for all y

equal x

, it is satisfied P y


Now let's create a proof step by step False

with eq_ind

(we should get a member at the end eq_ind A (fun e : AB ...)


Let's start, of course, with eq_ind

, then we'll apply it to some x

- let's say for this A

. Next, we need a predicate P

. One important thing to keep in mind when writing P

down is that we need to be able to prove it P x

. This goal is easy to achieve - we will use a proposition True

that has a trivial proof. Another thing to remember is the sentence we're trying to prove ( False

) - we have to return it if the input is not A

. With all this, the predicate almost writes itself:

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


We have the first two arguments for eq_ind

, and we need three more: the proof for the branch, where x

- A

, which is the proof True

, i.e. I

... Some y

that will lead us to the offer we want to receive, i.e. B

, and proof of that A = B

, which is called at the beginning of this answer H

. By stacking them on top of each other we get

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


And this is exactly what he gave us discriminate

(modulo some packing).



Another answer focuses on the discriminatory part, I will focus on the manual proof. You tried:

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


What should be noted, and makes me often uncomfortable to use Coq, is that Coq accepts mis-defined definitions, which it internally rewrites into well-typed terms. This allows it to be less verbose as Coq adds some parts. But on the other hand, Coq is manipulating a different term than the one we introduced.

This applies to your proof. Naturally, pattern matching e

should not include a constructor eq_refl

that is the only constructor for the type eq

. This is where Coq discovers that equality is not populated and thus understands how to change its code, but what you entered does not match the correct pattern.

Two ingredients can help you understand what is happening here:

  • definition eq

  • full syntax for pattern matching, with as

    , in

    and return


First, we can take a look at the definition eq


Inductive eq {A : Type} (x : A) : A -> Prop :=  eq_refl : x = x.


Note that this definition differs from what seems more natural (more symmetrical anyway).

Inductive eq {A : Type} : A -> A -> Prop :=  eq_refl : forall (x:A), x = x.


It really matters what eq

is defined by the first definition, not the second. In particular, for our task it is important that the x = y

parameter x

is a parameter, and y

is an index. That is, it x

is constant in all constructors, or it y

can be different in each constructor. You have the same difference with type Vector.t

. The type of the elements of the vector will not change if you add an element, so it is implemented as a parameter. Its size, however, can change, so it is implemented as an index.

Now let's take a look at the advanced pattern matching syntax. I am giving here a very brief explanation of what I understood. Feel free to look at the link for more secure information ( ). The proposal return

can specify a return type that will be different for each branch. This clause can use variables defined in clauses as

and in

pattern matches that bind the matched term and type indices, respectively. The suggestion return

will be interpreted in the context of each branch, replacing the variables as

and in

using that context to check out the branches one by one and be used for input match

from an external point of view.

Here's a contrived example with a suggestion as


Definition test n :=
  match n as n0 return (match n0 with | 0 => nat | S _ => bool end) with
  | 0 => 17
  | _ => true


Depending on the value, n

we don't return the same type. The type test

is forall n : nat, match n with | 0 => nat | S _ => bool end

. But when Coq can decide in which case we can match, it simplifies the type. For example:

Definition test2 n : bool := test (S n).


Coq here knows that all that is n

, S n

given test

, will look like something like bool


For equality, we can do something similar, this time using a sentence in


Definition test3 (e:A=B) : False :=
  match e in (_ = c) return (match c with | B => False | _ => True end) with
  | eq_refl => I


What's going on here? Essentially, the Coq type checks the match

and branches separately match

. In the only branch eq_refl

, c

equals A

(due to the definition eq_refl

that instantiates the index with the same value as the parameter), so we stated that we returned some type value True

, here I

. But from an external point of view, c

equals B

(because it e

has a type A=B

), and this time the clause return

claims to match

return some value type False

. We are using the Coq feature here to make it easier to match patterns in the types we just saw with test2

. Please note that we have used True

in other cases thanB

, but in particular we do not need True

. We only need some kind of residential type, so we can return something to the branches eq_refl


Coming back to the weird term Coq creates, the method used by Coq does something similar, but in this example it is certainly more complicated. In particular, Coq often uses IDProp

populated types IDProp

when it needs useless types and terms. They correspond to True

and I

used just above.

Finally, I provide a discussion link on coq-club which really helped me understand how advanced pattern matching is introduced into Coq.



All Articles