Experiment: remove always_forall.

This breaks the following things:

- Universally quantified Hoare triples are no longer persistent.
- The core operation on uPreds.

theories/base_logic/big_op.v

@@ -143,10 +143,14 @@ Section list.
     □ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x → Ψ k x) ∧ ([∗ list] k↦x ∈ l, Φ k x)
     ⊢ [∗ list] k↦x ∈ l, Ψ k x.
   Proof.
-    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
-    setoid_rewrite always_impl; setoid_rewrite always_pure.
-    rewrite -big_sepL_forall -big_sepL_sepL. apply big_sepL_mono; auto=> k x ?.
-    by rewrite -always_wand_impl always_elim wand_elim_l.
+    rewrite always_and_sep_l. revert Φ Ψ. induction l as [|x l IH]=> Φ Ψ /=; auto.
+    rewrite always_sep_dup' -assoc [(□ _ ∗ _)%I]comm -!assoc assoc.
+    apply sep_mono.
+    - rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
+      by rewrite -always_and_sep_l always_elim impl_elim_l.
+    - rewrite comm -(IH (Φ ∘ S) (Ψ ∘ S)) /=.
+      apply sep_mono_l, always_mono.
+      apply forall_intro=> k. by rewrite (forall_elim (S k)).
   Qed.
 
   Global Instance big_sepL_nil_persistent Φ :
@@ -334,10 +338,17 @@ Section gmap.
     □ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x → Ψ k x) ∧ ([∗ map] k↦x ∈ m, Φ k x)
     ⊢ [∗ map] k↦x ∈ m, Ψ k x.
   Proof.
-    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
-    setoid_rewrite always_impl; setoid_rewrite always_pure.
-    rewrite -big_sepM_forall -big_sepM_sepM. apply big_sepM_mono; auto=> k x ?.
-    by rewrite -always_wand_impl always_elim wand_elim_l.
+    rewrite always_and_sep_l. induction m as [|i x m ? IH] using map_ind.
+    { by rewrite sep_elim_r. }
+    rewrite !big_sepM_insert // always_sep_dup'.
+    rewrite -assoc [(□ _ ∗ _)%I]comm -!assoc assoc. apply sep_mono.
+    - rewrite (forall_elim i) (forall_elim x) pure_True ?lookup_insert //.
+      by rewrite-always_and_sep_l True_impl always_elim impl_elim_l.
+    - rewrite comm -IH /=.
+      apply sep_mono_l, always_mono, forall_mono=> k.
+      apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
+      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
+      by rewrite pure_True // True_impl.
   Qed.
 
   Global Instance big_sepM_empty_persistent Φ :
@@ -482,10 +493,15 @@ Section gset.
   Lemma big_sepS_impl Φ Ψ X :
     □ (∀ x, ⌜x ∈ X⌝ → Φ x → Ψ x) ∧ ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ X, Ψ x.
   Proof.
-    rewrite always_and_sep_l always_forall.
-    setoid_rewrite always_impl; setoid_rewrite always_pure.
-    rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
-    by rewrite -always_wand_impl always_elim wand_elim_l.
+    rewrite always_and_sep_l. induction X as [|x X ? IH] using collection_ind_L.
+    { by rewrite sep_elim_r. }
+    rewrite !big_sepS_insert // always_sep_dup'.
+    rewrite -assoc [(□ _ ∗ _)%I]comm -!assoc assoc. apply sep_mono.
+    - rewrite (forall_elim x) pure_True; last set_solver.
+      by rewrite -always_and_sep_l True_impl always_elim impl_elim_l.
+    - rewrite comm -IH /=. apply sep_mono_l, always_mono.
+      apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
+      by rewrite pure_True ?True_impl; last set_solver.
   Qed.
 
   Global Instance big_sepS_empty_persistent Φ : PersistentP ([∗ set] x ∈ ∅, Φ x).

theories/base_logic/derived.v

@@ -485,24 +485,14 @@ Lemma always_idemp P : □ □ P ⊣⊢ □ P.
 Proof. apply (anti_symm _); auto using always_idemp_2. Qed.
 
 Lemma always_pure φ : □ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
