Software Foundations Ch. 1 Coq exercises (Basics)

Let's read the Preface and the first chapter, Basics: Functional Programming in Coq, of Software Foundations (https://www.cis.upenn.edu/~bcpierce/sf/current/index.html) and do the exercises, then get together to discuss some of the solutions.

The Coq proof assistant is central to the whole ecosystem for verified software that is being developed under the Deep Specification initiative. Software Foundations is an online text in principles of verified software from a type theoretic point of view, emphasizing hands-on work with Coq.

VM image referenced below seems to be working fine. As noted further below, it actually turns out to have Coq 8.4, which is the version recommended for Software Foundations.