Merge branch 'ralf/ghost-var' into 'master'

ghost-var lib: more lemmas for when you own the two halves

See merge request iris/iris!511

theories/algebra/lib/frac_agree.v

@@ -25,6 +25,10 @@ Section lemmas.
   Global Instance to_frac_inj : Inj2 (≡) (≡) (≡) (@to_frac_agree A).
   Proof. by intros q1 a1 q2 a2 [??%(inj to_agree)]. Qed.
 
+  Lemma frac_agree_op q1 q2 a :
+    to_frac_agree (q1 + q2) a ≡ to_frac_agree q1 a ⋅ to_frac_agree q2 a.
+  Proof. rewrite /to_frac_agree -pair_op agree_idemp //. Qed.
+
   Lemma frac_agree_op_valid q1 a1 q2 a2 :
     ✓ (to_frac_agree q1 a1 ⋅ to_frac_agree q2 a2) →
     ✓ (q1 + q2)%Qp ∧ a1 ≡ a2.

theories/base_logic/lib/ghost_var.v

@@ -30,7 +30,7 @@ Section lemmas.
   Proof. apply _. Qed.
 
   Global Instance ghost_var_fractional γ a : Fractional (λ q, ghost_var γ q a).
-  Proof. intros q1 q2. rewrite /ghost_var -own_op -pair_op agree_idemp //. Qed.
+  Proof. intros q1 q2. rewrite /ghost_var -own_op -frac_agree_op //. Qed.
   Global Instance ghost_var_as_fractional γ a q :
     AsFractional (ghost_var γ q a) (λ q, ghost_var γ q a) q.
   Proof. split. done. apply _. Qed.
@@ -43,13 +43,20 @@ Section lemmas.
     ⊢ |==> ∃ γ, ghost_var γ 1 a.
   Proof. iApply own_alloc. done. Qed.
 
-  Lemma ghost_var_op_valid γ a1 q1 a2 q2 :
+  Lemma ghost_var_valid_2 γ a1 q1 a2 q2 :
     ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 -∗ ⌜✓ (q1 + q2)%Qp ∧ a1 = a2⌝.
   Proof.
     iIntros "Hvar1 Hvar2".
     iDestruct (own_valid_2 with "Hvar1 Hvar2") as %[Hq Ha]%frac_agree_op_valid.
     done.
   Qed.
+  (** Almost all the time, this is all you really need. *)
+  Lemma ghost_var_agree γ a1 q1 a2 q2 :
+    ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 -∗ ⌜a1 = a2⌝.
+  Proof.
+    iIntros "Hvar1 Hvar2".
+    iDestruct (ghost_var_valid_2 with "Hvar1 Hvar2") as %[_ ?]. done.
+  Qed.
 
   (** This is just an instance of fractionality above, but that can be hard to find. *)
   Lemma ghost_var_split γ a q1 q2 :
@@ -61,7 +68,22 @@ Section lemmas.
     ghost_var γ 1 a ==∗ ghost_var γ 1 b.
   Proof.
     iApply own_update. apply cmra_update_exclusive. done.
-  Qed. 
+  Qed.
+  Lemma ghost_var_update_2 b γ a1 q1 a2 q2 :
+    (q1 + q2 = 1)%Qp →
+    ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 ==∗ ghost_var γ q1 b ∗ ghost_var γ q2 b.
+  Proof.
+    iIntros (Hq) "H1 H2".
+    iDestruct (ghost_var_valid_2 with "H1 H2") as %[_ ->].
+    iDestruct (fractional_merge with "H1 H2") as "H". simpl. rewrite Hq.
+    iMod (ghost_var_update with "H") as "H".
+    rewrite -Hq. iApply ghost_var_split. done.
+  Qed.
+  Lemma ghost_var_update_halves b γ a1 a2 :
+    ghost_var γ (1/2) a1 -∗
+    ghost_var γ (1/2) a2 ==∗
+    ghost_var γ (1/2) b ∗ ghost_var γ (1/2) b.
+  Proof. iApply ghost_var_update_2. apply Qp_half_half. Qed.
 
 End lemmas.
 

theories/bi/lib/fractional.v

@@ -38,6 +38,11 @@ Section fractional.
     P1 -∗ P2 -∗ P.
   Proof. intros. apply bi.wand_intro_r. by rewrite -(fractional_split P). Qed.
 
+  Lemma fractional_merge P1 P2 Φ q1 q2 `{!Fractional Φ} :
+    AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
+    P1 -∗ P2 -∗ Φ (q1 + q2)%Qp.
+  Proof. move=>-[-> _] [-> _]. rewrite fractional. apply bi.wand_intro_r. done. Qed.
+
   Lemma fractional_half P P12 Φ q :
     AsFractional P Φ q → AsFractional P12 Φ (q/2) →
     P ⊣⊢ P12 ∗ P12.