Merge branch 'jh/bupd_fupd_classes' into 'gen_proofmode'

Type classes for fancy updates and basic updates.

See merge request FP/iris-coq!101

_CoqProject

@@ -29,6 +29,7 @@ theories/bi/interface.v
 theories/bi/derived_connectives.v
 theories/bi/derived_laws.v
 theories/bi/big_op.v
+theories/bi/updates.v
 theories/bi/bi.v
 theories/bi/tactics.v
 theories/bi/fractional.v

theories/base_logic/derived.v

@@ -58,9 +58,10 @@ Proof.
 Qed.
 
 (** * Derived rules *)
-Global Instance bupd_mono' : Proper ((⊢) ==> (⊢)) (@uPred_bupd M).
+Global Instance bupd_mono' : Proper ((⊢) ==> (⊢)) (@bupd _ (@uPred_bupd M)).
 Proof. intros P Q; apply bupd_mono. Qed.
-Global Instance bupd_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (@uPred_bupd M).
+Global Instance bupd_flip_mono' :
+  Proper (flip (⊢) ==> flip (⊢)) (@bupd _ (@uPred_bupd M)).
 Proof. intros P Q; apply bupd_mono. Qed.
 Lemma bupd_frame_l R Q : (R ∗ |==> Q) ==∗ R ∗ Q.
 Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed.
@@ -77,7 +78,7 @@ Proof.
 Qed.
 Lemma except_0_bupd P : ◇ (|==> P) ⊢ (|==> ◇ P).
 Proof.
-  rewrite /sbi_except_0. apply or_elim; auto using bupd_mono, or_intro_r.
+  rewrite /sbi_except_0. apply or_elim; eauto using bupd_mono, or_intro_r.
   by rewrite -bupd_intro -or_intro_l.
 Qed.
 

theories/base_logic/lib/fancy_updates.v

@@ -7,85 +7,64 @@ Set Default Proof Using "Type".
 Export invG.
 Import uPred.
 
-Program Definition fupd_def `{invG Σ}
-    (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
+Definition uPred_fupd_def `{invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
   (wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P))%I.
