make the proof term in the readiness type class "unreferencable"

As discussed at the RT-PROOFS meeting in Paris, proof terms should not
have a name so that we don't actually directly depend on them in
proofs. This patch removes the explicit name of the proof term in the
readiness type class and introduces an equivalent lemma.

restructuring/analysis/basic_facts/arrivals.v

@@ -14,14 +14,28 @@ Section Arrived.
      readiness. *)
   Context `{JobCost Job}.
   Context `{JobArrival Job}.
-  Context `{JobReady Job PState}.
+  (* We give the readiness typeclass instance a name here because we rely on it
+     explicitly in proofs. *)
+  Context {ReadyParam : JobReady Job PState}.
+
+  (** First, we note that readiness models are by definition consistent
+      w.r.t. [pending]. *)
+  Lemma any_ready_job_is_pending:
+    forall j t,
+      job_ready sched j t -> pending sched j t.
+  Proof.
+    move: ReadyParam => [is_ready CONSISTENT].
+    move=> j t READY.
+    apply CONSISTENT.
+    by exact READY.
+  Qed.
 
-  (** We observe that a given job must have arrived to be ready... *)
+  (** Next, we observe that a given job must have arrived to be ready... *)
   Lemma ready_implies_arrived:
     forall j t, job_ready sched j t -> has_arrived j t.
   Proof.
     move=> j t READY.
-    move: (any_ready_job_is_pending sched j t READY).
+    move: (any_ready_job_is_pending j t READY).
     by rewrite /pending => /andP [ARR _].
   Qed.
 

restructuring/analysis/basic_facts/completion.v

 From rt.restructuring.behavior Require Export all.
-From rt.restructuring.analysis.basic_facts Require Export service.
+From rt.restructuring.analysis.basic_facts Require Export service arrivals.
 
 From rt.util Require Import nat.
 

restructuring/behavior/ready.v

@@ -3,15 +3,20 @@ From rt.restructuring.behavior Require Export service.
 
 
 (** We define a general notion of readiness of a job: a job can be
-   scheduled only when it is ready. This notion of readiness is a general
-   concept that is used to model jitter, self-suspensions, etc.  Crucially, we
-   require that any sensible notion of readiness is a refinement of the notion
+   scheduled only when it is ready, as determined by the predicate
+   [job_ready]. This notion of readiness is a general concept that is
+   used to model jitter, self-suspensions, etc.  Crucially, we require
+   that any sensible notion of readiness is a refinement of the notion
    of a pending job, i.e., any ready job must also be pending. *)
 Class JobReady (Job : JobType) (PState : Type)
       `{ProcessorState Job PState} `{JobCost Job} `{JobArrival Job} :=
   {
     job_ready : schedule PState -> Job -> instant -> bool;
-    any_ready_job_is_pending : forall sched j t, job_ready sched j t -> pending sched j t;
+
+    (** What follows is the consistency requirement: We require any
+        reasonable readiness model to consider only pending jobs to be
+        ready. *)
+    _ : forall sched j t, job_ready sched j t -> pending sched j t;
   }.
 
 (** Based on the general notion of readiness, we define what it means to be