Remove unneeded parts of upred.

theories/algebra/upred_bi.v

@@ -14,15 +14,22 @@ Proof.
     intros P Q. split.
     + intros HPQ; split; split=> x i; apply HPQ.
     + intros [HPQ HQP]; split=> x n; by split; [apply HPQ|apply HQP].
-  - intros n P Q HPQ. apply equiv_dist. by apply pure_iff.
+  - intros n P Q HPQ. apply equiv_dist. unseal; split => ?????; auto.
   - intros ?? Himpl; eapply pure_elim; eauto; intros. etransitivity; last eapply Himpl; eauto.
   - by unseal.
+  - intros P Q. unseal. by split=> n x y ?? [? ?].
+  - intros P Q. unseal. by split=> n x y ?? [? ?].
+  - intros P Q. unseal. by split=> n x y ??; left.
+  - intros P Q. unseal. by split=> n x y ??; right.
   - apply impl_intro_r.
-  - apply impl_elim_l'.
+  - intros P Q R HP. eapply impl_elim with Q; auto.
+    * etransitivity; last eapply HP. apply and_elim_l.
+    * apply and_elim_r.
   - intros; by apply forall_intro.
   - intros; by apply forall_elim.
   - intros; by apply exist_intro.
   - intros; by apply exist_elim.
+  - apply sep_mono.
   - intros; by rewrite left_id.
   - intros; by rewrite left_id.
   - intros; by rewrite comm.
@@ -86,6 +93,7 @@ Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin (ofe_mixin_of (uPred M))
                 uPred_later.
 Proof.
   split; try apply _; eauto with I.
+  - unseal; split=> n x y ???; simpl. rewrite /uPred_holds => //=.
   - (* a ≡ b ⊢ Ψ a → Ψ b *)
     intros A a b Ψ Hnonexp.
     unseal; split=> n x ? Hab n' x' y' ????? HΨ. eapply Hnonexp with n a; auto.
@@ -104,7 +112,7 @@ Proof.
   - by unseal. 
   - apply later_mono.
   - apply löb.
-  - intros. by rewrite later_forall.
+  - intros. unseal; by split=> -[|n] x y.
   - intros A Φ. unseal; split=> -[|[|n]] x y ?? Hsat /=; eauto.
     * by left. 
     * destruct Hsat as (a&?). right. by exists a.
@@ -131,18 +139,6 @@ Canonical Structure uPredSI (M : ucmraT) : sbi :=
   {| sbi_ofe_mixin := ofe_mixin_of (uPred M);
      sbi_bi_mixin := uPred_bi_mixin M; sbi_sbi_mixin := uPred_sbi_mixin M |}.
 
