Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

algebra/frac.v

-From Coq Require Import Qcanon.
+From Coq.QArith Require Import Qcanon.
 From algebra Require Export cmra.
 From algebra Require Import functor upred.
 Local Arguments validN _ _ _ !_ /.

heap_lang/heap.v

@@ -132,6 +132,10 @@ Section heap.
     rewrite option_validI frac_validI discrete_valid. by apply const_elim_r.
   Qed.
 
+  Lemma heap_mapsto_op_split l q v :
+    (l ↦{q} v)%I ≡ (l ↦{q/2} v ★ l ↦{q/2} v)%I.
+  Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
+
   (** Weakest precondition *)
   Lemma wp_alloc N E e v P Φ :
     to_val e = Some v →
@@ -145,7 +149,7 @@ Section heap.
     apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e)))
       with N heap_name ∅; simpl; eauto with I.
     rewrite -later_intro. apply sep_mono_r,forall_intro=> h; apply wand_intro_l.
-    rewrite -assoc left_id discrete_valid; apply const_elim_sep_l=> ?.
+    rewrite -assoc left_id; apply const_elim_sep_l=> ?.
     rewrite -(wp_alloc_pst _ (of_heap h)) //.
     apply sep_mono_r; rewrite HP; apply later_mono.
     apply forall_mono=> l; apply wand_intro_l.
@@ -168,7 +172,7 @@ Section heap.
     apply (auth_fsa' heap_inv (wp_fsa _) id)
       with N heap_name {[ l := Frac q (DecAgree v) ]}; simpl; eauto with I.
     rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
-    rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
+    rewrite -assoc; apply const_elim_sep_l=> ?.
     rewrite -(wp_load_pst _ (<[l:=v]>(of_heap h))) ?lookup_insert //.
     rewrite const_equiv // left_id.
     rewrite /heap_inv of_heap_singleton_op //.
@@ -185,7 +189,7 @@ Section heap.
     apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v)) l))
       with N heap_name {[ l := Frac 1 (DecAgree v') ]}; simpl; eauto with I.
     rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
-    rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
+    rewrite -assoc; apply const_elim_sep_l=> ?.
     rewrite -(wp_store_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
     rewrite /heap_inv alter_singleton insert_insert !of_heap_singleton_op; eauto.
     rewrite const_equiv; last naive_solver.
@@ -202,7 +206,7 @@ Section heap.
     apply (auth_fsa' heap_inv (wp_fsa _) id)
       with N heap_name {[ l := Frac q (DecAgree v') ]}; simpl; eauto 10 with I.
     rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
-    rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
+    rewrite -assoc; apply const_elim_sep_l=> ?.
     rewrite -(wp_cas_fail_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
     rewrite const_equiv // left_id.
     rewrite /heap_inv !of_heap_singleton_op //.
@@ -219,7 +223,7 @@ Section heap.
     apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v2)) l))
       with N heap_name {[ l := Frac 1 (DecAgree v1) ]}; simpl; eauto 10 with I.
     rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
-    rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
+    rewrite -assoc; apply const_elim_sep_l=> ?.
     rewrite -(wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))) //;
       last by rewrite lookup_insert.
     rewrite /heap_inv alter_singleton insert_insert !of_heap_singleton_op; eauto.

program_logic/auth.v

@@ -101,15 +101,12 @@ Section auth.
 
   Context {V} (fsa : FSA Λ (globalF Σ) V) `{!FrameShiftAssertion fsaV fsa}.
 
-  (* Notice how the user has to prove that `b⋅a'` is valid at all
-     step-indices. However, since A is timeless, that should not be
-     a restriction. *)
   Lemma auth_fsa E N P (Ψ : V → iPropG Λ Σ) γ a :
     fsaV →
     nclose N ⊆ E →
     P ⊑ auth_ctx γ N φ →
     P ⊑ (▷ auth_own γ a ★ ∀ a',
-          ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
+          ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
           fsa (E ∖ nclose N) (λ x, ∃ L Lv (Hup : LocalUpdate Lv L),
             ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
             (auth_own γ (L a) -★ Ψ x))) →
@@ -124,7 +121,7 @@ Section auth.
     apply (fsa_strip_pvs fsa). apply exist_elim=>a'.
     rewrite (forall_elim a'). rewrite [(▷_ ★ _)%I]comm.
     eapply wand_apply_r; first (by eapply (wand_frame_l (own γ _))); last first.
-    { rewrite assoc [(_ ★ own _ _)%I]comm -assoc. done. }
+    { rewrite assoc [(_ ★ own _ _)%I]comm -assoc discrete_valid.  done. }
     rewrite fsa_frame_l.
     apply (fsa_mono_pvs fsa)=> x.
     rewrite sep_exist_l; apply exist_elim=> L.
@@ -141,7 +138,7 @@ Section auth.
     nclose N ⊆ E →
     P ⊑ auth_ctx γ N φ →
     P ⊑ (▷ auth_own γ a ★ (∀ a',
-          ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
+          ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
           fsa (E ∖ nclose N) (λ x,
             ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
             (auth_own γ (L a) -★ Ψ x)))) →