Only require `∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q)` for the modality when it's actually needed.

theories/proofmode/class_instances.v

@@ -10,7 +10,7 @@ Section always_modalities.
     always_modality_mixin (@bi_persistently PROP) AIEnvId AIEnvClear.
   Proof.
     split; eauto using equiv_entails_sym, persistently_intro, persistently_mono,
-      persistently_and, persistently_sep_2 with typeclass_instances.
+      persistently_sep_2 with typeclass_instances.
   Qed.
   Definition always_modality_persistently :=
     AlwaysModality _ always_modality_persistently_mixin.
@@ -19,7 +19,7 @@ Section always_modalities.
     always_modality_mixin (@bi_affinely PROP) AIEnvId (AIEnvForall Affine).
   Proof.
     split; eauto using equiv_entails_sym, affinely_intro, affinely_mono,
-      affinely_and, affinely_sep_2 with typeclass_instances.
+      affinely_sep_2 with typeclass_instances.
   Qed.
   Definition always_modality_affinely :=
     AlwaysModality _ always_modality_affinely_mixin.
@@ -29,7 +29,7 @@ Section always_modalities.
   Proof.
     split; eauto using equiv_entails_sym, affinely_persistently_emp,
       affinely_mono, persistently_mono, affinely_persistently_idemp,
-      affinely_persistently_and, affinely_persistently_sep_2 with typeclass_instances.
+      affinely_persistently_sep_2 with typeclass_instances.
   Qed.
   Definition always_modality_affinely_persistently :=
     AlwaysModality _ always_modality_affinely_persistently_mixin.
@@ -37,7 +37,7 @@ Section always_modalities.
   Lemma always_modality_plainly_mixin :
     always_modality_mixin (@bi_plainly PROP) (AIEnvForall Plain) AIEnvClear.
   Proof.
-    split; eauto using equiv_entails_sym, plainly_intro, plainly_mono,
+    split; split_and?; eauto using equiv_entails_sym, plainly_intro, plainly_mono,
       plainly_and, plainly_sep_2 with typeclass_instances.
   Qed.
   Definition always_modality_plainly :=
@@ -46,7 +46,7 @@ Section always_modalities.
   Lemma always_modality_affinely_plainly_mixin :
     always_modality_mixin (λ P : PROP, ■ P)%I (AIEnvForall Plain) AIEnvIsEmpty.
   Proof.
-    split; eauto using equiv_entails_sym, affinely_plainly_emp, affinely_intro,
+    split; split_and?; eauto using equiv_entails_sym, affinely_plainly_emp, affinely_intro,
       plainly_intro, affinely_mono, plainly_mono, affinely_plainly_idemp,
       affinely_plainly_and, affinely_plainly_sep_2 with typeclass_instances.
   Qed.

theories/proofmode/classes.v

@@ -123,8 +123,8 @@ Record always_modality_mixin {PROP : bi} (M : PROP → PROP)
   always_modality_mixin_persistent :
     match pspec with
     | AIEnvIsEmpty => True
-    | AIEnvForall C => ∀ P, C P → □ P ⊢ M (□ P)
-    | AIEnvTransform C => ∀ P Q, C P Q → □ P ⊢ M (□ Q)
+    | AIEnvForall C => (∀ P, C P → □ P ⊢ M (□ P)) ∧ (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q))
+    | AIEnvTransform C => (∀ P Q, C P Q → □ P ⊢ M (□ Q)) ∧ (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q))
     | AIEnvClear => True
     | AIEnvId => ∀ P, □ P ⊢ M (□ P)
     end;
@@ -138,7 +138,6 @@ Record always_modality_mixin {PROP : bi} (M : PROP → PROP)
     end;
   always_modality_mixin_emp : emp ⊢ M emp;
   always_modality_mixin_mono P Q : (P ⊢ Q) → M P ⊢ M Q;
-  always_modality_mixin_and P Q : M P ∧ M Q ⊢ M (P ∧ Q);
   always_modality_mixin_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q)
 }.
 
@@ -160,9 +159,15 @@ Section always_modality.
   Lemma always_modality_persistent_forall C P :
     always_modality_persistent_spec M = AIEnvForall C → C P → □ P ⊢ M (□ P).
   Proof. destruct M as [??? []]; naive_solver. Qed.
