Merge pull request #433 from Blaisorblade/pupd-prepare-2

Switch gDOT to persistent updates

theories/Dot/examples/old_fundamental.v

@@ -24,30 +24,32 @@ Section storeless_unstamped_lemmas.
   Lemma uT_ISub {Γ e T1 T2 i} :
     Γ u⊨ e : T1 -∗ Γ ⊨ T1, 0 <: T2, i -∗ Γ u⊨ iterate tskip i e : T2.
   Proof.
-    iIntros "#H1 #Hsub"; iMod "H1" as (e1s Hsk1) "H1"; iModIntro.
+    pupd; iIntros "#(%e1s & %Hsk1 & H1) #Hsub !>".
     iExists (iterate tskip i e1s); iSplit; last iApply (sT_ISub with "H1 Hsub").
     eauto using same_skel_tm_tskips.
   Qed.
 
   Lemma suetp_var Γ x T :
-    Γ su⊨ tv (ids x) : T ==∗ Γ s⊨ tv (ids x) : T.
+    Γ su⊨ tv (ids x) : T -∗ Γ s⊨ tv (ids x) : T.
   Proof.
-    iIntros "#H1"; iMod "H1" as (e1s Hsk1) "H1".
+    pupd'. iIntros "#(%e1s & %Hsk1 & #H1) !>". iMod "H1".
     by rewrite (same_skel_tv_var_tv_var Hsk1).
   Qed.
 
   Lemma suetp_vlit Γ b T :
-    Γ su⊨ tv (vlit b) : T ==∗ Γ s⊨ tv (vlit b) : T.
+    Γ su⊨ tv (vlit b) : T -∗ Γ s⊨ tv (vlit b) : T.
   Proof.
-    iIntros "#H1"; iMod "H1" as (e1s Hsk1) "H1".
+    (* pupd'. iIntros "#(%e1s & %Hsk1 & #H1)". iRevert "H1". pupd.
+    rewrite (same_skel_tv_vlit_tv_vlit Hsk1). iIntros "$". *)
+    pupd'. iIntros "#(%e1s & %Hsk1 & #H1) !>". iMod "H1".
     by rewrite (same_skel_tv_vlit_tv_vlit Hsk1).
   Qed.
 
   Lemma uT_All_Ex {Γ e1 x2 T1 T2} :
     Γ u⊨ e1 : TAll T1 T2 -∗ Γ u⊨ tv (ids x2) : T1 -∗ Γ u⊨ tapp e1 (tv (ids x2)) : T2.|[ids x2/].
   Proof.
-    iIntros "#H1 #H2"; iMod "H1" as (e1s Hsk1) "H1".
-    iMod (suetp_var with "H2") as "{H2} H2"; iModIntro.
+    pupd'. iIntros "#(%e1s & %Hsk1 & #H1) #H2 !>". iMod "H1" as "#H1".
+    iDestruct (suetp_var with "H2") as "{H2} #>#H2". iIntros "!> !>".
     by iExists (tapp e1s (tv (ids x2))); iSplit; last iApply (T_All_Ex with "H1 H2").
   Qed.
 

theories/Dot/examples/sem/ex_iris_utils.v

@@ -40,13 +40,14 @@ Section loop_sem.
   Context `{HdlangG : !dlangG Σ}.
   Context `{SwapPropI Σ}.
 
-  Lemma loopSemT : ⊢@{iPropI _} |==> WP hclose hloopTm {{ _, False }}.
+  Lemma loopSemT : ⊢@{iPropI _} <PB> WP hclose hloopTm {{ _, False }}.
   Proof using Type*.
-    iDestruct (fundamental_typed (loopTyp [])) as "#>H".
-    iDestruct "H" as (e_s Hsk1) ">H"; iModIntro.
+    iIntros "!>".
+    iDestruct (fundamental_typed (loopTyp [])) as "#>#(%e_s & %Hsk1 & #>#H)".
+    iIntros "!> !>".
     iSpecialize ("H" $! ids with "[//]"); rewrite hsubst_id.
     move E: hloopTm => e.
