From c276e5a174a4629e895a9feb771a4166df579577 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Mon, 22 Jul 2019 12:07:23 +0200 Subject: [PATCH] Fix direction of CONSTRUCTOR_NAME_op lemmas (fix #256) --- CHANGELOG.md | 3 +++ theories/algebra/auth.v | 24 ++++++++++++------------ theories/algebra/cmra.v | 2 +- theories/algebra/frac_auth.v | 8 ++++---- theories/algebra/gmap.v | 4 ++-- theories/algebra/local_updates.v | 2 +- theories/algebra/ufrac_auth.v | 6 +++--- theories/base_logic/lib/auth.v | 2 +- theories/base_logic/lib/gen_heap.v | 8 ++++---- theories/heap_lang/lib/counter.v | 2 +- 10 files changed, 32 insertions(+), 29 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 658317801..a099589ea 100644 --- a/CHANGELOG.md +++ b/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. +* Flip direction of `auth_frag_op`, `Some_op`, `auth_auth_frac_op`, + `auth_both_op`, `auth_both_frac_op`, `frac_auth_frag_op`, + `ufrac_auth_frag_op`, to orient them like reduction rules for the RA operation. * 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/theories/algebra/auth.v b/theories/algebra/auth.v index 646676291..b2e38167e 100644 --- a/theories/algebra/auth.v +++ b/theories/algebra/auth.v @@ -282,28 +282,28 @@ Canonical Structure authUR := UcmraT (auth A) auth_ucmra_mixin. Global Instance auth_frag_core_id a : CoreId a → CoreId (◯ a). Proof. do 2 constructor; simpl; auto. by apply core_id_core. Qed. -Lemma auth_frag_op a b : ◯ (a ⋅ b) = ◯ a ⋅ ◯ b. +Lemma auth_frag_op a b : ◯ a ⋅ ◯ b = ◯ (a ⋅ b). Proof. done. Qed. Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b. -Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed. +Proof. intros [c ->]. rewrite -auth_frag_op. apply cmra_included_l. Qed. Global Instance auth_frag_sep_homomorphism : MonoidHomomorphism op op (≡) (@auth_frag A). Proof. by split; [split; try apply _|]. Qed. -Lemma auth_both_frac_op q a b : Auth (Some (q,to_agree a)) b ≡ ●{q} a ⋅ ◯ b. +Lemma auth_both_frac_op q a b : ●{q} a ⋅ ◯ b ≡ Auth (Some (q,to_agree a)) b. Proof. by rewrite /op /auth_op /= left_id. Qed. -Lemma auth_both_op a b : Auth (Some (1%Qp,to_agree a)) b ≡ ● a ⋅ ◯ b. +Lemma auth_both_op a b : ● a ⋅ ◯ b ≡ Auth (Some (1%Qp,to_agree a)) b. Proof. by rewrite auth_both_frac_op. Qed. -Lemma auth_auth_frac_op p q a : ●{p + q} a ≡ ●{p} a ⋅ ●{q} a. +Lemma auth_auth_frac_op p q a : ●{p} a ⋅ ●{q} a ≡ ●{p + 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. @@ -333,7 +333,7 @@ Proof. by rewrite auth_validI. Qed. Lemma auth_both_validI {M} q (a b: A) : ✓ (●{q} a ⋅ ◯ b) ⊣⊢@{uPredI M} ✓ q ∧ (∃ c, a ≡ b ⋅ c) ∧ ✓ a. Proof. - rewrite -auth_both_frac_op auth_validI /=. apply bi.and_proper; [done|]. + rewrite auth_both_frac_op auth_validI /=. apply bi.and_proper; [done|]. setoid_rewrite agree_equivI. iSplit. - iDestruct 1 as (a') "[#Eq [H V]]". iDestruct "H" as (b') "H". iRewrite -"Eq" in "H". iRewrite -"Eq" in "V". auto. @@ -388,12 +388,12 @@ 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=> ?. destruct (Hup n bc) as [Hval' Heq]; eauto using cmra_validN_includedN. - rewrite -!auth_both_op auth_validN_eq /=. + rewrite !auth_both_op auth_validN_eq /=. split_and!; [done| |done]. exists a'. split_and!; [done|by apply cmra_included_includedN|by apply cmra_valid_validN]. Qed. @@ -408,7 +408,7 @@ Instance is_op_auth_frag {A : ucmraT} (a b1 b2 : A) : Proof. done. Qed. Instance is_op_auth_auth_frac {A : ucmraT} (q q1 q2 : frac) (a : A) : IsOp q q1 q2 → IsOp' (●{q} a) (●{q1} a) (●{q2} a). -Proof. rewrite /IsOp' /IsOp => ->. by rewrite -auth_auth_frac_op. Qed. +Proof. rewrite /IsOp' /IsOp => ->. by rewrite auth_auth_frac_op. Qed. (* Functor *) Definition auth_map {A B} (f : A → B) (x : auth A) : auth B := @@ -443,7 +443,7 @@ Proof. - 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. + by rewrite Some_op pair_op 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..691abede7 100644 --- a/theories/algebra/cmra.v +++ b/theories/algebra/cmra.v @@ -1281,7 +1281,7 @@ Section option. Definition Some_valid a : ✓ Some a ↔ ✓ a := reflexivity _. Definition Some_validN a n : ✓{n} Some a ↔ ✓{n} a := reflexivity _. - Definition Some_op a b : Some (a ⋅ b) = Some a ⋅ Some b := eq_refl. + Definition Some_op a b : Some a ⋅ Some b = Some (a ⋅ b) := eq_refl. Lemma Some_core `{CmraTotal A} a : Some (core a) = core (Some a). Proof. rewrite /core /=. by destruct (cmra_total a) as [? ->]. Qed. Lemma Some_op_opM a ma : Some a ⋅ ma = Some (a ⋅? ma). diff --git a/theories/algebra/frac_auth.v b/theories/algebra/frac_auth.v index 3f7d27c3c..fbb1c56a0 100644 --- a/theories/algebra/frac_auth.v +++ b/theories/algebra/frac_auth.v @@ -88,13 +88,13 @@ Section frac_auth. Lemma frac_auth_frag_valid q a : ✓ (◯F{q} a) ↔ ✓ q ∧ ✓ a. Proof. done. Qed. - Lemma frac_auth_frag_op q1 q2 a1 a2 : ◯F{q1+q2} (a1 ⋅ a2) ≡ ◯F{q1} a1 ⋅ ◯F{q2} a2. + Lemma frac_auth_frag_op q1 q2 a1 a2 : ◯F{q1} a1 ⋅ ◯F{q2} a2 ≡ ◯F{q1+q2} (a1 ⋅ a2). Proof. done. Qed. Lemma frac_auth_frag_validN_op_1_l n q a b : ✓{n} (◯F{1} a ⋅ ◯F{q} b) → False. - Proof. rewrite -frac_auth_frag_op frac_auth_frag_validN=> -[/exclusiveN_l []]. Qed. + Proof. rewrite frac_auth_frag_op frac_auth_frag_validN=> -[/exclusiveN_l []]. Qed. Lemma frac_auth_frag_valid_op_1_l q a b : ✓ (◯F{1} a ⋅ ◯F{q} b) → False. - Proof. rewrite -frac_auth_frag_op frac_auth_frag_valid=> -[/exclusive_l []]. Qed. + Proof. rewrite frac_auth_frag_op frac_auth_frag_valid=> -[/exclusive_l []]. Qed. Global Instance is_op_frac_auth (q q1 q2 : frac) (a a1 a2 : A) : IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯F{q} a) (◯F{q1} a1) (◯F{q2} a2). @@ -104,7 +104,7 @@ Section frac_auth. CoreId a → IsOp q q1 q2 → IsOp' (◯F{q} a) (◯F{q1} a) (◯F{q2} a). Proof. rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->. - by rewrite -frac_auth_frag_op -core_id_dup. + by rewrite frac_auth_frag_op -core_id_dup. Qed. Lemma frac_auth_update q a b a' b' : diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v index b41d6458a..fb9d4ca45 100644 --- a/theories/algebra/gmap.v +++ b/theories/algebra/gmap.v @@ -472,7 +472,7 @@ Proof. rewrite Hm=> j; destruct (decide (i = j)) as [<-|]. - rewrite lookup_op !lookup_delete left_id symmetry_iff dist_None. apply eq_None_not_Some=> -[y Hi']. - move: (Hmv i). rewrite Hm lookup_op Hi Hi' -Some_op. by apply exclusiveN_l. + move: (Hmv i). rewrite Hm lookup_op Hi Hi' Some_op. by apply exclusiveN_l. - by rewrite lookup_op !lookup_delete_ne // lookup_op. Qed. @@ -528,7 +528,7 @@ Proof. { move: (Hm i). by rewrite lookup_op Hi1 Hi2 left_id. } destruct (Hup n (mf !! i)) as [Hx'v Hx'eq]. { move: (Hm1v i). by rewrite Hi1. } - { by rewrite Hif -(inj_iff Some) -Some_op_opM -Some_op left_id. } + { by rewrite Hif -(inj_iff Some) -Some_op_opM Some_op left_id. } split. - by apply insert_validN. - simpl in Hx'eq. by rewrite -(insert_idN n mf i x) // -insert_op -Hm Hx'eq Hif. diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v index 93f185ff3..d9aa7955c 100644 --- a/theories/algebra/local_updates.v +++ b/theories/algebra/local_updates.v @@ -186,7 +186,7 @@ Lemma delete_option_local_update {A : cmraT} (x : option A) (y : A) : Proof. move=>Hex. apply local_update_unital=>n z /= Hy Heq. split; first done. destruct z as [z|]; last done. exfalso. - move: Hy. rewrite Heq /= -Some_op=>Hy. eapply Hex. + move: Hy. rewrite Heq /= Some_op=>Hy. eapply Hex. eapply cmra_validN_le. eapply Hy. lia. Qed. diff --git a/theories/algebra/ufrac_auth.v b/theories/algebra/ufrac_auth.v index d7c1e89ea..8986efc6b 100644 --- a/theories/algebra/ufrac_auth.v +++ b/theories/algebra/ufrac_auth.v @@ -109,7 +109,7 @@ Section ufrac_auth. Lemma ufrac_auth_frag_valid q a : ✓ (◯U{q} a) ↔ ✓ a. Proof. rewrite auth_frag_valid. split. by intros [??]. by split. Qed. - Lemma ufrac_auth_frag_op q1 q2 a1 a2 : ◯U{q1+q2} (a1 ⋅ a2) ≡ ◯U{q1} a1 ⋅ ◯U{q2} a2. + Lemma ufrac_auth_frag_op q1 q2 a1 a2 : ◯U{q1} a1 ⋅ ◯U{q2} a2 ≡ ◯U{q1+q2} (a1 ⋅ a2). Proof. done. Qed. Global Instance is_op_ufrac_auth q q1 q2 a a1 a2 : @@ -120,7 +120,7 @@ Section ufrac_auth. CoreId a → IsOp q q1 q2 → IsOp' (◯U{q} a) (◯U{q1} a) (◯U{q2} a). Proof. rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->. - by rewrite -ufrac_auth_frag_op -core_id_dup. + by rewrite ufrac_auth_frag_op -core_id_dup. Qed. Lemma ufrac_auth_update p q a b a' b' : @@ -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/auth.v b/theories/base_logic/lib/auth.v index c5a8b494a..9e62bff19 100644 --- a/theories/base_logic/lib/auth.v +++ b/theories/base_logic/lib/auth.v @@ -70,7 +70,7 @@ Section auth. Implicit Types γ : gname. Lemma auth_own_op γ a b : auth_own γ (a ⋅ b) ⊣⊢ auth_own γ a ∗ auth_own γ b. - Proof. by rewrite /auth_own -own_op auth_frag_op. Qed. + Proof. by rewrite /auth_own -own_op -auth_frag_op. Qed. (* Global Instance from_and_auth_own γ a b1 b2 : diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v index 309940e3b..0e9fbda35 100644 --- a/theories/base_logic/lib/gen_heap.v +++ b/theories/base_logic/lib/gen_heap.v @@ -189,7 +189,7 @@ Section gen_heap. Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed. 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 + intros p q. by rewrite mapsto_eq /mapsto_def -own_op auth_frag_op op_singleton pair_op agree_idemp. Qed. Global Instance mapsto_as_fractional l q v : @@ -199,7 +199,7 @@ Section gen_heap. Lemma mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜v1 = v2⌝. Proof. apply wand_intro_r. - rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op own_valid discrete_valid. + 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. by intros [_ ?%agree_op_invL']. Qed. @@ -255,7 +255,7 @@ Section gen_heap. iDestruct 1 as (γm1) "[#Hγm1 Hm1]". iDestruct 1 as (γm2) "[#Hγm2 Hm2]". iAssert ⌜ γm1 = γm2 ⌝%I as %->. { iDestruct (own_valid_2 with "Hγm1 Hγm2") as %Hγ; iPureIntro. - move: Hγ. rewrite -auth_frag_op op_singleton=> /auth_frag_valid /=. + move: Hγ. rewrite auth_frag_op op_singleton=> /auth_frag_valid /=. rewrite singleton_valid. apply: agree_op_invL'. } iDestruct (own_valid_2 with "Hm1 Hm2") as %?%namespace_map_token_valid_op. iExists γm2. iFrame "Hγm2". rewrite namespace_map_token_union //. by iSplitL "Hm1". @@ -281,7 +281,7 @@ Section gen_heap. iDestruct 1 as (γm1) "[Hγm1 Hm1]"; iDestruct 1 as (γm2) "[Hγm2 Hm2]". iAssert ⌜ γm1 = γm2 ⌝%I as %->. { iDestruct (own_valid_2 with "Hγm1 Hγm2") as %Hγ; iPureIntro. - move: Hγ. rewrite -auth_frag_op op_singleton=> /auth_frag_valid /=. + move: Hγ. rewrite auth_frag_op op_singleton=> /auth_frag_valid /=. rewrite singleton_valid. apply: agree_op_invL'. } iDestruct (own_valid_2 with "Hm1 Hm2") as %Hγ; iPureIntro. move: Hγ. rewrite -namespace_map_data_op namespace_map_data_valid. diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v index 4b7058988..4108e8bb5 100644 --- a/theories/heap_lang/lib/counter.v +++ b/theories/heap_lang/lib/counter.v @@ -108,7 +108,7 @@ Section contrib_spec. (** The main proofs. *) Lemma ccounter_op γ q1 q2 n1 n2 : ccounter γ (q1 + q2) (n1 + n2) ⊣⊢ ccounter γ q1 n1 ∗ ccounter γ q2 n2. - Proof. by rewrite /ccounter frac_auth_frag_op -own_op. Qed. + Proof. by rewrite /ccounter -frac_auth_frag_op -own_op. Qed. Lemma newcounter_contrib_spec (R : iProp Σ) : {{{ True }}} newcounter #() -- GitLab