I found this one quite useful from the aspect of proving (I'm reading it half way): https://coq.inria.fr/tutorial-nahas

At the end of the article, there is a coq source code of the entire article for you to play with in CoqIDE or Proof General: https://mdnahas.github.io/doc/nahas_tutorial.v