Commit 041d3b57 authored by Dan Frumin's avatar Dan Frumin

test/liftings.v quickfix

parent 134a7e51
......@@ -119,27 +119,6 @@ Section liftings.
(* iApply "HLA". *)
(* iSplitR; [done | iAlways]. *)
Lemma counter_atomic2 x E1 E2 Δ Γ :
atomic_logrel
(fun (n : nat) => x ↦ᵢ #n)%I
(fun (n : nat) (v : val) => v = #() x ↦ᵢ #(S n))%I
E2 E1
((FG_increment $/ LitV (Loc x)) #())
Δ Γ.
Proof.
iApply LA_atomic.
iIntros (K t τ R2 R1) "[HR2 #Hlog]".
iApply (bin_log_FG_increment_logatomic _ R1 with "HR2").
iAlways. iMod "Hlog" as (n) "(Hx & HR & Hlog)".
iModIntro. iExists _. iFrame.
iSplit.
- iDestruct "Hlog" as "[Hlog _]". done.
- iDestruct "Hlog" as "[_ Hlog]".
iIntros (m) "[Hx HR1] HR2".
iSpecialize ("Hlog" $! m #()). simpl.
iApply "Hlog". by iFrame.
Qed.
(* Increment refinement using the log atomic triple *)
Lemma FG_CG_increment_refinement2 l cnt cnt' Γ Δ :
inv counterN (counter_inv l cnt cnt') -
......
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