-Definition fupd_aux : seal (@fupd_def). by eexists. Qed.
-Definition fupd := unseal fupd_aux.
-Definition fupd_eq : @fupd = @fupd_def := seal_eq fupd_aux.
-Arguments fupd {_ _} _ _ _%I.
-Instance: Params (@fupd) 4.
-
-Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
-  (at level 99, E1, E2 at level 50, Q at level 200,
-   format "|={ E1 , E2 }=>  Q") : bi_scope.
-Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I
-  (at level 99, E1,E2 at level 50, Q at level 200,
-   format "P  ={ E1 , E2 }=∗  Q") : bi_scope.
-Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)
-  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
-
-Notation "|={ E }=> Q" := (fupd E E Q)
-  (at level 99, E at level 50, Q at level 200,
-   format "|={ E }=>  Q") : bi_scope.
-Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I
-  (at level 99, E at level 50, Q at level 200,
-   format "P  ={ E }=∗  Q") : bi_scope.
-Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)
-  (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope.
+Definition uPred_fupd_aux `{invG Σ} : seal uPred_fupd_def. by eexists. Qed.
+Instance uPred_fupd `{invG Σ} : FUpd (iProp Σ):= unseal uPred_fupd_aux.
+Definition uPred_fupd_eq `{invG Σ} : fupd = uPred_fupd_def := seal_eq uPred_fupd_aux.
 
 Section fupd.
 Context `{invG Σ}.
 Implicit Types P Q : iProp Σ.
 
-Global Instance fupd_ne E1 E2 : NonExpansive (@fupd Σ _ E1 E2).
-Proof. rewrite fupd_eq. solve_proper. Qed.
-Global Instance fupd_proper E1 E2 : Proper ((≡) ==> (≡)) (@fupd Σ _ E1 E2).
+Global Instance fupd_ne E1 E2 : NonExpansive (fupd E1 E2).
+Proof. rewrite uPred_fupd_eq. solve_proper. Qed.
+Global Instance fupd_proper E1 E2 : Proper ((≡) ==> (≡)) (fupd E1 E2).
 Proof. apply ne_proper, _. Qed.
 
 Lemma fupd_intro_mask E1 E2 P : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P.
 Proof.
   intros (E1''&->&?)%subseteq_disjoint_union_L.
-  rewrite fupd_eq /fupd_def ownE_op //.
+  rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
   by iIntros "$ ($ & $ & HE) !> !> [$ $] !> !>" .
 Qed.
 
 Lemma except_0_fupd E1 E2 P : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P.
-Proof. rewrite fupd_eq. iIntros ">H [Hw HE]". iApply "H"; by iFrame. Qed.
+Proof. rewrite uPred_fupd_eq. iIntros ">H [Hw HE]". iApply "H"; by iFrame. Qed.
 
 Lemma bupd_fupd E P : (|==> P) ={E}=∗ P.
-Proof. rewrite fupd_eq /fupd_def. by iIntros ">? [$ $] !> !>". Qed.
+Proof. rewrite uPred_fupd_eq. by iIntros ">? [$ $] !> !>". Qed.
 
 Lemma fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q.
 Proof.
-  rewrite fupd_eq /fupd_def. iIntros (HPQ) "HP HwE".
-  rewrite -HPQ. by iApply "HP".
+  rewrite uPred_fupd_eq. iIntros (HPQ) "HP HwE". rewrite -HPQ. by iApply "HP".
 Qed.
 
 Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P.
 Proof.
-  rewrite fupd_eq /fupd_def. iIntros "HP HwE".
+  rewrite uPred_fupd_eq. iIntros "HP HwE".
   iMod ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
 Qed.
 
 Lemma fupd_mask_frame_r' E1 E2 Ef P :
   E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P.
 Proof.
-  intros. rewrite fupd_eq /fupd_def ownE_op //. iIntros "Hvs (Hw & HE1 &HEf)".
+  intros. rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
+  iIntros "Hvs (Hw & HE1 &HEf)".
   iMod ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
   iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
   iIntros "!> !>". by iApply "HP".
 Qed.
 
 Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q.
-Proof. rewrite fupd_eq /fupd_def. by iIntros "[HwP $]". Qed.
+Proof. rewrite uPred_fupd_eq /uPred_fupd_def. by iIntros "[HwP $]". Qed.
 
 Lemma fupd_plain' E1 E2 E2' P Q `{!Plain P} :
   E1 ⊆ E2 →
   (Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P.
 Proof.
   iIntros ((E3&->&HE)%subseteq_disjoint_union_L) "HQP HQ".
-  rewrite fupd_eq /fupd_def ownE_op //. iIntros "H".
+  rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //. iIntros "H".
   iMod ("HQ" with "H") as ">(Hws & [HE1 HE3] & HQ)"; iModIntro.
   iAssert (◇ P)%I as "#HP".
   { by iMod ("HQP" with "HQ [$]") as "(_ & _ & HP)". }
@@ -94,16 +73,16 @@ Qed.
 
 Lemma later_fupd_plain E P `{!Plain P} : (▷ |={E}=> P) ={E}=∗ ▷ ◇ P.
 Proof.
-  rewrite fupd_eq /fupd_def. iIntros "HP [Hw HE]".
+  rewrite uPred_fupd_eq /uPred_fupd_def. iIntros "HP [Hw HE]".
   iAssert (▷ ◇ P)%I with "[-]" as "#$"; last by iFrame.
   iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
 Qed.
 
 (** * Derived rules *)
-Global Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (@fupd Σ _ E1 E2).
+Global Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (fupd E1 E2).
 Proof. intros P Q; apply fupd_mono. Qed.
 Global Instance fupd_flip_mono' E1 E2 :
-  Proper (flip (⊢) ==> flip (⊢)) (@fupd Σ _ E1 E2).
+  Proper (flip (⊢) ==> flip (⊢)) (fupd E1 E2).
 Proof. intros P Q; apply fupd_mono. Qed.
 
 Lemma fupd_intro E P : P ={E}=∗ P.

theories/base_logic/lib/invariants.v

@@ -45,7 +45,7 @@ Qed.
 
 Lemma inv_alloc N E P : ▷ P ={E}=∗ inv N P.
 Proof.
-  rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros "HP [Hw $]".
+  rewrite inv_eq /inv_def uPred_fupd_eq. iIntros "HP [Hw $]".
   iMod (ownI_alloc (∈ (↑N : coPset)) P with "[$HP $Hw]")
     as (i ?) "[$ ?]"; auto using fresh_inv_name.
 Qed.
@@ -53,7 +53,7 @@ Qed.
 Lemma inv_alloc_open N E P :
   ↑N ⊆ E → (|={E, E∖↑N}=> inv N P ∗ (▷P ={E∖↑N, E}=∗ True))%I.
 Proof.
-  rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros (Sub) "[Hw HE]".
+  rewrite inv_eq /inv_def uPred_fupd_eq. iIntros (Sub) "[Hw HE]".
   iMod (ownI_alloc_open (∈ (↑N : coPset)) P with "Hw")
     as (i ?) "(Hw & #Hi & HD)"; auto using fresh_inv_name.
   iAssert (ownE {[i]} ∗ ownE (↑ N ∖ {[i]}) ∗ ownE (E ∖ ↑ N))%I
@@ -72,7 +72,7 @@ Qed.
 Lemma inv_open E N P :
   ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ ▷ P ∗ (▷ P ={E∖↑N,E}=∗ True).
 Proof.
-  rewrite inv_eq /inv_def fupd_eq /fupd_def; iDestruct 1 as (i) "[Hi #HiP]".
+  rewrite inv_eq /inv_def uPred_fupd_eq /uPred_fupd_def; iDestruct 1 as (i) "[Hi #HiP]".
   iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
   rewrite {1 4}(union_difference_L (↑ N) E) // ownE_op; last set_solver.
   rewrite {1 5}(union_difference_L {[ i ]} (↑ N)) // ownE_op; last set_solver.

theories/base_logic/upred.v

 From iris.algebra Require Export cmra updates.
-From iris.bi Require Export derived_connectives.
+From iris.bi Require Export derived_connectives updates.
 From stdpp Require Import finite.
 Set Default Proof Using "Type".
 Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|].
