State `internal_eq_rewrite` in the logic.

This way, it can be used with `iApply`.

CHANGELOG.md

@@ -85,6 +85,8 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
   of evars, which often led to divergence. There are a few places where type
   annotations are now needed.
 * Move the `prelude` folder to its own project: std++
+* The rules `internal_eq_rewrite` and `internal_eq_rewrite_contractive` are now
+  stated in the logic, i.e. they are `iApply` friendly.
 
 ## Iris 3.0.0 (released 2017-01-11)
 

theories/base_logic/derived.v

@@ -298,13 +298,19 @@ Hint Resolve internal_eq_refl'.
 Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
 Proof. by intros ->. Qed.
 Lemma internal_eq_sym {A : ofeT} (a b : A) : a ≡ b ⊢ b ≡ a.
-Proof. apply (internal_eq_rewrite a b (λ b, b ≡ a)%I); auto. solve_proper. Qed.
-Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → uPred M) P
-  {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
 Proof.
-  move: HΨ=> /contractiveI HΨ Heq ?.
-  apply (internal_eq_rewrite (Ψ a) (Ψ b) id _)=>//=. by rewrite -HΨ.
+  rewrite (internal_eq_rewrite a b (λ b, b ≡ a)%I ltac:(solve_proper)).
+  by rewrite -internal_eq_refl True_impl.
 Qed.
+Lemma f_equiv {A B : ofeT} (f : A → B) `{!NonExpansive f} x y :
+  x ≡ y ⊢ f x ≡ f y.
+Proof.
+  rewrite (internal_eq_rewrite x y (λ y, f x ≡ f y)%I ltac:(solve_proper)).
+  by rewrite -internal_eq_refl True_impl.
+Qed.
+Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → uPred M)
+  {HΨ : Contractive Ψ} : ▷ (a ≡ b) ⊢ Ψ a → Ψ b.
+Proof. move: HΨ=> /contractiveI ->. by rewrite (internal_eq_rewrite _ _ id). Qed.
 
 Lemma pure_impl_forall φ P : (⌜φ⌝ → P) ⊣⊢ (∀ _ : φ, P).
 Proof.
@@ -345,8 +351,8 @@ Lemma equiv_iff P Q : (P ⊣⊢ Q) → (P ↔ Q)%I.
 Proof. intros ->; apply iff_refl. Qed.
 Lemma internal_eq_iff P Q : P ≡ Q ⊢ P ↔ Q.
 Proof.
-  apply (internal_eq_rewrite P Q (λ Q, P ↔ Q))%I;
-    first solve_proper; auto using iff_refl.
+  rewrite (internal_eq_rewrite P Q (λ Q, P ↔ Q)%I ltac:(solve_proper)).
+  by rewrite -(iff_refl True) True_impl.
 Qed.
 
 (* Derived BI Stuff *)
@@ -531,9 +537,8 @@ Qed.
 Lemma plainly_internal_eq {A:ofeT} (a b : A) : ■ (a ≡ b) ⊣⊢ a ≡ b.
 Proof.
   apply (anti_symm (⊢)); auto using persistently_elim.
-  apply (internal_eq_rewrite a b (λ b, ■ (a ≡ b))%I); auto.
-  { intros n; solve_proper. }
-  rewrite -(internal_eq_refl a) plainly_pure; auto.
+  rewrite {1}(internal_eq_rewrite a b (λ b, ■ (a ≡ b))%I ltac:(solve_proper)).
+  by rewrite -internal_eq_refl plainly_pure True_impl.
 Qed.
 
 Lemma plainly_and_sep_l_1 P Q : ■ P ∧ Q ⊢ ■ P ∗ Q.
@@ -946,8 +951,8 @@ Global Instance ownM_timeless (a : M) : Discrete a → Timeless (uPred_ownM a).
 Proof.
   intros ?. rewrite /Timeless later_ownM. apply exist_elim=> b.
   rewrite (timelessP (a≡b)) (except_0_intro (uPred_ownM b)) -except_0_and.
-  apply except_0_mono. rewrite internal_eq_sym.
-  apply (internal_eq_rewrite b a (uPred_ownM)); first apply _; auto.
+  apply except_0_mono. rewrite internal_eq_sym. apply impl_elim_r'.
+  apply: internal_eq_rewrite.
 Qed.
 Global Instance from_option_timeless {A} P (Ψ : A → uPred M) (mx : option A) :
   (∀ x, Timeless (Ψ x)) → Timeless P → Timeless (from_option Ψ P mx).

theories/base_logic/lib/boxes.v

@@ -273,7 +273,7 @@ Proof.
     iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
     { by eapply lookup_insert_None. }
     { by apply (lookup_insert_None (delete γ f) γ1 γ2 true). }
-    iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
+    iNext. iApply (internal_eq_rewrite_contractive with "[#] Hbox").
     iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
   - iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done.
     iMod (slice_insert_empty with "Hbox") as (γ1 ?) "[#Hslice1 Hbox]".
@@ -281,7 +281,7 @@ Proof.
     iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
     { by eapply lookup_insert_None. }
     { by apply (lookup_insert_None (delete γ f) γ1 γ2 false). }
-    iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
+    iNext. iApply (internal_eq_rewrite_contractive with "[#] Hbox").
     iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
 Qed.
 
@@ -298,14 +298,14 @@ Proof.
     iMod (slice_insert_full _ _ _ _ (Q1 ∗ Q2)%I with "[$HQ1 $HQ2] Hbox")
       as (γ ?) "[#Hslice Hbox]"; first done.
     iExists γ. iIntros "{$% $#} !>". iNext.
-    eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
+    iApply (internal_eq_rewrite_contractive with "[#] Hbox").
     iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
   - iMod (slice_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done.
     iMod (slice_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)"; first done.
     { by simplify_map_eq. }
     iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
     iExists γ. iIntros "{$% $#} !>". iNext.
-    eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
+    iApply (internal_eq_rewrite_contractive with "[#] Hbox").
     iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
 Qed.
 End box.

theories/base_logic/lib/iprop.v

@@ -152,6 +152,5 @@ Lemma iProp_unfold_equivI {Σ} (P Q : iProp Σ) :
   iProp_unfold P ≡ iProp_unfold Q ⊢ (P ≡ Q : iProp Σ).
 Proof.
   rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q).
-  eapply (uPred.internal_eq_rewrite _ _ (λ z,
-    iProp_fold (iProp_unfold P) ≡ iProp_fold z))%I; auto with I; solve_proper.
+  apply: uPred.f_equiv.
 Qed.

theories/base_logic/lib/saved_prop.v

@@ -43,8 +43,6 @@ Section saved_prop.
     assert (∀ z, G2 (G1 z) ≡ z) as help.
     { intros z. rewrite /G1 /G2 -cFunctor_compose -{2}[z]cFunctor_id.
       apply (ne_proper (cFunctor_map F)); split=>?; apply iProp_fold_unfold. }
-    rewrite -{2}[x]help -{2}[y]help. apply later_mono.
-    apply (internal_eq_rewrite (G1 x) (G1 y) (λ z, G2 (G1 x) ≡ G2 z))%I;
-      first solve_proper; auto with I.
+    rewrite -{2}[x]help -{2}[y]help. apply later_mono, f_equiv, _.
   Qed.
 End saved_prop.

theories/base_logic/primitive.v

@@ -395,13 +395,9 @@ Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed.
 
 Lemma internal_eq_refl {A : ofeT} (a : A) : uPred_valid (M:=M) (a ≡ a).
 Proof. unseal; by split=> n x ??; simpl. Qed.
-Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → uPred M) P
-  {HΨ : NonExpansive Ψ} : (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b.
-Proof.
-  unseal; intros Hab Ha; split=> n x ??. apply HΨ with n a; auto.
-  - by symmetry; apply Hab with x.
-  - by apply Ha.
-Qed.
+Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → uPred M) :
+  NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
+Proof. intros HΨ. unseal; split=> n x ?? n' x' ??? Ha. by apply HΨ with n a. Qed.
 
 (* BI connectives *)
 Lemma sep_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q'.

theories/proofmode/coq_tactics.v

@@ -770,12 +770,14 @@ Lemma tac_rewrite Δ i p Pxy d Q :
   ∀ {A : ofeT} (x y : A) (Φ : A → uPred M),
     (Pxy ⊢ x ≡ y) →
     (Q ⊣⊢ Φ (if d is Left then y else x)) →
-    (NonExpansive Φ) →
+    NonExpansive Φ →
     (Δ ⊢ Φ (if d is Left then x else y)) → Δ ⊢ Q.
 Proof.
-  intros ? A x y ? HPxy -> ?; apply internal_eq_rewrite; auto.
-  rewrite {1}envs_lookup_sound' //; rewrite sep_elim_l HPxy.
-  destruct d; auto using internal_eq_sym.
+  intros ? A x y Φ HPxy -> ? HΔ.
+  rewrite -(idemp (∧)%I (of_envs Δ)) {1}envs_lookup_sound' //.
+  rewrite sep_elim_l HPxy HΔ. apply impl_elim_l'. destruct d.
+  - by apply internal_eq_rewrite.
+  - rewrite internal_eq_sym. by apply internal_eq_rewrite.
 Qed.
 
 Lemma tac_rewrite_in Δ i p Pxy j q P d Q :
@@ -784,20 +786,19 @@ Lemma tac_rewrite_in Δ i p Pxy j q P d Q :
   ∀ {A : ofeT} Δ' x y (Φ : A → uPred M),
     (Pxy ⊢ x ≡ y) →
     (P ⊣⊢ Φ (if d is Left then y else x)) →
-    (NonExpansive Φ) →
+    NonExpansive Φ →
     envs_simple_replace j q (Esnoc Enil j (Φ (if d is Left then x else y))) Δ = Some Δ' →
     (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ?? A Δ' x y Φ HPxy HP ?? <-.
-  rewrite -(idemp uPred_and Δ) {2}(envs_lookup_sound' _ i) //.
+  rewrite -(idemp uPred_and (of_envs Δ)) {2}(envs_lookup_sound' _ i) //.
   rewrite sep_elim_l HPxy and_sep_r.
   rewrite (envs_simple_replace_sound _ _ j) //; simpl.
-  rewrite HP right_id -assoc; apply wand_elim_r'. destruct d.
-  - apply (internal_eq_rewrite x y (λ y, □?q Φ y -∗ Δ')%I);
-      eauto with I. solve_proper.
-  - apply (internal_eq_rewrite y x (λ y, □?q Φ y -∗ Δ')%I);
-      eauto using internal_eq_sym with I.
-    solve_proper.
+  rewrite HP right_id -assoc (sep_and _ (_ ≡ _)).
+  apply wand_elim_r', impl_elim_r'. destruct d.
+  - apply (internal_eq_rewrite _ _ (λ y, □?q Φ y -∗ _)%I). solve_proper.
+  - rewrite internal_eq_sym.
+    apply (internal_eq_rewrite _ _ (λ y, □?q Φ y -∗ _)%I). solve_proper.
 Qed.
 
 (** * Conjunction splitting *)