Move "classic" Prosa to rt.classic namespace and update documentation

As a first step towards completing #53 (closed) and #54 (closed), this MR moves the "old" Prosa to the rt.classic namespace and updates the documentation to reflect the "modern" Prosa.

doc/guidelines.md

@@ -15,7 +15,7 @@ This project targets Coq *non*-experts. Accordingly, great emphasis is placed on
 5. **Keep it simple.** Shy away from advanced Coq techniques. At the very least, the spec and all lemma/theorem claims should be readable and understandable with a basic understanding of Coq (proofs are not expected to be readable).
 
 
-## Specific Advice
+## Readability Advice
 
 - Use many, mostly short sections. Sections are a great way to structure code and to guide the reader; they serve the reader by establishing a local scope that is easier to remember.
 
@@ -23,14 +23,6 @@ This project targets Coq *non*-experts. Accordingly, great emphasis is placed on
 
 - Make extensive use of the `Hypothesis` feature. Hypotheses are very readable and are accessible even to non-Coq users, especially when paired with self-explanatory names.
 
-- For consistency, start the name of hypotheses with `H_`.
-
-- Make proofs "step-able." This means preferring `.` over `;` (within reason). This makes it easier for novices to learn from existing proofs.
-
-- Making proofs as concise as possible is a *non-goal*. We are **not** playing [code golf](https://en.wikipedia.org/wiki/Code_golf).
-
-- Document the tactics that you use in the [list of tactics](doc/tactics.md). For new users, it can be quite difficult to identify the right tactics to use. This list ist intended to give novices a starting to point in the search for the "right" tools.
-
 - Consider renaming general concepts with `let` bindings to introduce local names that are more meaningful. In many cases, this is also useful to bind necessary context to local names. For example:
 ```
     Let no_deadline_is_missed :=
@@ -49,28 +41,73 @@ This project targets Coq *non*-experts. Accordingly, great emphasis is placed on
 - Document the sources of lemmas and theorems in the comments. For example, say something like "Theorem XXX in (Foo & Bar, 2007)", and document at the beginning of the file what "(Foo & Bar, 2007)" refers to.
 
 
+## Naming Conventions
+
+1. For consistency, start the name of hypotheses with `H_`.
+
+- For case a case analysis of `foo`, use `foo_cases` as the lemma name.
+
+- For a basic lemma that is intended as a rewriting rule to avoid unfolding a definition `foo` directly, use `foo_def` as the lemma name.
+
+- Consistently name predicates that express that something "is valid" (i.e., satisfies basic assumptions) as `valid_*` or `respects_*`.  
+Examples: `valid_schedule`, `taskset_respects_sporadic_task_model`. 
+
+- Consistently name sections that define what it means to be valid w.r.t. to some concept `Foo` as `ValidFoo`.  
+Examples: `ValidSchedule`,  `ValidTask`, `ValidJobOfTask`, `ValidJobsOfTask`.
+
+- Job parameters are always prefixed with `job_`.  
+Examples: `job_cost`, `job_arrival`, `job_deadline`. 
+
+- Task parameters are always prefixed with `task_`.  
+Examples: `task_cost`, `task_deadline`. 
+
+- We do not follow ssreflects naming scheme. 
+
+
+## Coq Features
+
+- We use type classes sparingly. Primarily, type classes are used to introduce new job and task parameters. 
+
+- We rely heavily on type inference. Top-level definitions do *not* require type annotations if the semantics are clear from context and Coq can figure out the specific types.
+
+- We tend to not use a lot of custom syntax/notation. Heavy use of custom syntax reduces readability because readers are forced to remember all local syntax definitions. 
+
+- We rely heavily on ssreflect notation.
+
+
 ## Writing Proofs
 
-- Keep proofs short. Aim for just a few lines, and definitely not more than 30-40. Long arguments should be structured into many individual lemmas (in their own section) that correspond to high-level proof steps. Some exceptions may be needed, but such cases should truly remain *exceptional*.  
+When writing new proofs, please adhere to the following rules.
+
+### Structure
+
+1. Keep proofs short. Aim for just a few lines, and definitely not more than 30-40. Long arguments should be structured into many individual lemmas (in their own section) that correspond to high-level proof steps. Some exceptions may be needed, but such cases should truly remain *exceptional*.  
 Note: We employ an automatic proof-length checker that runs as part of continuous integration to enforce this.
 
+- However, making proofs as concise as possible is a *non-goal*. We are **not** playing [code golf](https://en.wikipedia.org/wiki/Code_golf). If a proof is too long, the right answer is usually **not** to maximally compress it; rather, one should identify semantically meaningful steps that can be factored out and documented as local  "helper" lemmas. Many small steps are good for readability.
+
 - Make use of the structured sub-proofs feature (i.e., indentation with `{` and `}`, or bulleted sub-proofs with `-`, `+`, `*`) to structure code.
 
-- Generally try to make proofs as robust to (minor) changes in definitions as possible. Longterm maintenance is a major concern.
+- Make proofs "step-able." This means preferring `.` over `;` (within reason). This makes it easier for novices to learn from existing proofs.
+
 
-- Make use of the `by` syntax to stop the proof script early in case of any changes in assumptions.
+### Maintainability
 
-- General principle: Rewrite with equalities, do not rely on definitions.
+Generally try to make proofs as robust to (minor) changes in definitions as possible. Longterm maintenance is a major concern.
 
-- Avoid unfolding definitions in anything but “basic facts” files. Main proofs should not unfold low-level definitions, processor models, etc. Rather, they should rely exclusively on basic facts so that we can change representations without breaking high-level proofs.
+1. Make use of the `by` tactical to stop the proof script early in case of any changes in assumptions.
 
-- In particular, for case analysis, prefer basic facts that express all possible cases as a disjunction. Do not destruct the actual definitions directly.
+- General principle: **Rewrite with equalities, do not unfold definitions.**   
+Avoid unfolding definitions in anything but “basic facts” files. Main proofs should not unfold low-level definitions, processor models, etc. Rather, they should rely exclusively on basic facts so that we can change representations without breaking high-level proofs.
 
+- In particular, for case analysis, prefer basic facts that express all possible cases as a disjunction. Do not destruct the actual definitions directly.  
 
-- Naming suggestion: for case a case analysis of foo, use foo_cases as the lemma name.
+- Do not explicitly reference proof terms in type classes (because they might change with the representation). Instead, introduce lemmas that restate the proof term in a general, abstract way that is unlikely to change and rely on those.  
+Guideline: do not name proof terms in type classes to prevent explicit dependencies.
 
+### Tactics
 
-- Do not explicitly reference proof terms in type classes (because they might change with the representation). Instead, introduce lemmas that restate the proof term in a general, abstract way that is unlikely to change and rely on those. Guideline: do not name proof terms in type classes to prevent explicit dependencies.
+- Document the tactics that you use in the [list of tactics](doc/tactics.md). For new users, it can be quite difficult to identify the right tactics to use. This list ist intended to give novices a starting to point in the search for the "right" tools.
 
 
 *To be continued… please feel free to propose new advice and better guidelines.*