Flip cmra_morphism_pcore

parent a51d5e1f
...@@ -162,7 +162,7 @@ Changes in Coq: ...@@ -162,7 +162,7 @@ Changes in Coq:
* Lemma `prop_ext` works in both directions; its default direction is the * Lemma `prop_ext` works in both directions; its default direction is the
opposite of what it used to be. opposite of what it used to be.
* Make direction of `f_op` rewrite lemmas more consistent: Flip `pair_op`, * Make direction of `f_op` rewrite lemmas more consistent: Flip `pair_op`,
`Cinl_op`, `Cinr_op`, `cmra_morphism_op`. `Cinl_op`, `Cinr_op`, `cmra_morphism_op`, `cmra_morphism_pcore`.
* Rename `C` suffixes into `O` since we no longer use COFEs but OFEs. Also * 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 rename `ofe_fun` into `discrete_fun` and the corresponding notation `-c>` into
`-d>`. The renaming can be automatically done using the following script (on `-d>`. The renaming can be automatically done using the following script (on
......
...@@ -251,7 +251,7 @@ Hint Mode CmraDiscrete ! : typeclass_instances. ...@@ -251,7 +251,7 @@ Hint Mode CmraDiscrete ! : typeclass_instances.
Class CmraMorphism {A B : cmraT} (f : A B) := { Class CmraMorphism {A B : cmraT} (f : A B) := {
cmra_morphism_ne :> NonExpansive f; cmra_morphism_ne :> NonExpansive f;
cmra_morphism_validN n x : {n} x {n} f x; cmra_morphism_validN n x : {n} x {n} f x;
cmra_morphism_pcore x : pcore (f x) f <$> pcore x; cmra_morphism_pcore x : f <$> pcore x pcore (f x);
cmra_morphism_op x y : f (x y) f x f y cmra_morphism_op x y : f (x y) f x f y
}. }.
Arguments cmra_morphism_validN {_ _} _ {_} _ _ _. Arguments cmra_morphism_validN {_ _} _ {_} _ _ _.
...@@ -761,7 +761,7 @@ Proof. ...@@ -761,7 +761,7 @@ Proof.
split. split.
- apply _. - apply _.
- move=> n x Hx /=. by apply cmra_morphism_validN, cmra_morphism_validN. - 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. - move=> x y /=. by rewrite !cmra_morphism_op.
Qed. Qed.
...@@ -769,7 +769,7 @@ Section cmra_morphism. ...@@ -769,7 +769,7 @@ Section cmra_morphism.
Local Set Default Proof Using "Type*". Local Set Default Proof Using "Type*".
Context {A B : cmraT} (f : A B) `{!CmraMorphism f}. Context {A B : cmraT} (f : A B) `{!CmraMorphism f}.
Lemma cmra_morphism_core x : core (f x) f (core x). Lemma cmra_morphism_core x : core (f x) f (core x).
Proof. unfold core, core'. rewrite cmra_morphism_pcore. by destruct (pcore x). Qed. 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. Lemma cmra_morphism_monotone x y : x y f x f y.
Proof. intros [z ->]. exists (f z). by rewrite cmra_morphism_op. Qed. 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. Lemma cmra_morphism_monotoneN n x y : x {n} y f x {n} f y.
...@@ -1207,8 +1207,8 @@ Instance prod_map_cmra_morphism {A A' B B' : cmraT} (f : A → A') (g : B → B' ...@@ -1207,8 +1207,8 @@ Instance prod_map_cmra_morphism {A A' B B' : cmraT} (f : A → A') (g : B → B'
Proof. Proof.
split; first apply _. split; first apply _.
- by intros n x [??]; split; simpl; apply cmra_morphism_validN. - by intros n x [??]; split; simpl; apply cmra_morphism_validN.
- intros x. etrans. apply (reflexivity (mbind _ _)). - intros x. etrans; last apply (reflexivity (mbind _ _)).
etrans; last apply (reflexivity (_ <$> mbind _ _)). simpl. etrans; first apply (reflexivity (_ <$> mbind _ _)). simpl.
assert (Hf := cmra_morphism_pcore f (x.1)). assert (Hf := cmra_morphism_pcore f (x.1)).
destruct (pcore (f (x.1))), (pcore (x.1)); inversion_clear Hf=>//=. destruct (pcore (f (x.1))), (pcore (x.1)); inversion_clear Hf=>//=.
assert (Hg := cmra_morphism_pcore g (x.2)). assert (Hg := cmra_morphism_pcore g (x.2)).
...@@ -1597,7 +1597,7 @@ Instance discrete_fun_map_cmra_morphism {A} {B1 B2 : A → ucmraT} (f : ∀ x, B ...@@ -1597,7 +1597,7 @@ Instance discrete_fun_map_cmra_morphism {A} {B1 B2 : A → ucmraT} (f : ∀ x, B
Proof. Proof.
split; first apply _. split; first apply _.
- intros n g Hg x; rewrite /discrete_fun_map; apply (cmra_morphism_validN (f _)), Hg. - intros n g Hg x; rewrite /discrete_fun_map; apply (cmra_morphism_validN (f _)), Hg.
- intros. apply Some_proper=>i. apply (cmra_morphism_core (f i)). - intros. apply Some_proper=>i. by rewrite (cmra_morphism_core (f i)).
- intros g1 g2 i. by rewrite /discrete_fun_map discrete_fun_lookup_op cmra_morphism_op. - intros g1 g2 i. by rewrite /discrete_fun_map discrete_fun_lookup_op cmra_morphism_op.
Qed. Qed.
......
...@@ -366,7 +366,7 @@ Instance csum_map_cmra_morphism {A A' B B' : cmraT} (f : A → A') (g : B → B' ...@@ -366,7 +366,7 @@ Instance csum_map_cmra_morphism {A A' B B' : cmraT} (f : A → A') (g : B → B'
Proof. Proof.
split; try apply _. split; try apply _.
- intros n [a|b|]; simpl; auto using cmra_morphism_validN. - intros n [a|b|]; simpl; auto using cmra_morphism_validN.
- move=> [a|b|]=>//=; rewrite cmra_morphism_pcore; by destruct pcore. - 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. Qed.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment