Commit d211f644 authored by Ralf Jung's avatar Ralf Jung
Browse files

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

parent 209933c8
......@@ -73,6 +73,9 @@ 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`. Those names were previously blocked by typeclass
instances.
**Changes in `bi`:**
......@@ -253,6 +256,8 @@ s/\bcmraT\b/cmra/g
s/\bCmraT\b/Cmra/g
s/\bucmraT\b/ucmra/g
s/\bUcmraT\b/Ucmra/g
# u?frac_op/valid lemmas
s/\b(u?frac_(op|valid))'/\1/g
EOF
```
......
......@@ -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.
......@@ -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 :
......
Supports Markdown
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