Commit d6c72828 authored by Hai Dang's avatar Hai Dang
Browse files

minor cleanup

parent f2e1c371
......@@ -1004,7 +1004,7 @@ Proof.
set E' := G'.(Es).
have LeE' : E3 E' by apply LeG'.
iCombine "GM" "GM'" as "GM".
iCombine "GM GM'" as "GM".
iMod (graph_master_update _ _ _ LeG' EGCs' with "GM") as "[[GM GM'] Gs']".
have LeV1' : V1 V'. { clear -LeV1 LeV2. rewrite /V'. solve_lat. }
......@@ -1146,7 +1146,7 @@ Proof.
iDestruct (ExchangerInv_graph_master_agree with "GM GM'")
as "(%Eq & GM & GM')". subst G4'.
iCombine "GM" "GM'" as "GM".
iCombine "GM GM'" as "GM".
iMod (graph_master_update _ _ _ LeG' EGCs' with "GM") as "[[GM GM'] Gs']".
(* TODO: duplicates with other CANCELLED case *)
......@@ -1800,7 +1800,7 @@ Proof.
iDestruct (ExchangerInv_graph_master_agree with "GM GM'")
as "(%Eq & GM & GM')". subst G3'.
iCombine "GM" "GM'" as "GM".
iCombine "GM GM'" as "GM".
iMod (graph_master_update _ _ _ LeG' EGCs' with "GM") as "[[GM GM'] Gs']".
have LeV0V' : V0 V'. { clear -LeV0 LeV1 LeV2. rewrite /V'. solve_lat. }
......
......@@ -85,8 +85,8 @@ Qed.
Lemma GsetDisjFrag_disj γ a b :
GsetDisjFrag γ a - GsetDisjFrag γ b - a b .
Proof.
iIntros "o1 o2". iCombine "o1 o2" as "o".
iDestruct (own_valid with "o") as %VALID%auth_frag_valid_1%gset_disj_valid_op.
iIntros "o1 o2".
iDestruct (own_valid_2 with "o1 o2") as %VALID%auth_frag_valid_1%gset_disj_valid_op.
iPureIntro. set_solver.
Qed.
End gset_disj.
......@@ -1961,7 +1961,7 @@ Proof.
by apply FRe' in Eqei. }
iDestruct (slots_masters_enq_slots_snap_agree with "SLM ST0") as %SubT0.
iCombine "GM" "GM'" as "GM".
iCombine "GM GM'" as "GM".
iMod (graph_master_update _ _ _ LeG' EGCs' with "GM") as "([GM GM'] & Gs')".
iAssert (@{V'} SeenLogview E' M')%I with "[]" as "#SL'".
......@@ -2796,7 +2796,7 @@ Proof.
}
iMod (slots_master_set_dequeued_L Vw3 Eqγi EqeT2 with "SLM") as "[SLM sDe]".
iCombine "GM" "GM'" as "GM".
iCombine "GM GM'" as "GM".
iMod (graph_master_update _ _ _ LeG' EGCs' with "GM") as "([GM GM'] & Gs')".
assert (LeV22': V2' V'). { clear -LeV22 LeV20 LeV2. rewrite /V'. solve_lat. }
......
......@@ -1904,7 +1904,7 @@ Proof.
{ clear. by simplify_list_eq. }
have SubCL2 : CL2 CL2' by eexists.
iCombine "GM'" "GM" as "GM".
iCombine "GM' GM" as "GM".
iMod (graph_master_update _ _ G2' LeG' EGCs' with "GM") as "([GM GM'] & #Gs')".
iMod (LTM_update_insert _ _ η enqId FRηT with "LTm") as "[LTm' #LTs']".
......@@ -2842,7 +2842,7 @@ Proof.
iMod "AU" as (G3') "[[_ >GM'] HClose]".
iDestruct (graph_master_agree with "GM' GM") as %->.
iCombine "GM" "GM'" as "GM".
iCombine "GM GM'" as "GM".
iMod (graph_master_update _ _ _ LeG' EGCs' with "GM") as "([GM GM'] & Gs')".
have SYE' : SyncEnqueues E' M'. {
......@@ -3269,7 +3269,7 @@ Proof.
destruct (CDT deqId) as [[vd Eqv] _]. { by exists η22. } clear -Eqv.
apply list_lookup_fmap_inv' in Eqv as (? & _ & ?%lookup_lt_Some). lia. }
iCombine "GM" "GM'" as "GM".
iCombine "GM GM'" as "GM".
iMod (graph_master_update _ _ _ LeG' EGCs' with "GM") as "([GM GM'] & #Gs')".
iMod (LDL_update_app _ _ [(η2', n2')] with "LDL") as "[LDL #LDL']".
have EqCL4' :
......
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