Documentation of structure of generated Coq proof statements
Gappa seems to create contradiction proofs with not always obvious proof statement. Also cause of the notations used it is not always easy to see what the actual proof statement is, especially in complex cases. A few thoughts on this:
- it would be worthwhile to document at least in a few lines what the struct of the generated proofs is and to give an example on how to work with these
- it might make sense to define the used notations as
only parsing
so that the proof statements are more easily visible - it might make sense to add a final lemma which has a proof statement which is closer and more explicitly (without notations or with using only notations as defined in the gappa script) related to the statement in the gappa script.