Merge branch 'fix-direction-op-lemmas' into 'master'

Fix #256: Fix direction of f_op lemmas

Closes #256

See merge request iris/iris!303

CHANGELOG.md

@@ -161,6 +161,9 @@ Changes in Coq:
   `s/◯!/◯F/g; s/●!/●F/g;`.
 * Lemma `prop_ext` works in both directions; its default direction is the
   opposite of what it used to be.
+* Make direction of `f_op` rewrite lemmas more consistent: Flip `pair_op`,
+  `Cinl_op`, `Cinr_op`, `cmra_morphism_op`, `cmra_morphism_pcore`,
+  `cmra_morphism_core`.
 * Rename `C` suffixes into `O` since we no longer use COFEs but OFEs. Also
   rename `ofe_fun` into `discrete_fun` and the corresponding notation `-c>` into
   `-d>`. The renaming can be automatically done using the following script (on

tests/one_shot_once.v

@@ -40,7 +40,7 @@ Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=
 Lemma pending_split γ q :
   own γ (Pending q) ⊣⊢ own γ (Pending (q/2)) ∗ own γ (Pending (q/2)).
 Proof.
-  rewrite /Pending. rewrite -own_op Cinl_op. rewrite frac_op' Qp_div_2 //.
+  rewrite /Pending. rewrite -own_op -Cinl_op. rewrite frac_op' Qp_div_2 //.
 Qed.
 
 Lemma pending_shoot γ n :

theories/algebra/auth.v

@@ -299,11 +299,11 @@ Proof. by rewrite auth_both_frac_op. Qed.
 Lemma auth_auth_frac_op p q a : ●{p + q} a ≡ ●{p} a ⋅ ●{q} a.
 Proof.
   intros; split; simpl; last by rewrite left_id.
-  by rewrite -Some_op pair_op agree_idemp.
+  by rewrite -Some_op -pair_op agree_idemp.
 Qed.
 Lemma auth_auth_frac_op_invN n p a q b : ✓{n} (●{p} a ⋅ ●{q} b) → a ≡{n}≡ b.
 Proof.
-  rewrite /op /auth_op /= left_id -Some_op pair_op auth_validN_eq /=.
+  rewrite /op /auth_op /= left_id -Some_op -pair_op auth_validN_eq /=.
   intros (?&?& Eq &?&?). apply to_agree_injN, agree_op_invN. by rewrite Eq.
 Qed.
 Lemma auth_auth_frac_op_inv p a q b : ✓ (●{p} a ⋅ ●{q} b) → a ≡ b.
@@ -388,7 +388,7 @@ Lemma auth_local_update (a b0 b1 a' b0' b1': A) :
 Proof.
   rewrite !local_update_unital=> Hup ? ? n /=.
     move=> [[[qc ac]|] bc] /auth_both_validN [Le Val] [] /=.
-  - move => Ha. exfalso. move : Ha. rewrite right_id -Some_op pair_op.
+  - move => Ha. exfalso. move : Ha. rewrite right_id -Some_op -pair_op.
     move => /Some_dist_inj [/=]. rewrite frac_op' => Eq _.
     apply (Qp_not_plus_q_ge_1 qc). by rewrite -Eq.
   - move => _. rewrite !left_id=> ?.
@@ -442,8 +442,7 @@ Proof.
     naive_solver eauto using cmra_morphism_monotoneN, cmra_morphism_validN.
   - intros [??]. apply Some_proper; rewrite /auth_map /=.
     by f_equiv; rewrite /= cmra_morphism_core.
-  - intros [[[??]|]?] [[[??]|]?]; try apply Auth_proper=>//=; try by rewrite cmra_morphism_op.
-    by rewrite -Some_op pair_op cmra_morphism_op.
+  - intros [[[??]|]?] [[[??]|]?]; try apply Auth_proper=>//=; by rewrite cmra_morphism_op.
 Qed.
 Definition authO_map {A B} (f : A -n> B) : authO A -n> authO B :=
   OfeMor (auth_map f).

theories/algebra/cmra.v

@@ -251,8 +251,8 @@ Hint Mode CmraDiscrete ! : typeclass_instances.
 Class CmraMorphism {A B : cmraT} (f : A → B) := {
   cmra_morphism_ne :> NonExpansive f;
   cmra_morphism_validN n x : ✓{n} x → ✓{n} f x;
-  cmra_morphism_pcore x : pcore (f x) ≡ f <$> pcore x;
-  cmra_morphism_op x y : f x ⋅ f y ≡ f (x ⋅ y)
+  cmra_morphism_pcore x : f <$> pcore x ≡ pcore (f x);
+  cmra_morphism_op x y : f (x ⋅ y) ≡ f x ⋅ f y
 }.
 Arguments cmra_morphism_validN {_ _} _ {_} _ _ _.
 Arguments cmra_morphism_pcore {_ _} _ {_} _.
@@ -761,15 +761,15 @@ Proof.
   split.
   - apply _.
   - move=> n x Hx /=. by apply cmra_morphism_validN, cmra_morphism_validN.
-  - move=> x /=. by rewrite 2!cmra_morphism_pcore option_fmap_compose.
+  - move=> x /=. by rewrite option_fmap_compose !cmra_morphism_pcore.
   - move=> x y /=. by rewrite !cmra_morphism_op.
 Qed.
 
 Section cmra_morphism.
   Local Set Default Proof Using "Type*".
   Context {A B : cmraT} (f : A → B) `{!CmraMorphism f}.
-  Lemma cmra_morphism_core x : core (f x) ≡ f (core x).
-  Proof. unfold core, core'. rewrite cmra_morphism_pcore. by destruct (pcore x). Qed.
+  Lemma cmra_morphism_core x : f (core x) ≡ core (f x).
+  Proof. unfold core, core'. rewrite -cmra_morphism_pcore. by destruct (pcore x). Qed.
   Lemma cmra_morphism_monotone x y : x ≼ y → f x ≼ f y.
   Proof. intros [z ->]. exists (f z). by rewrite cmra_morphism_op. Qed.
   Lemma cmra_morphism_monotoneN n x y : x ≼{n} y → f x ≼{n} f y.
@@ -1136,7 +1136,7 @@ Section prod.
   Qed.
   Canonical Structure prodR := CmraT (prod A B) prod_cmra_mixin.
 
-  Lemma pair_op (a a' : A) (b b' : B) : (a, b) ⋅ (a', b') = (a ⋅ a', b ⋅ b').
+  Lemma pair_op (a a' : A) (b b' : B) : (a ⋅ a', b ⋅ b') = (a, b) ⋅ (a', b').
   Proof. done. Qed.
   Lemma pair_valid (a : A) (b : B) : ✓ (a, b) ↔ ✓ a ∧ ✓ b.
   Proof. done. Qed.
@@ -1193,7 +1193,7 @@ Section prod_unit.
   Canonical Structure prodUR := UcmraT (prod A B) prod_ucmra_mixin.
 
   Lemma pair_split (x : A) (y : B) : (x, y) ≡ (x, ε) ⋅ (ε, y).
-  Proof. by rewrite pair_op left_id right_id. Qed.
+  Proof. by rewrite -pair_op left_id right_id. Qed.
 
   Lemma pair_split_L `{!LeibnizEquiv A, !LeibnizEquiv B} (x : A) (y : B) :
     (x, y) = (x, ε) ⋅ (ε, y).
@@ -1207,14 +1207,14 @@ Instance prod_map_cmra_morphism {A A' B B' : cmraT} (f : A → A') (g : B → B'
 Proof.
   split; first apply _.
   - by intros n x [??]; split; simpl; apply cmra_morphism_validN.
-  - intros x. etrans. apply (reflexivity (mbind _ _)).
-    etrans; last apply (reflexivity (_ <$> mbind _ _)). simpl.
+  - intros x. etrans; last apply (reflexivity (mbind _ _)).
+    etrans; first apply (reflexivity (_ <$> mbind _ _)). simpl.
     assert (Hf := cmra_morphism_pcore f (x.1)).
     destruct (pcore (f (x.1))), (pcore (x.1)); inversion_clear Hf=>//=.
     assert (Hg := cmra_morphism_pcore g (x.2)).
     destruct (pcore (g (x.2))), (pcore (x.2)); inversion_clear Hg=>//=.
     by setoid_subst.
-  - intros. by rewrite /prod_map /= -!cmra_morphism_op.
+  - intros. by rewrite /prod_map /= !cmra_morphism_op.
 Qed.
 
 Program Definition prodRF (F1 F2 : rFunctor) : rFunctor := {|
@@ -1475,7 +1475,7 @@ Proof.
   split; first apply _.
   - intros n [a|] ?; rewrite /cmra_validN //=. by apply (cmra_morphism_validN f).
   - move=> [a|] //. by apply Some_proper, cmra_morphism_pcore.
-  - move=> [a|] [b|] //=. by rewrite -(cmra_morphism_op f).
+  - move=> [a|] [b|] //=. by rewrite (cmra_morphism_op f).
 Qed.
 
 Program Definition optionRF (F : rFunctor) : rFunctor := {|

theories/algebra/csum.v

@@ -172,9 +172,9 @@ Instance csum_op : Op (csum A B) := λ x y,
   | _, _ => CsumBot
   end.
 
-Lemma Cinl_op a a' : Cinl a ⋅ Cinl a' = Cinl (a ⋅ a').
+Lemma Cinl_op a a' : Cinl (a ⋅ a') = Cinl a ⋅ Cinl a'.
 Proof. done. Qed.
-Lemma Cinr_op b b' : Cinr b ⋅ Cinr b' = Cinr (b ⋅ b').
+Lemma Cinr_op b b' : Cinr (b ⋅ b') = Cinr b ⋅ Cinr b'.
 Proof. done. Qed.
 
 Lemma csum_included x y :
@@ -366,8 +366,8 @@ Instance csum_map_cmra_morphism {A A' B B' : cmraT} (f : A → A') (g : B → B'
 Proof.
   split; try apply _.
   - intros n [a|b|]; simpl; auto using cmra_morphism_validN.
-  - move=> [a|b|]=>//=; rewrite cmra_morphism_pcore; by destruct pcore.
-  - intros [xa|ya|] [xb|yb|]=>//=; by rewrite -cmra_morphism_op.
+  - move=> [a|b|]=>//=; rewrite -cmra_morphism_pcore; by destruct pcore.
+  - intros [xa|ya|] [xb|yb|]=>//=; by rewrite cmra_morphism_op.
 Qed.
 
 Program Definition csumRF (Fa Fb : rFunctor) : rFunctor := {|

theories/algebra/ufrac_auth.v

@@ -137,7 +137,7 @@ Section ufrac_auth.
     intros n m; simpl; intros [Hvalid1 Hvalid2] Heq.
     split.
     - split; by apply cmra_valid_validN.
-    - rewrite -pair_op Some_op Heq comm.
+    - rewrite pair_op Some_op Heq comm.
       destruct m; simpl; [rewrite left_id | rewrite right_id]; done.
   Qed.
 End ufrac_auth.

theories/base_logic/lib/gen_heap.v

@@ -190,7 +190,7 @@ Section gen_heap.
   Global Instance mapsto_fractional l v : Fractional (λ q, l ↦{q} v)%I.
   Proof.
     intros p q. by rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op
-      op_singleton pair_op agree_idemp.
+      op_singleton -pair_op agree_idemp.
   Qed.
   Global Instance mapsto_as_fractional l q v :
     AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
@@ -200,7 +200,7 @@ Section gen_heap.
   Proof.
     apply wand_intro_r.
     rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op own_valid discrete_valid.
-    f_equiv. rewrite auth_frag_valid op_singleton singleton_valid pair_op.
+    f_equiv. rewrite auth_frag_valid op_singleton singleton_valid -pair_op.
     by intros [_ ?%agree_op_invL'].
   Qed.
 

theories/base_logic/lib/na_invariants.v

@@ -63,7 +63,7 @@ Section proofs.
   Lemma na_own_union p E1 E2 :
     E1 ## E2 → na_own p (E1 ∪ E2) ⊣⊢ na_own p E1 ∗ na_own p E2.
   Proof.
-    intros ?. by rewrite /na_own -own_op pair_op left_id coPset_disj_union.
+    intros ?. by rewrite /na_own -own_op -pair_op left_id coPset_disj_union.
   Qed.
 
   Lemma na_own_acc E2 E1 tid :