option monad tactic

1 files changed, 8 insertions, 19 deletions

diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v
index 36f49d28..cf35abad 100644
--- a/scheduling/BTL_SEimpl.v
+++ b/scheduling/BTL_SEimpl.v
@@ -14,10 +14,6 @@ Local Open Scope impure.
 Import ListNotations.
 Local Open Scope list_scope.
 
-(** Tactics *)
-
-Ltac simplify_SOME x := repeat inversion_SOME x; try_simplify_someHyps.
-
 (** Notations to make lemmas more readable *)
 Notation "'sval_refines' ctx sv1 sv2" := (eval_sval ctx sv1 = eval_sval ctx sv2)
   (only parsing, at level 0, ctx at next level, sv1 at next level, sv2 at next level): hse.
@@ -495,7 +491,7 @@ Proof.
   wlp_simplify.
   eapply rset_mem_correct; simpl; eauto.
   - intros X; erewrite H1; eauto.
-    rewrite X. simplify_SOME z.
+    simplify_option.
   - intros X; inversion REF.
     erewrite H1; eauto.
 Qed.
@@ -612,7 +608,7 @@ Proof.
     destruct (is_move_operation _ _) eqn: Hmove.
     { wlp_simplify; exploit is_move_operation_correct; eauto.
       intros (Hop & Hlsv); subst; simpl in *. inv REF.
-      simplify_SOME z; erewrite H; eauto. }
+      simplify_option. erewrite H; eauto. }
     destruct (target_op_simplify _ _ _) eqn: Htarget_op_simp; wlp_simplify.
     { destruct (eval_list_sval _ _) eqn: OKlist; try congruence.
       rewrite <- H; exploit target_op_simplify_correct; eauto. }
@@ -623,9 +619,7 @@ Proof.
     + erewrite H0; eauto.
       erewrite H; [|eapply REG_EQ; eauto].
       erewrite MEM_EQ; eauto.
-      repeat simplify_SOME z.
-      * destruct (Memory.Mem.loadv _ _ _); try congruence.
-      * rewrite H1 in OK1; congruence.
+      simplify_option.
     + erewrite H0; eauto.
 Qed.
 Global Opaque simplify.
@@ -752,12 +746,7 @@ Proof.
   induction l.
   - intuition discriminate.
   - intros ALLR. simpl.
-    inversion_SOME v.
-    + intro SVAL. inversion_SOME lv; [discriminate|].
-      assert (forall r : reg, In r l -> eval_sval ctx (si_sreg st r) = None -> False).
-      { intros r INR. eapply ALLR. right. assumption. }
-      intro SVALLIST. intro. eapply IHl; eauto.
-    + intros. exploit (ALLR a); simpl; eauto.
+    simplify_option.
 Qed.
 
 Lemma hrs_sreg_set_correct r lr rsv hrs:
@@ -1118,7 +1107,7 @@ Proof.
     exploit H; eauto; intros SEVAL; auto.
     all:
       simpl in SOUT; generalize SOUT; clear SOUT;
-      inversion_SOME b0; try_simplify_someHyps.
+      simplify_option.
     + intros; eapply IHib1; eauto.
     + intros; eapply IHib2; eauto.
 Qed.
@@ -1155,7 +1144,7 @@ Proof.
   - (* Bstore *)
     wlp_simplify; exploit hrs_ok_store_okpreserv; eauto.
   - (* Bcond *)
-    wlp_simplify; generalize H2; clear H2; inversion_SOME b; destruct b; try_simplify_someHyps.
+    wlp_simplify; generalize H2; clear H2; simplify_option.
 Qed.
 Local Hint Resolve hrexec_rec_okpreserv: wlp.
 
@@ -1194,14 +1183,14 @@ Proof.
   - (* Bcond *)
     simpl; intros; wlp_simplify.
     assert (rOK: ris_ok ctx hrs). {
-      simpl in H2; generalize H2; inversion_SOME b0; destruct b0; try_simplify_someHyps.
+      simpl in H2; generalize H2; simplify_option.
     }
     exploit (Refcond ctx (fst exta) cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1
               (sexec_rec (cf ctx) ib1 sis k) (sexec_rec (cf ctx) ib2 sis k));
     exploit H; eauto; intros SEVAL; auto.
     all:
       simpl in H2; generalize H2; clear H2;
-      inversion_SOME b0; try_simplify_someHyps.
+      simplify_option.
     + intros; eapply IHib1; eauto.
     + intros; eapply IHib2; eauto.
     Unshelve. all: auto.