From dac2b6196b756c1566dc9889608d4ee8476d784d Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Sat, 6 Nov 2021 17:46:02 +0100 Subject: option monad tactic --- scheduling/BTL_SEimpl.v | 27 ++++++++------------------- 1 file changed, 8 insertions(+), 19 deletions(-) (limited to 'scheduling') 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. -- cgit