Tweaks.

iris/algebra/lib/gmap_view.v

@@ -40,8 +40,9 @@ Section rel.
   It is possible that [∀ k, ∃ dq, let auth := (pair dq) <$> m !! k in ✓{n} auth
   ∧ f !! k ≼{n} auth] would also work, but now the proofs are all done already.  ;)
   The two are probably equivalent, with a proof similar to [lookup_includedN]? *)
-  Local Definition gmap_view_rel_raw n m f : Prop :=
-    map_Forall (λ k dv, ∃ v dq, m !! k = Some v ∧ ✓{n} (dq, v) ∧ (Some dv ≼{n} Some (dq, v))) f.
+  Local Definition gmap_view_rel_raw n m f :=
+    map_Forall (λ k dv,
+      ∃ v dq, m !! k = Some v ∧ ✓{n} (dq, v) ∧ (Some dv ≼{n} Some (dq, v))) f.
 
   Local Lemma gmap_view_rel_raw_mono n1 n2 m1 m2 f1 f2 :
     gmap_view_rel_raw n1 m1 f1 →
@@ -52,8 +53,8 @@ Section rel.
   Proof.
     intros Hrel Hm Hf Hn k [dqa va] Hk.
     (* For some reason applying the lemma in [Hf] does not work... *)
-    destruct (lookup_includedN n2 f2 f1) as [Hf' _]. specialize (Hf' Hf). clear Hf.
-    specialize (Hf' k). rewrite Hk in Hf'.
+    destruct (lookup_includedN n2 f2 f1) as [Hf' _].
+    specialize (Hf' Hf k). clear Hf. rewrite Hk in Hf'.
     destruct (Some_includedN_is_Some _ _ _ Hf') as [[q' va'] Heq]. rewrite Heq in Hf'.
     specialize (Hrel _ _ Heq) as (v & dq & Hm1 & [Hvval Hdqval] & Hvincl). simpl in *.
     specialize (Hm k).
@@ -61,7 +62,7 @@ Section rel.
     eexists. exists dq. split; first done. split.
     { split; first done. simpl. rewrite -Hv. eapply cmra_validN_le; done. }
     rewrite -Hv. etrans; first exact Hf'.
-    apply: cmra_includedN_le; eassumption.
+    apply: cmra_includedN_le; done.
   Qed.
 
   Local Lemma gmap_view_rel_raw_valid n m f :
@@ -228,9 +229,10 @@ Section lemmas.
   Qed.
 
   Lemma gmap_view_frag_op k dq1 dq2 v1 v2 :
-    gmap_view_frag k (dq1 ⋅ dq2) (v1 ⋅ v2) ≡ gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2.
+    gmap_view_frag k (dq1 ⋅ dq2) (v1 ⋅ v2) ≡
+      gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2.
   Proof. rewrite -view_frag_op singleton_op -pair_op //. Qed.
- Lemma gmap_view_frag_add k q1 q2 v1 v2 :
+  Lemma gmap_view_frag_add k q1 q2 v1 v2 :
     gmap_view_frag k (DfracOwn (q1 + q2)) (v1 ⋅ v2) ≡
       gmap_view_frag k (DfracOwn q1) v1 ⋅ gmap_view_frag k (DfracOwn q2) v2.
   Proof. rewrite -gmap_view_frag_op. done. Qed.
@@ -243,7 +245,8 @@ Section lemmas.
     by rewrite -pair_op pair_validN.
   Qed.
   Lemma gmap_view_frag_op_valid k dq1 dq2 v1 v2 :
-    ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔ ✓ (dq1 ⋅ dq2) ∧ ✓ (v1 ⋅ v2).
+    ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔
+      ✓ (dq1 ⋅ dq2) ∧ ✓ (v1 ⋅ v2).
   Proof.
     rewrite view_frag_valid. setoid_rewrite gmap_view_rel_exists.
     rewrite -cmra_valid_validN singleton_op singleton_valid.
@@ -252,7 +255,8 @@ Section lemmas.
 
   Lemma gmap_view_both_dfrac_validN n dp m k dq v :
     ✓{n} (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) ↔
-      ✓ dp ∧ ∃ v' dq', m !! k = Some v' ∧ ✓{n} (dq', v') ∧ Some (dq, v) ≼{n} Some (dq', v').
+      ✓ dp ∧ ∃ v' dq', m !! k = Some v' ∧ ✓{n} (dq', v') ∧
+        Some (dq, v) ≼{n} Some (dq', v').
   Proof.
     rewrite /gmap_view_auth /gmap_view_frag.
     rewrite view_both_dfrac_validN gmap_view_rel_lookup. done.
@@ -281,7 +285,9 @@ Section lemmas.
   (and [dq' > dq]) while at higher step-indices, [v] has no frame (and [dq' = dq]). *)
   Lemma gmap_view_both_dfrac_valid_discrete `{!CmraDiscrete V} dp m k dq v :
     ✓ (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) ↔
-    ✓ dp ∧ ∃ v' dq', m !! k = Some v' ∧ ✓ (dq', v') ∧ Some (dq, v) ≼ Some (dq', v').
+      ✓ dp ∧ ∃ v' dq', m !! k = Some v' ∧
+                       ✓ (dq', v') ∧
+                       Some (dq, v) ≼ Some (dq', v').
   Proof.
     rewrite cmra_valid_validN. setoid_rewrite gmap_view_both_dfrac_validN. split.
     - intros Hvalid. specialize (Hvalid 0).
@@ -294,7 +300,8 @@ Section lemmas.
       split; first by apply cmra_valid_validN.
       by apply: cmra_included_includedN.
   Qed.
-  Lemma gmap_view_both_dfrac_valid_discrete_total `{!CmraDiscrete V, !CmraTotal V} dp m k dq v :
+  Lemma gmap_view_both_dfrac_valid_discrete_total
+      `{!CmraDiscrete V, !CmraTotal V} dp m k dq v :
     ✓ (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) →
     ✓ dp ∧ ✓ dq ∧ ∃ v', m !! k = Some v' ∧ ✓ v' ∧ v ≼ v'.
   Proof.
@@ -327,7 +334,8 @@ Section lemmas.
     m !! k = None →
     ✓ dq →
     ✓ v →
-    gmap_view_auth (DfracOwn 1) m ~~> gmap_view_auth (DfracOwn 1) (<[k := v]> m) ⋅ gmap_view_frag k dq v.
+    gmap_view_auth (DfracOwn 1) m ~~>
+      gmap_view_auth (DfracOwn 1) (<[k := v]> m) ⋅ gmap_view_frag k dq v.
   Proof.
     intros Hfresh Hdq Hval. apply view_update_alloc=>n bf Hrel j [df va] /=.
     rewrite lookup_op. destruct (decide (j = k)) as [->|Hne].
@@ -352,9 +360,11 @@ Section lemmas.
     ✓ dq →
     map_Forall (λ k v, ✓ v) m' →
     gmap_view_auth (DfracOwn 1) m ~~>
-      gmap_view_auth (DfracOwn 1) (m' ∪ m) ⋅ ([^op map] k↦v ∈ m', gmap_view_frag k dq v).
+      gmap_view_auth (DfracOwn 1) (m' ∪ m) ⋅
+      ([^op map] k↦v ∈ m', gmap_view_frag k dq v).
   Proof.
-    intros ?? Hm'. induction m' as [|k v m' ? IH] using map_ind; decompose_map_disjoint.
+    intros ?? Hm'.
+    induction m' as [|k v m' ? IH] using map_ind; decompose_map_disjoint.
     { rewrite big_opM_empty left_id_L right_id. done. }
     rewrite IH //.
     2:{ by eapply map_Forall_insert_1_2. }
@@ -384,8 +394,9 @@ Section lemmas.
   Qed.
 
   Lemma gmap_view_delete_big m m' :
-    gmap_view_auth (DfracOwn 1) m ⋅ ([^op map] k↦v ∈ m', gmap_view_frag k (DfracOwn 1) v) ~~>
-    gmap_view_auth (DfracOwn 1) (m ∖ m').
+    gmap_view_auth (DfracOwn 1) m ⋅
+    ([^op map] k↦v ∈ m', gmap_view_frag k (DfracOwn 1) v) ~~>
+      gmap_view_auth (DfracOwn 1) (m ∖ m').
   Proof.
     induction m' as [|k v m' ? IH] using map_ind.
     { rewrite right_id_L big_opM_empty right_id //. }
@@ -401,18 +412,20 @@ Section lemmas.
      m !! k = Some mv → ✓{n} ((dq, v) ⋅? f) → mv ≡{n}≡ v ⋅? (snd <$> f) →
      ✓{n} ((dq', v') ⋅? f) ∧ mv' ≡{n}≡ v' ⋅? (snd <$> f)) →
     gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k dq v ~~>
-    gmap_view_auth (DfracOwn 1) (<[k := mv']> m) ⋅ gmap_view_frag k dq' v'.
+      gmap_view_auth (DfracOwn 1) (<[k := mv']> m) ⋅ gmap_view_frag k dq' v'.
   Proof.
     intros Hup. apply view_update=> n bf Hrel j [df va].
     rewrite lookup_op.
     destruct (decide (j = k)) as [->|Hne]; last first.
     { (* prove that other keys are unaffected *)
-      simplify_map_eq. rewrite lookup_singleton_ne //. (* FIXME simplify_map_eq should have done this *)
+      simplify_map_eq. rewrite lookup_singleton_ne //.
+      (* FIXME simplify_map_eq should have done this *)
       rewrite left_id. intros Hbf.
       edestruct (Hrel j) as (mva & mdf & Hlookup & Hval & Hincl).
       { rewrite lookup_op lookup_singleton_ne // left_id //. }
       naive_solver. }
-    simplify_map_eq. rewrite lookup_singleton. (* FIXME simplify_map_eq should have done this *)
+    simplify_map_eq. rewrite lookup_singleton.
+    (* FIXME simplify_map_eq should have done this *)
     intros Hbf.
     edestruct (Hrel k) as (mv & mdf & Hlookup & Hval & Hincl).
     { rewrite lookup_op lookup_singleton // Some_op_opM //. }
@@ -472,8 +485,10 @@ Section lemmas.
   Lemma gmap_view_replace_big m m0 m1 :
     dom m0 = dom m1 →
     map_Forall (λ k v, ✓ v) m1 →
-    gmap_view_auth (DfracOwn 1) m ⋅ ([^op map] k↦v ∈ m0, gmap_view_frag k (DfracOwn 1) v) ~~>
-      gmap_view_auth (DfracOwn 1) (m1 ∪ m) ⋅ ([^op map] k↦v ∈ m1, gmap_view_frag k (DfracOwn 1) v).
+    gmap_view_auth (DfracOwn 1) m ⋅
+    ([^op map] k↦v ∈ m0, gmap_view_frag k (DfracOwn 1) v) ~~>
+      gmap_view_auth (DfracOwn 1) (m1 ∪ m) ⋅
+      ([^op map] k↦v ∈ m1, gmap_view_frag k (DfracOwn 1) v).
   Proof.
     intros Hdom%eq_sym. revert m1 Hdom.
     induction m0 as [|k v m0 Hnotdom IH] using map_ind; intros m1 Hdom Hval.
@@ -511,7 +526,8 @@ Section lemmas.
   Proof.
     intros Hdq.
     eapply cmra_updateP_weaken;
-      [apply view_updateP_frag with (P := λ b', ∃ dq', ◯V b' = gmap_view_frag k dq' v ∧ P dq')
+      [apply view_updateP_frag
+         with (P := λ b', ∃ dq', ◯V b' = gmap_view_frag k dq' v ∧ P dq')
       |naive_solver].
     intros m n bf Hrel.
     destruct (Hrel k ((dq, v) ⋅? bf !! k)) as (v' & dq' & Hlookup & Hval & Hincl).
@@ -547,7 +563,8 @@ Section lemmas.
   Qed.
 
   Lemma gmap_view_frag_unpersist k v :
-    gmap_view_frag k DfracDiscarded v ~~>: λ a, ∃ q, a = gmap_view_frag k (DfracOwn q) v.
+    gmap_view_frag k DfracDiscarded v ~~>:
+      λ a, ∃ q, a = gmap_view_frag k (DfracOwn q) v.
   Proof.
     eapply cmra_updateP_weaken.
     { apply gmap_view_frag_dfrac, dfrac_undiscard_update. }
@@ -559,7 +576,8 @@ Section lemmas.
     CoreId dq → CoreId v → CoreId (gmap_view_frag k dq v).
   Proof. apply _. Qed.
 
-  Global Instance gmap_view_cmra_discrete : CmraDiscrete V → CmraDiscrete (gmap_viewR K V).
+  Global Instance gmap_view_cmra_discrete :
+    CmraDiscrete V → CmraDiscrete (gmap_viewR K V).
   Proof. apply _. Qed.
 
   Global Instance gmap_view_frag_mut_is_op dq dq1 dq2 k v v1 v2 :
@@ -616,7 +634,8 @@ Next Obligation.
   rewrite !lookup_fmap.
   destruct (f !! k) as [[df' va']|] eqn:Hfk; rewrite Hfk; last done.
   simpl=>[= <- <-].
-  specialize (Hrel _ _ Hfk). simpl in Hrel. destruct Hrel as (v & dq & Hlookup & Hval & Hincl).
+  specialize (Hrel _ _ Hfk). simpl in Hrel.
+  destruct Hrel as (v & dq & Hlookup & Hval & Hincl).
   eexists (rFunctor_map F fg v), dq.
   rewrite Hlookup. split; first done. split.
   - split; first by apply Hval. simpl. apply: cmra_morphism_validN. apply Hval.

iris/base_logic/algebra.v

@@ -146,11 +146,15 @@ Section upred.
     Qed.
 
     Lemma to_agree_includedI a b :
-      to_agree a ≼ to_agree b ⊢ a ≡ b.
+      to_agree a ≼ to_agree b ⊣⊢ a ≡ b.
     Proof.
-      apply bi.exist_elim=>c. rewrite internal_eq_sym.
-      rewrite agree_op_equiv_to_agreeI -agree_equivI.
-      apply internal_eq_trans.
+      apply (anti_symm _).
+      - apply bi.exist_elim=>c. rewrite internal_eq_sym.
+        rewrite agree_op_equiv_to_agreeI -agree_equivI.
+        apply internal_eq_trans.
+      - apply: (internal_eq_rewrite' _ _ (λ b, to_agree a ≼ to_agree b)%I);
+          [solve_proper|done|].
+        rewrite -internal_included_refl. apply bi.True_intro.
     Qed.
 
   End agree.

iris/base_logic/lib/ghost_map.v

@@ -62,29 +62,23 @@ Section lemmas.
   Proof. unseal. apply _. Qed.
   Global Instance ghost_map_elem_persistent k γ v : Persistent (k ↪[γ]□ v).
   Proof. unseal. apply _. Qed.
-  Global Instance ghost_map_elem_fractional k γ v : Fractional (λ q, k ↪[γ]{#q} v)%I.
-  Proof. unseal. intros p q. rewrite -own_op -gmap_view_frag_add agree_idemp //. Qed.
+  Global Instance ghost_map_elem_fractional k γ v :
+    Fractional (λ q, k ↪[γ]{#q} v)%I.
+  Proof. unseal=> p q. rewrite -own_op -gmap_view_frag_add agree_idemp //. Qed.
   Global Instance ghost_map_elem_as_fractional k γ q v :
     AsFractional (k ↪[γ]{#q} v) (λ q, k ↪[γ]{#q} v)%I q.
   Proof. split; first done. apply _. Qed.
 
   Local Lemma ghost_map_elems_unseal γ m dq :
     ([∗ map] k ↦ v ∈ m, k ↪[γ]{dq} v) ==∗
-    own γ ([^op map] k↦v ∈ m, gmap_view_frag (V:=agreeR (leibnizO V)) k dq (to_agree v)).
+    own γ ([^op map] k↦v ∈ m,
+      gmap_view_frag (V:=agreeR (leibnizO V)) k dq (to_agree v)).
   Proof.
     unseal. destruct (decide (m = ∅)) as [->|Hne].
     - rewrite !big_opM_empty. iIntros "_". iApply own_unit.
     - rewrite big_opM_own //. iIntros "?". done.
   Qed.
 
-  Local Lemma to_agree_map_valid m : map_Forall (λ _ (v : agreeR (leibnizO V)), ✓ v) (to_agree <$> m).
-  Proof.
-    (* FIXME use map_Forall_fmap *)
-    intros i v. rewrite lookup_fmap.
-    destruct (m !! i) as [y|] eqn:EQ; last done. simpl.
-    intros [= <-]. done.
-  Qed.
-
   Lemma ghost_map_elem_valid k γ dq v : k ↪[γ]{dq} v -∗ ⌜✓ dq⌝.
   Proof.
     unseal. iIntros "Helem".
@@ -96,7 +90,7 @@ Section lemmas.
   Proof.
     unseal. iIntros "H1 H2".
     iCombine "H1 H2" gives %[? Hag]%gmap_view_frag_op_valid.
-    iPureIntro. split; first done. rewrite to_agree_op_valid_L in Hag. done.
+    rewrite to_agree_op_valid_L in Hag. done.
   Qed.
   Lemma ghost_map_elem_agree k γ dq1 dq2 v1 v2 :
     k ↪[γ]{dq1} v1 -∗ k ↪[γ]{dq2} v2 -∗ ⌜v1 = v2⌝.
@@ -162,15 +156,16 @@ Section lemmas.
     ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ ghost_map_auth γ 1 m ∗ [∗ map] k ↦ v ∈ m, k ↪[γ] v.
   Proof.
     unseal. intros.
-    iMod (own_alloc_strong (gmap_view_auth (V:=agreeR (leibnizO V)) (DfracOwn 1) ∅) P)
+    iMod (own_alloc_strong
+      (gmap_view_auth (V:=agreeR (leibnizO V)) (DfracOwn 1) ∅) P)
       as (γ) "[% Hauth]"; first done.
     { apply gmap_view_auth_valid. }
     iExists γ. iSplitR; first done.
     rewrite -big_opM_own_1 -own_op. iApply (own_update with "Hauth").
-    etrans; first apply: (gmap_view_alloc_big (V:=agreeR (leibnizO V)) _ (to_agree <$> m) (DfracOwn 1)).
+    etrans; first apply (gmap_view_alloc_big _ (to_agree <$> m) (DfracOwn 1)).
     - apply map_disjoint_empty_r.
     - done.
-    - apply to_agree_map_valid.
+    - by apply map_Forall_fmap.
     - rewrite right_id big_opM_fmap. done.
   Qed.
   Lemma ghost_map_alloc_strong_empty P :
@@ -226,7 +221,8 @@ Section lemmas.
     ghost_map_auth γ q m -∗ k ↪[γ]{dq} v -∗ ⌜m !! k = Some v⌝.
   Proof.
     unseal. iIntros "Hauth Hel".
-    iCombine "Hauth Hel" gives %(_ & _ & (av' & Hav' & _ & Hincl))%gmap_view_both_dfrac_valid_discrete_total.
+    iCombine "Hauth Hel" gives
+      %(_ & _ & (av' & Hav' & _ & Hincl))%gmap_view_both_dfrac_valid_discrete_total.
     iPureIntro.
     apply lookup_fmap_Some in Hav' as [v' [<- Hv']].
     apply to_agree_included_L in Hincl. by rewrite Hincl.
@@ -297,7 +293,7 @@ Section lemmas.
     etrans; first apply: (gmap_view_alloc_big _ (to_agree <$> m') (DfracOwn 1)).
     - apply map_disjoint_fmap. done.
     - done.
-    - apply to_agree_map_valid.
+    - by apply map_Forall_fmap.
     - rewrite map_fmap_union big_opM_fmap. done.
   Qed.
   Lemma ghost_map_insert_persist_big {γ m} m' :
@@ -318,12 +314,7 @@ Section lemmas.
   Proof.
     iIntros "Hauth Hfrag". iMod (ghost_map_elems_unseal with "Hfrag") as "Hfrag".
     unseal. iApply (own_update_2 with "Hauth Hfrag").
-    replace (to_agree <$> m ∖ m0) with ((to_agree <$> m) ∖ (to_agree <$> m0)).
-    2:{ (* FIXME use map_difference_fmap *)
-      apply map_eq. intros i.
-      unfold difference, map_difference; rewrite lookup_difference_with.
-      rewrite !lookup_fmap !lookup_difference_with.
-      destruct (m !! i), (m0 !! i); done. }
+    rewrite map_fmap_difference.
     etrans; last apply: gmap_view_delete_big.
     rewrite big_opM_fmap. done.
   Qed.
@@ -335,15 +326,15 @@ Section lemmas.
     ghost_map_auth γ 1 (m1 ∪ m) ∗
         [∗ map] k↦v ∈ m1, k ↪[γ] v.
   Proof.
-    iIntros (?) "Hauth Hfrag". iMod (ghost_map_elems_unseal with "Hfrag") as "Hfrag".
+    iIntros (?) "Hauth Hfrag".
+    iMod (ghost_map_elems_unseal with "Hfrag") as "Hfrag".
     unseal. rewrite -big_opM_own_1 -own_op.
     iApply (own_update_2 with "Hauth Hfrag").
     rewrite map_fmap_union.
-    etrans; last etrans; [|apply: (gmap_view_replace_big _ (to_agree <$> m0) (to_agree <$> m1))|].
-    - rewrite big_opM_fmap. done.
+    rewrite -!(big_opM_fmap to_agree (λ k, gmap_view_frag k (DfracOwn 1))).
+    apply gmap_view_replace_big.
     - rewrite !dom_fmap_L. done.
-    - apply to_agree_map_valid.
-    - rewrite big_opM_fmap. done.
+    - by apply map_Forall_fmap.
   Qed.
 
 End lemmas.

iris/base_logic/lib/wsat.v

@@ -36,7 +36,8 @@ Local Existing Instances wsat_inG wsatGpreS_inv wsatGpreS_enabled wsatGpreS_disa
 Definition invariant_unfold {Σ} (P : iProp Σ) : later (iProp Σ) :=
   Next P.
 Definition ownI `{!wsatGS Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
-  own invariant_name (gmap_view_frag i DfracDiscarded (to_agree $ invariant_unfold P)).
+  own invariant_name
+    (gmap_view_frag i DfracDiscarded (to_agree $ invariant_unfold P)).
 Global Typeclasses Opaque ownI.
 Global Instance: Params (@invariant_unfold) 1 := {}.
 Global Instance: Params (@ownI) 3 := {}.
@@ -53,7 +54,8 @@ Global Instance: Params (@ownD) 3 := {}.
 
 Definition wsat `{!wsatGS Σ} : iProp Σ :=
   locked (∃ I : gmap positive (iProp Σ),
-    own invariant_name (gmap_view_auth (DfracOwn 1) (to_agree <$> (invariant_unfold <$> I))) ∗
+    own invariant_name
+      (gmap_view_auth (DfracOwn 1) (to_agree <$> (invariant_unfold <$> I))) ∗
     [∗ map] i ↦ Q ∈ I, ▷ Q ∗ ownD {[i]} ∨ ownE {[i]})%I.
 
 Section wsat.

iris/bi/internal_eq.v

@@ -112,7 +112,7 @@ Section internal_eq_derived.
   Lemma internal_eq_trans {A : ofe} (a b c : A) : a ≡ b ∧ b ≡ c ⊢ a ≡ c.
   Proof.
     apply (internal_eq_rewrite' b a (λ b, b ≡ c)%I); auto.
-    rewrite bi.and_elim_l. apply internal_eq_sym.
+    rewrite and_elim_l. apply internal_eq_sym.
   Qed.
   Lemma internal_eq_iff P Q : P ≡ Q ⊢ P ↔ Q.
   Proof. apply (internal_eq_rewrite' P Q (λ Q, P ↔ Q))%I; auto using iff_refl. Qed.