### Move and rename some tactics.

parent c905411d
 ... @@ -146,19 +146,10 @@ Tactic Notation "ecancel" open_constr(Ps) := ... @@ -146,19 +146,10 @@ Tactic Notation "ecancel" open_constr(Ps) := close Ps (@nil (uPred M)) ltac:(fun Qs => cancel Qs) close Ps (@nil (uPred M)) ltac:(fun Qs => cancel Qs) end. end. (* Some more generic uPred tactics. TODO: Naming. *) Ltac revert_intros tac := lazymatch goal with | |- ∀ _, _ => let H := fresh in intro H; revert_intros tac; revert H | |- _ => tac end. (** Assumes a goal of the shape P ⊑ ▷ Q. Alterantively, if Q (** Assumes a goal of the shape P ⊑ ▷ Q. Alterantively, if Q is built of ★, ∧, ∨ with ▷ in all branches; that will work, too. is built of ★, ∧, ∨ with ▷ in all branches; that will work, too. Will turn this goal into P ⊑ Q and strip ▷ in P below ★, ∧, ∨. *) Will turn this goal into P ⊑ Q and strip ▷ in P below ★, ∧, ∨. *) Ltac u_strip_later := Ltac strip_later := let rec strip := let rec strip := lazymatch goal with lazymatch goal with | |- (_ ★ _) ⊑ ▷ _ => | |- (_ ★ _) ⊑ ▷ _ => ... @@ -190,23 +181,22 @@ Ltac u_strip_later := ... @@ -190,23 +181,22 @@ Ltac u_strip_later := | |- _ ⊑ ▷ _ => apply later_mono; reflexivity | |- _ ⊑ ▷ _ => apply later_mono; reflexivity (* We fail if we don't find laters in all branches. *) (* We fail if we don't find laters in all branches. *) end end in revert_intros ltac:(etrans; [|shape_Q]; in intros_revert ltac:(etrans; [|shape_Q]; etrans; last eapply later_mono; first solve [ strip ]). etrans; last eapply later_mono; first solve [ strip ]). (** Transforms a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2 (** Transforms a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2 into True ⊑ ∀..., ■?0... → ?1 → ?2, applies tac, and into True ⊑ ∀..., ■?0... → ?1 → ?2, applies tac, and the moves all the assumptions back. *) the moves all the assumptions back. *) Ltac u_revert_all := (* TODO: this name may be a big too general *) Ltac revert_all := lazymatch goal with lazymatch goal with | |- ∀ _, _ => let H := fresh in intro H; u_revert_all; | |- ∀ _, _ => let H := fresh in intro H; revert_all; (* TODO: Really, we should distinguish based on whether this is a (* TODO: Really, we should distinguish based on whether this is a dependent function type or not. Right now, we distinguish based dependent function type or not. Right now, we distinguish based on the sort of the argument, which is suboptimal. *) on the sort of the argument, which is suboptimal. *) first [ apply (const_intro_impl _ _ _ H); clear H first [ apply (const_intro_impl _ _ _ H); clear H | revert H; apply forall_elim'] | revert H; apply forall_elim'] | |- ?C ⊑ _ => trans (True ∧ C)%I; | |- ?C ⊑ _ => apply impl_entails first (apply equiv_entails_sym, left_id, _; reflexivity); apply impl_elim_l' end. end. (** This starts on a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2. (** This starts on a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2. ... @@ -215,8 +205,8 @@ Ltac u_revert_all := ... @@ -215,8 +205,8 @@ Ltac u_revert_all := applies [tac] on the goal (now of the form _ ⊑ _), and then reverts the applies [tac] on the goal (now of the form _ ⊑ _), and then reverts the Coq assumption so that we end up with the same shape as where we started, Coq assumption so that we end up with the same shape as where we started, but with an additional assumption ★-ed to the context *) but with an additional assumption ★-ed to the context *) Ltac u_löb tac := Ltac löb tac := u_revert_all; revert_all; (* Add a box *) (* Add a box *) etrans; last (eapply always_elim; reflexivity); etrans; last (eapply always_elim; reflexivity); (* We now have a goal for the form True ⊑ P, with the "original" conclusion (* We now have a goal for the form True ⊑ P, with the "original" conclusion ... @@ -233,7 +223,7 @@ Ltac u_löb tac := ... @@ -233,7 +223,7 @@ Ltac u_löb tac := | |- _ ⊑ (■ _ → _) => apply impl_intro_l, const_elim_l; | |- _ ⊑ (■ _ → _) => apply impl_intro_l, const_elim_l; let H := fresh in intro H; go; revert H let H := fresh in intro H; go; revert H (* This is the "bottom" of the goal, where we see the impl introduced (* This is the "bottom" of the goal, where we see the impl introduced by u_revert_all as well as the ▷ from löb_strong and the □ we added. *) by uPred_revert_all as well as the ▷ from löb_strong and the □ we added. *) | |- ▷ □ ?R ⊑ (?L → _) => apply impl_intro_l; | |- ▷ □ ?R ⊑ (?L → _) => apply impl_intro_l; trans (L ★ ▷ □ R)%I; trans (L ★ ▷ □ R)%I; first (eapply equiv_entails, always_and_sep_r, _; reflexivity); first (eapply equiv_entails, always_and_sep_r, _; reflexivity); ... ...
 ... @@ -81,7 +81,7 @@ Proof. ... @@ -81,7 +81,7 @@ Proof. do 4 (rewrite big_sepS_insert; last set_solver). do 4 (rewrite big_sepS_insert; last set_solver). rewrite !fn_lookup_insert fn_lookup_insert_ne // !fn_lookup_insert. rewrite !fn_lookup_insert fn_lookup_insert_ne // !fn_lookup_insert. rewrite 3!assoc. apply sep_mono. rewrite 3!assoc. apply sep_mono. - rewrite saved_prop_agree. u_strip_later. - rewrite saved_prop_agree. strip_later. apply wand_intro_l. rewrite [(_ ★ (_ -★ Π★{set _} _))%I]comm !assoc wand_elim_r. apply wand_intro_l. rewrite [(_ ★ (_ -★ Π★{set _} _))%I]comm !assoc wand_elim_r. rewrite (big_sepS_delete _ I i) //. rewrite (big_sepS_delete _ I i) //. rewrite [(_ ★ Π★{set _} _)%I]comm [(_ ★ Π★{set _} _)%I]comm -!assoc. rewrite [(_ ★ Π★{set _} _)%I]comm [(_ ★ Π★{set _} _)%I]comm -!assoc. ... @@ -116,8 +116,7 @@ Proof. ... @@ -116,8 +116,7 @@ Proof. rewrite [(▷ _ ★ _)%I]comm -!assoc. eapply wand_apply_l. rewrite [(▷ _ ★ _)%I]comm -!assoc. eapply wand_apply_l. { by rewrite <-later_wand, <-later_intro. } { by rewrite <-later_wand, <-later_intro. } { by rewrite later_sep. } { by rewrite later_sep. } u_strip_later. strip_later. apply: (eq_rewrite R Q (λ x, x)%I); eauto with I. apply: (eq_rewrite R Q (λ x, x)%I); eauto with I. Qed. Qed. (** Actual proofs *) (** Actual proofs *) ... @@ -181,7 +180,7 @@ Proof. ... @@ -181,7 +180,7 @@ Proof. apply const_elim_sep_l=>Hs. destruct p; last done. apply const_elim_sep_l=>Hs. destruct p; last done. rewrite {1}/barrier_inv =>/={Hs}. rewrite later_sep. rewrite {1}/barrier_inv =>/={Hs}. rewrite later_sep. eapply wp_store with (v' := '0); eauto with I ndisj. eapply wp_store with (v' := '0); eauto with I ndisj. u_strip_later. cancel [l ↦ '0]%I. strip_later. cancel [l ↦ '0]%I. apply wand_intro_l. rewrite -(exist_intro (State High I)). apply wand_intro_l. rewrite -(exist_intro (State High I)). rewrite -(exist_intro ∅). rewrite const_equiv /=; last by eauto using signal_step. rewrite -(exist_intro ∅). rewrite const_equiv /=; last by eauto using signal_step. rewrite left_id -later_intro {2}/barrier_inv -!assoc. apply sep_mono_r. rewrite left_id -later_intro {2}/barrier_inv -!assoc. apply sep_mono_r. ... @@ -212,7 +211,7 @@ Proof. ... @@ -212,7 +211,7 @@ Proof. apply const_elim_sep_l=>Hs. apply const_elim_sep_l=>Hs. rewrite {1}/barrier_inv =>/=. rewrite later_sep. rewrite {1}/barrier_inv =>/=. rewrite later_sep. eapply wp_load; eauto with I ndisj. eapply wp_load; eauto with I ndisj. rewrite -!assoc. apply sep_mono_r. u_strip_later. rewrite -!assoc. apply sep_mono_r. strip_later. apply wand_intro_l. destruct p. apply wand_intro_l. destruct p. { (* a Low state. The comparison fails, and we recurse. *) { (* a Low state. The comparison fails, and we recurse. *) rewrite -(exist_intro (State Low I)) -(exist_intro {[ Change i ]}). rewrite -(exist_intro (State Low I)) -(exist_intro {[ Change i ]}). ... @@ -242,8 +241,7 @@ Proof. ... @@ -242,8 +241,7 @@ Proof. apply wand_intro_l. rewrite [(heap_ctx _ ★ _)%I]sep_elim_r. apply wand_intro_l. rewrite [(heap_ctx _ ★ _)%I]sep_elim_r. rewrite [(sts_own _ _ _ ★ _)%I]sep_elim_r [(sts_ctx _ _ _ ★ _)%I]sep_elim_r. rewrite [(sts_own _ _ _ ★ _)%I]sep_elim_r [(sts_ctx _ _ _ ★ _)%I]sep_elim_r. rewrite !assoc [(_ ★ saved_prop_own i Q)%I]comm !assoc saved_prop_agree. rewrite !assoc [(_ ★ saved_prop_own i Q)%I]comm !assoc saved_prop_agree. wp_op>; last done. intros _. u_strip_later. wp_op; [|done]=> _. wp_if. wp_if. eapply wand_apply_r; [done..|]. eapply wand_apply_r; [done..|]. eapply wand_apply_r; [done..|]. eapply wand_apply_r; [done..|]. apply: (eq_rewrite Q' Q (λ x, x)%I); last by eauto with I. apply: (eq_rewrite Q' Q (λ x, x)%I); last by eauto with I. rewrite eq_sym. eauto with I. rewrite eq_sym. eauto with I. ... ...
 ... @@ -12,7 +12,7 @@ Ltac wp_strip_later := ... @@ -12,7 +12,7 @@ Ltac wp_strip_later := | |- _ ⊑ ▷ _ => apply later_intro | |- _ ⊑ ▷ _ => apply later_intro | |- _ ⊑ _ => reflexivity | |- _ ⊑ _ => reflexivity end end in revert_intros ltac:(first [ u_strip_later | etrans; [|go] ] ). in intros_revert ltac:(first [ strip_later | etrans; [|go] ] ). Ltac wp_bind K := Ltac wp_bind K := lazymatch eval hnf in K with lazymatch eval hnf in K with | [] => idtac | [] => idtac ... @@ -29,10 +29,10 @@ Ltac wp_finish := ... @@ -29,10 +29,10 @@ Ltac wp_finish := try (eapply pvs_intro; try (eapply pvs_intro; match goal with |- _ ⊑ wp _ _ _ => simpl | _ => fail end) match goal with |- _ ⊑ wp _ _ _ => simpl | _ => fail end) | _ => idtac | _ => idtac end in simpl; revert_intros go. end in simpl; intros_revert go. Tactic Notation "wp_rec" ">" := Tactic Notation "wp_rec" ">" := u_löb ltac:((* Find the redex and apply wp_rec *) löb ltac:((* Find the redex and apply wp_rec *) idtac; (* *) idtac; (* *) lazymatch goal with lazymatch goal with | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => ... ...
 ... @@ -228,6 +228,14 @@ Ltac setoid_subst := ... @@ -228,6 +228,14 @@ Ltac setoid_subst := | H : @equiv ?A ?e _ ?x |- _ => symmetry in H; setoid_subst_aux (@equiv A e) x | H : @equiv ?A ?e _ ?x |- _ => symmetry in H; setoid_subst_aux (@equiv A e) x end. end. (** The tactic [intros_revert tac] introduces all foralls/arrows, performs tac, and then reverts them. *) Ltac intros_revert tac := lazymatch goal with | |- ∀ _, _ => let H := fresh in intro H; intros_revert tac; revert H | |- _ => tac end. (** Given a tactic [tac2] generating a list of terms, [iter tac1 tac2] (** Given a tactic [tac2] generating a list of terms, [iter tac1 tac2] runs [tac x] for each element [x] until [tac x] succeeds. If it does not runs [tac x] for each element [x] until [tac x] succeeds. If it does not suceed for any element of the generated list, the whole tactic wil fail. *) suceed for any element of the generated list, the whole tactic wil fail. *) ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!