Special proof mode class for adding a modality to a goal.

This used to be done by using `ElimModal` in backwards direction. Having
a separate type class for this gets rid of some hacks:

- Both `Hint Mode`s in forward and backwards direction for `ElimModal`.
- Weird type class precedence hacks to make sure the right instance is picked.
  These were needed because using `ElimModal` in backwards direction caused
  ambiguity.

theories/base_logic/lib/fancy_updates.v

@@ -211,17 +211,18 @@ Section proofmode_classes.
   Global Instance from_modal_fupd E P : FromModal (|={E}=> P) P.
   Proof. rewrite /FromModal. apply fupd_intro. Qed.
 
-  (* Put a lower priority compared to [elim_modal_fupd_fupd], so that
-     it is not taken when the first parameter is not specified (in
-     spec. patterns). *)
   Global Instance elim_modal_bupd_fupd E1 E2 P Q :
-    ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
+    ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
   Proof.
     by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
   Qed.
   Global Instance elim_modal_fupd_fupd E1 E2 E3 P Q :
     ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
   Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
+
+  Global Instance add_modal_fupd E1 E2 P Q :
+    AddModal (|={E1}=> P) P (|={E1,E2}=> Q).
+  Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_trans. Qed.
 End proofmode_classes.
 
 Hint Extern 2 (coq_tactics.envs_entails _ (|={_}=> _)) => iModIntro.

theories/program_logic/weakestpre.v