@@ -328,16 +328,17 @@ Next Obligation.
   apply uPred_mono with x'; eauto using cmra_includedN_l.
 Qed.
 Next Obligation. naive_solver. Qed.
-Definition uPred_bupd_aux : seal (@uPred_bupd_def). by eexists. Qed.
-Definition uPred_bupd {M} := unseal uPred_bupd_aux M.
-Definition uPred_bupd_eq : @uPred_bupd = @uPred_bupd_def := seal_eq uPred_bupd_aux.
+Definition uPred_bupd_aux {M} : seal (@uPred_bupd_def M). by eexists. Qed.
+Instance uPred_bupd {M} : BUpd (uPred M) := unseal uPred_bupd_aux.
+Definition uPred_bupd_eq {M} :
+  @bupd _ uPred_bupd = @uPred_bupd_def M := seal_eq uPred_bupd_aux.
 
 Module uPred_unseal.
 Definition unseal_eqs :=
   (uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
   uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq,
   uPred_plainly_eq, uPred_persistently_eq, uPred_later_eq, uPred_ownM_eq,
-  uPred_cmra_valid_eq, uPred_bupd_eq).
+  uPred_cmra_valid_eq, @uPred_bupd_eq).
 Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
   unfold bi_emp; simpl;
   unfold uPred_emp, bi_pure, bi_and, bi_or, bi_impl, bi_forall, bi_exist,
@@ -566,12 +567,6 @@ Coercion uPred_valid {M} : uPred M → Prop := bi_valid.
 
 (* Latest notation *)
 Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope.
-Notation "|==> Q" := (uPred_bupd Q)
-  (at level 99, Q at level 200, format "|==>  Q") : bi_scope.
-Notation "P ==∗ Q" := (P ⊢ |==> Q)
-  (at level 99, Q at level 200, only parsing) : stdpp_scope.
-Notation "P ==∗ Q" := (P -∗ |==> Q)%I
-  (at level 99, Q at level 200, format "P  ==∗  Q") : bi_scope.
 
 Module uPred.
 Include uPred_unseal.
@@ -599,14 +594,15 @@ Qed.
 Global Instance cmra_valid_proper {A : cmraT} :
   Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
 
-Global Instance bupd_ne : NonExpansive (@uPred_bupd M).
+Global Instance bupd_ne : NonExpansive (@bupd _ (@uPred_bupd M)).
 Proof.
   intros n P Q HPQ.
   unseal; split=> n' x; split; intros HP k yf ??;
     destruct (HP k yf) as (x'&?&?); auto;
     exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
 Qed.
-Global Instance bupd_proper : Proper ((≡) ==> (≡)) (@uPred_bupd M) := ne_proper _.
+Global Instance bupd_proper :
+  Proper ((≡) ==> (≡)) (@bupd _ (@uPred_bupd M)) := ne_proper _.
 
 (** BI instances *)
 

theories/bi/bi.v

-From iris.bi Require Export derived_laws big_op.
+From iris.bi Require Export derived_laws big_op updates.
 Set Default Proof Using "Type".
 
 Module Import bi.

theories/bi/interface.v

@@ -522,4 +522,5 @@ Proof. eapply (sbi_mixin_later_persistently_2 bi_entails), sbi_sbi_mixin. Qed.
 Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
 Proof. eapply sbi_mixin_later_false_em, sbi_sbi_mixin. Qed.
 End sbi_laws.
+
 End bi.

theories/bi/updates.v

+From stdpp Require Import coPset.
+From iris.bi Require Import interface.
+
+Class BUpd (A : Type) : Type := bupd : A → A.
+Instance : Params (@bupd) 2.
+
+Notation "|==> Q" := (bupd Q)
+  (at level 99, Q at level 200, format "|==>  Q") : bi_scope.
+Notation "P ==∗ Q" := (P ⊢ |==> Q)
+  (at level 99, Q at level 200, only parsing) : stdpp_scope.
+Notation "P ==∗ Q" := (P -∗ |==> Q)%I
+  (at level 99, Q at level 200, format "P  ==∗  Q") : bi_scope.
+
+Class FUpd (A : Type) : Type := fupd : coPset → coPset → A → A.
+Instance: Params (@fupd) 4.
+
+Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "|={ E1 , E2 }=>  Q") : bi_scope.
+Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I
+  (at level 99, E1,E2 at level 50, Q at level 200,
+   format "P  ={ E1 , E2 }=∗  Q") : bi_scope.
+Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)
+  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
+
+Notation "|={ E }=> Q" := (fupd E E Q)
+  (at level 99, E at level 50, Q at level 200,
+   format "|={ E }=>  Q") : bi_scope.
+Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I
+  (at level 99, E at level 50, Q at level 200,
+   format "P  ={ E }=∗  Q") : bi_scope.
+Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)
+  (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope.

theories/program_logic/adequacy.v

@@ -73,7 +73,7 @@ Lemma wp_step e1 σ1 e2 σ2 efs Φ :
   world σ1 ∗ WP e1 {{ Φ }} ==∗ ▷ |==> ◇ (world σ2 ∗ WP e2 {{ Φ }} ∗ wptp efs).
 Proof.
   rewrite {1}wp_unfold /wp_pre. iIntros (?) "[(Hw & HE & Hσ) H]".
-  rewrite (val_stuck e1 σ1 e2 σ2 efs) // fupd_eq /fupd_def.
+  rewrite (val_stuck e1 σ1 e2 σ2 efs) // uPred_fupd_eq.
   iMod ("H" $! σ1 with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
   iModIntro; iNext.
   iMod ("H" $! e2 σ2 efs with "[%] [$Hw $HE]") as ">($ & $ & $ & $)"; auto.
@@ -125,7 +125,7 @@ Lemma wptp_result n e1 t1 v2 t2 σ1 σ2 φ :
 Proof.
   intros. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
   iDestruct 1 as (e2 t2' ?) "((Hw & HE & _) & H & _)"; simplify_eq.
-  iDestruct (wp_value_inv with "H") as "H". rewrite fupd_eq /fupd_def.
+  iDestruct (wp_value_inv with "H") as "H". rewrite uPred_fupd_eq.
   iMod ("H" with "[Hw HE]") as ">(_ & _ & $)"; iFrame; auto.
 Qed.
 
@@ -133,8 +133,8 @@ Lemma wp_safe e σ Φ :
   world σ -∗ WP e {{ Φ }} ==∗ ▷ ⌜is_Some (to_val e) ∨ reducible e σ⌝.
 Proof.
   rewrite wp_unfold /wp_pre. iIntros "(Hw&HE&Hσ) H".
-  destruct (to_val e) as [v|] eqn:?; [eauto 10|].
-  rewrite fupd_eq. iMod ("H" with "Hσ [-]") as ">(?&?&%&?)"; eauto 10 with iFrame.
+  destruct (to_val e) as [v|] eqn:?; [eauto 10|]. rewrite uPred_fupd_eq.
+  iMod ("H" with "Hσ [-]") as ">(?&?&%&?)"; eauto 10 with iFrame.
 Qed.
 
 Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ :
@@ -157,7 +157,7 @@ Proof.
   intros ?. rewrite wptp_steps // bupd_iter_frame_l laterN_later.
   apply: bupd_iter_laterN_mono.
   iIntros "[Hback H]"; iDestruct "H" as (e2' t2' ->) "[(Hw&HE&Hσ) _]".
-  rewrite fupd_eq.
+  rewrite uPred_fupd_eq.
   iMod ("Hback" with "Hσ [$Hw $HE]") as "> (_ & _ & $)"; auto.
 Qed.
 End adequacy.
@@ -172,14 +172,14 @@ Proof.
   intros Hwp; split.
   - intros t2 σ2 v2 [n ?]%rtc_nsteps.
     eapply (soundness (M:=iResUR Σ) _ (S (S n))).
-    iMod wsat_alloc as (Hinv) "[Hw HE]".
-    rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
+    iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _).
+    rewrite uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
     iDestruct "Hwp" as (Istate) "[HI Hwp]".
     iApply (@wptp_result _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
   - intros t2 σ2 e2 [n ?]%rtc_nsteps ?.
     eapply (soundness (M:=iResUR Σ) _ (S (S n))).
-    iMod wsat_alloc as (Hinv) "[Hw HE]".
-    rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
+    iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _).
+    rewrite uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
     iDestruct "Hwp" as (Istate) "[HI Hwp]".
     iApply (@wptp_safe _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
 Qed.
@@ -194,8 +194,8 @@ Theorem wp_invariance Σ Λ `{invPreG Σ} e σ1 t2 σ2 φ :
 Proof.
   intros Hwp [n ?]%rtc_nsteps.
   eapply (soundness (M:=iResUR Σ) _ (S (S n))).
-  iMod wsat_alloc as (Hinv) "[Hw HE]".
-  rewrite {1}fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
+  iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _).
+  rewrite {1}uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
   iDestruct "Hwp" as (Istate) "(HIstate & Hwp & Hclose)".
   iApply (@wptp_invariance _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
 Qed.