From a51d5e1fa3fbd874f757254d129224826f1e8028 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Mon, 12 Aug 2019 16:29:18 +0200
Subject: [PATCH] Fix #256: Fix direction of f_op lemmas
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Turn all `f_op` lemmas to have shape `f (x â‹… y) = f x â‹… f y`, following the plan
in https://gitlab.mpi-sws.org/iris/iris/merge_requests/295#note_39151, plus
`cmra_morphism_op`.
---
CHANGELOG.md | 2 ++
tests/one_shot_once.v | 2 +-
theories/algebra/auth.v | 9 ++++-----
theories/algebra/cmra.v | 10 +++++-----
theories/algebra/csum.v | 6 +++---
theories/algebra/ufrac_auth.v | 2 +-
theories/base_logic/lib/gen_heap.v | 4 ++--
theories/base_logic/lib/na_invariants.v | 2 +-
8 files changed, 19 insertions(+), 18 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 658317801..386bf5298 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -161,6 +161,8 @@ 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`.
* 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
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index ad8ea8147..9bc49a9eb 100644
--- a/tests/one_shot_once.v
+++ b/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 :
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 646676291..b2dad6a87 100644
--- a/theories/algebra/auth.v
+++ b/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).
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 54f32f720..f96b8c5b0 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -252,7 +252,7 @@ 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_op x y : f (x ⋅ y) ≡ f x ⋅ f y
}.
Arguments cmra_morphism_validN {_ _} _ {_} _ _ _.
Arguments cmra_morphism_pcore {_ _} _ {_} _.
@@ -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).
@@ -1214,7 +1214,7 @@ Proof.
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 := {|
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index a16994265..f41f2d81d 100644
--- a/theories/algebra/csum.v
+++ b/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 :
@@ -367,7 +367,7 @@ 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.
+ - intros [xa|ya|] [xb|yb|]=>//=; by rewrite cmra_morphism_op.
Qed.
Program Definition csumRF (Fa Fb : rFunctor) : rFunctor := {|
diff --git a/theories/algebra/ufrac_auth.v b/theories/algebra/ufrac_auth.v
index d7c1e89ea..cec6d972f 100644
--- a/theories/algebra/ufrac_auth.v
+++ b/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.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 309940e3b..18ba74aba 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/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.
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index c92594bf0..680d34295 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/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 :
--
GitLab