From 6b25b7247f005b6d04467cbd900d148ec2271cfd Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Thu, 3 Mar 2022 11:13:27 +0100
Subject: [PATCH] WIP
---
doc/tutorial.v | 163 +++++++++++++++++++++++++++++++++----------------
1 file changed, 111 insertions(+), 52 deletions(-)
diff --git a/doc/tutorial.v b/doc/tutorial.v
index edba31c33..980b1480d 100644
--- a/doc/tutorial.v
+++ b/doc/tutorial.v
@@ -856,10 +856,118 @@ all scheduled jobs ``j_hp`` at that instant ``t`` have higher or equal priority.
Analysis
========
-TODO describe needed analysis for results/fixed_priority/rta/fully_preemptive.v
+The `analysis/ <https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/tree/master/analysis>`_
+directory contains the proofs of real-time analyses themselves.
+Even more than pen&paper proofs, formal proofs need to be appropriately
+factored out into small reusable lemmas. Thus, the `analysis/` directory
+also contains many basic lemmas about all the definitions introduced above.
+Since this document only attempts to present a specific analysis, namely
+fixed priority tasks on a fully preemptive uniprocessor, we only introduce
+here the lemmas used in that analysis. However, at the end of the section,
+the reader should be able to navigate herself through all the lemmas
+of the directory.
-* definitions.job_properties
-* definitions.schedule_prefix
+First Lemmas
+------------
+
+Some definitions are used only internally into `analysis/`,
+thus they aren't located in `behavior/` nor `model/`.
+Among them, let's mention
+|*)
+Require Import prosa.analysis.definitions.job_properties.
+
+Print job_cost_positive.
+(*|
+and
+|*)
+Require Import prosa.analysis.definitions.schedule_prefix.
+
+Print identical_prefix.
+(*|
+
+Equipped with all these definitions, we can finally introduce
+our first lemmas. The files in the directory
+`analysis/facts/behavior/ <https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/tree/master/analysis/facts/behavior>`_
+contain many lemmas establishing basic facts about all the definitions
+introduced in the behavior_ section above.
+The user can load all those lemmas by simply requiring
+|*)
+Require Import prosa.analysis.facts.behavior.all.
+(*|
+The files in `analysis/facts/behavior/` are developed in a literate
+programming style like the remaining of Prosa. Thus, they can be read
+inextenso like any other file in the library. However, lemmas are mostly
+made to be used inside proofs and such reading is a very ineffective way to
+find the lemma one needs when carrying a proof. Indeed, once one gets a Coq
+interface up and running, it is much more convenient to just load the files
+with the above `Require` command and use the `Search` utility of Coq.
+For instance, to find all lemmas about `scheduled_at` and `service_at`,
+one can type
+|*)
+Search scheduled_at service_at.
+(*|
+The `Search` command can also be used with a pattern, for instance
+to look for lemmas of the shape
+`service at some point <= service at some other point`, one can type
+|*)
+Search (service _ _ _ <= service _ _ _). (* .unfold *)
+(*|
+The `Search` command is even more powerful, as documented in
+`Coq's reference manual <https://coq.inria.fr/distrib/current/refman/proof-engine/vernacular-commands.html#coq:cmd.Search>`_.
+
+.. note::
+ The `reference manual of Coq <https://coq.inria.fr/distrib/current/refman/>`_
+ is of high quality nowadays. It is a good first place to learn about the
+ details of any Coq feature.
+
+Back to the `service_monotonic` lemma found above, if one looks in
+the file
+`analysis/facts/behavior/service.v <https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/tree/master/analysis/facts/behavior/service.v>`_,
+one will find the following text
+|*)
+(** We establish a basic fact about the monotonicity of service. *)
+Section Monotonicity.
+
+ (** Consider any job type and any processor model. *)
+ Context {Job : JobType} {PState : ProcessorState Job}.
+
+ (** Consider any given schedule... *)
+ Variable sched: schedule PState.
+
+ (** ...and a given job that is to be scheduled. *)
+ Variable j: Job.
+
+ (** We observe that the amount of service received
+ is monotonic by definition. *)
+ Lemma service_monotonic : forall t1 t2, t1 <= t2 ->
+ service sched j t1 <= service sched j t2.
+ Proof. by move=> t1 t2 ?; rewrite -(service_cat _ _ t1 t2)// leq_addr. Qed.
+
+End Monotonicity.
+(*|
+The whole `Section` business should now be familiar to the reader.
+The `Lemma` keyword is new. It is used to introduce a lemma,
+followed by its name, a colon sign and the statement of the theorem itself,
+ending with a dot, as any Coq sentence.
+The line between `Proof` and `Qed` can be ignored for now.
+It instructs Coq how to perform the proof of the previously stated lemma.
+The only thing to notice is that this proof is terminated by a `Qed`
+(for the latin words "Quod Erat Demonstrandum") meaning that,
+if Coq can compile the `Qed` it managed to check the proof and the new lemma
+is now available for use in future proofs.
+
+.. note::
+ Naming lemmas is a delicate business. Some libraries have very specific
+ and elaborated naming schemes, usually based on the statement of the
+ theorem itself. Although there is no such strict naming scheme in Prosa,
+ one can find a few generic advices in
+ `doc/guidelines.md <https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/tree/master/doc/guidelines.md#naming-conventions>`_.
+
+Search avec pattern
+
+mentionner la doc de Coq
+
+retrieve material below about first proof.
* facts.behavior.service
* facts.behavior.arrivals
@@ -914,55 +1022,6 @@ describe results/fixed_priority/rta/fully_preemptive.v
(probably very short)
|*)
-(*|
-First Lemmas
-------------
-
-TODO: old material, will probably disappear
-
-Based on the previous definitions, some lemmas can be proved.
-Prosa indeed proves a lot of more or less basic lemmas.
-we only present here one such simple lemma from the file
-`analysis/facts/behavior/service.v <https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/blob/master/analysis/facts/behavior/service.v>`_
-|*)
-Require Import prosa.analysis.facts.behavior.service.
-
-(** We establish a basic fact about the monotonicity of service. *)
-Section Monotonicity.
-
- (** Consider any job type and any processor model. *)
- Context {Job: JobType}.
- Context {PState: Type}.
- Context `{ProcessorState Job PState}.
-
- (** Consider any given schedule... *)
- Variable sched: schedule PState.
-
- (** ...and a given job that is to be scheduled. *)
- Variable j: Job.
-
- (** We observe that the amount of service received
- is monotonic by definition. *)
- Lemma service_monotonic:
- forall t1 t2,
- t1 <= t2 ->
- service sched j t1 <= service sched j t2.
- Proof.
- move=> t1 t2 let1t2.
- rewrite -(service_cat _ _ t1 t2) //.
- exact: leq_addr.
- Qed.
-
-End Monotonicity.
-(*|
-The three lines between `Proof` and `Qed` can be ignored for now.
-The instruct Coq how to perform the proof of the previously stated lemma.
-The only thing to notice is that this proof is terminated by a `Qed`
-(for the latin "words Quod Erat Demonstrandum") meaning that,
-if Coq can compile the `Qed` it managed to check the proof and the new lemma
-is now available for use in future proofs.
-|*)
-
(*|
Contributing
============
--
GitLab