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

algebra/sts.v

@@ -103,15 +103,21 @@ Proof.
 Qed.
 Instance up_proper : Proper ((=) ==> (≡) ==> (≡)) up.
 Proof. by intros ??? ?? [??]; split; apply up_preserving. Qed.
+Instance up_set_preserving : Proper ((⊆) ==> flip (⊆) ==> (⊆)) up_set.
+Proof.
+  intros S1 S2 HS T1 T2 HT. rewrite /up_set.
+  f_equiv; last done. move =>s1 s2 Hs. simpl in HT. by apply up_preserving.
+Qed.
 Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set.
 Proof.
-  intros S1 S2 HS T1 T2 HT. rewrite /up_set HS.
-  f_equiv=>s1 s2 Hs. by rewrite Hs HT.
+    by intros ?? EQ1 ?? EQ2; split; apply up_set_preserving; rewrite ?EQ1 ?EQ2.
 Qed.
 Lemma elem_of_up s T : s ∈ up s T.
 Proof. constructor. Qed.
 Lemma subseteq_up_set S T : S ⊆ up_set S T.
 Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed.
+Lemma up_up_set s T : up s T ≡ up_set {[ s ]} T.
+Proof. by rewrite /up_set collection_bind_singleton. Qed.
 Lemma closed_up_set S T :
   (∀ s, s ∈ S → tok s ∩ T ≡ ∅) → S ≢ ∅ → closed (up_set S T) T.
 Proof.
@@ -213,6 +219,7 @@ Context {A B : Type} (R : relation A) (tok : A → set B).
 Canonical Structure stsRA := validityRA (sts R tok).
 Definition sts_auth (s : A) (T : set B) : stsRA := to_validity (auth s T).
 Definition sts_frag (S : set A) (T : set B) : stsRA := to_validity (frag S T).
+
 Lemma sts_update s1 s2 T1 T2 :
   sts.step R tok (s1,T1) (s2,T2) → sts_auth s1 T1 ~~> sts_auth s2 T2.
 Proof.
@@ -220,4 +227,24 @@ Proof.
   destruct (sts.step_closed R tok s1 s2 T1 T2 S Tf) as (?&?&?); auto.
   repeat (done || constructor).
 Qed.
+
+Lemma sts_frag_included S1 S2 T1 T2 Tdf :
+  sts.closed R tok S1 T1 → sts.closed R tok S2 T2 →
+  T2 ≡ T1 ∪ Tdf → T1 ∩ Tdf ≡ ∅ →
+  S2 ≡ (S1 ∩ sts.up_set R tok S2 Tdf) →
+  sts_frag S1 T1 ≼ sts_frag S2 T2.
+Proof.
+  move=>Hcl1 Hcl2 Htk Hdf Hs. exists (sts_frag (sts.up_set R tok S2 Tdf) Tdf).
+  split; first split; simpl.
+  - intros _. split_ands.
+    + done.
+    + apply sts.closed_up_set.
+      * move=>s Hs2. move:(sts.closed_disjoint _ _ _ _ Hcl2 _ Hs2).
+        solve_elem_of +Htk.
+      * by eapply sts.closed_ne.
+    + constructor; last done. rewrite -Hs. by eapply sts.closed_ne.
+  - done.
+  - intros _. constructor; [ solve_elem_of +Htk | done].
+Qed.  
+
 End stsRA.

algebra/upred.v

@@ -846,6 +846,8 @@ Proof. done. Qed.
 (* Own and valid derived *)
 Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊑ False.
 Proof. by intros; rewrite ownM_valid valid_elim. Qed.
+Global Instance ownM_mono : Proper (flip (≼) ==> (⊑)) (@uPred_ownM M).
+Proof. move=>a b [c H]. rewrite H ownM_op. eauto. Qed.
 
 (* Timeless *)
 Lemma timelessP_spec P : TimelessP P ↔ ∀ x n, ✓{n} x → P 0 x → P n x.

prelude/collections.v

