Remove property `(∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝` from the BI canonical structure and

put it into a type class `BiPureForall`.

This property does not hold for embeddings of classical logic into Coq.

tests/heapprop.v

@@ -149,8 +149,6 @@ Section mixins.
       unseal=> φ P ?; by split.
     - (* [(φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P] *)
       unseal=> φ P HP; split=> σ ?. by apply HP.
-    - (* [(∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝] *)
-      unseal=> A φ; by split.
     - (* [P ∧ Q ⊢ P] *)
       unseal=> P Q; split=> σ [??]; done.
     - (* [P ∧ Q ⊢ Q] *)
@@ -222,6 +220,9 @@ Canonical Structure heapPropI : bi :=
   {| bi_ofe_mixin := ofe_mixin_of heapProp;
      bi_bi_mixin := heapProp_bi_mixin; bi_bi_later_mixin := heapProp_bi_later_mixin |}.
 
+Instance heapProp_pure_forall : BiPureForall heapPropI.
+Proof. intros A φ. rewrite /bi_forall /bi_pure /=. unseal. by split. Qed.
+
 Lemma heapProp_proofmode_test {A} (P Q R : heapProp) (Φ Ψ : A → heapProp) :
   P ∗ Q -∗
   □ R -∗

tests/proofmode.v

@@ -215,7 +215,7 @@ Proof.
   Show. auto.
 Qed.
 
-Lemma test_iIntros_pure_not : ⊢@{PROP} ⌜ ¬False ⌝.
+Lemma test_iIntros_pure_not `{!BiPureForall PROP} : ⊢@{PROP} ⌜ ¬False ⌝.
 Proof. by iIntros (?). Qed.
 
 Lemma test_fast_iIntros `{!BiInternalEq PROP} P Q :

tests/telescopes.v

@@ -27,7 +27,7 @@ Section basic_tests.
   Lemma test_pure_texist {TT : tele} (φ : TT → Prop) :
     (∃.. x, ⌜ φ x ⌝) -∗ ∃.. x, ⌜ φ x ⌝ : PROP.
   Proof. iIntros (H) "!%". done. Qed.
-  Lemma test_pure_tforall {TT : tele} (φ : TT → Prop) :
+  Lemma test_pure_tforall `{!BiPureForall PROP} {TT : tele} (φ : TT → Prop) :
     (∀.. x, ⌜ φ x ⌝) -∗ ∀.. x, ⌜ φ x ⌝ : PROP.
   Proof. iIntros (H) "!%". done. Qed.
   Lemma test_pure_tforall_persistent {TT : tele} (Φ : TT → PROP) :

theories/base_logic/bi.v

@@ -30,7 +30,6 @@ Proof.
   - exact: persistently_ne.
   - exact: pure_intro.
   - exact: pure_elim'.
-  - exact: @pure_forall_2.
   - exact: and_elim_l.
   - exact: and_elim_r.
   - exact: and_intro.
@@ -90,6 +89,9 @@ Canonical Structure uPredI (M : ucmraT) : bi :=
      bi_bi_mixin := uPred_bi_mixin M;
      bi_bi_later_mixin := uPred_bi_later_mixin M |}.
 
+Instance uPred_pure_forall M : BiPureForall (uPredI M).
+Proof. exact: @pure_forall_2. Qed.
+
 Instance uPred_later_contractive {M} : BiLaterContractive (uPredI M).
 Proof. apply later_contractive. Qed.
 

theories/bi/derived_connectives.v

@@ -133,3 +133,8 @@ Arguments löb_weak {_ _} _ _.
 
 Notation BiLaterContractive PROP :=
   (Contractive (bi_later (PROP:=PROP))) (only parsing).
+
+(* An instance of [BiPureForall] is derivable if we assume excluded middle in
+Coq, see the lemma [bi_pure_forall_em] in [derived_laws]. *)
+Class BiPureForall (PROP : bi) :=
+  pure_forall_2 : ∀ {A} (φ : A → Prop), (∀ a, ⌜ φ a ⌝) ⊢@{PROP} ⌜ ∀ a, φ a ⌝.

theories/bi/derived_laws.v

@@ -526,18 +526,20 @@ Proof.
   - eapply pure_elim=> // -[?|?]; auto using pure_mono.
   - apply or_elim; eauto using pure_mono.
 Qed.
-Lemma pure_impl φ1 φ2 : ⌜φ1 → φ2⌝ ⊣⊢ (⌜φ1⌝ → ⌜φ2⌝).
-Proof.
-  apply (anti_symm _).
-  - apply impl_intro_l. rewrite -pure_and. apply pure_mono. naive_solver.
-  - rewrite -pure_forall_2. apply forall_intro=> ?.
-    by rewrite -(left_id True bi_and (_→_))%I (pure_True φ1) // impl_elim_r.
-Qed.
-Lemma pure_forall {A} (φ : A → Prop) : ⌜∀ x, φ x⌝ ⊣⊢ ∀ x, ⌜φ x⌝.
-Proof.
-  apply (anti_symm _); auto using pure_forall_2.
-  apply forall_intro=> x. eauto using pure_mono.
-Qed.
+Lemma pure_impl_1 φ1 φ2 : ⌜φ1 → φ2⌝ ⊢ (⌜φ1⌝ → ⌜φ2⌝).
+Proof. apply impl_intro_l. rewrite -pure_and. apply pure_mono. naive_solver. Qed.
+Lemma pure_impl_2 `{!BiPureForall PROP} φ1 φ2 : (⌜φ1⌝ → ⌜φ2⌝) ⊢ ⌜φ1 → φ2⌝.
+Proof.
+  rewrite -pure_forall_2. apply forall_intro=> ?.
+  by rewrite -(left_id True bi_and (_→_))%I (pure_True φ1) // impl_elim_r.
+Qed.
+Lemma pure_impl `{!BiPureForall PROP} φ1 φ2 : ⌜φ1 → φ2⌝ ⊣⊢ (⌜φ1⌝ → ⌜φ2⌝).
+Proof. apply (anti_symm _); auto using pure_impl_1, pure_impl_2. Qed.
+Lemma pure_forall_1 {A} (φ : A → Prop) : ⌜∀ x, φ x⌝ ⊢ ∀ x, ⌜φ x⌝.
+Proof. apply forall_intro=> x. eauto using pure_mono. Qed.
+Lemma pure_forall `{!BiPureForall PROP} {A} (φ : A → Prop) :
+  ⌜∀ x, φ x⌝ ⊣⊢ ∀ x, ⌜φ x⌝.
+Proof. apply (anti_symm _); auto using pure_forall_1, pure_forall_2. Qed.
 Lemma pure_exist {A} (φ : A → Prop) : ⌜∃ x, φ x⌝ ⊣⊢ ∃ x, ⌜φ x⌝.
 Proof.
   apply (anti_symm _).

theories/bi/interface.v

@@ -65,9 +65,6 @@ Section bi_mixin.
     (** Higher-order logic *)
     bi_mixin_pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ ⌝;
     bi_mixin_pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P;
-    (* This is actually derivable if we assume excluded middle in Coq,
-       via [(∀ a, φ a) ∨ (∃ a, ¬φ a)]. *)
-    bi_mixin_pure_forall_2 {A} (φ : A → Prop) : (∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝;
 
     bi_mixin_and_elim_l P Q : P ∧ Q ⊢ P;
     bi_mixin_and_elim_r P Q : P ∧ Q ⊢ Q;
@@ -310,8 +307,6 @@ Lemma pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ ⌝.
 Proof. eapply bi_mixin_pure_intro, bi_bi_mixin. Qed.
 Lemma pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P.
 Proof. eapply bi_mixin_pure_elim', bi_bi_mixin. Qed.
-Lemma pure_forall_2 {A} (φ : A → Prop) : (∀ a, ⌜ φ a ⌝) ⊢@{PROP} ⌜ ∀ a, φ a ⌝.
-Proof. eapply bi_mixin_pure_forall_2, bi_bi_mixin. Qed.
 
 Lemma and_elim_l P Q : P ∧ Q ⊢ P.
 Proof. eapply bi_mixin_and_elim_l, bi_bi_mixin. Qed.

theories/bi/monpred.v

@@ -259,7 +259,6 @@ Proof.
     + intros [[] []]. split=>i. by apply bi.equiv_spec.
   - intros P φ ?. split=> i. by apply bi.pure_intro.
   - intros φ P HP. split=> i. apply bi.pure_elim'=> ?. by apply HP.
-  - intros A φ. split=> i. by apply bi.pure_forall_2.
   - intros P Q. split=> i. by apply bi.and_elim_l.
   - intros P Q. split=> i. by apply bi.and_elim_r.
   - intros P Q R [?] [?]. split=> i. by apply bi.and_intro.
@@ -402,6 +401,9 @@ Proof. unseal. split. solve_proper. Qed.
 Global Instance monPred_in_flip_mono : Proper ((⊑) ==> flip (⊢)) (@monPred_in I PROP).
 Proof. solve_proper. Qed.
 
+Global Instance monPred_pure_forall : BiPureForall PROP → BiPureForall monPredI.
+Proof. intros ? A φ. split=> /= i. unseal. by apply pure_forall_2. Qed.
+
 Global Instance monPred_later_contractive :
   BiLaterContractive PROP → BiLaterContractive monPredI.
 Proof. unseal=> ? n P Q HPQ. split=> i /=. f_contractive. apply HPQ. Qed.

theories/proofmode/class_instances.v

@@ -155,9 +155,9 @@ Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.
 Global Instance into_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
   IntoPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 ∨ P2) (φ1 ∨ φ2).
 Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed.
-Global Instance into_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
+Global Instance into_pure_pure_impl `{!BiPureForall PROP} (φ1 φ2 : Prop) P1 P2 :
   FromPure false P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 → P2) (φ1 → φ2).
-Proof. rewrite /FromPure /IntoPure pure_impl=> <- -> //. Qed.
+Proof. rewrite /FromPure /IntoPure /= => <- ->. apply pure_impl_2. Qed.
 
 Global Instance into_pure_exist {A} (Φ : A → PROP) (φ : A → Prop) :
   (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∃ x, Φ x) (∃ x, φ x).
@@ -165,10 +165,12 @@ Proof. rewrite /IntoPure=>Hx. rewrite pure_exist. by setoid_rewrite Hx. Qed.
 Global Instance into_pure_texist {TT : tele} (Φ : TT → PROP) (φ : TT → Prop) :
   (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∃.. x, Φ x) (∃.. x, φ x).
 Proof. rewrite /IntoPure texist_exist bi_texist_exist. apply into_pure_exist. Qed.
-Global Instance into_pure_forall {A} (Φ : A → PROP) (φ : A → Prop) :
+Global Instance into_pure_forall `{!BiPureForall PROP}
+    {A} (Φ : A → PROP) (φ : A → Prop) :
   (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∀ x, Φ x) (∀ x, φ x).
 Proof. rewrite /IntoPure=>Hx. rewrite -pure_forall_2. by setoid_rewrite Hx. Qed.
-Global Instance into_pure_tforall {TT : tele} (Φ : TT → PROP) (φ : TT → Prop) :
+Global Instance into_pure_tforall `{!BiPureForall PROP}
+    {TT : tele} (Φ : TT → PROP) (φ : TT → Prop) :
   (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∀.. x, Φ x) (∀.. x, φ x).
 Proof.
   rewrite /IntoPure !tforall_forall bi_tforall_forall. apply into_pure_forall.
@@ -177,7 +179,7 @@ Qed.
 Global Instance into_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
   IntoPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 ∗ P2) (φ1 ∧ φ2).
 Proof. rewrite /IntoPure=> -> ->. by rewrite sep_and pure_and. Qed.
-Global Instance into_pure_pure_wand a (φ1 φ2 : Prop) P1 P2 :
+Global Instance into_pure_pure_wand `{!BiPureForall PROP} a (φ1 φ2 : Prop) P1 P2 :
   FromPure a P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 -∗ P2) (φ1 → φ2).
 Proof.
   rewrite /FromPure /IntoPure=> <- -> /=. rewrite pure_impl.
@@ -218,7 +220,7 @@ Qed.
 Global Instance from_pure_pure_impl a (φ1 φ2 : Prop) P1 P2 :
   IntoPure P1 φ1 → FromPure a P2 φ2 → FromPure a (P1 → P2) (φ1 → φ2).
 Proof.
-  rewrite /FromPure /IntoPure pure_impl=> -> <-. destruct a=>//=.
+  rewrite /FromPure /IntoPure pure_impl_1=> -> <-. destruct a=>//=.
   apply bi.impl_intro_l. by rewrite affinely_and_r bi.impl_elim_r.
 Qed.
 
@@ -234,7 +236,7 @@ Proof. rewrite /FromPure texist_exist bi_texist_exist. apply from_pure_exist. Qe
 Global Instance from_pure_forall {A} a (Φ : A → PROP) (φ : A → Prop) :
   (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (∀ x, Φ x) (∀ x, φ x).
 Proof.
-  rewrite /FromPure=>Hx. rewrite pure_forall. setoid_rewrite <-Hx.
+  rewrite /FromPure=>Hx. rewrite pure_forall_1. setoid_rewrite <-Hx.
   destruct a=>//=. apply affinely_forall.
 Qed.
 Global Instance from_pure_tforall {TT : tele} a (Φ : TT → PROP) (φ : TT → Prop) :
@@ -260,8 +262,8 @@ Proof.
   destruct a; simpl.
   - destruct Ha as [Ha|?]; first inversion Ha.
     rewrite -persistent_and_affinely_sep_r -(affine_affinely P1) HP1.
-    by rewrite affinely_and_l pure_impl impl_elim_r.
-  - by rewrite HP1 sep_and pure_impl impl_elim_r.
+    by rewrite affinely_and_l pure_impl_1 impl_elim_r.
+  - by rewrite HP1 sep_and pure_impl_1 impl_elim_r.
 Qed.
 
 Global Instance from_pure_persistently P a φ :
@@ -880,15 +882,16 @@ Proof. by rewrite /FromForall. Qed.
 Global Instance from_forall_tforall {TT : tele} (Φ : TT → PROP) name :
   AsIdentName Φ name → FromForall (bi_tforall Φ) Φ name.
 Proof. by rewrite /FromForall bi_tforall_forall. Qed.
-Global Instance from_forall_pure {A} (φ : A → Prop) name :
+Global Instance from_forall_pure `{!BiPureForall PROP} {A} (φ : A → Prop) name :
   AsIdentName φ name → @FromForall PROP A ⌜∀ a : A, φ a⌝ (λ a, ⌜ φ a ⌝)%I name.
-Proof. by rewrite /FromForall pure_forall. Qed.
-Global Instance from_tforall_pure {TT : tele} (φ : TT → Prop) name :
+Proof. by rewrite /FromForall pure_forall_2. Qed.
+Global Instance from_tforall_pure `{!BiPureForall PROP}
+    {TT : tele} (φ : TT → Prop) name :
   AsIdentName φ name → @FromForall PROP TT ⌜tforall φ⌝ (λ x, ⌜ φ x ⌝)%I name.
 Proof. by rewrite /FromForall tforall_forall pure_forall. Qed.
 
 (* [H] is the default name for the [φ] hypothesis, in the following three instances *)
-Global Instance from_forall_pure_not (φ : Prop) :
+Global Instance from_forall_pure_not `{!BiPureForall PROP} (φ : Prop) :
   @FromForall PROP φ ⌜¬ φ⌝ (λ _ : φ, False)%I (to_ident_name H).
 Proof. by rewrite /FromForall pure_forall. Qed.
 Global Instance from_forall_impl_pure P Q φ :

theories/si_logic/bi.v

@@ -37,7 +37,6 @@ Proof.
   - solve_proper.
   - exact: pure_intro.
   - exact: pure_elim'.
-  - exact: @pure_forall_2.
   - exact: and_elim_l.
   - exact: and_elim_r.
   - exact: and_intro.
@@ -116,6 +115,9 @@ Canonical Structure siPropI : bi :=
   {| bi_ofe_mixin := ofe_mixin_of siProp;
      bi_bi_mixin := siProp_bi_mixin; bi_bi_later_mixin := siProp_bi_later_mixin |}.
 
+Instance siProp_pure_forall : BiPureForall siPropI.
+Proof. exact: @pure_forall_2. Qed.
+
 Instance siProp_later_contractive : BiLaterContractive siPropI.
 Proof. apply later_contractive. Qed.