More Exercises

This directory contains additional exercises.

The files below in the directory texts are Coq scripts with a lot of admitted theorems and/or lacking or incomplete definitions. You have just to replace some Admitted, Parameter, etc. with Coq code ended by Qed or Defined.

• classic_well_founded.v
• vectors.v

Please feel tree to add any additional lemma or auxiliary function if it helps. Please do not require libraries which contain axioms (like Classical, ClassicalChoice), unless explicitely suggested.

The files below in the directory solutions contain solutions to the exercises above.

• classic_well_founded.v
• vectors.v

Please feel free to suggest improvements on our propositions, and new interesting exercises.

Pierre Casteran