simplification of normRTL

1 files changed, 27 insertions, 67 deletions

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index 7cd8e47d..a22be1d5 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -27,13 +27,6 @@ Definition is_RTLbasic (ib: iblock): bool :=
  | _ => true
  end.
 
-
-Definition Bnop_dec k: { k=Bnop None} + { k<>(Bnop None) }.
-Proof.
-  destruct k; simpl; try destruct oiinfo;
-  intuition congruence.
-Defined.
-
 (** The strict [is_normRTL] property specifying the ouput of [normRTL] below *)
 Inductive is_normRTL: iblock -> Prop :=
   | norm_Bseq ib1 ib2:
@@ -50,11 +43,11 @@ Inductive is_normRTL: iblock -> Prop :=
      .
 Local Hint Constructors is_normRTL: core.
 
-(** Weaker version with less restrictive hypothesis for conditions *)
+(** Weaker version allowing for trailing [Bnop None]. *)
 Inductive is_wnormRTL: iblock -> Prop :=
   | wnorm_Bseq ib1 ib2:
      is_RTLbasic ib1 = true ->
-     is_wnormRTL ib2 -> 
+     (ib2 <> Bnop None -> is_wnormRTL ib2) -> 
      is_wnormRTL (Bseq ib1 ib2)
   | wnorm_Bcond cond args ib1 ib2 iinfo:
      (ib1 <> Bnop None -> is_wnormRTL ib1) ->
@@ -66,7 +59,7 @@ Inductive is_wnormRTL: iblock -> Prop :=
      .
 Local Hint Constructors is_wnormRTL: core.
 
-(* NB: [k] is a "continuation" (e.g. semantically [normRTLrec ib k] is like [BSeq ib k]) *)
+(* NB: [k] is a "continuation" (e.g. semantically [normRTLrec ib k] is like [Bseq ib k]) *)
 Fixpoint normRTLrec (ib: iblock) (k: iblock): iblock :=
   match ib with
   | Bseq ib1 ib2 => normRTLrec ib1 (normRTLrec ib2 k)
@@ -74,8 +67,7 @@ Fixpoint normRTLrec (ib: iblock) (k: iblock): iblock :=
      Bcond cond args (normRTLrec ib1 k) (normRTLrec ib2 k) iinfo
   | BF fin iinfo => BF fin iinfo
   | Bnop None => k
-  | ib =>
-      if Bnop_dec k then ib else Bseq ib k
+  | ib => Bseq ib k
   end.
 
 Definition normRTL ib := normRTLrec ib (Bnop None).
@@ -130,17 +122,13 @@ Lemma normRTLrec_iblock_istep_correct tge sp ib rs0 m0 rs1 m1 ofin1:
          end),
   iblock_istep tge sp rs0 m0 (normRTLrec ib k) rs2 m2 ofin2.
 Proof.
-  induction 1; simpl; intros; intuition subst; eauto.
-  { (* Bnop *)
-    autodestruct; intros OI; inv OI; destruct (Bnop_dec k); subst;
-    try (inv CONT; constructor; fail); repeat econstructor; eauto. }
+  induction 1; simpl; intuition subst; eauto.
+  { (* Bnop *) autodestruct; eauto. }
   1-3: (* Bop, Bload, Bstore *)
-    intros; destruct (Bnop_dec k); subst; repeat econstructor; eauto;
-    inv CONT; econstructor; eauto.
-  - (* Bcond *)
-    destruct ofin; intros;
-    econstructor; eauto;
-    destruct b; eapply IHISTEP; eauto.
+     intros; repeat econstructor; eauto.
+  (* Bcond *)
+  destruct ofin; intuition subst;
+  destruct b; eapply IHISTEP; eauto.
 Qed.
 
 Lemma normRTL_iblock_istep_correct tge sp ib rs0 m0 rs1 m1 ofin:
@@ -152,9 +140,8 @@ Proof.
 Qed.
 
 Lemma normRTLrec_iblock_istep_run_None tge sp ib:
