What is a Coq type system in this example?
I am confused about the behavior of a Coq type system in the overlapping part of the proof in the definition of h below:
Set Implicit Arguments.
Definition h := fun (a b : nat) (e : a = b) =>
(fun (x y : nat)(HC : b = y)(H : x = y) =>
(match H in (_ = y0) return (b = y0 -> b = x) with
| @eq_refl _ _ => fun HC0 : b = x => HC0
end HC)) a b (eq_refl b) e.
Checking h tells us that the generic type is "forall ab: nat, a = b → b = a".
Since the type of H is x = y, it looks like the match returns a member of type b = y -> b = x due to the return clause. After applying the various terms that follow, we get the expected type for h.
However, the fun HC0: b = x => HC0 is the identity function of the type b = x → b = x. I don't believe there is any coercion that would cause b = x -> b = x to be recognized as a type b = y -> b = x.
My best guess is that the constructor for H being @eq_refl nat x of type x = x is unique. Since H also has type x = y, the names x and y are associated with the same term. So the type system solves b = x → b = x is of type b = y → b = x. It's close? Is this behavior explained or documented somewhere? I looked at decreasing iota but I don't think it is correct.
source to share
That's pretty much it. This behavior is documented (look for "match ... with ... end construction" in this chapter of the manual ), although understanding what is going on is a little trickier.
First, remember how typical is match
noted in Coq:
Inductive list (T : Type) :=
| nil : list T
| cons : T -> list T -> list T.
Definition tail (T : Type) (l : list T) : list T :=
match l with
| nil => nil
| cons x l' => l'
end.
Coq checks (1) that each type constructor list
has a corresponding branch in match
and (2) that each branch is of the same type (in this case list T
), assuming that the constructor arguments entered in each branch are of the corresponding types (here, assuming which x
has a type T
and l'
has a type list T
in the second branch).
In such simple cases, the type used to check each branch is exactly the same as the type of the entire match expression. However, this is not always the case: sometimes Coq uses a more specialized type based on the information it pulls from the branch it checks out. This often happens when analyzing cases on indexed inductive types such as eq
:
Inductive eq (T : Type) (x : T) : T -> Prop :=
| eq_refl : eq T x x.
(Notation =
is just the syntactic syntax for eq
.)
Inductive type arguments given to the right of the colon are special in Coq: they are known as indices. The ones that appear on the left (in this case T
and x
) are known as parameters. The parameters must be different in the inductive type declaration and must exactly match those used in the result of all constructors. For example, consider the following illegal snippet:
Inductive eq' (T : Type) (x : T) : T -> Type :=
| eq_refl' : eq nat 4 3.
Coq rejects this example because it finds nat
instead T
in the result of the constructor eq_refl'
.
Indexes, on the other hand, do not have this limitation: the indexes that appear in the return type of constructors can be any expression of the corresponding type. In addition, this expression can differ depending on the constructor we are in. Because of this, Coq allows you to return the type of each branch based on the choice of the index of each branch. Consider the following slightly simplified version of your original example.
Definition h (a b : nat) (e : a = b) : b = a :=
match e in _ = x return x = a with
| eq_refl => eq_refl : a = a
end.
Since the second argument eq
is an index, it can in principle change depending on the constructor used. Since we only know what the index is when we look at the constructor used, Coq allows us to return a match type depending on that index: the in
match clause gives names to all indices of the inductive type, and these names become bind variables that can be used in the clause return
.
As you enter the branch, Coq finds out what the index values are and replaces those values for the variables declared in the sentence in
. This match only has one branch, and this branch causes the index to be equal to the second argument in the type e
(in this case a
). Thus, Coq tries to make sure that the type of this branch a = a
(i.e. x = a
, is a
replaced with x
). So we can just provide eq_refl : a = a
and we're done.
Now that Coq has verified that all branches are correct, it assigns the entire match expression to the clause type return
with the type index e
replaced by x
. This variable e
has a type a = b
, an index b
, and therefore a result type b = a
(i.e. x = a
from b
replaced to x
).
This answer provides more explanation of the difference between parameters and indices, if that helps.
source to share