Update READMEs

As discussed at the RT-PROOFS meeting in Paris, we should provide some brief documentation/guidelines in the restructured Prosa to document "where goes what".

CC: @sbozhko @sophie @mlesourd

changed milestone to %Prosa v0.4

Here are some of the notes that I took:

• Behavior: minimal trace semantics, universally agreed-upon foundation. Everyone uses this; there is no alternative.

• Model: Key concepts, but there are potentially different alternatives to choose from.

• New job and task parameters are defined where they are first needed. Exception: the three fundamental ones in the behavior spec (cost, arrival, deadline).

• Analysis: see #52 (closed)

We also wanted to document some rules for working with typeclasses. Here is what I wrote down:

---

Goal: make proofs more robust to change in definitions

“Rewrite with equalities, do not rely on 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.

Specific case: 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.

Example: do this for uniprocessors in general to reason about “scheduled” / “not scheduled”.

Mention in the guidelines how to exploit case analysis lemmas in SSReflect.

---

Do you have anything to add? Any other guidelines that we should write down?

CC: @proux

mentioned in commit 0aa08782

mentioned in merge request !60 (merged)

mentioned in commit dbbad1f8

LGTM

Just a small remark:

express all possible cases as a disjunction

Sometimes, it is more convenient to use a specific inductive rather than a disjunction. See for instance PeanoNat.Nat.compare_spec in the Coq standard library or Section 4.2.1 of the Mathcomp book for more details https://math-comp.github.io/mcb/book.pdf.

Thanks for the hint! I've added it to the guidelines in commit d5f388f3.

mentioned in commit d5f388f3

With 82045899, 07ebbf4d, and 85c8f5e1, this issue is done.

closed

mentioned in merge request !77 (merged)