EECS 755

Software Requirements Modeling and Analysis



As promised in class, I’ve created a yet another Coq project file Natlist.v that includes the natlist examples I did in class. Almost everything in the file is from Software Foundations, but I added a couple of things that Pierce does not talk about. One is the use of lemmas and the assert command and the other is a peek at using Ltac to simplify proofs. We will go over the rest of the module in class, but will likely not do much with Ltac right now. Just wanted to give you a taste of where we’re headed.