-    suff ->: e_s = e. { iApply (wp_wand with "H"). iIntros (v). by rw. }
+    suff ->: e_s = e. { iApply (wp_wand with "H"). iIntros "%v {H}". by rw. }
     subst; clear -Hsk1. cbv; repeat constrain_bisimulating.
   Qed.
 

theories/Dot/examples/sem/from_pdot_mutual_rec_sem.v

@@ -251,12 +251,14 @@ Tactic Notation "lrSimpl" "in" constr(iSelP) :=
 Lemma newTypeRef_semTyped Γ :
   ⊢ newTypeRefΓ Γ u⊨ newTypeRefBody : x1 @; "TypeRef".
 Proof.
-  iMod (fundamental_typed (Hx0 Γ)) as (x0_s Hsk) ">#Hx0".
-  iMod (fundamental_subtype (HvT Γ)) as "#HvT".
-  iMod (fundamental_subtype (HvF Γ)) as "#HvF".
-  iMod (fundamental_subtype (Hsublast Γ)) as "#Hsub".
-  iMod loopSemT as "#Hl".
-  unstamp_goal_tm; iIntros "!> %ρ #Hg".
+  iIntros "!>".
+  iDestruct (fundamental_typed (Hx0 Γ)) as "#>#(%x0_s & %Hsk & #>#Hx0)".
+  iDestruct (fundamental_subtype (HvT Γ)) as "#>#HvT".
+  iDestruct (fundamental_subtype (HvF Γ)) as "#>#HvF".
+  iDestruct (fundamental_subtype (Hsublast Γ)) as "#>#Hsub".
+  iDestruct loopSemT as "#>#Hl".
+  iIntros "!>".
+  unstamp_goal_tm. pupd. iIntros "!> %ρ #Hg".
   iSpecialize ("Hx0" with "Hg").
 
   wp_abind; rewrite -wp_value; iSimpl.

theories/Dot/examples/sem/no_russell_paradox.v

@@ -21,7 +21,7 @@ Section Russell.
     *)
   Definition uAu u := oSel (pv u) "A" anil ids u.
 
-  Definition russell_p : envD Σ := λI ρ v, uAu v -∗ False.
+  Definition russell_p : envD Σ := λI ρ v, □ (uAu v -∗ False).
   (* This would internalize as [russell_p ρ v := v : μ x. not (x.A)]. *)
 
   Context (s : stamp).
@@ -58,7 +58,7 @@ Section Russell.
     iApply ("Hvav" with "HuauV").
   Qed.
 
-  Lemma uauEquiv : Hs ⊢ ▷ (uAu v -∗ False) ∗-∗ uAu v.
+  Lemma uauEquiv : Hs ⊢ ▷ □ (uAu v -∗ False) ∗-∗ uAu v.
   Proof.
     iIntros "#Hs"; iSplit.
     - iIntros "#HnotVAV /=".
@@ -68,7 +68,7 @@ Section Russell.
         eauto using objLookupIntro.
       }
       + by iApply (dm_to_type_intro with "Hs").
-      + iApply "HnotVAV".
+      + iIntros "!>!>". rewrite /uAu/= path_wp_pv_eq. iApply "HnotVAV".
     - iIntros "#Hvav".
       by iDestruct (later_not_UAU with "Hs Hvav") as "#>[]".
   Qed.
