Simplify lock, counter and coarse-grained stack

F_mu_ref_par/examples/counter.v

@@ -8,16 +8,15 @@ Section CG_Counter.
 
   (* Coarse-grained increment *)
   Definition CG_increment (x : expr) : expr :=
-    Lam (App (Lam (Store x.[ren (+ 4)] (NBOP Add (♯ 1) (Var 1))))
-             (Load x.[ren (+ 2)])).
+    Lam ((Store x.[ren (+ 2)] (NBOP Add (♯ 1) (Load x.[ren (+ 2)])))).
 
   Lemma CG_increment_type x Γ :
     typed Γ x (Tref TNat) →
     typed Γ (CG_increment x) (TArrow TUnit TUnit).
   Proof.
     intros H1. repeat econstructor.
-    eapply (context_weakening [_; _; _; _]); eauto.
-    eapply (context_weakening [_; _]); eauto.
+    - eapply (context_weakening [_; _]); eauto.
+    - eapply (context_weakening [_; _]); eauto.
   Qed.
 
   Lemma CG_increment_closed (x : expr) :
@@ -37,15 +36,11 @@ Section CG_Counter.
     intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_increment.
     iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
     iFrame "Hspec Hj"; trivial. simpl.
-    Unshelve. 3: simpl; auto. asimpl.
-    iPvs (step_load _ _ _ j (K ++ [AppRCtx (LamV _)])
+    iPvs (step_load _ _ _ j (K ++ [StoreRCtx (LocV _); NBOPRCtx _ (♯v _)])
                     _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
     rewrite ?fill_app. simpl.
     iFrame "Hspec Hj"; trivial.
     rewrite ?fill_app. simpl.
-    iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
-    iFrame "Hspec Hj"; trivial. simpl.
-    Unshelve. 3: simpl; auto.
     iPvs (step_nat_bin_op _ _ _ j (K ++ [StoreRCtx (LocV _)])
                           _ _ _  with "[Hj]") as "Hj"; eauto.
     rewrite ?fill_app. simpl.
@@ -54,9 +49,9 @@ Section CG_Counter.
     iPvs (step_store _ _ _ j K _ _ _ _ _
           with "[Hj Hx]") as "[Hj Hx]"; eauto.
     iFrame "Hspec Hj"; trivial.
-    Unshelve. 3: trivial.
     iPvsIntro.
     iFrame "Hj Hx"; trivial.
+    Unshelve. all: trivial.
   Qed.
 
   Global Opaque CG_increment.

F_mu_ref_par/examples/lock.v

@@ -9,26 +9,16 @@ Definition release : expr := Lam (Store (Var 1) (♭ false)).
 
 Definition with_lock (e : expr) (l : expr) : expr :=
   Lam
-    (App
-       (Lam
-          (App (Lam (App (Lam (App (Lam (Var 3)) (App release (Var 5))))
-                         (App e.[ren (+6)] (Var 5))))
-               (App acquire (Var 1))
-          )
-       )
-       l.[ren (+2)]
+    (App (Lam (App (Lam (App (Lam (Var 3)) (App release l.[ren (+6)])))
+                   (App e.[ren (+4)] (Var 3))))
+         (App acquire l.[ren (+2)])
     ).
 
 Definition with_lockV (e l : expr) : val :=
   LamV
-    (App
-       (Lam
-          (App (Lam (App (Lam (App (Lam (Var 3)) (App release (Var 5))))
-                         (App e.[ren (+6)] (Var 5))))
-               (App acquire (Var 1))
-          )
-       )
-       l.[ren (+2)]
+    (App (Lam (App (Lam (App (Lam (Var 3)) (App release l.[ren (+6)])))
+                   (App e.[ren (+4)] (Var 3))))
+         (App acquire l.[ren (+2)])
     ).
 
 Lemma with_lock_to_val e l :
@@ -76,9 +66,11 @@ Lemma with_lock_type e l Γ τ τ' :
   typed Γ l LockType →
   typed Γ (with_lock e l) (TArrow τ τ').
 Proof.
-  intros H1 H2. do 2 econstructor; eauto.
-  - repeat (econstructor; eauto using release_type, acquire_type).
-    eapply (context_weakening [_; _; _; _; _; _]); eauto.
+  intros H1 H2. do 3 econstructor; eauto.
+  - repeat (econstructor; eauto using release_type).
+    + eapply (context_weakening [_; _; _; _; _; _]); eauto.
+    + eapply (context_weakening [_; _; _; _]); eauto.
+  - eapply acquire_type.
   - eapply (context_weakening [_; _]); eauto.
 Qed.
 
@@ -155,9 +147,6 @@ Section proof.
     iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
     iFrame "Hspec Hj"; trivial. simpl.
     rewrite ?acquire_closed ?release_closed ?H1. asimpl.
-    iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
-    iFrame "Hspec Hj"; trivial. simpl.
-    rewrite ?acquire_closed ?release_closed ?H1. asimpl.
     iPvs (steps_acquire _ _ _ j (K ++ [AppRCtx (LamV _)])
                    _ _ with "[Hj Hl]") as "[Hj Hl]"; eauto.
     rewrite fill_app; simpl.

F_mu_ref_par/examples/stack/CG_stack.v

@@ -11,16 +11,16 @@ Section CG_Stack.
 
   (* Coarse-grained push *)
   Definition CG_push (st : expr) : expr :=
-    Lam (App (Lam (Store st.[ren (+ 4)] (Fold (InjR (Pair (Var 3) (Var 1))))))
-             (Load st.[ren (+ 2)])).
+    Lam (Store
+           (st.[ren (+2)]) (Fold (InjR (Pair (Var 1) (Load st.[ren (+ 2)]))))).
 
   Lemma CG_push_type st Γ τ :
     typed Γ st (Tref (CG_StackType τ)) →
     typed Γ (CG_push st) (TArrow τ TUnit).
   Proof.
     intros H1. repeat econstructor.
-    eapply (context_weakening [_; _; _; _]); eauto.
-    repeat constructor; by asimpl.
+    eapply (context_weakening [_; _]); eauto.
+    repeat constructor; asimpl; trivial.
     eapply (context_weakening [_; _]); eauto.
   Qed.
 
@@ -41,13 +41,12 @@ Section CG_Stack.
     intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_push.
     iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
     iFrame "Hspec Hj"; trivial. asimpl.
-    iPvs (step_load _ _ _ j (K ++ [AppRCtx (LamV _)])
+    iPvs (step_load _ _ _ j (K ++ [StoreRCtx (LocV _); FoldCtx;
+                                   InjRCtx; PairRCtx _])
                     _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
     rewrite ?fill_app. simpl.
     iFrame "Hspec Hj"; trivial.
     rewrite ?fill_app. simpl.
-    iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
-    iFrame "Hspec Hj"; trivial. asimpl.
     iPvs (step_store _ _ _ j K _ _ _ _ _
           with "[Hj Hx]") as "[Hj Hx]"; eauto.
     iFrame "Hspec Hj"; trivial.
@@ -116,17 +115,12 @@ Section CG_Stack.
 
   (* Coarse-grained pop *)
   Definition CG_pop (st : expr) : expr :=
-    Lam (App (Lam
-                (
-                  Case (Var 1)
-                       (InjL Unit)
-                       (
-                         App (Lam (InjR (Fst (Var 2))))
-                             (Store st.[ren (+ 5)] (Snd (Var 0)))
-                       )
-                )
-             )
-             (Unfold (Load st.[ren (+ 2)]))
+    Lam (Case (Unfold (Load st.[ren (+ 2)]))
+              (InjL Unit)
+              (
+                App (Lam (InjR (Fst (Var 2))))
+                    (Store st.[ren (+ 3)] (Snd (Var 0)))
+              )
         ).
 
   Lemma CG_pop_type st Γ τ :
@@ -134,10 +128,15 @@ Section CG_Stack.
     typed Γ (CG_pop st) (TArrow TUnit (TSum TUnit τ)).
   Proof.
     intros H1.
-    do 2 econstructor;
-      [|do 2 econstructor; eapply (context_weakening [_; _]); eauto].
-    repeat econstructor; asimpl; eauto.
-    eapply (context_weakening [_; _; _; _; _]); eauto.
+    econstructor.
+    eapply (Case_typed _ _ _ _ TUnit);
+      [| repeat constructor
+       | repeat econstructor; eapply (context_weakening [_; _; _]); eauto].
+    replace (TSum TUnit (TProd τ (CG_StackType τ))) with
+    ((TSum TUnit (TProd τ.[ren (+1)] (TVar 0))).[(CG_StackType τ)/])
+      by (by asimpl).
+    repeat econstructor.
+    eapply (context_weakening [_; _]); eauto.
   Qed.
 
   Lemma CG_pop_closed (st : expr) :
@@ -157,18 +156,16 @@ Section CG_Stack.
     intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_pop.
     iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
     iFrame "Hspec Hj"; trivial. asimpl.
-    iPvs (step_load _ _ _ j (K ++ [AppRCtx (LamV _); UnfoldCtx])
+    iPvs (step_load _ _ _ j (K ++ [CaseCtx _ _; UnfoldCtx])
                     _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
     rewrite ?fill_app. simpl.
     iFrame "Hspec Hj"; trivial.
     rewrite ?fill_app. simpl.
-    iPvs (step_Fold _ _ _ j (K ++ [AppRCtx (LamV _)])
+    iPvs (step_Fold _ _ _ j (K ++ [CaseCtx _ _])
                     _ _ _ _ with "[Hj]") as "Hj"; eauto.
     rewrite ?fill_app. simpl.
     iFrame "Hspec Hj"; trivial.
     rewrite ?fill_app. simpl.
-    iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
-    iFrame "Hspec Hj"; trivial. asimpl.
     iPvs (step_case_inr _ _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto.
     iFrame "Hspec Hj"; trivial. asimpl.
     iPvs (step_snd _ _ _ j (K ++ [AppRCtx (LamV _); StoreRCtx (LocV _)]) _ _ _ _
@@ -202,18 +199,16 @@ Section CG_Stack.
     intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_pop.
     iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
     iFrame "Hspec Hj"; trivial. asimpl.
-    iPvs (step_load _ _ _ j (K ++ [AppRCtx (LamV _); UnfoldCtx])
+    iPvs (step_load _ _ _ j (K ++ [CaseCtx _ _; UnfoldCtx])
                     _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
     rewrite ?fill_app. simpl.
     iFrame "Hspec Hj"; trivial.
     rewrite ?fill_app. simpl.
-    iPvs (step_Fold _ _ _ j (K ++ [AppRCtx (LamV _)])
+    iPvs (step_Fold _ _ _ j (K ++ [CaseCtx _ _])
                     _ _ _ _ with "[Hj]") as "Hj"; eauto.
     rewrite ?fill_app. simpl.
     iFrame "Hspec Hj"; trivial.
     rewrite ?fill_app. simpl.
-    iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
-    iFrame "Hspec Hj"; trivial. asimpl.
     iPvs (step_case_inl _ _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto.
     iFrame "Hspec Hj"; trivial. asimpl.
     iPvsIntro. iFrame "Hj Hx"; trivial.
@@ -360,35 +355,23 @@ Section CG_Stack.
 
   (* Coarse-grained iter *)
   Definition CG_iter (f : expr) : expr :=
-    (Lam (App (Lam
-                 (
-                   Case (Var 1)
-                        Unit
-                        (
-                          App (Lam (App (Var 5) (Snd (Var 2))))
-                              (App f.[ren (+5)] (Fst (Var 0)))
-                        )
-                 )
+    Lam (Case (Unfold (Var 1))
+              Unit
+              (
+                App (Lam (App (Var 3) (Snd (Var 2))))
+                    (App f.[ren (+3)] (Fst (Var 0)))
               )
-              (Unfold (Var 1))
-         )
-    ).
+        ).
 
   Lemma CG_iter_folding (f : expr) :
     CG_iter f =
-    (Lam (App (Lam
-                 (
-                   Case (Var 1)
-                        Unit
-                        (
-                          App (Lam (App (Var 5) (Snd (Var 2))))
-                              (App f.[ren (+5)] (Fst (Var 0)))
-                        )
-                 )
+    Lam (Case (Unfold (Var 1))
+              Unit
+              (
+                App (Lam (App (Var 3) (Snd (Var 2))))
+                    (App f.[ren (+3)] (Fst (Var 0)))
               )
-              (Unfold (Var 1))
-         )
-    ).
+        ).
   Proof. trivial. Qed.
 
   Lemma CG_iter_type f Γ τ :
@@ -396,9 +379,14 @@ Section CG_Stack.
     typed Γ (CG_iter f) (TArrow (CG_StackType τ) TUnit).
   Proof.
     intros H1.
-    do 2 econstructor; [|by do 2 econstructor].
+    econstructor.
+    eapply (Case_typed _ _ _ _ TUnit);
+      [| repeat constructor
+       | repeat econstructor; eapply (context_weakening [_; _; _]); eauto].
+    replace (TSum TUnit (TProd τ (CG_StackType τ))) with
+    ((TSum TUnit (TProd τ.[ren (+1)] (TVar 0))).[(CG_StackType τ)/])
+      by (by asimpl).
     repeat econstructor.
-    asimpl. eapply (context_weakening [_; _; _; _; _]); eauto.
   Qed.
 
   Lemma CG_iter_closed (f : expr) :
@@ -427,14 +415,11 @@ Section CG_Stack.
     iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
     iFrame "Hspec Hj"; trivial.
     rewrite -CG_iter_folding. Opaque CG_iter. asimpl.
-    iPvs (step_Fold _ _ _ j (K ++ [AppRCtx (LamV _)])
+    iPvs (step_Fold _ _ _ j (K ++ [CaseCtx _ _])
                     _ _ _ with "[Hj]") as "Hj"; eauto.
     rewrite ?fill_app. simpl.
     iFrame "Hspec Hj"; trivial.
     rewrite ?fill_app. asimpl.
-    iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
-    iFrame "Hspec Hj"; trivial.
-    simpl. asimpl.
     iPvs (step_case_inr _ _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto.
     iFrame "Hspec Hj"; trivial. asimpl.
     iPvs (step_fst _ _ _ j (K ++ [AppRCtx (LamV _); AppRCtx f]) _ _ _ _
@@ -460,14 +445,11 @@ Section CG_Stack.
     iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
     iFrame "Hspec Hj"; trivial.
     rewrite -CG_iter_folding. Opaque CG_iter. asimpl.
-    iPvs (step_Fold _ _ _ j (K ++ [AppRCtx (LamV _)])
+    iPvs (step_Fold _ _ _ j (K ++ [CaseCtx _ _])
                     _ _ _ with "[Hj]") as "Hj"; eauto.
     rewrite ?fill_app. simpl.
     iFrame "Hspec Hj"; trivial.
     rewrite ?fill_app. asimpl.
-    iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
-    iFrame "Hspec Hj"; trivial.
-    simpl. asimpl.
     iPvs (step_case_inl _ _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto.
     iFrame "Hspec Hj"; trivial. asimpl.
     by iPvsIntro.