A good resource to learn Coq is "Software Foundation": https://www.cis.upenn.edu/~bcpierce/sf/current/index.html https://www.cis.upenn.edu/~bcpierce/sf/curren

A good resource to learn Coq is "Software Foundation": https://www.cis.upenn.edu/~bcpierce/sf/current/index.html https://www.cis.upenn.edu/~bcpierce/sf/current/index.html It teaches the foundation of software with simply typed lambda calculus, but also teaches how to use coq and use it for software verification. I found it more approachable than Coq'Art, which is also very good but I'd suggest starting with SF first then read Coq'Art.