-Proof.
-  apply (anti_symm _); auto.
-  apply pure_elim'=> Hφ.
-  trans (∀ x : False, □ True : uPred M)%I; [by apply forall_intro|].
-  rewrite always_forall_2. auto using always_mono, pure_intro.
-Qed.
-Lemma always_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a).
-Proof.
-  apply (anti_symm _); auto using always_forall_2.
-  apply forall_intro=> x. by rewrite (forall_elim x).
-Qed.
+Proof. apply (anti_symm _); auto using always_pure_2. Qed.
 Lemma always_exist {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊣⊢ (∃ a, □ Ψ a).
 Proof.
   apply (anti_symm _); auto using always_exist_1.
   apply exist_elim=> x. by rewrite (exist_intro x).
 Qed.
 Lemma always_and P Q : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q.
-Proof. rewrite !and_alt always_forall. by apply forall_proper=> -[]. Qed.
+Proof. apply (anti_symm _); auto using always_and_2. Qed.
 Lemma always_or P Q : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q.
 Proof. rewrite !or_alt always_exist. by apply exist_proper=> -[]. Qed.
 Lemma always_impl P Q : □ (P → Q) ⊢ □ P → □ Q.
@@ -884,17 +874,17 @@ Qed.
 (* Persistence *)
 Global Instance pure_persistent φ : PersistentP (⌜φ⌝ : uPred M)%I.
 Proof. by rewrite /PersistentP always_pure. Qed.
-Global Instance pure_impl_persistent φ Q :
+(* Global Instance pure_impl_persistent φ Q :
   PersistentP Q → PersistentP (⌜φ⌝ → Q)%I.
 Proof.
-  rewrite /PersistentP pure_impl_forall always_forall. auto using forall_mono.
+  rewrite /PersistentP pure_impl_forall. always_forall. auto using forall_mono.
 Qed.
 Global Instance pure_wand_persistent φ Q :
   PersistentP Q → PersistentP (⌜φ⌝ -∗ Q)%I.
 Proof.
   rewrite /PersistentP -always_impl_wand pure_impl_forall always_forall.
   auto using forall_mono.
-Qed.
+Qed. *)
 Global Instance always_persistent P : PersistentP (□ P).
 Proof. by intros; apply always_intro'. Qed.
 Global Instance and_persistent P Q :
@@ -906,9 +896,6 @@ Proof. by intros; rewrite /PersistentP always_or; apply or_mono. Qed.
 Global Instance sep_persistent P Q :
   PersistentP P → PersistentP Q → PersistentP (P ∗ Q).
 Proof. by intros; rewrite /PersistentP always_sep; apply sep_mono. Qed.
-Global Instance forall_persistent {A} (Ψ : A → uPred M) :
-  (∀ x, PersistentP (Ψ x)) → PersistentP (∀ x, Ψ x).
-Proof. by intros; rewrite /PersistentP always_forall; apply forall_mono. Qed.
 Global Instance exist_persistent {A} (Ψ : A → uPred M) :
   (∀ x, PersistentP (Ψ x)) → PersistentP (∃ x, Ψ x).
 Proof. by intros; rewrite /PersistentP always_exist; apply exist_mono. Qed.

theories/base_logic/lib/core.v

@@ -26,8 +26,10 @@ Section core.
   Lemma coreP_intro P : P -∗ coreP P.
   Proof. iIntros "HP". by iIntros (Q HQ ->). Qed.
 
+(*
   Global Instance coreP_persistent P : PersistentP (coreP P).
   Proof. rewrite /coreP. apply _. Qed.
+*)
 
   Global Instance coreP_mono : Proper ((⊢) ==> (⊢)) (@coreP M).
   Proof.
@@ -41,6 +43,7 @@ Section core.
   Lemma coreP_elim P : PersistentP P → coreP P -∗ P.
   Proof. rewrite /coreP. iIntros (?) "HCP". unshelve iApply ("HCP" $! P); auto. Qed.
 
+(*
   Lemma coreP_wand P Q :
     (coreP P ⊢ Q) ↔ (P ⊢ □ Q).
   Proof.
@@ -50,4 +53,5 @@ Section core.
     - iIntros (HPQ) "HcP". iDestruct (coreP_mono _ _ HPQ with "HcP") as "HcQ".
       iDestruct (coreP_elim with "HcQ") as "#HQ". done.
   Qed.
+*)
 End core.

theories/base_logic/primitive.v

@@ -430,7 +430,9 @@ Qed.
 Lemma always_idemp_2 P : □ P ⊢ □ □ P.
 Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed.
 
-Lemma always_forall_2 {A} (Ψ : A → uPred M) : (∀ a, □ Ψ a) ⊢ (□ ∀ a, Ψ a).
+Lemma always_pure_2 φ : ⌜ φ ⌝ ⊢ □ ⌜ φ ⌝.
+Proof. by unseal. Qed.
+Lemma always_and_2 P Q : □ P ∧ □ Q ⊢ □ (P ∧ Q).
 Proof. by unseal. Qed.
 Lemma always_exist_1 {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊢ (∃ a, □ Ψ a).
 Proof. by unseal. Qed.

theories/program_logic/hoare.v

@@ -49,7 +49,7 @@ Lemma ht_val E v : {{ True }} of_val v @ E {{ v', ⌜v = v'⌝ }}.
 Proof. iIntros "!# _". by iApply wp_value'. Qed.
 
 Lemma ht_vs E P P' Φ Φ' e :
-  (P ={E}=> P') ∧ {{ P' }} e @ E {{ Φ' }} ∧ (∀ v, Φ' v ={E}=> Φ v)
+  (P ={E}=> P') ∧ {{ P' }} e @ E {{ Φ' }} ∧ □ (∀ v, Φ' v ={E}=> Φ v)
   ⊢ {{ P }} e @ E {{ Φ }}.
 Proof.
   iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iMod ("Hvs" with "HP") as "HP".
@@ -59,7 +59,7 @@ Qed.
 
 Lemma ht_atomic E1 E2 P P' Φ Φ' e :
   atomic e →
-  (P ={E1,E2}=> P') ∧ {{ P' }} e @ E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
+  (P ={E1,E2}=> P') ∧ {{ P' }} e @ E2 {{ Φ' }} ∧ □ (∀ v, Φ' v ={E2,E1}=> Φ v)
   ⊢ {{ P }} e @ E1 {{ Φ }}.
 Proof.
   iIntros (?) "(#Hvs & #Hwp & #HΦ) !# HP". iApply (wp_atomic _ E2); auto.
@@ -69,7 +69,7 @@ Proof.
 Qed.
 
 Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
-  {{ P }} e @ E {{ Φ }} ∧ (∀ v, {{ Φ v }} K (of_val v) @ E {{ Φ' }})
+  {{ P }} e @ E {{ Φ }} ∧ □ (∀ v, {{ Φ v }} K (of_val v) @ E {{ Φ' }})
   ⊢ {{ P }} K e @ E {{ Φ' }}.
 Proof.
   iIntros "[#Hwpe #HwpK] !# HP". iApply wp_bind.

theories/proofmode/class_instances.v

@@ -693,9 +693,11 @@ Proof. rewrite /IntoExist=> HP ?. by rewrite HP except_0_exist. Qed.
 (* IntoForall *)
 Global Instance into_forall_forall {A} (Φ : A → uPred M) : IntoForall (∀ a, Φ a) Φ.
 Proof. done. Qed.
+(*
 Global Instance into_forall_always {A} P (Φ : A → uPred M) :
   IntoForall P Φ → IntoForall (□ P) (λ a, □ (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP always_forall. Qed.
+*)
 
 (* FromModal *)
 Global Instance from_modal_later P : FromModal (▷ P) P.

theories/tests/joining_existentials.v

@@ -33,7 +33,7 @@ Definition barrier_res γ (Φ : X → iProp Σ) : iProp Σ :=
   (∃ x, own γ (Shot x) ∗ Φ x)%I.
 
 Lemma worker_spec e γ l (Φ Ψ : X → iProp Σ) `{!Closed [] e} :
-  recv N l (barrier_res γ Φ) -∗ (∀ x, {{ Φ x }} e {{ _, Ψ x }}) -∗
+  recv N l (barrier_res γ Φ) -∗ □ (∀ x, {{ Φ x }} e {{ _, Ψ x }}) -∗
   WP wait #l ;; e {{ _, barrier_res γ Ψ }}.
 Proof.
   iIntros "Hl #He". wp_apply (wait_spec with "[- $Hl]"); simpl.
@@ -69,8 +69,8 @@ Qed.
 Lemma client_spec_new eM eW1 eW2 `{!Closed [] eM, !Closed [] eW1, !Closed [] eW2} :
   P -∗
   {{ P }} eM {{ _, ∃ x, Φ x }} -∗
-  (∀ x, {{ Φ1 x }} eW1 {{ _, Ψ1 x }}) -∗
-  (∀ x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }}) -∗
+  □ (∀ x, {{ Φ1 x }} eW1 {{ _, Ψ1 x }}) -∗
+  □ (∀ x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }}) -∗
   WP client eM eW1 eW2 {{ _, ∃ γ, barrier_res γ Ψ }}.
 Proof using All.
   iIntros "/= HP #He #He1 #He2"; rewrite /client.

theories/tests/one_shot.v

@@ -38,7 +38,7 @@ Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=
 
 Lemma wp_one_shot (Φ : val → iProp Σ) :
   (∀ f1 f2 : val,
-    (∀ n : Z, □ WP f1 #n {{ w, ⌜w = #true⌝ ∨ ⌜w = #false⌝ }}) ∗
+    □ (∀ n : Z, WP f1 #n {{ w, ⌜w = #true⌝ ∨ ⌜w = #false⌝ }}) ∗
     □ WP f2 #() {{ g, □ WP g #() {{ _, True }} }} -∗ Φ (f1,f2)%V)
   ⊢ WP one_shot_example #() {{ Φ }}.
 Proof.
@@ -48,7 +48,7 @@ Proof.
   iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
   { iNext. iLeft. by iSplitL "Hl". }
   iModIntro. iApply "Hf"; iSplit.
-  - iIntros (n) "!#". wp_let.
+  - iIntros "!#" (n). wp_let.
     iInv N as ">[[Hl Hγ]|H]" "Hclose"; last iDestruct "H" as (m) "[Hl Hγ]".
     + wp_cas_suc. iMod (own_update with "Hγ") as "Hγ".
       { by apply cmra_update_exclusive with (y:=Shot n). }

theories/tests/proofmode.v

@@ -8,7 +8,7 @@ Implicit Types P Q R : uPred M.
 
 Lemma demo_0 P Q : □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P).
 Proof.
-  iIntros "#H #H2".
+  iIntros "#H H2".
   (* should remove the disjunction "H" *)
   iDestruct "H" as "[?|?]"; last by iLeft.
   (* should keep the disjunction "H" because it is instantiated *)