@@ -533,12 +533,21 @@ End fresh.
 Section collection_monad.
   Context `{CollectionMonad M}.
 
+  Global Instance collection_fmap_mono {A B} :
+    Proper (pointwise_relation _ (=) ==> (⊆) ==> (⊆)) (@fmap M _ A B).
+  Proof. intros f g ? X Y ?; solve_elem_of. Qed.
   Global Instance collection_fmap_proper {A B} :
     Proper (pointwise_relation _ (=) ==> (≡) ==> (≡)) (@fmap M _ A B).
   Proof. intros f g ? X Y [??]; split; solve_elem_of. Qed.
+  Global Instance collection_bind_mono {A B} :
+    Proper (((=) ==> (⊆)) ==> (⊆) ==> (⊆)) (@mbind M _ A B).
+  Proof. unfold respectful; intros f g Hfg X Y ?; solve_elem_of. Qed.
   Global Instance collection_bind_proper {A B} :
     Proper (((=) ==> (≡)) ==> (≡) ==> (≡)) (@mbind M _ A B).
   Proof. unfold respectful; intros f g Hfg X Y [??]; split; solve_elem_of. Qed.
+  Global Instance collection_join_mono {A} :
+    Proper ((⊆) ==> (⊆)) (@mjoin M _ A).
+  Proof. intros X Y ?; solve_elem_of. Qed.
   Global Instance collection_join_proper {A} :
     Proper ((≡) ==> (≡)) (@mjoin M _ A).
   Proof. intros X Y [??]; split; solve_elem_of. Qed.

prelude/sets.v

@@ -28,4 +28,4 @@ Instance set_join : MJoin set := λ A (XX : set (set A)),
 Instance set_collection_monad : CollectionMonad set.
 Proof. by split; try apply _. Qed.
 
-Global Opaque set_union set_intersection.
+Global Opaque set_union set_intersection set_difference.

program_logic/auth.v

@@ -116,7 +116,7 @@ Section auth.
     (* Getting this wand eliminated is really annoying. *)
     rewrite [(■_ ★ _)%I]comm -!assoc [(▷φ _ ★ _ ★ _)%I]assoc [(▷φ _ ★ _)%I]comm.
     rewrite wand_elim_r fsa_frame_l.
-    apply (fsa_mono_pvs fsa)=> v.
+    apply (fsa_mono_pvs fsa)=> x.
     rewrite sep_exist_l; apply exist_elim=> L.
     rewrite sep_exist_l; apply exist_elim=> Lv.
     rewrite sep_exist_l; apply exist_elim=> ?.

program_logic/ghost_ownership.v

@@ -66,6 +66,8 @@ Global Instance own_proper γ : Proper ((≡) ==> (≡)) (own i γ) := ne_proper
 
 Lemma own_op γ a1 a2 : own i γ (a1 ⋅ a2) ≡ (own i γ a1 ★ own i γ a2)%I.
 Proof. by rewrite /own -ownG_op to_globalF_op. Qed.
+Global Instance own_mono γ : Proper (flip (≼) ==> (⊑)) (own i γ).
+Proof. move=>a b [c H]. rewrite H own_op. eauto with I. Qed.
 Lemma always_own_unit γ a : (□ own i γ (unit a))%I ≡ own i γ (unit a).
 Proof. by rewrite /own -to_globalF_unit always_ownG_unit. Qed.
 Lemma own_valid γ a : own i γ a ⊑ ✓ a.

program_logic/ownership.v

@@ -50,6 +50,8 @@ Proof. by intros m m' Hm; unfold ownG; rewrite Hm. Qed.
 Global Instance ownG_proper : Proper ((≡) ==> (≡)) (@ownG Λ Σ) := ne_proper _.
 Lemma ownG_op m1 m2 : ownG (m1 ⋅ m2) ≡ (ownG m1 ★ ownG m2)%I.
 Proof. by rewrite /ownG -uPred.ownM_op Res_op !left_id. Qed.
+Global Instance ownG_mono : Proper (flip (≼) ==> (⊑)) (@ownG Λ Σ).
+Proof. move=>a b [c H]. rewrite H ownG_op. eauto with I. Qed.
 Lemma always_ownG_unit m : (□ ownG (unit m))%I ≡ ownG (unit m).
 Proof.
   apply uPred.always_ownM.
@@ -64,6 +66,7 @@ Proof. apply (uPred.always_entails_r _ _), ownG_valid. Qed.
 Global Instance ownG_timeless m : Timeless m → TimelessP (ownG m).
 Proof. rewrite /ownG; apply _. Qed.
 
+
 (* inversion lemmas *)
 Lemma ownI_spec r n i P :
   ✓{n} r →

program_logic/sts.v

@@ -58,11 +58,11 @@ Section sts.
       rewrite [(_ ★ φ _)%I]comm -assoc. apply sep_mono; first done.
       rewrite -own_op. apply equiv_spec, own_proper.
       split; first split; simpl.
-      - intros; solve_elem_of-.
-      - intros _. split_ands; first by solve_elem_of-.
-        + apply closed_up. solve_elem_of-.
-        + constructor; last solve_elem_of-. apply sts.elem_of_up. 
-      - intros _. constructor. solve_elem_of-. }
+      - intros; solve_elem_of+.
+      - intros _. split_ands; first by solve_elem_of+.
+        + apply closed_up. solve_elem_of+.
+        + constructor; last solve_elem_of+. apply sts.elem_of_up. 
+      - intros _. constructor. solve_elem_of+. }
     rewrite (inv_alloc N) /ctx pvs_frame_r. apply pvs_mono.
     by rewrite always_and_sep_l.
   Qed.
@@ -80,47 +80,53 @@ Section sts.
     inversion_clear Hdisj. rewrite const_equiv // left_id.
     rewrite comm. apply sep_mono; first done.
     apply equiv_spec, own_proper. split; first split; simpl.
-    - intros Hdisj. split_ands; first by solve_elem_of-.
+    - intros Hdisj. split_ands; first by solve_elem_of+.
       + done.
       + constructor; [done | solve_elem_of-].
     - intros _. by eapply closed_disjoint.
-    - intros _. constructor. solve_elem_of-.
+    - intros _. constructor. solve_elem_of+.
   Qed.
 
-  Lemma closing E γ s T s' S' T' :
-    step sts.(st) sts.(tok) (s, T) (s', T') → s' ∈ S' → closed sts.(st) sts.(tok) S' T' →
+  Lemma closing E γ s T s' T' :
+    step sts.(st) sts.(tok) (s, T) (s', T') →
     (▷ φ s' ★ own StsI γ (sts_auth sts.(st) sts.(tok) s T))
-    ⊑ pvs E E (▷ inv StsI sts γ φ ★ states StsI sts γ S' T').
+    ⊑ pvs E E (▷ inv StsI sts γ φ ★ state StsI sts γ s' T').
   Proof.
-    intros Hstep Hin Hcl. rewrite /inv /states -(exist_intro s').
+    intros Hstep. rewrite /inv /states -(exist_intro s').
     rewrite later_sep [(_ ★ ▷φ _)%I]comm -assoc.
     rewrite -pvs_frame_l. apply sep_mono; first done.
     rewrite -later_intro.
+    rewrite own_valid_l discrete_validI. apply const_elim_sep_l=>Hval. simpl in Hval.
     transitivity (pvs E E (own StsI γ (sts_auth sts.(st) sts.(tok) s' T'))).
     { by apply own_update, sts_update. }
     apply pvs_mono. rewrite -own_op. apply equiv_spec, own_proper.
     split; first split; simpl.
-    - intros _. by eapply closed_disjoint.
-    - intros ?. split_ands; first by solve_elem_of-.
-      + done.
-      + constructor; [done | solve_elem_of-].
-    - intros _. constructor. solve_elem_of-.
+    - intros _.
+      set Tf := set_all ∖ sts.(tok) s ∖ T.
+      assert (closed (st sts) (tok sts) (up sts.(st) sts.(tok) s Tf) Tf).
+      { apply closed_up. rewrite /Tf. solve_elem_of+. }
+      eapply step_closed; [done..| |].
+      + apply elem_of_up.
+      + rewrite /Tf. solve_elem_of+.
+    - intros ?. split_ands; first by solve_elem_of+.
+      + apply closed_up. done.
+      + constructor; last solve_elem_of+. apply elem_of_up.
+    - intros _. constructor. solve_elem_of+.
   Qed.
 
   Context {V} (fsa : FSA Λ (globalF Σ) V) `{!FrameShiftAssertion fsaV fsa}.
 
