# 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.
intro.
discriminate.
Defined.
```

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).
Defined.
```

Let's take another look at what Coq did 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 completely confused. This is even more difficult. Can anyone explain what is going on here?

source to share

We go over this term `l1`

and describe each part of it.

```
l1 : A = B -> False
```

`l1`

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
```

`eq_ind`

- 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
end
```

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
end)
I
B
H
```

And this is exactly what he gave us `discriminate`

(modulo some packing).

source to share

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).
Defined.
```

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`

terms

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 ( https://coq.inria.fr/refman/Reference-Manual020.html ). 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
end.
```

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
end.
```

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 than`B`

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

source to share