Commit b94d1262 authored by Ralf Jung's avatar Ralf Jung
Browse files

sts, auth: use cancel

parent ccc7a5df
From algebra Require Export auth. From algebra Require Export auth upred_tactics.
From program_logic Require Export invariants global_functor. From program_logic Require Export invariants global_functor.
Import uPred. Import uPred.
...@@ -56,8 +56,7 @@ Section auth. ...@@ -56,8 +56,7 @@ Section auth.
rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ). rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
trans ( auth_inv γ φ auth_own γ a)%I. trans ( auth_inv γ φ auth_own γ a)%I.
{ rewrite /auth_inv -(exist_intro a) later_sep. { rewrite /auth_inv -(exist_intro a) later_sep.
rewrite const_equiv // left_id. rewrite const_equiv // left_id. cancel (▷ φ a)%I.
rewrite [(_ φ _)%I]comm -assoc. apply sep_mono; first done.
rewrite -later_intro /auth_own -own_op auth_both_op. done. } rewrite -later_intro /auth_own -own_op auth_both_op. done. }
rewrite (inv_alloc N) /auth_ctx pvs_frame_r. apply pvs_mono. rewrite (inv_alloc N) /auth_ctx pvs_frame_r. apply pvs_mono.
by rewrite always_and_sep_l. by rewrite always_and_sep_l.
...@@ -81,8 +80,7 @@ Section auth. ...@@ -81,8 +80,7 @@ Section auth.
{ by move=>n ? ? /timeless_iff ->. } { by move=>n ? ? /timeless_iff ->. }
{ by eauto with I. } { by eauto with I. }
rewrite const_equiv // left_id comm. rewrite const_equiv // left_id comm.
apply sep_mono; first done. apply sep_mono_r. by rewrite sep_elim_l.
by rewrite sep_elim_l.
Qed. Qed.
Lemma auth_closing `{!LocalUpdate Lv L} E γ a a' : Lemma auth_closing `{!LocalUpdate Lv L} E γ a a' :
...@@ -91,6 +89,7 @@ Section auth. ...@@ -91,6 +89,7 @@ Section auth.
(|={E}=> auth_inv γ φ auth_own γ (L a)). (|={E}=> auth_inv γ φ auth_own γ (L a)).
Proof. Proof.
intros HL Hv. rewrite /auth_inv /auth_own -(exist_intro (L a a')). intros HL Hv. rewrite /auth_inv /auth_own -(exist_intro (L a a')).
(* TODO it would be really nice to use cancel here *)
rewrite later_sep [(_ ▷φ _)%I]comm -assoc. rewrite later_sep [(_ ▷φ _)%I]comm -assoc.
rewrite -pvs_frame_l. apply sep_mono; first done. rewrite -pvs_frame_l. apply sep_mono; first done.
rewrite const_equiv // left_id -later_intro -own_op. rewrite const_equiv // left_id -later_intro -own_op.
...@@ -146,7 +145,7 @@ Section auth. ...@@ -146,7 +145,7 @@ Section auth.
P fsa E Ψ. P fsa E Ψ.
Proof. Proof.
intros ??? HP. eapply auth_fsa with N γ a; eauto. intros ??? HP. eapply auth_fsa with N γ a; eauto.
rewrite HP; apply sep_mono; first done; apply forall_mono=> a'. rewrite HP; apply sep_mono_r, forall_mono=> a'.
apply wand_mono; first done. apply (fsa_mono fsa)=> b. apply wand_mono; first done. apply (fsa_mono fsa)=> b.
rewrite -(exist_intro L). by repeat erewrite <-exist_intro by apply _. rewrite -(exist_intro L). by repeat erewrite <-exist_intro by apply _.
Qed. Qed.
......
From algebra Require Export sts. From algebra Require Export sts upred_tactics.
From program_logic Require Export invariants global_functor. From program_logic Require Export invariants global_functor.
Import uPred. Import uPred.
...@@ -85,7 +85,7 @@ Section sts. ...@@ -85,7 +85,7 @@ Section sts.
rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ). rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
trans ( sts_inv γ φ sts_own γ s ( sts.tok s))%I. trans ( sts_inv γ φ sts_own γ s ( sts.tok s))%I.
{ rewrite /sts_inv -(exist_intro s) later_sep. { rewrite /sts_inv -(exist_intro s) later_sep.
rewrite [(_ φ _)%I]comm -assoc. apply sep_mono_r. cancel ( φ s)%I.
by rewrite -later_intro -own_op sts_op_auth_frag_up; last set_solver. } by rewrite -later_intro -own_op sts_op_auth_frag_up; last set_solver. }
rewrite (inv_alloc N) /sts_ctx pvs_frame_r. rewrite (inv_alloc N) /sts_ctx pvs_frame_r.
by rewrite always_and_sep_l. by rewrite always_and_sep_l.
...@@ -112,8 +112,9 @@ Section sts. ...@@ -112,8 +112,9 @@ Section sts.
sts.steps (s, T) (s', T') sts.steps (s, T) (s', T')
( φ s' own γ (sts_auth s T)) (|={E}=> sts_inv γ φ sts_own γ s' T'). ( φ s' own γ (sts_auth s T)) (|={E}=> sts_inv γ φ sts_own γ s' T').
Proof. Proof.
intros Hstep. rewrite /sts_inv /sts_own -(exist_intro s'). intros Hstep. rewrite /sts_inv /sts_own -(exist_intro s') later_sep.
rewrite later_sep [(_ ▷φ _)%I]comm -assoc. (* TODO it would be really nice to use cancel here *)
rewrite [(_ ▷φ _)%I]comm -assoc.
rewrite -pvs_frame_l. apply sep_mono_r. rewrite -later_intro. rewrite -pvs_frame_l. apply sep_mono_r. rewrite -later_intro.
rewrite own_valid_l discrete_validI. apply const_elim_sep_l=>Hval. rewrite own_valid_l discrete_validI. apply const_elim_sep_l=>Hval.
trans (|={E}=> own γ (sts_auth s' T'))%I. trans (|={E}=> own γ (sts_auth s' T'))%I.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment