Misc improvements to `head` and `tail` functions for lists

• Define head as notation that prints (Coq defines it as parsing only).
• Declare tail as simpl nomatch.
• Add lemmas about head and tail.

mentioned in merge request !278 (merged)

Define head l as notation for l !! 0 (we had no lemmas about head, so now we can use all the !! lemmas).

SearchAbout head will not show any of them, or will it?

Also head is not even our own notation, so this could be very confusing when composing with "standard Coq" code.

added 6 commits

• ca70af1d - 1 commit from branch master
• 220cd9d3 - Make sure `tail` is not `simpl`ed too much.
• 4d261250 - More properties of `last` function.
• 917fa796 - Define `head` as notation that also prints (Coq defines it as `parsing only`).
• aa3d33cc - Add lemmas for `head` similar to those for `tail`.
• 7122102b - CHANGELOG.

Compare with previous version

head turns out to be a weird thing in Coq: it's a parsing only notation for hd_error, see https://github.com/coq/coq/blob/master/theories/Lists/List.v#L3371. This is very confusing, because head prints back as hd_error.

Following @jung's comment in !277 (comment 69359), I now define head as a notation that prints (i.e., it's not parsing only). Also, I added a set of lemmas that's dual to the set of lemmas for last`.

What do you think @jung?

changed the description

added 11 commits

• 7122102b...34e363f0 - 4 commits from branch master
• cae78970 - Make sure `tail` is not `simpl`ed too much.
• e60abdf3 - More properties of `last` function.
• f3c4eb0a - Define `head` as notation that also prints (Coq defines it as `parsing only`).
• 40d86146 - Add lemmas for `head` similar to those for `tail`.
• 7d8bf699 - CHANGELOG.
• e1e8316a - Comment about `head` and `tail` notations.
• 195c8282 - Add tests for `simpl` on `last`.

Compare with previous version

resolved all threads

mentioned in commit b2a8bf65

merged