A Formal Study of Moessner's Sieve
Final monograph also available at: http://ebooks.au.dk/index.php/aul/catalog/book/213
- Download the 3rd party library paco, located at: http://plv.mpi-sws.org/paco/paco-1.2.7.zip More info about the project can be found at: http://plv.mpi-sws.org/paco/
- Unzip the paco project and run 'make install' in the 'src' folder of the project. This will install 'paco' in the Coq installation directory such that it can be 'Required' like any other standard library module.
- Now run 'make install' in the 'src' folder of the Moessner project in order to compile all Coq scripts.
- The code base of the Moessner project is now ready to be explored and stepped through.
Below we list the Coq scripts which accompany each of the different chapters.
Chapter 4 (lists and streams):
Chapter 5 (A dual to Moessner's sieve):
Chapter 6 (Pascals' triangle and the binomial coefficient):
Chapter 7 (A characteristic function of Moessner's sieve):
Chapter 8 (Proving Moessner's theorem):
Chapter 9 (A grid of triangles):
Chapter 10 (Proving Long's theorem):
Chapter 11 (Deriving Moessner's sieve from Horner's method):