Add chapter to outline the difference between coercion mechanism and mechanism of canonical structures

[andreykl]

I think a (sub)chapter about differences between coercions and canonical structures might be added somewhere after Chapter 6.3.

I think content may be built on 1-2 examples of coercions from the book (so, repeating) and 1-2 examples of Cannonical Structures from the book (again, repeating). So, examples are well known to reader and one can rather easily lean them a bit better when see outlined difference between them.

Coercion mechanism is described in Chapter 5.5 (Notational aspects of specifications, page 112).
The Canonical Structure language is introduced In Chapter 6.3 (Records as relations, page 121).

I think good place might be Chapter 6.9 (so, current 6.9 will become 6.10, etc) or Chapter 6.10 or Chapter 6.11.

Below is discussion https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/reading.20ssreflect.20related.20books/near/243306458
Andrey Klaus: Here we have code for tnth https://math-comp.github.io/mcb/snippets/ch7_4.html (line 42).
I would like to put next string on line 44 (so, right after tnth definition): Eval compute in tnth ([:: 1; 2; 3]) 1.
After reading the book I had an impression that this should just work (it is possible it is wrong impression).
Question: should Eval compute in tnth ([:: 1; 2; 3]) 1. work and if yes - how to make it work?
Enrico Tassi: No, you have to write something like

Eval compute in tnth (@Tuple 3 nat [:: 1; 2; 3] isT) (@Ordinal 3 1 isT).

I see why you thought so, but the automatic "enrichment" works if something is already a tuple, and is projected down to a sequence in order to apply a sequence operation. Here [:: 1;2;3] is a sequence, plain and simple. One needs to wrap it into a constructor and prove a property a bout the length, that in this case is trivial (isT proves "true = true"). Ditto for the ordinal, 1 is a nat, you have to prove first that is is smaller than 3 in order to use it with tnth.

Said that, tuples are useful mostly to reason about abstract sequences with an invariant on the length. Not on concrete ones.
If you feel like the book should be improved to clarify all that, please open an issue on github.
Also, it may be worth putting this example in the jscoq code snippet as well.
Andrey Klaus: Thank you. I see in general that i didnt understand this part.. but in a bit more details, if you have a minute, shouldn't the problem like Tuple _ _ ~ seq nat arise when I write tnth _ [::1;2;3]?
Enrico Tassi: Yes, precisely the type error comes from tuple_of _ _ =?= seq nat. This does not fall in the domain of Canonical Structures (e.g. there is no projection involved, in particular no occurrence of tval). It could be covered by Coercions, but at the time of writing the elaborator of Coq is too limited. I mean, the term [:: 1;2;3] has type seq nat but is expected to have type tuple_of _ _: one could apply this "cast" code @Tuple _ _ <here> isT every time this problem pops up, and elaborate [:: 1;2;3] into @Tuple _ _ [:: 1;2;3] isT which has the expected type tuple_of _ _ (and infer the _ running type inference again).
Today you can't declare a coercion like that
Emilio Jesús Gallego Arias: I think today you can use some of the notations, that is Eval compute in tnth [tuple 1; 2; 3] (sub_ord 1).

Related issue #126