+  Lemma always_modality_and_forall C P Q :
+    always_modality_persistent_spec M = AIEnvForall C → M P ∧ M Q ⊢ M (P ∧ Q).
+  Proof. destruct M as [??? []]; naive_solver. Qed.
   Lemma always_modality_persistent_transform C P Q :
     always_modality_persistent_spec M = AIEnvTransform C → C P Q → □ P ⊢ M (□ Q).
   Proof. destruct M as [??? []]; naive_solver. Qed.
+  Lemma always_modality_and_transform C P Q :
+    always_modality_persistent_spec M = AIEnvTransform C → M P ∧ M Q ⊢ M (P ∧ Q).
+  Proof. destruct M as [??? []]; naive_solver. Qed.
   Lemma always_modality_persistent_id P :
     always_modality_persistent_spec M = AIEnvId → □ P ⊢ M (□ P).
   Proof. destruct M as [??? []]; naive_solver. Qed.
@@ -183,8 +188,6 @@ Section always_modality.
   Proof. eapply always_modality_mixin_emp, always_modality_mixin_of. Qed.
   Lemma always_modality_mono P Q : (P ⊢ Q) → M P ⊢ M Q.
   Proof. eapply always_modality_mixin_mono, always_modality_mixin_of. Qed.
-  Lemma always_modality_and P Q : M P ∧ M Q ⊢ M (P ∧ Q).
-  Proof. eapply always_modality_mixin_and, always_modality_mixin_of. Qed.
   Lemma always_modality_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q).
   Proof. eapply always_modality_mixin_sep, always_modality_mixin_of. Qed.
   Global Instance always_modality_mono' : Proper ((⊢) ==> (⊢)) M.
@@ -200,7 +203,7 @@ Section always_modality.
   Proof.
     induction 2 as [|P Ps ? _ IH]; simpl.
     - by rewrite persistently_pure affinely_True_emp affinely_emp -always_modality_emp.
-    - rewrite affinely_persistently_and -always_modality_and -IH.
+    - rewrite affinely_persistently_and -always_modality_and_forall // -IH.
       by rewrite {1}(always_modality_persistent_forall _ P).
   Qed.
   Lemma always_modality_spatial_forall_big_sep C Ps :

theories/proofmode/coq_tactics.v

@@ -589,6 +589,7 @@ Class TransformPersistentEnv
     (M : always_modality PROP) (C : PROP → PROP → Prop) (Γ1 Γ2 : env PROP) := {
   transform_persistent_env :
     (∀ P Q, C P Q → □ P ⊢ M (□ Q)) →
+    (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q)) →
     □ ([∧] Γ1) ⊢ M (□ ([∧] Γ2));
   transform_persistent_env_wf : env_wf Γ1 → env_wf Γ2;
   transform_persistent_env_dom i : Γ1 !! i = None → Γ2 !! i = None;
@@ -604,8 +605,8 @@ Global Instance transform_persistent_env_snoc M (C : PROP → PROP → Prop) Γ
   TransformPersistentEnv M C (Esnoc Γ i P) (Esnoc Γ' i Q).
 Proof.
   intros ? [HΓ Hwf Hdom]; split; simpl.
-  - intros HC. rewrite affinely_persistently_and HC // HΓ //.
-    by rewrite always_modality_and -affinely_persistently_and.
+  - intros HC Hand. rewrite affinely_persistently_and HC // HΓ //.
+    by rewrite Hand -affinely_persistently_and.
   - inversion 1; constructor; auto.
   - intros j. destruct (ident_beq _ _); naive_solver.
 Qed.
@@ -614,7 +615,7 @@ Global Instance transform_persistent_env_snoc_not M (C : PROP → PROP → Prop)
   TransformPersistentEnv M C (Esnoc Γ i P) Γ' | 100.
 Proof.
   intros [HΓ Hwf Hdom]; split; simpl.
-  - intros HC. by rewrite and_elim_r HΓ.
+  - intros HC Hand. by rewrite and_elim_r HΓ.
   - inversion 1; auto.
   - intros j. destruct (ident_beq _ _); naive_solver.
 Qed.
@@ -702,7 +703,8 @@ Proof.
     + by rewrite {1}affinely_elim_emp (always_modality_emp M)
         persistently_True_emp affinely_persistently_emp.
     + eauto using always_modality_persistent_forall_big_and.
-    + eauto using always_modality_persistent_transform.
+    + eauto using always_modality_persistent_transform,
+        always_modality_and_transform.
     + by rewrite {1}affinely_elim_emp (always_modality_emp M)
         persistently_True_emp affinely_persistently_emp.
     + eauto using always_modality_persistent_id. }