Playing around with liftings some more

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.