From 2099c5912004726cdce88c74b635e2b694e25957 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Fri, 12 Jan 2018 17:01:47 +0100 Subject: [PATCH] Playing around with liftings some more --- theories/tests/liftings.v | 83 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) diff --git a/theories/tests/liftings.v b/theories/tests/liftings.v index 502b5f6..94335db 100644 --- a/theories/tests/liftings.v +++ b/theories/tests/liftings.v @@ -94,4 +94,87 @@ Section liftings. - iApply (lift_ht with "HT HR2"). eauto. Abort. + Lemma LA_lift_wtf {A : Type} α (e : expr) β E Δ Γ : + (∀ (x : A), lhs_ht (α x) e (β x) E Δ Γ) -∗ + atomic_logrel α β E E e Δ Γ. + Proof. + rewrite /atomic_logrel. + iIntros "#HT" (K t τ). + iIntros (R2 R1) "[HR2 #Hlog]". + iMod "Hlog" as (x) "(Hα & HR & Hm)". + iApply ("HT" $! x K t τ with "Hα"). + iIntros (v) "Hβ". + iDestruct "Hm" as "[_ Hm]". + iApply "Hm". by iFrame. + Qed. + + (* Lemma LA_hoare {A : Type} α (e : expr) β E1 E2 Δ Γ : *) + (* □ atomic_logrel α β E2 E1 e Δ Γ -∗ *) + (* (∀ (x : A), lhs_ht (α x) e (β x) E1 Δ Γ). *) + (* Proof. *) + (* rewrite /atomic_logrel /lhs_ht. *) + (* iIntros "#HLA" (x K t τ). *) + (* iSpecialize ("HLA" $! K t τ True%I (fun _ => True)%I). *) + (* iAlways. iIntros "Hα Hv". *) + (* 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') -∗ + {Δ;Γ} ⊨ FG_increment $/ LitV (Loc cnt) ≤log≤ CG_increment $/ LitV (Loc cnt') $/ LitV (Loc l) : TArrow TUnit TUnit. + Proof. + iIntros "#Hinv". + iApply bin_log_related_arrow_val. + { unfold FG_increment. unlock; simpl_subst. reflexivity. } + { unfold CG_increment. unlock; simpl_subst. reflexivity. } + { unfold FG_increment. unlock; simpl_subst/=. solve_closed. (* TODO: add a clause to the reflection mechanism that reifies a [lambdasubst] expression as a closed one *) } + { unfold CG_increment. unlock; simpl_subst/=. solve_closed. } + + iAlways. iIntros (v v') "[% %]"; simplify_eq/=. + pose (F := (fun (n : nat) => (l ↦ₛ #false) ∗ cnt' ↦ₛ #n)%I). + iPoseProof (counter_atomic cnt ⊤ (⊤ ∖ ↑counterN) Δ Γ + $! [] _ TUnit True%I F) + as "Hrule /=". + iApply "Hrule". iSplitR; first done. iAlways. + iInv counterN as ">Hcnt" "Hcl". iModIntro. + iDestruct "Hcnt" as (n) "[Hl [Hcnt Hcnt']]". + iExists n. iFrame. clear n. + iSplit; cbv[F]. + - iDestruct 1 as (n) "[Hcnt [Hl Hcnt']]". + iMod ("Hcl" with "[-]"). + { iNext. iExists _. iFrame. } + done. + - iIntros (m ?) "([% Hcnt] & [Hl Hcnt'] & _)"; simplify_eq/=. + iApply (bin_log_related_CG_increment_r _ _ [] with "[Hcnt'] [Hl]"); auto. + { solve_ndisj. } + iIntros "Hcnt' Hl". + iMod ("Hcl" with "[-]"). + { iNext. iExists _. iFrame. } + simpl. + by rel_vals. + Qed. + + End liftings. -- GitLab