@@ -78,10 +78,10 @@ Section Russell.
   Lemma taut0 (P : Prop) : ((P → False) ↔ P) → False. Proof. tauto. Qed.
   (** But with later, there's no paradox — we get instead not (not P). *)
   Lemma irisTaut (P : iProp Σ) :
-    (▷ (P -∗ False) ∗-∗ P) -∗ (P -∗ False) -∗ False.
-  Proof using Type*. iIntros "Eq #NP". iApply "NP". by iApply "Eq". Qed.
+    (▷ □ (P -∗ False) ∗-∗ P) -∗ □ (P -∗ False) -∗ False.
+  Proof. iIntros "Eq #NP". iApply "NP". by iApply "Eq". Qed.
 
-  Lemma notNotVAV : Hs ⊢ (uAu v -∗ False) → False.
+  Lemma notNotVAV : Hs ⊢ □ (uAu v -∗ False) → False.
   Proof.
     iIntros "#Hs #notVAV". iApply (irisTaut (uAu v)) => //.
     by iApply uauEquiv.

theories/Dot/examples/sem/positive_div.v

@@ -89,18 +89,18 @@ Section helpers.
   Lemma wp_nge m n (Hnge : ¬ m > n) : ⊢ WP m > n {{ w, w ≡ vbool false }}.
   Proof. wp_bin. ev; simplify_eq/=. case_decide; by [|lia]. Qed.
 
-  Lemma setp_value Γ (T : olty Σ) v : Γ s⊨ v : T ⊣⊢ |==> ∀ ρ, sG⟦ Γ ⟧* ρ → T anil ρ v.[ρ].
+  Lemma setp_value Γ (T : olty Σ) v : Γ s⊨ v : T ⊣⊢ <PB> ∀ ρ, sG⟦ Γ ⟧* ρ → T anil ρ v.[ρ].
   Proof.
     rewrite /setp/=; properness => //; iSplit;
       [rewrite wp_value_inv|rewrite -wp_value]; iIntros "#$".
   Qed.
 
-  Lemma setp_value_eq (T : olty Σ) v : (|==> ∀ ρ, T anil ρ v.[ρ]) ⊣⊢ [] s⊨ v : T.
+  Lemma setp_value_eq (T : olty Σ) v : (<PB> ∀ ρ, T anil ρ v.[ρ]) ⊣⊢ [] s⊨ v : T.
   Proof.
-    iSplit.
-    - iIntros ">#H !>" (? _).
+    iSplit; pupd.
+    - iIntros "#H !>" (? _).
       rewrite /= -wp_value'. iApply "H".
-    - iIntros "/= >H !>" (ρ).
+    - iIntros "/= #H !>" (ρ).
       iSpecialize ("H" $! ρ with "[//]").
       by rewrite /= wp_value_inv'.
   Qed.
@@ -117,7 +117,7 @@ Section div_example.
   Lemma wp_if_ge :
     ⊢@{iPropI _} |==> ∀ (n : Z), WP hclose (hmkPosBodyV n) {{ w, ⌜ w =@{vl} n ∧ n > 0 ⌝}}.
   Proof using Type*.
-    iMod loopSemT as "#Hl"; iIntros "!> %n".
+    iDestruct loopSemT as "#>#Hl"; iIntros "!> %n".
     wp_bind (IfCtx _ _).
     wp_bin; ev; simplify_eq/=.
     case_decide; wp_pure; first by auto.
@@ -127,8 +127,8 @@ Section div_example.
   Lemma ty_mkPos :
     ⊢ [] s⊨ hmkPosV : oAll V⟦ 𝐙 ⟧ (olty0 (λI ρ v, ⌜ ∃ n : Z, v = n ∧ n > 0 ⌝)).
   Proof using Type*.
-    rewrite -sT_All_I /setp /= /shead; iMod wp_if_ge as "#Hge".
-    iIntros "!>" (ρ). rewrite /hsubst/hsubst_hoEnvD. rw.
+    rewrite -sT_All_I /setp /= /shead. iMod wp_if_ge as "#Hge".
+    pupd; iIntros "!>" (ρ). rewrite /hsubst/hsubst_hoEnvD. rw.
     iDestruct 1 as %(_ & n & Hw); simplify_eq/=; rewrite Hw.
     iApply wp_wand; [iApply "Hge" | naive_solver].
   Qed.
@@ -142,7 +142,7 @@ Section div_example.
   Close Scope Z_scope.
 
   Lemma sStp_ipos_nat Γ i : ⊢ Γ s⊨ ipos <:[ i ] oInt.
-  Proof. iIntros "!> % _ !%"; rewrite /pos /pure_interp_prim; naive_solver. Qed.
+  Proof. pupd; iIntros "!> % _ !%"; rewrite /pos /pure_interp_prim; naive_solver. Qed.
 
   Lemma posTMem_widen Γ l i : ⊢ Γ s⊨ oTMemL l ipos ipos <:[ i ] oTMemL l ⊥ oInt.
   Proof using Type*.
@@ -184,17 +184,17 @@ Section div_example.
     iApply suD_Cons; [done|iApply suD_posDm_ipos|].
     iApply suD_Cons; [done| iApply suD_Val|iApply suD_Sing; iApply suD_Val];
       iApply (suT_All_I_Strong _ _ _ HctxSub).
-    - unstamp_goal_tm; iMod wp_if_ge as "#Hge".
-      iIntros "!> %ρ [[_ [#Hpos _]] %Hnpos]"; lazy in Hnpos.
+    - pupd; unstamp_goal_tm; iMod wp_if_ge as "#Hge".
+      pupd; iIntros "!> %ρ [[_ [#Hpos _]] %Hnpos]"; lazy in Hnpos.
       case: Hnpos => [n Hw].
       iApply wp_wand; [rewrite /= {}Hw; iApply "Hge" |
         iIntros (v [-> Hnpos])].
       iEval rewrite /= path_wp_pv_eq.
       iApply (vl_sel_lb with "[] Hpos").
       iIntros "!%"; hnf. naive_solver.
     - iApply suT_All_I.
-      unstamp_goal_tm.
-      iIntros "!> %ρ #[[[_ [Hpos _]] %Hw] Harg]".
+      pupd; unstamp_goal_tm.
+      pupd; iIntros "!> %ρ #[[[_ [Hpos _]] %Hw] Harg]".
       rewrite /shead /stail. iSimpl.
       destruct Hw as [m ->].
       setoid_rewrite path_wp_pv_eq.

theories/Dot/examples/sem/semtyp_lemmas/sub_lr.v

@@ -18,7 +18,7 @@ Section defs.
 
   (** Legacy: (double)-indexed subtyping. *)
   Definition sstpi `{!dlangG Σ} i j Γ τ1 τ2 : iProp Σ :=
-    |==> sstpi' i j Γ τ1 τ2.
+    <PB> sstpi' i j Γ τ1 τ2.
   #[global] Arguments sstpi /.
 End defs.
 (** Indexed subtyping *)
@@ -41,6 +41,8 @@ End Propers.
 Section judgment_lemmas.
   Context `{!dlangG Σ}.
 
+  #[global] Instance sstpi_persistent i j Γ τ1 τ2 : Persistent (sstpi i j Γ τ1 τ2) := _.
+
   Lemma sstpi_app ρ Γ (T1 T2 : olty Σ) i j :
     sstpi' i j Γ T1 T2 -∗ sG⟦ Γ ⟧* ρ -∗
     oClose (oLaterN i T1) ρ ⊆ oClose (oLaterN j T2) ρ.
@@ -71,7 +73,7 @@ Section StpLemmas.
     (*───────────────────────────────*)
     Γ s⊨p p : T2, i + j.
   Proof.
-    iIntros ">#HpT1 >#Hsub !> %ρ #Hg".
+    pupd; iIntros "#HpT1 #Hsub !> %ρ #Hg".
     iSpecialize ("HpT1" with "Hg").
     rewrite !path_wp_eq.
     iDestruct "HpT1" as (v) "Hpv"; iExists v.

theories/Dot/examples/sem/small_sem_ex.v

@@ -60,8 +60,8 @@ Section small_ex.
       iApply suD_Cons; [done| by iApply suD_posDm_ipos | ].
       iApply suD_Sing; iApply suD_Val.
       iApply (suT_Sub (T1 := ipos)).
-      unstamp_goal_tm.
-      by rewrite setp_value /ipos /pos; iIntros "!> %ρ _ /= !%"; naive_solver.
+      pupd; unstamp_goal_tm.
+      rewrite setp_value /ipos /pos; pupd; iIntros "!> %ρ _ /= !%"; naive_solver.
       iApply sStp_Trans; first iApply sStp_Add_Later.
       iApply sStp_Trans; first iApply sStp_Add_Later.
       iApply sLater_Stp_Eq.

theories/Dot/examples/sem/syntyp_lemmas/examples_lr_syn.v

@@ -42,7 +42,7 @@ Section Lemmas.
     (* We're stuck again! *)
     Fail iApply "Hsub".
     Restart. *)
-    rw. iIntros ">#Hsub >#Hp !> %ρ %v #Hg Heq".
+    rw. pupd. iIntros "#Hsub #Hp !> %ρ %v #Hg Heq".
     iSpecialize ("Hp" with "Hg").
     iAssert (▷^i ⟦ T1 ⟧ (v .: ρ) v)%I as "#HT1".
     by iNext i; iDestruct "Heq" as %Heq;
@@ -58,7 +58,7 @@ Section Lemmas.
     Γ ⊨p p : TMu T1, i -∗
     Γ ⊨ TSing p, i <: TMu T2, i.
   Proof.
-    rw. iIntros ">#Hsub >#Hp !> %ρ %v #Hg /= Heq"; iSpecialize ("Hp" with "Hg").
+    rw. pupd. iIntros "#Hsub #Hp !> %ρ %v #Hg /= Heq"; iSpecialize ("Hp" with "Hg").
     iSpecialize ("Hsub" $! ρ v with "[#$Hg] [#]"); iNext i;
       iDestruct "Heq" as %Heq;
       rewrite -(psubst_one_repl Hrepl1, psubst_one_repl Hrepl2) //
@@ -99,10 +99,11 @@ Section Lemmas.
   Proof. rw. rewrite interp_commute_subst. apply sT_Mu_E. Qed.
 
   Lemma suetp_var_lift1 {Γ} x T1 T2 :
-    (Γ s⊨ tv (ids x) : T1 -∗ Γ s⊨ tv (ids x) : T2) ⊢
+    □(Γ s⊨ tv (ids x) : T1 -∗ Γ s⊨ tv (ids x) : T2) ⊢
     Γ su⊨ tv (ids x) : T1 -∗ Γ su⊨ tv (ids x) : T2.
   Proof.
-    iIntros "#Hr #H1"; iMod (suetp_var with "H1") as "{H1} H1"; iModIntro.
+    iIntros "#Hr".
+    rewrite suetp_var. pupd; iIntros "#H1 !>".
     by iExists (tv (ids x)); iSplit; last iApply ("Hr" with "H1").
   Qed.
 

theories/Dot/examples/sem/syntyp_lemmas/sub_lr_syn.v

@@ -22,6 +22,6 @@ Section judgment_lemmas.
   (** ** Show this typing judgment is equivalent to the more direct definition. *)
   Lemma istpi_eq Γ T1 i T2 j :
     Γ ⊨ T1, i <: T2, j ⊣⊢
-    |==> ∀ ρ v, G⟦Γ⟧ ρ → ▷^i V⟦T1⟧ anil ρ v → ▷^j V⟦T2⟧ anil ρ v.
+    <PB> ∀ ρ v, G⟦Γ⟧ ρ → ▷^i V⟦T1⟧ anil ρ v → ▷^j V⟦T2⟧ anil ρ v.
   Proof. reflexivity. Qed.
 End judgment_lemmas.