-  Lemma states_fsa E N P (Q : V → iPropG Λ Σ) γ S T S' T' :
-    fsaV → closed sts.(st) sts.(tok) S' T' →
-    nclose N ⊆ E →
+  Lemma states_fsa E N P (Q : V → iPropG Λ Σ) γ S T :
+    fsaV → nclose N ⊆ E →
     P ⊑ ctx StsI sts γ N φ →
     P ⊑ (states StsI sts γ S T ★ ∀ s,
           ■ (s ∈ S) ★ ▷ φ s -★
-          fsa (E ∖ nclose N) (λ x, ∃ s',
-            ■ (step sts.(st) sts.(tok) (s, T) (s', T') ∧ s' ∈ S') ★ ▷ φ s' ★
-            (states StsI sts γ S' T' -★ Q x))) →
+          fsa (E ∖ nclose N) (λ x, ∃ s' T',
+            ■ (step sts.(st) sts.(tok) (s, T) (s', T')) ★ ▷ φ s' ★
+            (state StsI sts γ s' T' -★ Q x))) →
     P ⊑ fsa E Q.
   Proof.
-    rewrite /ctx=>? Hcl HN Hinv Hinner.
+    rewrite /ctx=>? HN Hinv Hinner.
     eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}.
     apply wand_intro_l. rewrite assoc.
     rewrite (opened (E ∖ N)) !pvs_frame_r !sep_exist_r.
@@ -129,15 +135,29 @@ Section sts.
     (* Getting this wand eliminated is really annoying. *)
     rewrite [(■_ ★ _)%I]comm -!assoc [(▷φ _ ★ _ ★ _)%I]assoc [(▷φ _ ★ _)%I]comm.
     rewrite wand_elim_r fsa_frame_l.
-    apply (fsa_mono_pvs fsa)=> v.
+    apply (fsa_mono_pvs fsa)=> x.
     rewrite sep_exist_l; apply exist_elim=> s'.
-    rewrite comm -!assoc. apply const_elim_sep_l=>-[Hstep Hin].
+    rewrite sep_exist_l; apply exist_elim=>T'.
+    rewrite comm -!assoc. apply const_elim_sep_l=>-Hstep.
     rewrite assoc [(_ ★ (_ -★ _))%I]comm -assoc.
     rewrite (closing (E ∖ N)) //; [].
     rewrite pvs_frame_l. apply pvs_mono.
     by rewrite assoc [(_ ★ ▷_)%I]comm -assoc wand_elim_l.
   Qed.
 
+  Lemma state_fsa E N P (Q : V → iPropG Λ Σ) γ s0 T :
+    fsaV → nclose N ⊆ E →
+    P ⊑ ctx StsI sts γ N φ →
+    P ⊑ (state StsI sts γ s0 T ★ ∀ s,
+          ■ (s ∈ up sts.(st) sts.(tok) s0 T) ★ ▷ φ s -★
+          fsa (E ∖ nclose N) (λ x, ∃ s' T',
+            ■ (step sts.(st) sts.(tok) (s, T) (s', T')) ★ ▷ φ s' ★
+            (state StsI sts γ s' T' -★ Q x))) →
+    P ⊑ fsa E Q.
+  Proof.
+    rewrite {1}/state. apply states_fsa.
+  Qed.
+
 End sts.
 
 End sts.

program_logic/wsat.v

@@ -102,7 +102,7 @@ Proof.
   { by rewrite (comm _ rP) -assoc big_opM_insert. }
   exists (<[i:=rP]>rs); constructor; rewrite ?Hr; auto.
   * intros j; rewrite Hr lookup_insert_is_Some=>-[?|[??]]; subst.
-    + rewrite !lookup_op HiP !op_is_Some; solve_elem_of -.
+    + rewrite !lookup_op HiP !op_is_Some; solve_elem_of +.
     + destruct (HE j) as [Hj Hj']; auto; solve_elem_of +Hj Hj'.
   * intros j P'; rewrite Hr elem_of_union elem_of_singleton=>-[?|?]; subst.
     + rewrite !lookup_wld_op_l ?HiP; auto=> HP.