Formalisation with the Coq proof assistant, SSReflect, Mathematical Components library
From now on you can follow the following link only:
We use the Coq proof assistant and follow (a modified version of) the
Volume 1: Logical Foundations of the electronic textbook Software Foundations.
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.
The modifications are mainly aimed at using the SSReflect set of tactics, which allows us to achieve the same things with fewer tactics to know.
Link to the modified volume 1 (modifiied chapters currently include Preface up to More Basic Tactics):
Link to try Coq code in your browser:
You may also want to try another editor, CoqIDE. You can install it with the Coq Platform (link: https://github.com/coq/platform).