Skip to content

GitLab

Commit 35520fdf authored by Ralf Jung's avatar Ralf Jung
Browse files

auth.v: do not depend on argument order of commutative

parent 560bd3a9
Show whitespace changes
Inline Side-by-side
program_logic/auth.v
View file @ 35520fdf
...@@ -39,7 +39,7 @@ Section auth. ...@@ -39,7 +39,7 @@ Section auth.
rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ). rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
transitivity (▷auth_inv γ ★ auth_own γ a)%I. transitivity (▷auth_inv γ ★ auth_own γ a)%I.
{ rewrite /auth_inv -later_intro -(exist_intro a). { rewrite /auth_inv -later_intro -(exist_intro a).
rewrite (commutative _ _ (φ _)) -associative. apply sep_mono; first done. rewrite [(_ ★ φ _)%I]commutative -associative. apply sep_mono; first done.
rewrite /auth_own -own_op auth_both_op. done. } rewrite /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'.
......
Supports Markdown
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