Hi,I am trying to figure out what the in-clause component of match expression effects.
Consider the following examples.
In briefly, why does we can use “in list (S n)” for matching v, even thought v is nil?

Inductive list :nat->Set :=
| nil :list 0
| cat: forall (n:nat),nat->list n->list (S n).
Notation "{| x , .. , y |}" :=
(cat _ x ..(cat _ y nil)..).
Check {| 1,2,3,4 |}.
Definition Head {n} (v :list (S n)) :=
match v in list (S n) return nat with
| nil => nil
| cat _ h _ => h
end.
(* We can't do this:
Compute Head nil.
But this is okay:
*)
Compute Head {|2,3,4|}.
Inductive Animal:= rabbit|other_animal.
(*
Notice that the part of "return nat" could be omited,
it seems that this branch could return any value of arbitrary type,
then we rewrite this head function as below.
*)
Definition OptionHead {n} (v :list n) :=
match v in list (S n) return nat with
| nil => rabbit
| cat _ h _ => h
end.
(*Why does this function just works?*)
Compute (OptionHead nil).
Compute (OptionHead {| 1,2,3,4 |} ).
Unset Printing Matching.
(*What is the type of the results of this function OptionHead?
What is the meaning of the symbol "[|-]"?
Where is the document for these symbols?
*)
Check OptionHead.

Actually, you cannot use in list (S n). Coq is just trying to be smart and turns it into something that makes a bit more sense. More precisely, in foo (S n) return bar n becomes

in foo n' return
match n' with
| O => _
| S n => bar n
end

Well, thanks for your answer, it made sense.
Could we say that the match expression is just a kind of type?
But it seems that there is a complicate rule for
such transformation, I am not sure if we could use this code reliably,
and be afraid that it may be an undocumented features which may no longer
works in future versions,since I found other tutorials do not use such simple
style,and are prone to use an idiom named “convoy pattern”.

For me,another strange thing in your explanation is that why and when the “_” could be inferred?
Maybe it just doesn’t matter,since it may be one of the heuristic algorithm COQ used.
We don’t need to know all the details,but still want to know if this is a well-defined behavior.
Is there any description about such things in the reference manual?
I had read the chapter 2.2.1 of the manual, but there are many unclear points in my view:

Expressions often contain redundant pieces of information. Subterms that can be automatically inferred by Coq can be
replaced by the symbol _ and Coq will guess the missing piece of information.

We need a definition of subterm,I guess that subterm is a term occur in another term,
and I assumed those terms should be satisfied to the grammar of term. I’m not sure.
And what’s more,it is not clear what are the missing piece of information,
I guess this information are the types of some terms.

2.2.2 Implicit arguments
An implicit argument of a function is an argument which can be inferred from contextual knowledge.
There are diﬀerent kinds of implicit arguments that can be considered implicit in
diﬀerent ways. There are also various commands to control the setting or the inference
of implicit arguments.

This paragraphs mentions that implicit arguments of a function is an argument
which can be inferred, but I could not clarify if the match construct is a function.
All of inference rules about symbol _ I found are related to implicit arguments,
after doing a search in the pdf doc.
I guess that they are different concepts but shares the similar rules,
but they are little obscured. I did not see any index about type inference
in the glossary table and need some helps to sort out these concepts.

Not just “kind of”. It is an actual type (assuming bar n is a type). In the setting of Coq, types are plain terms, so any construct can be used in a type, including match, fun, fix, and so on.

The “why” should be obvious, so perhaps I am misunderstanding your question. Since you did not provide this branch of the match to Coq, Coq has to infer it. As for the “when”, consider your example again:

Definition OptionHead {n} (v: list n) :=
match v in list n' return
match n' with
| O => _
| S n => nat
end
with
| nil => rabbit
| cat _ h _ => h
end.

Coq tries to unify the type match n' with O => _ | ... end with the type of each branch. For the nil => rabbit branch, nil is of type list O, so n' is O. Thus, the match n' reduces to just the underscore, which means that the underscore needs to be exactly the type of rabbit, that is, Animal. That is it.

Yes, subterms are just terms; the word “subterm” is just meant to convey the idea that they are possibly part of a larger term. As for the inference, Coq does not care whether it is a type, it just tries to infer the value of any term that is an underscore.

As for implicit arguments, Coq simply replaces them with underscores during parsing. (And conversely, it removes implicit arguments from the output when printing.) This is just syntax.