Structure Guidelines

Directory structure

The directory structure of theories is organized as follows

• ProblemClass
  • ProblemFamily.v, ProblemFamily_undec.v
  • Reductions
    • ForeignProblem_to_Problem.v
    • HaltTM_1_chain_Problem.v
  • Util, Misc, Shared, ...

In the above

• ProblemClass is a general class of Problems
• ProblemFamily.v contains a cohesive (overlapping preliminaries) family of decision problems (Coq predicates) in ProblemClass
  • ProblemFamily.v should be a minimalistic, possibly self-contained problem specification, suitable for modular reuse
  • ProblemFamily.v should be well-documented via comments and feasible to understand with minimal Coq knowledge
  • ProblemFamily.v should not contains any reasoning, dependencies to undecidability results etc.
• ProblemFamily_undec.v contains exactly the proofs of Theorem Problem_undec : undecidable Problem. for each Problem defined in ProblemFamily.v
  • ProblemFamily_undec.v should contain only high-level reasoning (transitive application of reduction steps)
  • ProblemFamily_undec.v should be documented via comments and feasible to understand with a basic Coq knowledge
  • ProblemFamily_undec.v should not contains auxiliary lemmas
• Reductions contains relevant reductions to problems in ProblemClass
  • ForeignProblem_to_Problem.v contains the main argument to reduce ForeignProblem to Problem in ProblemClass
    • ForeignProblem_to_Problem.v should (if possible) contain Theorem reduction : ForeignProblem ⪯ Problem.
    • ForeignProblem_to_Problem.v may encapsulate all other lemmas and theorems necessary for reduction in a Module
    • ForeignProblem_to_Problem.v should not contain proofs of ForeignProblem' ⪯ Problem' where either ForeignProblem' differs from ForeignProblem or Problem' differs from Problem
    • ForeignProblem_to_Problem.v should (if possible) not depend on any other ForeignProblem'_to_Problem'.v for parallel compilation of atomic reduction steps
  • HaltTM_1_chain_Problem.v is optional and contains the conjunction of reduction steps from Turing machine halting HaltTM 1 to Problem
    • HaltTM_1_chain_Problem.v should (if possible) contain Theorem HaltTM_1_chain_Problem : HaltTM 1 ⪯ Problem_1 /\ ... /\ Problem_n ⪯ Problem.
    • HaltTM_1_chain_Problem.v should be documented via comments and feasible to understand with a basic Coq knowledge
    • HaltTM_1_chain_Problem.v should not contains auxiliary lemmas
    • HaltTM_1_chain_Problem.v should not used in other arguments (it should be a compilation leaf)
    • HaltTM_1_chain_Problem.v should be used for presentations, publications, code review, etc.
• Util, Misc, Shared, etc. contain auxiliary lemmas used for proofs in ProblemClass to keep the top-level of ProblemClass clean
• Intermediate files should not depend on ProblemFamily_undec.v files (otherwise, this could pollute the overall context)

Design principles

• Modularity: ProblemClass should not contain proofs regarding inherent properties of OtherProblemClass that could as well be proven in OtherProblemClass.
• Specification surveyability: ProblemFamily.v is intended to be surveyed by mathematicians with little effort. This should not be obstructed by ltac hacks, interspersed lemmas, dependencies, etc.
• Result surveyability: ProblemFamily_undec.v is intended to be surveyed by mathematicians with little effort. Same design guidelines as for ProblemFamily.v apply. This is also true for HaltTM_1_chain_Problem.v.
• Name uniformity: Names of important files and theorems should be easy to guess. For example, a file showing HaltTM 1 ⪯ Problem should neither be called Halt_Prob.v, HALTTM_Problem.v, nor HALTTM_1_Problem.v. The preferred name would be HaltTM_1_to_Problem.v.
• Opt-in notations: Notations (also coercions, typeclasses, hints) should not be exposed at the top level of specification. A good practice (cf. Coq List containing ListNotations) is to encapsulate notations (also coercions, typeclasses, hints) in a Module. Adding hints to core is discouraged in favor of specialized hint databases.

Other suggestions

• Fast Interfaces: Whenever using Section for code structure, also use Set Default Proof Using "Type". to ensure fast interface file (vos) compilation. Avoid too many Let definitions in a Section for compact interfaces.

• Structured Proofs: Use Set Default Goal Selector "!". to ensure precise goal selection and improve maintainability.
• Principled Naming: Avoid referring to automatically generated names (e.g. from inversion). Such names often break code between Coq version changes. A good guideline is compatibility with Set Mangle Names..
• Regarding Anti-Patterns: For stable code, it is recommended to have a look at Anti-patterns and avoid them when possible.