I'm trying to write a function which removes the zeros from a list. Here is the first try of my implementation.
Require Import Nat.
Require Import List.
Fixpoint shrink (x : list nat) list nat := (* Mistake! Needs a : list nat *)
match x with
| nil => nil
| h :: t => if h =? 0 then shrink t else (h :: shrink t)
end.
However, I get this error:
Error:
In environment
shrink : forall (x : Datatypes.list Datatypes.nat)
(list0 : ?T) (nat : ?T0@{list:=list0}),
Datatypes.list ?T1@{x:=x; list:=list0; x1:=x}
x : list nat
list : ?T
nat : ?T0
h : Datatypes.nat
t : Datatypes.list Datatypes.nat
The term "shrink t" has type
"forall (list0 : ?T@{x:=t}) (nat : ?T0@{x:=t; list:=list0}),
Datatypes.list ?T1@{x:=t; list:=list0; x1:=t}"
while it is expected to have type "Datatypes.list ?T1@{x1:=h :: t}".
The correct function implementation is this:
Fixpoint shrink (x : list nat) : list nat :=
match x with
| nil => nil
| h :: t => if h =? 0 then shrink t else (h :: shrink t)
end.
But how am I supposed to interpret the error, in particular (list0 : ?T@{x:=t})? In particular,
list0 instead of list?? mean before the T?@{ ... } mean after the T?For your first point, this is just a printing thing but essentially local variables names are just hints for Coq and it may not respect them to avoid confusion. Here it's probably because of the list := list0 we see later.
Letters preceded by ? are existential variables or evars, used for unification. Here it doesn't know what the type of list0 should be because you did not give any, but it knows it has to be something. So for now it's ?T and it will try to figure out later what it should be by looking at its uses.
For nat it's the same, but it also knows it might depend on some list and in this case its value should be list0 so it does the instantiation ?T0{list:=list0}. This notation is for substitution in evars.
I invite you to look at the documentation of evars in the manual to know more.