generalize nested

1 files changed, 74 insertions, 71 deletions

diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index 4f472e3e..5098659d 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -660,16 +660,15 @@ Fixpoint history ctx ib sis (k:sistate -> option (list sistate)): option (list s
   end
   .
 
-Inductive nested ctx: sistate -> list sistate -> Type :=
-  ns_nil sis: nested ctx sis nil
-| ns_cons sis1 sis2 lsis:
-   (sis_ok ctx sis2 -> sis_ok ctx sis1) ->
-   nested ctx sis2 lsis ->
-   nested ctx sis1 (sis2::lsis)
+Inductive nested: Prop -> list Prop -> Type :=
+  ns_nil ok: nested ok nil
+| ns_cons (ok1 ok2: Prop) loks:
+   (ok2 -> ok1) ->
+   nested ok2 loks ->
+   nested ok1 (ok2::loks)
    .
 Local Hint Constructors nested: core.
 
-(* TODO: A REVOIR !
 Lemma nested_monotonic ok1 oks: 
   nested ok1 oks ->
   forall (ok2: Prop), (ok1 -> ok2) ->
@@ -680,10 +679,10 @@ Qed.
 
 Lemma history_nested ctx ib:
   forall k
-  (CONT: forall sis hsis, (k sis) = Some hsis -> nested (sis_ok ctx sis) hsis)
+  (CONT: forall sis hsis, (k sis) = Some hsis -> nested (sis_ok ctx sis) (List.map (sis_ok ctx) hsis))
   sis hsis 
   (RET: history ctx ib sis k = Some hsis),
-  nested (sis_ok ctx sis) hsis.
+  nested (sis_ok ctx sis) (List.map (sis_ok ctx) hsis).
 Proof.
   induction ib; simpl; intros; try_simplify_someHyps.
   + econstructor; eauto. admit.
@@ -727,75 +726,73 @@ Proof.
     * eapply nested_last_1; eauto.
     * eapply IHLAST; eauto.
 Qed.
+
 Local Hint Constructors is_last: core.
 
-Lemma run_sem_isstate_okcnd_last ctx ib: forall ks kok
-  (CONT: forall sis1 sis2 sfv, run_sem_isstate ctx (ks sis1) = Some (sout sis2 sfv) -> exists hsis, kok sis1 = Some hsis /\ is_last (sis_ok ctx sis2) hsis)
-  sis1 sis2 sfv
+Lemma is_last_map {A B} (f: A -> B) x l: is_last x l -> is_last (f x) (List.map f l).
+Proof.
+  induction 1; simpl; eauto.
+Qed.
+
+Lemma run_sem_is_last ctx ib: forall ks kok
+  (CONT: forall sis1 sis2 sfv hsis, run_sem_isstate ctx (ks sis1) = Some (sout sis2 sfv) -> kok sis1 = Some hsis -> is_last sis2 hsis)
+  sis1 sis2 sfv hsis
   (RUN: run_sem_isstate ctx (sexec_rec (cf ctx) ib sis1 ks) = Some (sout sis2 sfv))
-  ,exists hsis, history ctx ib sis1 kok = Some hsis /\ is_last (sis_ok ctx sis2) hsis.
+  (HIST: history ctx ib sis1 kok = Some hsis)
+  ,is_last sis2 hsis.
 Proof.
   induction ib; simpl; intros; try_simplify_someHyps.
   + destruct trap; simpl; try_simplify_someHyps.
   + (* seq *)
-    intros; eapply IHib1; eauto.
+    intros; eapply IHib1. 2-3: eauto.
     simpl; intros; eapply IHib2; eauto.
   + (* cond *)
-    autodestruct. intros; destruct b.
-    - exploit IHib1; eauto.
-      intros (hsis & OK & LAST).
-      rewrite OK; simpl.
-      eexists; split; eauto.
-    - exploit IHib2; eauto.
-      intros (hsis & OK & LAST).
-      rewrite OK; simpl.
-      eexists; split; eauto.
+    autodestruct.
+    destruct (history _ _ _ _) eqn: HIST; try_simplify_someHyps.
+    intros; econstructor.
+    destruct b; eauto.
 Qed.
-*)
-
-Inductive histOK ctx: list sistate -> sstate -> Prop :=
-  | Final_ok sis sfv
-      : histOK ctx (sis::nil) (Sfinal sis sfv)
-  | Cond_ok b sis hsis cond args ifso ifnot
-      (OK: (sis_ok ctx sis))
-      (EVAL: seval_condition ctx cond args sis.(si_smem) = Some b)
-      (REC: histOK ctx hsis (if b then ifso else ifnot))
-      : histOK ctx (sis::hsis) (Scond cond args sis.(si_smem) ifso ifnot)
-  .
-Local Hint Constructors histOK: core.
 
-(* TODO: pour prouver ça, faut généraliser avec nested + is_last en hypothèse ?  
-
-Lemma run_sem_isstate_okentails ctx ib: forall ks kok
-  (CONT: forall sis st, ks sis = st -> run_sem_isstate ctx st <> None -> exists hsis, kok sis = Some hsis /\ histOK ctx hsis st)
-  sis st
-  (EXEC: sexec_rec (cf ctx) ib sis ks = st)
-  (OK: run_sem_isstate ctx st <> None)
-  ,exists hsis, history ctx ib sis kok = Some hsis /\ histOK ctx hsis st.
+Lemma run_sem_history_None ctx ib: forall ks kok
+  (CONT: forall sis, kok sis = None -> run_sem_isstate ctx (ks sis) = None)
+  sis
+  (HIST: history ctx ib sis kok = None)
+  ,run_sem_isstate ctx (sexec_rec (cf ctx) ib sis ks) = None.
 Proof.
-  induction ib; simpl; intros; subst; try_simplify_someHyps.
-  + destruct trap; simpl in *; try_simplify_someHyps. congruence.
+  induction ib; simpl; intros; try_simplify_someHyps.
+  + destruct trap; simpl in *; try_simplify_someHyps.
   + (* seq *)
-    intros; eapply IHib1; eauto.
+    intros; eapply IHib1. 2: eauto.
     simpl; intros; eapply IHib2; eauto.
   + (* cond *)
     simpl in *.
     autodestruct.
-    intros; destruct b.
-    - exploit IHib1; eauto.
-      intros (hsis & OK1 & X).
-      rewrite OK1; simpl.
-      eexists; split; eauto.
-      econstructor; eauto.
-      admit.
-    - exploit IHib2; eauto.
-      intros (hsis & OK2 & LAST).
-      rewrite OK2; simpl.
-      eexists; split; eauto.
-      econstructor; eauto.
-      admit.
-Admitted.
-*)
+    destruct (history _ _ _ _) eqn: X; try congruence.
+    intros; destruct b; eauto.
+Qed.
+
+(* TODO:  bof, "historys_spec" un peu lourd pour l'usage qui en est fait ? *)
+Inductive history_spec ctx sis1 sis2: option (list sistate) -> Prop :=
+  history_exist hsis 
+    (NESTED: nested (sis_ok ctx sis1) (List.map (sis_ok ctx) hsis))
+    (LAST: is_last sis2 hsis)
+    : history_spec ctx sis1 sis2 (Some hsis)
+  .
+Local Hint Resolve history_exist: core.
+
+Lemma run_sem_history ctx ib sis svf
+  (OK: run_sem_isstate ctx (sexec (cf ctx) ib) = Some (sout sis svf))
+  :history_spec ctx sis_init sis (history ctx ib sis_init (fun _ => None)).
+Proof.
+  unfold sexec in *; destruct (history _ _ _ _) eqn: HIST.
+  + econstructor.
+    * eapply history_nested; eauto.
+      simpl; try congruence.
+    * eapply run_sem_is_last. 2-3: eauto.
+      simpl; try congruence.
+  + exploit (run_sem_history_None ctx ib (fun _ => Sabort)); eauto.
+    congruence.
+Qed.
 
 (** RAFFINEMENT EXEC SYMBOLIQUE **)
 
@@ -826,12 +823,12 @@ Local Hint Constructors rst_refines: core.
 
 Lemma rexec_rec_correct ctx ib: 
   forall kok rk k
-  (CONT: forall ris sis hsis st, ris_refines ctx ris sis -> k sis = st -> kok sis = Some hsis -> histOK ctx hsis st -> rst_refines ctx (rk ris) (k sis))
+  (CONT: forall ris sis hsis st, ris_refines ctx ris sis -> k sis = st -> kok sis = Some hsis -> (forall sis, List.In sis hsis -> sis_ok ctx sis) -> rst_refines ctx (rk ris) (k sis))
   ris sis hsis st
   (REF: ris_refines ctx ris sis)
   (EXEC: sexec_rec (cf ctx) ib sis k = st)
   (OK1: history ctx ib sis kok = Some hsis)
-  (OK2: histOK ctx hsis st)
+  (OK2: forall sis, List.In sis hsis -> sis_ok ctx sis)
   , rst_refines ctx (rexec_rec (cf ctx) ib ris rk) st.
 Proof.
   induction ib; simpl; try (intros; subst; eauto; fail).
@@ -843,13 +840,12 @@ Proof.
   - (* cond *)
     intros rk k kok CONT ris sis hsis st REF EXEC. subst.
     autodestruct.
-    intros EQb.
+    intros COND.
     destruct (history _ _ _ _) eqn: EQl;
     intros; try_simplify_someHyps; intros.
-    inv OK2.
+    exploit (OK2 sis); auto.
     assert (rOK: ris_ok ctx ris). { erewrite <- OK_EQUIV; eauto. }
-    try_simplify_someHyps; intros.
-    generalize EVAL.
+    generalize COND.
     erewrite seval_condition_valid_preserv, <- seval_condition_refpreserv; eauto.
     intros;
     econstructor; try_simplify_someHyps.
@@ -857,11 +853,18 @@ Qed.
 
 Definition rexec f ib := rexec_rec f ib ris_init (fun _ => Rabort).
 
-Lemma rexec_correct ctx ib hsis:
-  history ctx ib sis_init (fun _ : sistate => None) = Some hsis ->
-  histOK ctx hsis (sexec_rec (cf ctx) ib sis_init (fun _ : sistate => Sabort)) ->
+Lemma rexec_correct ctx ib sis sfv:
+  run_sem_isstate ctx (sexec (cf ctx) ib) = Some (sout sis sfv) ->
+  (sis_ok ctx sis) ->
   rst_refines ctx (rexec (cf ctx) ib) (sexec (cf ctx) ib).
 Proof.
+  intros RUN SIS; exploit run_sem_history; eauto.
+  intros HIST; inv HIST.
   unfold sexec; intros; eapply rexec_rec_correct; eauto.
-  simpl; congruence.
+  + simpl; intros; subst; eauto.
+  + intros; eapply nested_last_all.
+    - eapply is_last_map; eauto.
+    - eapply NESTED.
+    - eapply SIS.
+    - eapply List.in_map; eauto.
 Qed.