@@ -393,10 +393,13 @@ Section proofmode_classes.
     ElimModal (|={E}=> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
   Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
 
-  (* lower precedence, if possible, it should persistently pick elim_upd_fupd_wp *)
   Global Instance elim_modal_fupd_wp_atomic s E1 E2 e P Φ :
     Atomic (stuckness_to_atomicity s) e →
     ElimModal (|={E1,E2}=> P) P
-            (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
+            (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I.
   Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
+
+  Global Instance add_modal_fupd_wp s E e P Φ :
+    AddModal (|={E}=> P) P (WP e @ s; E {{ Φ }}).
+  Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_wp. Qed.
 End proofmode_classes.

theories/proofmode/class_instances.v

@@ -881,6 +881,22 @@ Proof.
   intros _ _. by rewrite /ElimModal wand_elim_r.
 Qed.
 
+(* AddModal *)
+Global Instance add_modal_wand P P' Q R :
+  AddModal P P' Q → AddModal P P' (R -∗ Q).
+Proof.
+  rewrite /AddModal=> H. apply wand_intro_r.
+  by rewrite wand_curry -assoc (comm _ P') -wand_curry wand_elim_l.
+Qed.
+Global Instance add_modal_forall {A} P P' (Φ : A → uPred M) :
+  (∀ x, AddModal P P' (Φ x)) → AddModal P P' (∀ x, Φ x).
+Proof.
+  rewrite /AddModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
+Qed.
+Global Instance add_modal_bupd P Q : AddModal (|==> P) P (|==> Q).
+Proof. by rewrite /AddModal bupd_frame_r wand_elim_r bupd_trans. Qed.
+
+(** IsExcept0 *)
 Global Instance is_except_0_except_0 P : IsExcept0 (◇ P).
 Proof. by rewrite /IsExcept0 except_0_idemp. Qed.
 Global Instance is_except_0_later P : IsExcept0 (▷ P).

theories/proofmode/classes.v

@@ -236,10 +236,16 @@ Class ElimModal {M} (P P' : uPred M) (Q Q' : uPred M) :=
   elim_modal : P ∗ (P' -∗ Q') ⊢ Q.
 Arguments elim_modal {_} _ _ _ _ {_}.
 Hint Mode ElimModal + ! - ! - : typeclass_instances.
-Hint Mode ElimModal + - ! - ! : typeclass_instances.
 
-Lemma elim_modal_dummy {M} (P Q : uPred M) : ElimModal P P Q Q.
-Proof. by rewrite /ElimModal wand_elim_r. Qed.
+(* Used by the specialization pattern [ > ] in [iSpecialize] and [iAssert] to
+add a modality to the goal corresponding to a premise/asserted proposition. *)
+Class AddModal {M} (P P' : uPred M) (Q : uPred M) :=
+  add_modal : P ∗ (P' -∗ Q) ⊢ Q.
+Arguments add_modal {_} _ _ _ {_}.
+Hint Mode AddModal + - ! ! : typeclass_instances.
+
+Lemma add_modal_id {M} (P Q : uPred M) : AddModal P P Q.
+Proof. by rewrite /AddModal wand_elim_r. Qed.
 
 Class IsExcept0 {M} (Q : uPred M) := is_except_0 : ◇ Q ⊢ Q.
 Arguments is_except_0 {_} _ {_}.

theories/proofmode/coq_tactics.v

@@ -644,7 +644,7 @@ Qed.
 
 Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q neg js R P1 P2 P1' Q :
   envs_lookup_delete j Δ = Some (q, R, Δ') →
-  IntoWand false R P1 P2 → ElimModal P1' P1 Q Q →
+  IntoWand false R P1 P2 → AddModal P1' P1 Q →
   (''(Δ1,Δ2) ← envs_split (if neg is true then Right else Left) js Δ';
     Δ2' ← envs_app false (Esnoc Enil j P2) Δ2;
     Some (Δ1,Δ2')) = Some (Δ1,Δ2') → (* does not preserve position of [j] *)
@@ -656,7 +656,7 @@ Proof.
   rewrite envs_lookup_sound // envs_split_sound //.
   rewrite (envs_app_sound Δ2) //; simpl.
   rewrite right_id (into_wand _ R) HP1 assoc -(comm _ P1') -assoc.
-  rewrite -(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
+  rewrite -(add_modal P1' P1 Q). apply sep_mono_r, wand_intro_l.
   by rewrite persistently_if_elim assoc !wand_elim_r.
 Qed.
 
@@ -666,7 +666,7 @@ Proof. by unlock. Qed.
 Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
   envs_lookup_delete j Δ = Some (q, R, Δ') →
   IntoWand false R P1 P2 →
-  ElimModal P1' P1 Q Q →
+  AddModal P1' P1 Q →
   envs_entails Δ' (P1' ∗ locked Q') →
   Q' = (P2 -∗ Q)%I →
   envs_entails Δ Q.
@@ -674,7 +674,7 @@ Proof.
   rewrite /envs_entails. intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
   rewrite envs_lookup_sound //. rewrite HPQ -lock.
   rewrite (into_wand _ R) assoc -(comm _ P1') -assoc persistently_if_elim.
-  rewrite -{2}(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
+  rewrite -{2}(add_modal P1' P1 Q). apply sep_mono_r, wand_intro_l.
   by rewrite assoc !wand_elim_r.
 Qed.
 
@@ -748,7 +748,7 @@ Proof.
 Qed.
 
 Lemma tac_assert Δ Δ1 Δ2 Δ2' neg js j P P' Q :
-  ElimModal P' P Q Q →
+  AddModal P' P Q →
   envs_split (if neg is true then Right else Left) js Δ = Some (Δ1,Δ2) →
   envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' →
   envs_entails Δ1 P' → envs_entails Δ2' Q → envs_entails Δ Q.

theories/proofmode/tactics.v

@@ -456,7 +456,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
          [env_reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
          |lazymatch m with
-          | GSpatial => apply elim_modal_dummy
+          | GSpatial => apply add_modal_id
           | GModal => apply _ || fail "iSpecialize: goal not a modality"
           end
          |env_reflexivity ||
@@ -479,7 +479,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
          [env_reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
          |lazymatch m with
-          | GSpatial => apply elim_modal_dummy
+          | GSpatial => apply add_modal_id
           | GModal => apply _ || fail "iSpecialize: goal not a modality"
           end
          |iFrame "∗ #"; apply tac_unlock ||
@@ -1588,7 +1588,7 @@ Tactic Notation "iAssertCore" open_constr(Q)
      | false =>
        eapply tac_assert with _ _ _ lr Hs' H Q _;
          [lazymatch m with
-          | GSpatial => apply elim_modal_dummy
+          | GSpatial => apply add_modal_id
           | GModal => apply _ || fail "iAssert: goal not a modality"
           end
          |env_reflexivity ||