-  forall rs0 m0 o k
-  (ISTEP: iblock_istep_run tge sp ib rs0 m0 = o)
-  (CONT: match o with
+  forall rs0 m0 k
+  (CONT: match iblock_istep_run tge sp ib rs0 m0 with
          | Some (out rs1 m1 ofin) =>
              ofin = None /\
              iblock_istep_run tge sp k rs1 m1 = None
@@ -162,44 +149,23 @@ Lemma normRTLrec_iblock_istep_run_None tge sp ib:
      end),
   iblock_istep_run tge sp (normRTLrec ib k) rs0 m0 = None.
 Proof.
-  induction ib; simpl;
-  try discriminate.
-  - (* BF *)
-    intros; destruct o; try discriminate; simpl in *.
-    inv ISTEP. destruct CONT as [HO ISTEP]; inv HO.
+  induction ib; simpl; intros; subst; intuition (try discriminate).
   - (* Bnop *)
-    intros; destruct o; inv ISTEP; destruct oiinfo, CONT; auto.
-    destruct (Bnop_dec k); subst; repeat econstructor; eauto.
+    intros. autodestruct; auto.
   - (* Bop *)
-    intros; destruct o; destruct (Bnop_dec k);
-    destruct (eval_operation _ _ _ _ _) eqn:EVAL; inv ISTEP;
-    simpl; rewrite EVAL; auto; destruct CONT as [HO ISTEP];
-    trivial.
+    intros; repeat autodestruct; simpl; intuition congruence.
   - (* Bload *)
-    intros; destruct o; destruct (Bnop_dec k);
-    destruct (trap) eqn:TRAP;
-    try destruct (eval_addressing _ _ _ _) eqn:EVAL;
-    try destruct (Mem.loadv _ _ _) eqn:MEM; inv ISTEP;
-    simpl; try rewrite EVAL; try rewrite MEM; simpl; auto;
-    destruct CONT as [HO ISTEP]; trivial.
+    intros; repeat autodestruct; simpl; intuition congruence.
   - (* Bstore *)
-    intros; destruct o; destruct (Bnop_dec k);
-    destruct (eval_addressing _ _ _ _) eqn:EVAL;
-    try destruct (Mem.storev _ _ _) eqn:MEM; inv ISTEP;
-    simpl; try rewrite EVAL; try rewrite MEM; simpl; auto;
-    destruct CONT as [HO ISTEP]; inv HO; trivial.
+    intros; repeat autodestruct; simpl; intuition congruence.
   - (* Bseq *)
     intros.
     eapply IHib1; eauto.
-    destruct (iblock_istep_run tge sp ib1 rs0 m0) eqn:EQib1; try auto.
-    destruct o0; simpl in *. destruct _fin; inv ISTEP.
-    + destruct CONT as [CONTRA _]; inv CONTRA.
-    + split; auto. eapply IHib2; eauto.
+    autodestruct; simpl in *; destruct o; simpl in *; intuition eauto.
+    + destruct _fin; intuition eauto.
+    + destruct _fin; intuition congruence || eauto.
   - (* Bcond *)
-    intros; destruct (eval_condition _ _ _); trivial.
-    destruct b.
-    + eapply IHib1; eauto.
-    + eapply IHib2; eauto.
+    intros; repeat autodestruct; simpl; intuition congruence || eauto.
 Qed.
 
 Lemma normRTL_preserves_iblock_istep_run_None tge sp ib:
@@ -207,7 +173,7 @@ Lemma normRTL_preserves_iblock_istep_run_None tge sp ib:
   -> iblock_istep_run tge sp (normRTL ib) rs m = None.
 Proof.
   intros; eapply normRTLrec_iblock_istep_run_None; eauto.
-  simpl; auto.
+  rewrite H; simpl; auto.
 Qed.
 
 Lemma normRTL_preserves_iblock_istep_run tge sp ib:
@@ -234,17 +200,11 @@ Lemma normRTLrec_matchiblock_correct dupmap cfg ib pc isfst:
          end),
   match_iblock dupmap cfg isfst pc (normRTLrec ib k) opc2.
 Proof.
-  induction 1; simpl; intros; eauto.
-  { (* BF *)
-    inv CONT; econstructor; eauto. }
-  1-4: (* Bnop, Bop, Bload, Bstore *)
-    destruct (Bnop_dec k); subst; eauto; inv CONT; econstructor; eauto.
-  { (* Bgoto *)
-    intros; inv CONT; apply mib_exit; auto. }
-  { (* Bcond *)
-    intros. inv H0;
-    econstructor; eauto; try econstructor.
-    destruct opc0; econstructor. }
+  induction 1; simpl; intros; subst; eauto.
+  (* Bcond *)
+  intros. inv H0;
+  econstructor; eauto; try econstructor.
+  destruct opc0; econstructor.
 Qed.
 
 Lemma normRTL_matchiblock_correct dupmap cfg ib pc isfst opc: