# 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?

+3

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

+4

source

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.

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

+4

source

All Articles