Merge branch 'master' into gen_proofmode

benchmark/gitlab-extract.py

@@ -114,5 +114,5 @@ for commit in parse_log.parse_git_commits(args.commits):
             found_build = True
             print(" success")
             break
-    if not found_build:
+    if not found_build and not BREAK:
         print(" found no succeessful build")

ci @ 39c267a4

-Subproject commit d2edcd474159cc883d09c0a08dbd463c2d2780df
+Subproject commit 39c267a40904232496986518530eea6169fb8168

theories/base_logic/lib/cancelable_invariants.v

@@ -38,9 +38,9 @@ Section proofs.
   Global Instance cinv_persistent N γ P : Persistent (cinv N γ P).
   Proof. rewrite /cinv; apply _. Qed.
 
-  Global Instance cinv_own_fractionnal γ : Fractional (cinv_own γ).
+  Global Instance cinv_own_fractional γ : Fractional (cinv_own γ).
   Proof. intros ??. by rewrite /cinv_own -own_op. Qed.
-  Global Instance cinv_own_as_fractionnal γ q :
+  Global Instance cinv_own_as_fractional γ q :
     AsFractional (cinv_own γ q) (cinv_own γ) q.
   Proof. split. done. apply _. Qed.
 

theories/base_logic/lib/invariants.v

@@ -94,6 +94,19 @@ Proof.
   iApply "HP'". iFrame.
 Qed.
 
+Lemma inv_open_strong E N P :
+  ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ ▷ P ∗ ∀ E', ▷ P ={E',↑N ∪ E'}=∗ True.
+Proof.
+  iIntros (?) "Hinv".
+  iPoseProof (inv_open (↑ N) N P with "Hinv") as "H"; first done.
+  rewrite difference_diag_L.
+  iPoseProof (fupd_mask_frame_r _ _ (E ∖ ↑ N) with "H") as "H"; first set_solver.
+  rewrite left_id_L -union_difference_L //. iMod "H" as "[$ H]"; iModIntro.
+  iIntros (E') "HP". iSpecialize ("H" with "HP").
+  iPoseProof (fupd_mask_frame_r _ _ E' with "H") as "H"; first set_solver.
+  by rewrite left_id_L.
+Qed.
+
 Global Instance into_inv_inv N P : IntoInv (inv N P) N.
 
 Global Instance elim_inv_inv E N P Q Q' :

theories/bi/big_op.v

@@ -158,6 +158,28 @@ Section sep_list.
       apply forall_intro=> k. by rewrite (forall_elim (S k)).
   Qed.
 
+  Lemma big_sepL_delete Φ l i x :
+    l !! i = Some x →
+    ([∗ list] k↦y ∈ l, Φ k y)
+    ⊣⊢ Φ i x ∗ [∗ list] k↦y ∈ l, if decide (k = i) then emp else Φ k y.
+  Proof.
+    intros. rewrite -(take_drop_middle l i x) // !big_sepL_app /= Nat.add_0_r.
+    rewrite take_length_le; last eauto using lookup_lt_Some, Nat.lt_le_incl.
+    rewrite decide_True // left_id.
+    rewrite assoc -!(comm _ (Φ _ _)) -assoc. do 2 f_equiv.
+    - apply big_sepL_proper=> k y Hk. apply lookup_lt_Some in Hk.
+      rewrite take_length in Hk. by rewrite decide_False; last lia.
+    - apply big_sepL_proper=> k y _. by rewrite decide_False; last lia.
+  Qed.
+
+  Lemma big_sepL_delete' `{!BiAffine PROP} Φ l i x :
+    l !! i = Some x →
+    ([∗ list] k↦y ∈ l, Φ k y) ⊣⊢ Φ i x ∗ [∗ list] k↦y ∈ l, ⌜ k ≠ i ⌝ → Φ k y.
+  Proof.
+    intros. rewrite big_sepL_delete //. (do 2 f_equiv)=> k y.
+    rewrite -decide_emp. by repeat case_decide.
+  Qed.
+
   Global Instance big_sepL_nil_persistent Φ :
     Persistent ([∗ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.