From 2ff603e9d564862cf500db82a04e8a68527f43ce Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 15 Mar 2019 15:18:22 +0100
Subject: [PATCH] Bump stdpp (typeclasses opaque).
---
theories/algebra/cmra.v | 16 ++++++++++++++++
theories/algebra/deprecated.v | 6 ++++--
theories/algebra/frac.v | 2 +-
theories/algebra/functions.v | 2 +-
theories/algebra/gmap.v | 3 ++-
theories/algebra/list.v | 6 +++---
theories/algebra/ufrac.v | 2 +-
theories/bi/weakestpre.v | 2 +-
theories/program_logic/total_weakestpre.v | 6 ++++--
theories/proofmode/monpred.v | 4 ++--
10 files changed, 35 insertions(+), 14 deletions(-)
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index d4418c515..cff69e8da 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -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 (≡)).
diff --git a/theories/algebra/deprecated.v b/theories/algebra/deprecated.v
index 2c8165cf1..245cb63fd 100644
--- a/theories/algebra/deprecated.v
+++ b/theories/algebra/deprecated.v
@@ -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.
diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index f5f84eb01..003a4fe23 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -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.
diff --git a/theories/algebra/functions.v b/theories/algebra/functions.v
index 4ace8f8f7..3375a0af2 100644
--- a/theories/algebra/functions.v
+++ b/theories/algebra/functions.v
@@ -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) :
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index f2bcdfe99..9b0d7c5fe 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -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.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 8d9aa0db0..976d4d2dd 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -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 ]}.
diff --git a/theories/algebra/ufrac.v b/theories/algebra/ufrac.v
index 1b378db33..75ec408d3 100644
--- a/theories/algebra/ufrac.v
+++ b/theories/algebra/ufrac.v
@@ -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.
diff --git a/theories/bi/weakestpre.v b/theories/bi/weakestpre.v
index 387b24bf8..d48098738 100644
--- a/theories/bi/weakestpre.v
+++ b/theories/bi/weakestpre.v
@@ -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 :=
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index 3b964c1fe..f9c150142 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -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.
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 5d85ca71d..4fe446718 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -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.
--
GitLab