Commit 7b4a04ce authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ralf/frac-op-valid' into 'master'

rename u?frac_op/valid' to remove the final '

See merge request iris/iris!632
parents 209933c8 28e33534
......@@ -73,6 +73,12 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
* Rename typeclass instances of CMRA operational typeclasses (`Op`, `Core`,
`PCore`, `Valid`, `ValidN`, `Unit`) to have a `_instance` suffix, so that
their original names are available to use as lemma names.
* Rename `frac_valid'``frac_valid`, `frac_op'``frac_op`,
`ufrac_op'``ufrac_op`, `coPset_op_union``coPset_op`, `coPset_core_self`
`coPset_core`, `gset_op_union``gset_op`, `gset_core_self``gset_core`,
`gmultiset_op_disj_union``gmultiset_op`, `gmultiset_core_empty`
`gmultiset_core`, `nat_op_plus``nat_op`, `max_nat_op_max`
`max_nat_op`. Those names were previously blocked by typeclass instances.
**Changes in `bi`:**
......@@ -253,6 +259,14 @@ s/\bcmraT\b/cmra/g
s/\bCmraT\b/Cmra/g
s/\bucmraT\b/ucmra/g
s/\bUcmraT\b/Ucmra/g
# _op/valid/core lemmas
s/\b(u?frac_(op|valid))'/\1/g
s/\b((coPset|gset)_op)_union\b/\1/g
s/\b((coPset|gset)_core)_self\b/\1/g
s/\b(gmultiset_op)_disj_union\b/\1/g
s/\b(gmultiset_core)_empty\b/\1/g
s/\b(nat_op)_plus\b/\1/g
s/\b(max_nat_op)_max\b/\1/g
EOF
```
......
......@@ -16,14 +16,14 @@ Section coPset.
Local Instance coPset_op_instance : Op coPset := union.
Local Instance coPset_pcore_instance : PCore coPset := Some.
Lemma coPset_op_union X Y : X Y = X Y.
Lemma coPset_op X Y : X Y = X Y.
Proof. done. Qed.
Lemma coPset_core_self X : core X = X.
Lemma coPset_core X : core X = X.
Proof. done. Qed.
Lemma coPset_included X Y : X Y X Y.
Proof.
split.
- intros [Z ->]. rewrite coPset_op_union. set_solver.
- intros [Z ->]. rewrite coPset_op. set_solver.
- intros (Z&->&?)%subseteq_disjoint_union_L. by exists Z.
Qed.
......@@ -33,9 +33,9 @@ Section coPset.
- solve_proper.
- solve_proper.
- solve_proper.
- intros X1 X2 X3. by rewrite !coPset_op_union assoc_L.
- intros X1 X2. by rewrite !coPset_op_union comm_L.
- intros X. by rewrite coPset_core_self idemp_L.
- intros X1 X2 X3. by rewrite !coPset_op assoc_L.
- intros X1 X2. by rewrite !coPset_op comm_L.
- intros X. by rewrite coPset_core idemp_L.
Qed.
Canonical Structure coPsetR := discreteR coPset coPset_ra_mixin.
......@@ -43,7 +43,7 @@ Section coPset.
Proof. apply discrete_cmra_discrete. Qed.
Lemma coPset_ucmra_mixin : UcmraMixin coPset.
Proof. split; [done | | done]. intros X. by rewrite coPset_op_union left_id_L. Qed.
Proof. split; [done | | done]. intros X. by rewrite coPset_op left_id_L. Qed.
Canonical Structure coPsetUR := Ucmra coPset coPset_ucmra_mixin.
Lemma coPset_opM X mY : X ? mY = X default mY.
......@@ -56,7 +56,7 @@ Section coPset.
Proof.
intros (Z&->&?)%subseteq_disjoint_union_L.
rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
split; first done. rewrite coPset_op_union. set_solver.
split; first done. rewrite coPset_op. set_solver.
Qed.
End coPset.
......
......@@ -19,9 +19,9 @@ Section frac.
Local Instance frac_pcore_instance : PCore frac := λ _, None.
Local Instance frac_op_instance : Op frac := λ x y, (x + y)%Qp.
Lemma frac_valid' p : p (p 1)%Qp.
Lemma frac_valid p : p (p 1)%Qp.
Proof. done. Qed.
Lemma frac_op' p q : p q = (p + q)%Qp.
Lemma frac_op p q : p q = (p + q)%Qp.
Proof. done. Qed.
Lemma frac_included p q : p q (p < q)%Qp.
Proof. by rewrite Qp_lt_sum. Qed.
......@@ -32,7 +32,7 @@ Section frac.
Definition frac_ra_mixin : RAMixin frac.
Proof.
split; try apply _; try done.
intros p q. rewrite !frac_valid' frac_op'=> ?.
intros p q. rewrite !frac_valid frac_op=> ?.
trans (p + q)%Qp; last done. apply Qp_le_add_l.
Qed.
Canonical Structure fracR := discreteR frac frac_ra_mixin.
......@@ -51,5 +51,5 @@ Section frac.
Global Instance frac_is_op q1 q2 : IsOp (q1 + q2)%Qp q1 q2 | 10.
Proof. done. Qed.
Global Instance is_op_frac q : IsOp' q (q/2)%Qp (q/2)%Qp.
Proof. by rewrite /IsOp' /IsOp frac_op' Qp_div_2. Qed.
Proof. by rewrite /IsOp' /IsOp frac_op Qp_div_2. Qed.
End frac.
......@@ -147,6 +147,8 @@ Local Instance gmap_pcore_instance : PCore (gmap K A) := λ m, Some (omap pcore
Local Instance gmap_valid_instance : Valid (gmap K A) := λ m, i, (m !! i).
Local Instance gmap_validN_instance : ValidN (gmap K A) := λ n m, i, {n} (m !! i).
Lemma gmap_op m1 m2 : m1 m2 = merge op m1 m2.
Proof. done. Qed.
Lemma lookup_op m1 m2 i : (m1 m2) !! i = m1 !! i m2 !! i.
Proof. by apply lookup_merge. Qed.
Lemma lookup_core m i : core m !! i = core (m !! i).
......
......@@ -16,15 +16,15 @@ Section gmultiset.
Local Instance gmultiset_op_instance : Op (gmultiset K) := disj_union.
Local Instance gmultiset_pcore_instance : PCore (gmultiset K) := λ X, Some .
Lemma gmultiset_op_disj_union X Y : X Y = X Y.
Lemma gmultiset_op X Y : X Y = X Y.
Proof. done. Qed.
Lemma gmultiset_core_empty X : core X = .
Lemma gmultiset_core X : core X = .
Proof. done. Qed.
Lemma gmultiset_included X Y : X Y X Y.
Proof.
split.
- intros [Z ->%leibniz_equiv].
rewrite gmultiset_op_disj_union. apply gmultiset_disj_union_subseteq_l.
rewrite gmultiset_op. apply gmultiset_disj_union_subseteq_l.
- intros ->%gmultiset_disj_union_difference. by exists (Y X).
Qed.
......@@ -34,10 +34,10 @@ Section gmultiset.
- by intros X Y Z ->%leibniz_equiv.
- by intros X Y ->%leibniz_equiv.
- solve_proper.
- intros X1 X2 X3. by rewrite !gmultiset_op_disj_union assoc_L.
- intros X1 X2. by rewrite !gmultiset_op_disj_union comm_L.
- intros X. by rewrite gmultiset_core_empty left_id.
- intros X1 X2 HX. rewrite !gmultiset_core_empty. exists .
- intros X1 X2 X3. by rewrite !gmultiset_op assoc_L.
- intros X1 X2. by rewrite !gmultiset_op comm_L.
- intros X. by rewrite gmultiset_core left_id.
- intros X1 X2 HX. rewrite !gmultiset_core. exists .
by rewrite left_id.
Qed.
......@@ -49,7 +49,7 @@ Section gmultiset.
Lemma gmultiset_ucmra_mixin : UcmraMixin (gmultiset K).
Proof.
split; [done | | done]. intros X.
by rewrite gmultiset_op_disj_union left_id_L.
by rewrite gmultiset_op left_id_L.
Qed.
Canonical Structure gmultisetUR := Ucmra (gmultiset K) gmultiset_ucmra_mixin.
......@@ -68,7 +68,7 @@ Section gmultiset.
Proof.
intros HXY. rewrite local_update_unital_discrete=> Z' _. intros ->%leibniz_equiv.
split; first done. apply leibniz_equiv_iff, (inj (. Y)).
rewrite -HXY !gmultiset_op_disj_union.
rewrite -HXY !gmultiset_op.
by rewrite -(comm_L _ Y) (comm_L _ Y') assoc_L.
Qed.
......
......@@ -15,21 +15,21 @@ Section gset.
Local Instance gset_op_instance : Op (gset K) := union.
Local Instance gset_pcore_instance : PCore (gset K) := λ X, Some X.
Lemma gset_op_union X Y : X Y = X Y.
Lemma gset_op X Y : X Y = X Y.
Proof. done. Qed.
Lemma gset_core_self X : core X = X.
Lemma gset_core X : core X = X.
Proof. done. Qed.
Lemma gset_included X Y : X Y X Y.
Proof.
split.
- intros [Z ->]. rewrite gset_op_union. set_solver.
- intros [Z ->]. rewrite gset_op. set_solver.
- intros (Z&->&?)%subseteq_disjoint_union_L. by exists Z.
Qed.
Lemma gset_ra_mixin : RAMixin (gset K).
Proof.
apply ra_total_mixin; apply _ || eauto; [].
intros X. by rewrite gset_core_self idemp_L.
intros X. by rewrite gset_core idemp_L.
Qed.
Canonical Structure gsetR := discreteR (gset K) gset_ra_mixin.
......@@ -37,7 +37,7 @@ Section gset.
Proof. apply discrete_cmra_discrete. Qed.
Lemma gset_ucmra_mixin : UcmraMixin (gset K).
Proof. split; [ done | | done ]. intros X. by rewrite gset_op_union left_id_L. Qed.
Proof. split; [ done | | done ]. intros X. by rewrite gset_op left_id_L. Qed.
Canonical Structure gsetUR := Ucmra (gset K) gset_ucmra_mixin.
Lemma gset_opM X mY : X ? mY = X default mY.
......@@ -50,11 +50,11 @@ Section gset.
Proof.
intros (Z&->&?)%subseteq_disjoint_union_L.
rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
split; [done|]. rewrite gset_op_union. set_solver.
split; [done|]. rewrite gset_op. set_solver.
Qed.
Global Instance gset_core_id X : CoreId X.
Proof. by apply core_id_total; rewrite gset_core_self. Qed.
Proof. by apply core_id_total; rewrite gset_core. Qed.
Lemma big_opS_singletons X :
([^op set] x X, {[ x ]}) = X.
......
......@@ -171,7 +171,7 @@ Section gset_bij.
Lemma gset_bij_elem_agree a1 b1 a2 b2 :
(gset_bij_elem a1 b1 gset_bij_elem a2 b2) (a1 = a2 b1 = b2).
Proof.
rewrite /gset_bij_elem -view_frag_op gset_op_union view_frag_valid.
rewrite /gset_bij_elem -view_frag_op gset_op view_frag_valid.
setoid_rewrite gset_bij_view_rel_iff. intros. apply gset_bijective_pair.
naive_solver eauto using subseteq_gset_bijective, O.
Qed.
......@@ -188,7 +188,7 @@ Section gset_bij.
gset_bij_auth 1 L ~~> gset_bij_auth 1 ({[(a, b)]} L).
Proof.
intros. apply view_update=> n bijL.
rewrite !gset_bij_view_rel_iff gset_op_union.
rewrite !gset_bij_view_rel_iff gset_op.
set_solver by eauto using gset_bijective_extend.
Qed.
End gset_bij.
......@@ -33,13 +33,13 @@ Section mono_nat.
Lemma mono_nat_lb_op n1 n2 :
mono_nat_lb n1 mono_nat_lb n2 = mono_nat_lb (n1 `max` n2).
Proof. rewrite -auth_frag_op max_nat_op_max //. Qed.
Proof. rewrite -auth_frag_op max_nat_op //. Qed.
Lemma mono_nat_auth_lb_op q n :
mono_nat_auth q n mono_nat_auth q n mono_nat_lb n.
Proof.
rewrite /mono_nat_auth /mono_nat_lb.
rewrite -!assoc -auth_frag_op max_nat_op_max.
rewrite -!assoc -auth_frag_op max_nat_op.
rewrite Nat.max_id //.
Qed.
......
......@@ -7,7 +7,7 @@ Section nat.
Local Instance nat_validN_instance : ValidN nat := λ n x, True.
Local Instance nat_pcore_instance : PCore nat := λ x, Some 0.
Local Instance nat_op_instance : Op nat := plus.
Definition nat_op_plus x y : x y = x + y := eq_refl.
Definition nat_op x y : x y = x + y := eq_refl.
Lemma nat_included (x y : nat) : x y x y.
Proof. by rewrite nat_le_sum. Qed.
Lemma nat_ra_mixin : RAMixin nat.
......@@ -56,7 +56,7 @@ Section max_nat.
Local Instance max_nat_validN_instance : ValidN max_nat := λ n x, True.
Local Instance max_nat_pcore_instance : PCore max_nat := Some.
Local Instance max_nat_op_instance : Op max_nat := λ n m, MaxNat (max_nat_car n `max` max_nat_car m).
Definition max_nat_op_max x y : MaxNat x MaxNat y = MaxNat (x `max` y) := eq_refl.
Definition max_nat_op x y : MaxNat x MaxNat y = MaxNat (x `max` y) := eq_refl.
Lemma max_nat_included x y : x y max_nat_car x max_nat_car y.
Proof.
......@@ -67,9 +67,9 @@ Section max_nat.
Lemma max_nat_ra_mixin : RAMixin max_nat.
Proof.
apply ra_total_mixin; apply _ || eauto.
- intros [x] [y] [z]. repeat rewrite max_nat_op_max. by rewrite Nat.max_assoc.
- intros [x] [y]. by rewrite max_nat_op_max Nat.max_comm.
- intros [x]. by rewrite max_nat_op_max Max.max_idempotent.
- intros [x] [y] [z]. repeat rewrite max_nat_op. by rewrite Nat.max_assoc.
- intros [x] [y]. by rewrite max_nat_op Nat.max_comm.
- intros [x]. by rewrite max_nat_op Max.max_idempotent.
Qed.
Canonical Structure max_natR : cmra := discreteR max_nat max_nat_ra_mixin.
......@@ -88,12 +88,12 @@ Section max_nat.
Proof.
move: x y x' => [x] [y] [y'] /= ?.
rewrite local_update_unital_discrete=> [[z]] _.
rewrite 2!max_nat_op_max. intros [= ?].
rewrite 2!max_nat_op. intros [= ?].
split; first done. apply f_equal. lia.
Qed.
Global Instance : IdemP (=@{max_nat}) ().
Proof. intros [x]. rewrite max_nat_op_max. apply f_equal. lia. Qed.
Proof. intros [x]. rewrite max_nat_op. apply f_equal. lia. Qed.
Global Instance max_nat_is_op (x y : nat) :
IsOp (MaxNat (x `max` y)) (MaxNat x) (MaxNat y).
......
......@@ -18,7 +18,7 @@ Section ufrac.
Local Instance ufrac_pcore_instance : PCore ufrac := λ _, None.
Local Instance ufrac_op_instance : Op ufrac := λ x y, (x + y)%Qp.
Lemma ufrac_op' p q : p q = (p + q)%Qp.
Lemma ufrac_op p q : p q = (p + q)%Qp.
Proof. done. Qed.
Lemma ufrac_included p q : p q (p < q)%Qp.
Proof. by rewrite Qp_lt_sum. Qed.
......@@ -39,5 +39,5 @@ Section ufrac.
Proof. intros p _. apply Qp_add_id_free. Qed.
Global Instance is_op_ufrac q : IsOp' q (q/2)%Qp (q/2)%Qp.
Proof. by rewrite /IsOp' /IsOp ufrac_op' Qp_div_2. Qed.
Proof. by rewrite /IsOp' /IsOp ufrac_op Qp_div_2. Qed.
End ufrac.
......@@ -518,7 +518,7 @@ Section cmra.
Proof.
rewrite !local_update_unital.
move=> Hup Hrel n [[[q ag]|] bf] /view_both_validN Hrel' [/=].
- rewrite right_id -Some_op -pair_op frac_op'=> /Some_dist_inj [/= H1q _].
- rewrite right_id -Some_op -pair_op frac_op=> /Some_dist_inj [/= H1q _].
by destruct (Qp_add_id_free 1 q).
- rewrite !left_id=> _ Hb0.
destruct (Hup n bf) as [? Hb0']; [by eauto using view_rel_validN..|].
......
......@@ -23,7 +23,7 @@ Lemma discrete_fun_validI {A} {B : A → ucmra} (g : discrete_fun B) :
Proof. by uPred.unseal. Qed.
Lemma frac_validI (q : Qp) : q q 1%Qp.
Proof. rewrite uPred.discrete_valid frac_valid' //. Qed.
Proof. rewrite uPred.discrete_valid frac_valid //. Qed.
Section gmap_ofe.
Context `{Countable K} {A : ofe}.
......
......@@ -45,7 +45,7 @@ Local Hint Extern 0 (environments.envs_entails _ (one_shot_inv _ _)) =>
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 :
......
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