The Coq proof assistant

You can try some Coq code directly in your browser, here:
https://coq.vercel.app/wa/

You may also want to try another editor, CoqIDE. You can install it with the Coq Platform (link: https://github.com/coq/platform).

The Volume 1: Logical Foundations of the electronic textbook Software Foundations is a good book to start with. The authors of Volume 1 are: Benjamin C. Pierce and Arthur Azevedo de Amorim and Chris Casinghino and Marco Gaboardiand and Michael Greenberg and Cătălin Hriţcu and Vilhelm Sjöbergand and Brent Yorge.

With the modern set of tactics of Coq, one can achieve the same things with fewer tactics to know.
Link to the modified volume 1 (modified chapters currently include Preface up to More Basic Tactics) to work with the modern set of tactics:
http://158.39.201.94:80