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
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
andreturn
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 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.
source to share