Commit 2ff603e9 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump stdpp (typeclasses opaque).

parent 3f7f9f4e
......@@ -874,6 +874,22 @@ Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
ra_valid_op_l x y : (x y) x
}.
Section leibniz.
Local Set Default Proof Using "Type*".
Context A `{Equiv A, PCore A, Op A, Valid A}.
Context `{!Equivalence (@{A}), !LeibnizEquiv A}.
Context (op_assoc : Assoc (=@{A}) ()).
Context (op_comm : Comm (=@{A}) ()).
Context (pcore_l : (x : A) cx, pcore x = Some cx cx x = x).
Context (ra_pcore_idemp : (x : A) cx, pcore x = Some cx pcore cx = Some cx).
Context (ra_pcore_mono : (x y : A) cx,
x y pcore x = Some cx cy, pcore y = Some cy cx cy).
Context (ra_valid_op_l : x y : A, (x y) x).
Definition ra_leibniz_mixin : RAMixin A.
Proof. split; repeat intro; fold_leibniz; naive_solver. Qed.
End leibniz.
Section discrete.
Local Set Default Proof Using "Type*".
Context `{Equiv A, PCore A, Op A, Valid A} (Heq : @Equivalence A ()).
......
......@@ -40,10 +40,12 @@ Instance dec_agree_pcore : PCore (dec_agree A) := Some.
Definition dec_agree_ra_mixin : RAMixin (dec_agree A).
Proof.
apply ra_total_mixin; apply _ || eauto.
apply ra_leibniz_mixin; try (apply _ || done).
- intros [?|] [?|] [?|]; by repeat (simplify_eq/= || case_match).
- intros [?|] [?|]; by repeat (simplify_eq/= || case_match).
- intros [?|]; by repeat (simplify_eq/= || case_match).
- rewrite /pcore /dec_agree_pcore=> -? [?|] [->];
by repeat (simplify_eq/= || case_match).
- rewrite /pcore /dec_agree_pcore. naive_solver.
- by intros [?|] [?|] ?.
Qed.
......
......@@ -28,7 +28,7 @@ Proof. intros ?%frac_included. auto using Qclt_le_weak. Qed.
Definition frac_ra_mixin : RAMixin frac.
Proof.
split; try apply _; try done.
apply ra_leibniz_mixin; try (apply _ || done).
unfold valid, op, frac_op, frac_valid. intros x y. trans (x+y)%Qp; last done.
rewrite -{1}(Qcplus_0_r x) -Qcplus_le_mono_l; auto using Qclt_le_weak.
Qed.
......
......@@ -89,7 +89,7 @@ Section cmra.
Proof.
move=>x'; destruct (decide (x = x')) as [->|];
by rewrite ofe_fun_lookup_core ?ofe_fun_lookup_singleton
?ofe_fun_lookup_singleton_ne // (core_id_core ).
?ofe_fun_lookup_singleton_ne // (core_id_core ε).
Qed.
Global Instance ofe_fun_singleton_core_id x (y : B x) :
......
......@@ -92,7 +92,8 @@ Proof.
by apply: discrete; rewrite -Hm lookup_insert_ne.
Qed.
Global Instance gmap_singleton_discrete i x :
Discrete x Discrete ({[ i := x ]} : gmap K A) := _.
Discrete x Discrete ({[ i := x ]} : gmap K A).
Proof. rewrite /singletonM. apply _. Qed.
Lemma insert_idN n m i x :
m !! i {n} Some x <[i:=x]>m {n} m.
Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
......
......@@ -296,10 +296,10 @@ Section properties.
Lemma replicate_valid n (x : A) : x replicate n x.
Proof. apply Forall_replicate. Qed.
Global Instance list_singletonM_ne i :
NonExpansive (@list_singletonM A i).
NonExpansive (singletonM (M:=list A) i).
Proof. intros n l1 l2 ?. apply Forall2_app; by repeat constructor. Qed.
Global Instance list_singletonM_proper i :
Proper (() ==> ()) (list_singletonM i) := ne_proper _.
Proper (() ==> ()) (singletonM (M:=list A) i) := ne_proper _.
Lemma elem_of_list_singletonM i z x : z ({[i := x]} : list A) z = ε z = x.
Proof.
......@@ -332,7 +332,7 @@ Section properties.
Lemma list_core_singletonM i (x : A) : core {[ i := x ]} {[ i := core x ]}.
Proof.
rewrite /singletonM /list_singletonM.
by rewrite {1}/core /= fmap_app fmap_replicate (core_id_core ).
by rewrite {1}/core /= fmap_app fmap_replicate (core_id_core ε).
Qed.
Lemma list_op_singletonM i (x y : A) :
{[ i := x ]} {[ i := y ]} {[ i := x y ]}.
......
......@@ -24,7 +24,7 @@ Corollary ufrac_included_weak (x y : ufrac) : x ≼ y → (x ≤ y)%Qc.
Proof. intros ?%ufrac_included. auto using Qclt_le_weak. Qed.
Definition ufrac_ra_mixin : RAMixin ufrac.
Proof. split; try apply _; try done. Qed.
Proof. apply ra_leibniz_mixin; try (apply _ || done). Qed.
Canonical Structure ufracR := discreteR ufrac ufrac_ra_mixin.
Global Instance ufrac_cmra_discrete : CmraDiscrete ufracR.
......
......@@ -10,7 +10,7 @@ Definition stuckness_leb (s1 s2 : stuckness) : bool :=
| _, _ => true
end.
Instance stuckness_le : SqSubsetEq stuckness := stuckness_leb.
Instance stuckness_le_po : PreOrder stuckness_le.
Instance stuckness_le_po : PreOrder (@{stuckness}).
Proof. split; by repeat intros []. Qed.
Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
......
......@@ -47,7 +47,8 @@ Proof.
- iIntros (wp1 wp2) "#H"; iIntros ([[E e1] Φ]); iRevert (E e1 Φ).
iApply twp_pre_mono. iIntros "!#" (E e Φ). iApply ("H" $! (E,e,Φ)).
- intros wp Hwp n [[E1 e1] Φ1] [[E2 e2] Φ2]
[[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=.
[[?%(discrete_iff _ _)%leibniz_equiv ?%(discrete_iff _ _)%leibniz_equiv] ?];
simplify_eq/=.
rewrite /uncurry3 /twp_pre. do 24 (f_equiv || done). by apply pair_ne.
Qed.
......@@ -79,7 +80,8 @@ Proof.
prodC (prodC (leibnizC coPset) (exprC Λ)) (val Λ -c> iProp Σ) iProp Σ).
assert (NonExpansive Ψ').
{ intros n [[E1 e1] Φ1] [[E2 e2] Φ2]
[[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=. by apply HΨ. }
[[?%(discrete_iff _ _)%leibniz_equiv ?%(discrete_iff _ _)%leibniz_equiv] ?];
simplify_eq/=. by apply HΨ. }
iApply (least_fixpoint_strong_ind _ Ψ' with "[] H").
iIntros "!#" ([[??] ?]) "H". by iApply "IH".
Qed.
......
......@@ -375,7 +375,7 @@ Global Instance frame_monPred_at_wand p P R Q1 Q2 i j :
Frame p R Q1 Q2
FrameMonPredAt p j (R i) (P - Q1) ((P - Q2) i).
Proof.
rewrite /Frame /FrameMonPredAt=>-> Hframe.
rewrite /IsBiIndexRel /Frame /FrameMonPredAt=>-> Hframe.
rewrite -monPred_at_intuitionistically_if -monPred_at_sep. apply monPred_in_entails.
change ((?p R (P - Q2)) - P - Q1). apply bi.wand_intro_r.
rewrite -assoc bi.wand_elim_l. done.
......@@ -385,7 +385,7 @@ Global Instance frame_monPred_at_impl P R Q1 Q2 i j :
Frame true R Q1 Q2
FrameMonPredAt true j (R i) (P Q1) ((P Q2) i).
Proof.
rewrite /Frame /FrameMonPredAt=>-> Hframe.
rewrite /IsBiIndexRel /Frame /FrameMonPredAt=>-> Hframe.
rewrite -monPred_at_intuitionistically_if -monPred_at_sep. apply monPred_in_entails.
change (( R (P Q2)) - P Q1).
rewrite -bi.persistently_and_intuitionistically_sep_l. apply bi.impl_intro_r.
......
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