-(*
-Global Instance ownM_persistent {M: ucmraT} (a : M) :
-  cmra.Persistent a → Persistent (uPred_ownM a).
-Proof.
-  intros HPa. rewrite /Persistent. unseal.
-  split=> n x y ?? [a' Hx].
-  eapply uPred_mono with a y; eauto.
-  - exists (core a). by rewrite cmra_core_r persistent_core.
-  - by eexists.
-Qed.
-*)
-
 Global Notation "■ φ" := (uPred_pure φ%stdpp%type)
   (at level 20, right associativity) : bi_scope.
 Global Notation "⧆ P" := (bi_affinely P%I)
@@ -214,7 +210,7 @@ Proof. unseal; split=> n x y ??. rewrite /uPred_holds //=. Qed.
 Lemma uPred_affine_bi_affinely {M: ucmraT} (P: uPred M):
   uPred_affine P ⊣⊢  bi_affinely P.
 Proof.
-  rewrite affine_equiv. rewrite and_comm. by repeat unseal.
+  rewrite affine_equiv. rewrite comm. by repeat unseal.
 Qed.
 
 Global Instance valid_persistent {M: ucmraT} {A : cmraT} (a : A) :
@@ -222,7 +218,7 @@ Global Instance valid_persistent {M: ucmraT} {A : cmraT} (a : A) :
 Proof.
   intros; rewrite /Persistent. rewrite -uPred_affine_bi_affinely.
   rewrite -{1}relevant_valid. unfold_bi. rewrite -unlimited_persistent.
-  by rewrite relevant_affine affine_affine0.
+  by rewrite relevant_affine affine_affine_idemp.
 Qed.
 
 Global Instance ownM_persistent {M: ucmraT} (a: M) :
@@ -230,14 +226,14 @@ Global Instance ownM_persistent {M: ucmraT} (a: M) :
 Proof.
   intros; rewrite /Persistent. rewrite -uPred_affine_bi_affinely.
   unfold_bi. rewrite -unlimited_persistent.
-  rewrite relevant_affine unlimited_ownM affine_affine0 //=.
+  rewrite relevant_affine unlimited_ownM affine_affine_idemp //=.
 Qed.
 Global Instance ownMl_relevant {M: ucmraT} (a: M) :
   cmra.Persistent a → Persistent (⧆(@uPred_ownMl M a)).
 Proof.
   intros; rewrite /Persistent. rewrite -uPred_affine_bi_affinely.
   unfold_bi. rewrite -unlimited_persistent.
-  rewrite relevant_affine relevant_ownMl affine_affine0 //=.
+  rewrite relevant_affine relevant_ownMl affine_affine_idemp //=.
 Qed.
 
 Class ATimeless {PROP: sbi} (P: PROP)
@@ -341,11 +337,17 @@ Section ATimeless_uPred.
   Proof.
     rewrite /ATimeless.
     rewrite -?uPred_affine_bi_affinely.
-    unfold_bi. rewrite -unlimited_affine_persistent.
+    rewrite -unlimited_affine_persistent.
     rewrite -relevant_affine affine_relevant_later.
-    rewrite -relevant_affine. rewrite {2}(affine_elim P) => ->.
-    rewrite except_0_relevant. apply except_0_mono. rewrite relevant_affine.
-      by rewrite affine_affine0.
+    rewrite -relevant_affine.
+    rewrite ?uPred_affine_bi_affinely => H.
+    rewrite relevant_mono; last first.
+    { apply affinely_mono. eauto. }
+    rewrite -?uPred_affine_bi_affinely.
+    rewrite -relevant_affine affine_affine_idemp.
+    rewrite -except_0_relevant. apply relevant_mono.
+    rewrite ?(uPred_affine_bi_affinely).
+    rewrite {1}(affinely_elim P) H. done.
   Qed.
 
   Global Instance eq_atimeless {A : ofeT} (a b : A) :
@@ -357,46 +359,6 @@ Section ATimeless_uPred.
   Global Instance pure_atimeless φ : ATimeless (bi_pure φ : uPred M).
   Proof. apply timeless_atimeless, _. Qed.
 
-(*
-Global Instance sep_atimeless_2 P Q: 
-  Affine P → Affine Q → ATimeless P → ATimeless Q → ATimeless (P ★ Q).
-Proof.
-  intros; rewrite /ATimeless.
-  rewrite affine_affinely.
-  rewrite except_0_sep.
-  rewrite -(affine_affinely P).
-  rewrite -(affine_affinely Q).
-  rewrite later_sep.
-  rewrite later_sep.
-  rewrite (atimeless P) (atimelessP Q).
-  rewrite sep_or_l. rewrite sep_or_r.
-  apply or_elim.
-  - apply or_elim.
-    * apply or_intro_l'. apply sep_affine_1.
-    * apply or_intro_r'. apply sep_elim_l.
-  - apply or_intro_r'. rewrite sep_or_r.
-    apply or_elim; first apply sep_elim_r.
-    unseal. split=> -[|n] x y ?? Hfalse /=; auto.
-    destruct Hfalse as (?&?&?&?&?&?&?&?). auto.
-Qed.
-Global Instance wand_atimeless P Q : AffineP P → ATimeless Q → ATimeless (P -★ Q).
-Proof.
-  rewrite !atimelessP_spec. 
-  unseal=> HA HP [|n] x ? HPQ [|n'] x' y' ??? HP'; auto.
-  apply affineP in HP'; eauto using cmra_validN_op_r.
-  revert HP'. unseal.
-  intros (HP'&Haff).
-  rewrite Haff ?right_id.
-  apply HP; auto.
-  specialize (HPQ 0 x' ∅). rewrite ?left_id in HPQ *=> HPQ.
-  eapply HPQ;
-    eauto 3 using cmra_validN_le, cmra_validN_op_r, cmra_validN_op_l, cmra_included_l.
-  apply uPred_closed with (S n');
-    eauto 3 using cmra_validN_le, cmra_validN_op_r, cmra_validN_op_l, cmra_included_l.
-  rewrite -Haff. eauto.
-Qed.
- *)
-
   Global Instance into_sep_affinely_later P Q1 Q2 :
     IntoSep P Q1 Q2 → Affine Q1 → Affine Q2 →
     IntoSep (bi_affinely (▷ P)) (bi_affinely (▷ Q1)) (bi_affinely (▷ Q2)).
@@ -411,12 +373,6 @@ Qed.
   Qed.
 End ATimeless_uPred.
 
-(*
-Global Instance elim_modal_affinely {M: ucmraT} (P Q: uPred M) :
-  ElimModal True (bi_affinely P) P Q Q.
-Proof. by rewrite /ElimModal bi.affinely_elim bi.wand_elim_r. Qed.
-*)
-
 Global Instance into_except_0_affine_later {PROP : sbi} (P : PROP):
   ATimeless P → IntoExcept0 (⧆▷ P) (⧆P).
 Proof.
@@ -434,7 +390,17 @@ Proof.
 Qed.
 
 Lemma pure_elim_sep_l {M: ucmraT} (φ : Prop) (Q R: uPred M) : (φ → Q ⊢ R) → ⧆■ φ ★ Q ⊢ R.
-Proof. rewrite -?uPred_affine_bi_affinely. unfold_bi. apply pure_elim_sep_l. Qed.
+Proof. rewrite -?uPred_affine_bi_affinely. unfold_bi.
+  intros H. eapply (pure_elim_spare φ _ Q); auto.
+  rewrite ?uPred_affine_bi_affinely.
+  iIntros (?) "(?&?)". iApply H; eauto.
+Qed.
+
+Lemma sep_affine_3 {M: ucmraT} (P Q: uPred M):
+   (⧆ (⧆ P ★ Q)) ⊢ (⧆ P ★ ⧆ Q).
+Proof.
+  rewrite -?uPred_affine_bi_affinely; unfold_bi. apply sep_affine_3.
+Qed.
 
 Tactic Notation "iApply" open_constr(lem) "in" open_constr(H) :=
   let Hfresh := iFresh in

theories/locks/lock_reln.v

@@ -201,11 +201,11 @@ Section lr.
          reflexivity.
   Qed.
 
-  Lemma expr_rel_aff_pres (vrel: valC -n> valC -n> iProp): (∀ v v', AffineP (vrel v v')) → 
+  Lemma expr_rel_aff_pres (vrel: valC -n> valC -n> iProp): 
                                 ∀ e e', Affine (expr_rel_lift vrel e e'). 
   Proof. apply _.  Qed.
 
-  Lemma expr_rel_rel_pres (vrel: valC -n> valC -n> iProp): (∀ v v', RelevantP (vrel v v')) → 
+  Lemma expr_rel_rel_pres (vrel: valC -n> valC -n> iProp):
                                 ∀ e e', Persistent (expr_rel_lift vrel e e'). 
   Proof. apply _. Qed. 
 

theories/locks/ticket_clh_triples.v

@@ -531,11 +531,9 @@ Section proof.
     rewrite /is_lock; intros; apply _.
   Qed.
 
-  (* TODO: either I'm using this in an unintended way, or there are some
-     obvious lemmas missing from library about STS and core *)
   Instance sts_empty_relevant: Persistent (sts_ownS γ (sts.up s ∅) ∅).
   Proof.
-    rewrite /RelevantP /sts_ownS => γ n. 
+    rewrite /sts_ownS => γ n. 
     apply own_core_persistent.
     rewrite /Persistent /pcore /cmra_pcore //=.
     rewrite /dra.validity_pcore //=.

theories/program_logic/adequacy_inf.v

@@ -559,7 +559,7 @@ Section bounded_nondet_hom2.
     - econstructor; [|econstructor].
       rewrite /ht wp_eq in Hht *.
       rewrite bi.affinely_persistently_elim in Hht * => Hht.
-      eapply wand_entails in Hht.
+      eapply bi.wand_entails in Hht.
       eapply Hht.
       
       * split_and!; simpl; try econstructor; auto.

theories/program_logic/pviewshifts.v

@@ -94,24 +94,6 @@ Proof.
   destruct (HP k Ef σ rf rfl) as (r2&?&?); eauto.
   exists r2; eauto using uPred_in_entails.
 Qed.
-Lemma pvs_timeless E P : TimelessP P → ▷ P ={E}=> P.
-Proof.
-  rewrite /pvs_FUpd pvs_eq uPred.timelessP_spec=> HP.
-  rewrite /pvs_FUpd.
-  uPred.unseal; split=>-[|n] r ? HP' k Ef σ rf ???; first lia.
-  exists r; split; last done.
-  apply HP, uPred_closed with n; eauto using cmra_validN_le.
-Qed.
-Lemma pvs_timeless_affine E P : ATimelessP P → ⧆▷ P ={E}=> ⧆P.
-Proof.
-  rewrite /pvs_FUpd pvs_eq uPred.atimelessP_spec=> HP.
-  repeat unseal; split=>-[|n] r rl ?? [Haff HP'] k Ef σ ???; first lia.
-  exists r; split; last done.
-  split.
-  - rewrite (dist_le _ _ _ _ Haff); auto; split; eauto.
-  - rewrite (dist_le _ _ _ _ Haff); auto. apply HP, uPred_closed with n; eauto using cmra_validN_le.
-    rewrite -(dist_le _ _ _ _ Haff); auto; split; eauto.
-Qed.
 Lemma pvs_trans E1 E2 E3 P :
   E2 ⊆ E1 ∪ E3 → (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=> P.
 Proof.
@@ -236,37 +218,12 @@ Lemma pvs_strip_pvs E P Q : (P ={E}=> Q) → (|={E}=> P) ={E}=> Q.
 Proof. move=>->. by rewrite pvs_trans'. Qed.
 Lemma pvs_frame_l E1 E2 P Q : (P ∗ |={E1,E2}=> Q) ⊢ |={E1,E2}=> P ∗ Q.
 Proof. rewrite !(comm _ P%I); apply pvs_frame_r. Qed.
-Lemma pvs_always_l E1 E2 P Q `{!RelevantP P} :
-  P ∧ (|={E1,E2}=> Q) ⊢ |={E1,E2}=> P ∗ Q.
-Proof.
-  rewrite -{1}(relevant_relevant' P); unfold_bi.
-  rewrite !relevant_and_sep_l_1 pvs_frame_l relevant_elim //=.
-Qed.
-Lemma pvs_always_r E1 E2 P Q `{!RelevantP Q} :
-  (|={E1,E2}=> P) ∧ Q ⊢ |={E1,E2}=> P ∗ Q.
-Proof. rewrite -(comm _ Q) -(comm _ Q). eapply pvs_always_l; auto. Qed.
 Lemma pvs_wand_l E1 E2 P Q : (P -∗ Q) ∗ (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q.
 Proof. by rewrite pvs_frame_l wand_elim_l. Qed.
 Lemma pvs_wand_r E1 E2 P Q : (|={E1,E2}=> P) ∗ (P -∗ Q) ={E1,E2}=> Q.
 Proof. by rewrite pvs_frame_r wand_elim_r. Qed.
 Lemma pvs_sep E P Q : (|={E}=> P) ∗ (|={E}=> Q) ={E}=> P ∗ Q.
 Proof. rewrite pvs_frame_r pvs_frame_l pvs_trans //. set_solver. Qed.
-(*
-Lemma pvs_big_sepM `{Countable K} {A} E (Φ : K → A → iProp Λ Σ) (m : gmap K A) :
-  ([∗ map] k↦x ∈ m, |={E}=> Φ k x) ={E}=> [∗ map] k↦x ∈ m, Φ k x.
-Proof.
-  rewrite /uPred_big_sepM.
-  induction (map_to_list m) as [|[i x] l IH]; csimpl; auto using pvs_intro.
-  by rewrite IH pvs_sep.
-Qed.
-Lemma pvs_big_sepS `{Countable A} E (Φ : A → iProp Λ Σ) X :
-  ([∗ set] x ∈ X, |={E}=> Φ x) ={E}=> [∗ set] x ∈ X, Φ x.
-Proof.
-  rewrite /uPred_big_sepS.
-  induction (elements X) as [|x l IH]; csimpl; csimpl; auto using pvs_intro.
-  by rewrite IH pvs_sep.
-Qed.
-*)
 
 Lemma pvs_mask_frame' E1 E1' E2 E2' P :
   E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' → (|={E1',E2'}=> P) ={E1,E2}=> P.
@@ -302,7 +259,7 @@ Proof. auto using pvs_mask_frame'. Qed.
 Lemma pvs_ownG_update E m m' : m ~~> m' → ownG m ={E}=> ownG m'.
 Proof.
   intros; rewrite (pvs_ownG_updateP E _ (m' =)); last by apply cmra_update_updateP.
-  by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.pure_elim_l=> ->.
+  by apply pvs_mono, uPred.exist_elim=> m''; apply pure_elim_l=> ->.
 Qed.
 
 Lemma except_0_pvs E1 E2 P : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P.

theories/program_logic/saved_prop.v

@@ -42,8 +42,6 @@ Section saved_prop.
     { intros z. rewrite /G1 /G2 -cFunctor_compose -{2}[z]cFunctor_id.
       apply (ne_proper (cFunctor_map F)); split=>?; apply iProp_fold_unfold. }
     rewrite -{2}[x]help -{2}[y]help. apply bi.affinely_mono. apply later_mono.
-    apply (eq_rewrite (G1 x) (G1 y) (λ z, G2 (G1 x) ≡ G2 z))%I; auto with I.
-    { intros ? ?? ->. auto. }
-     iIntros "Heq". rewrite //=.
+    iIntros "Heq". by iRewrite "Heq".
   Qed.
 End saved_prop.

theories/program_logic/viewshifts.v

@@ -44,10 +44,6 @@ Qed.
 Lemma vs_false_elim E1 E2 P : False ={E1,E2}=> P.
 Proof. by iIntros "[]". Qed.
 
-Lemma vs_timeless E P : TimelessP P → ▷ P ={E}=> P.
-Proof. by apply pvs_timeless. Qed.
-
-
 Lemma vs_transitive E1 E2 E3 P Q R :
   E2 ⊆ E1 ∪ E3 → ((P ={E1,E2}=> Q) ★ (Q ={E2,E3}=> R)) ⊢ (P ={E1,E3}=> R).
 Proof.

theories/tests/heap_lang.v

@@ -243,12 +243,6 @@ Section LiftingTests.
         iAlways; iFrame.
   Qed.
 
-  Lemma sep_affine_3 {M: ucmraT} (P Q: uPred M):
-    (⧆ P ★ ⧆ Q) ⊣⊢ (⧆ (⧆ P ★ Q)).
-  Proof.
-    rewrite -?uPred_affine_bi_affinely; unfold_bi; apply sep_affine_3.
-  Qed.
-
   Lemma do_while_hoist_read K E (P Q: val → iProp) (e e': expr) (l: loc) q u0 i
     `{!Closed ["x"] e} `{!Closed ["x"] e'}:
     nclose heapN ⊆ E →
@@ -309,7 +303,7 @@ Section LiftingTests.
     - iApply wp_mono; last iAssumption.
       iIntros (v) "(?&H1&?)". 
       rewrite -(bi.affine_affinely (l ↦s{q} u0)%I).
-      iFrame. rewrite {1}comm -sep_affine_3. iDestruct "H1" as "(?&?)"; iFrame. 
+      iFrame. rewrite {1}comm. rewrite upred_bi.sep_affine_3. iDestruct "H1" as "(?&?)"; iFrame. 
   Qed.
   
   Lemma reorder_writes E vold1 vold2 (l1 l1': loc) (v1: val) (l2 l2': loc) (v2: val) i K: