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

theories/base_logic/lib/invariants.v

@@ -41,6 +41,33 @@ Proof.
   - rewrite /uPred_except_0; eauto.
 Qed.
 
+Lemma inv_alloc_open N E P :
+  ↑N ⊆ E → True ={E, E∖↑N}=∗ inv N P ∗ (▷P ={E∖↑N, E}=∗ True).
+Proof.
+  rewrite inv_eq /inv_def fupd_eq /fupd_def.
+  iIntros (Sub) "[Hw HE]".
+  iMod (ownI_alloc_open (∈ ↑ N) P with "Hw") as (i) "(% & Hw & #Hi & HD)".
+  - intros Ef. exists (coPpick (↑ N ∖ coPset.of_gset Ef)).
+    rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
+    apply coPpick_elem_of=> Hfin.
+    eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
+    apply of_gset_finite.
+  - iAssert (ownE {[i]} ∗ ownE (↑ N ∖ {[i]}) ∗ ownE (E ∖ ↑ N))%I with "[HE]" as "(HEi & HEN\i & HE\N)".
+    { rewrite -?ownE_op; [|set_solver|set_solver].
+      rewrite assoc_L. rewrite <-!union_difference_L; try done; set_solver. }
+    iModIntro. rewrite /uPred_except_0. iRight. iFrame.
+    iSplitL "Hw HEi".
+    + by iApply "Hw".
+    + iSplitL "Hi"; [eauto|].
+      iIntros "HP [Hw HE\N]".
+      iDestruct (ownI_close with "[$Hw $Hi $HP $HD]") as "[? HEi]".
+      iModIntro. iRight. iFrame. iSplitL; [|done].
+      iCombine "HEi" "HEN\i" as "HEN".
+      iCombine "HEN" "HE\N" as "HE".
+      rewrite -?ownE_op; [|set_solver|set_solver].
+      rewrite <-!union_difference_L; try done; set_solver.
+Qed.
+
 Lemma inv_open E N P :
   ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ ▷ P ∗ (▷ P ={E∖↑N,E}=∗ True).
 Proof.

theories/base_logic/lib/wsat.v

@@ -142,4 +142,28 @@ Proof.
   iApply (big_sepM_insert _ I); first done.
   iFrame "HI". iLeft. by rewrite /ownD; iFrame.
 Qed.
+
+Lemma ownI_alloc_open φ P :
+  (∀ E : gset positive, ∃ i, i ∉ E ∧ φ i) →
+  wsat ==∗ ∃ i, ⌜φ i⌝ ∗ (ownE {[i]} -∗ wsat) ∗ ownI i P ∗ ownD {[i]}.
+Proof.
+  iIntros (Hfresh) "Hw". iDestruct "Hw" as (I) "[? HI]".
+  iMod (own_empty (gset_disjUR positive) disabled_name) as "HD".
+  iMod (own_updateP with "HD") as "HD".
+  { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
+    intros E. destruct (Hfresh (E ∪ dom _ I))
+      as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
+  iDestruct "HD" as (X) "[Hi HD]"; iDestruct "Hi" as %(i & -> & HIi & ?).
+  iMod (own_update with "Hw") as "[Hw HiP]".
+  { eapply auth_update_alloc,
+     (alloc_singleton_local_update _ i (invariant_unfold P)); last done.
+    by rewrite /= lookup_fmap HIi. }
+  iModIntro; iExists i;  iSplit; [done|]. rewrite /ownI; iFrame "HiP".
+  rewrite -/(ownD _). iFrame "HD".
+  iIntros "HE". iExists (<[i:=P]>I); iSplitL "Hw".
+  { by rewrite fmap_insert insert_singleton_op ?lookup_fmap ?HIi. }
+  iApply (big_sepM_insert _ I); first done.
+  iFrame "HI". by iRight.
+Qed.
+
 End wsat.

theories/prelude/sorting.v

@@ -114,7 +114,7 @@ End sorted.
 
 (** ** Correctness of merge sort *)
 Section merge_sort_correct.
-  Context  {A} (R : relation A) `{∀ x y, Decision (R x y)} `{!Total R}.
+  Context  {A} (R : relation A) `{∀ x y, Decision (R x y)}.
 
   Lemma list_merge_cons x1 x2 l1 l2 :
     list_merge R (x1 :: l1) (x2 :: l2) =
@@ -127,7 +127,7 @@ Section merge_sort_correct.
     destruct 1 as [|x1 l1 IH1], 1 as [|x2 l2 IH2];
       rewrite ?list_merge_cons; simpl; repeat case_decide; auto.
   Qed.
-  Lemma Sorted_list_merge l1 l2 :
+  Lemma Sorted_list_merge `{!Total R} l1 l2 :
     Sorted R l1 → Sorted R l2 → Sorted R (list_merge R l1 l2).
   Proof.
     intros Hl1. revert l2. induction Hl1 as [|x1 l1 IH1];
@@ -158,7 +158,7 @@ Section merge_sort_correct.
     | Some l :: st => l ++ merge_stack_flatten st
     end.
 
-  Lemma Sorted_merge_list_to_stack st l :
+  Lemma Sorted_merge_list_to_stack `{!Total R} st l :
     merge_stack_Sorted st → Sorted R l →
     merge_stack_Sorted (merge_list_to_stack R st l).
   Proof.
@@ -172,7 +172,7 @@ Section merge_sort_correct.
     revert l. induction st as [|[l'|] st IH]; intros l; simpl; auto.
     by rewrite IH, merge_Permutation, (assoc_L _), (comm (++) l).
   Qed.
-  Lemma Sorted_merge_stack st :
+  Lemma Sorted_merge_stack `{!Total R} st :
     merge_stack_Sorted st → Sorted R (merge_stack R st).
   Proof. induction 1; simpl; auto using Sorted_list_merge. Qed.
   Lemma merge_stack_Permutation st : merge_stack R st ≡ₚ merge_stack_flatten st.
@@ -180,7 +180,7 @@ Section merge_sort_correct.
     induction st as [|[] ? IH]; intros; simpl; auto.
     by rewrite merge_Permutation, IH.
   Qed.
-  Lemma Sorted_merge_sort_aux st l :
+  Lemma Sorted_merge_sort_aux `{!Total R} st l :
     merge_stack_Sorted st → Sorted R (merge_sort_aux R st l).
   Proof.
     revert st. induction l; simpl;
@@ -194,11 +194,11 @@ Section merge_sort_correct.
     - rewrite IH, merge_list_to_stack_Permutation; simpl.
       by rewrite Permutation_middle.
   Qed.
-  Lemma Sorted_merge_sort l : Sorted R (merge_sort R l).
+  Lemma Sorted_merge_sort `{!Total R} l : Sorted R (merge_sort R l).
   Proof. apply Sorted_merge_sort_aux. by constructor. Qed.
   Lemma merge_sort_Permutation l : merge_sort R l ≡ₚ l.
   Proof. unfold merge_sort. by rewrite merge_sort_aux_Permutation. Qed.
-  Lemma StronglySorted_merge_sort `{!Transitive R} l :
+  Lemma StronglySorted_merge_sort `{!Transitive R, !Total R} l :
     StronglySorted R (merge_sort R l).
   Proof. auto using Sorted_StronglySorted, Sorted_merge_sort. Qed.
 End merge_sort_correct.