Implement `iRewrite` using type classes.

theories/proofmode/class_instances.v

@@ -142,6 +142,14 @@ Proof.
   rewrite -Hx. apply pure_intro. done.
 Qed.
 
+(* IntoInternalEq *)
+Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
+  @IntoInternalEq PROP A (x ≡ y) x y.
+Proof. by rewrite /IntoInternalEq. Qed.
+Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
+  IntoInternalEq P x y → IntoInternalEq (□ P) x y.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
+
 (* IntoPersistent *)
 Global Instance into_persistent_persistently_trans p P Q :
   IntoPersistent true P Q → IntoPersistent p (□ P) Q | 0.

theories/proofmode/classes.v

@@ -54,6 +54,11 @@ Class FromPure {M} (P : uPred M) (φ : Prop) := from_pure : ⌜φ⌝ ⊢ P.
 Arguments from_pure {_} _ _ {_}.
 Hint Mode FromPure + ! - : typeclass_instances.
 
+Class IntoInternalEq {M} {A : ofeT} (P : uPred M) (x y : A) :=
+  into_internal_eq : P ⊢ x ≡ y.
+Arguments into_internal_eq {_ _} _ _ _ {_}.
+Hint Mode IntoInternalEq + - ! - - : typeclass_instances.
+
 Class IntoPersistent {M} (p : bool) (P Q : uPred M) :=
   into_persistent : □?p P ⊢ □ Q.
 Arguments into_persistent {_} _ _ _ {_}.

theories/proofmode/coq_tactics.v

@@ -768,7 +768,7 @@ Qed.
 Lemma tac_rewrite Δ i p Pxy d Q :
   envs_lookup i Δ = Some (p, Pxy) →
   ∀ {A : ofeT} (x y : A) (Φ : A → uPred M),
-    (Pxy ⊢ x ≡ y) →
+    IntoInternalEq Pxy x y →
     (Q ⊣⊢ Φ (if d is Left then y else x)) →
     NonExpansive Φ →
     (Δ ⊢ Φ (if d is Left then x else y)) → Δ ⊢ Q.
@@ -784,7 +784,7 @@ Lemma tac_rewrite_in Δ i p Pxy j q P d Q :
   envs_lookup i Δ = Some (p, Pxy) →
   envs_lookup j Δ = Some (q, P) →
   ∀ {A : ofeT} Δ' x y (Φ : A → uPred M),
-    (Pxy ⊢ x ≡ y) →
+    IntoInternalEq Pxy x y →
     (P ⊣⊢ Φ (if d is Left then y else x)) →
     NonExpansive Φ →
     envs_simple_replace j q (Esnoc Enil j (Φ (if d is Left then x else y))) Δ = Some Δ' →

theories/proofmode/tactics.v

@@ -1628,11 +1628,9 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
   iPoseProofCore lem as true true (fun Heq =>
     eapply (tac_rewrite _ Heq _ _ lr);
       [env_reflexivity || fail "iRewrite:" Heq "not found"
-      |let P := match goal with |- ?P ⊢ _ => P end in
-       (* use ssreflect apply: which is better at dealing with unification
-       involving canonical structures. This is useful for the COFE canonical
-       structure in uPred_eq that it may have to infer. *)
-       apply: reflexivity || fail "iRewrite:" P "not an equality"
+      |apply _ ||
+       let P := match goal with |- IntoInternalEq ?P _ _ ⊢ _ => P end in
+       fail "iRewrite:" P "not an equality"
       |iRewriteFindPred
       |intros ??? ->; reflexivity|lazy beta; iClear Heq]).
 
@@ -1644,8 +1642,8 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H)
     eapply (tac_rewrite_in _ Heq _ _ H _ _ lr);
       [env_reflexivity || fail "iRewrite:" Heq "not found"
       |env_reflexivity || fail "iRewrite:" H "not found"
-      |apply: reflexivity ||
-       let P := match goal with |- ?P ⊢ _ => P end in
+      |apply _ ||
+       let P := match goal with |- IntoInternalEq ?P _ _ ⊢ _ => P end in
        fail "iRewrite:" P "not an equality"
       |iRewriteFindPred
       |intros ??? ->; reflexivity