Commit e8edb3d8 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump std++ (multiset changes).

parent 8a8c1405
......@@ -11,5 +11,5 @@ install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { (>= "8.7.1" & < "8.10~") | (= "dev") }
"coq-stdpp" { (= "dev.2019-02-20.2.c8c298d4") | (= "dev") }
"coq-stdpp" { (= "dev.2019-02-21.1.5eabf109") | (= "dev") }
]
......@@ -381,9 +381,9 @@ Section gmultiset.
Lemma big_opMS_empty f : ([^o mset] x , f x) = monoid_unit.
Proof. by rewrite /big_opMS gmultiset_elements_empty. Qed.
Lemma big_opMS_union f X Y :
([^o mset] y X Y, f y) ([^o mset] y X, f y) `o` [^o mset] y Y, f y.
Proof. by rewrite /big_opMS gmultiset_elements_union big_opL_app. Qed.
Lemma big_opMS_disj_union f X Y :
([^o mset] y X Y, f y) ([^o mset] y X, f y) `o` [^o mset] y Y, f y.
Proof. by rewrite /big_opMS gmultiset_elements_disj_union big_opL_app. Qed.
Lemma big_opMS_singleton f x : ([^o mset] y {[ x ]}, f y) f x.
Proof.
......@@ -393,14 +393,14 @@ Section gmultiset.
Lemma big_opMS_delete f X x :
x X ([^o mset] y X, f y) f x `o` [^o mset] y X {[ x ]}, f y.
Proof.
intros. rewrite -big_opMS_singleton -big_opMS_union.
by rewrite -gmultiset_union_difference'.
intros. rewrite -big_opMS_singleton -big_opMS_disj_union.
by rewrite -gmultiset_disj_union_difference'.
Qed.
Lemma big_opMS_unit X : ([^o mset] y X, monoid_unit) (monoid_unit : M).
Proof.
induction X using gmultiset_ind;
rewrite /= ?big_opMS_union ?big_opMS_singleton ?left_id //.
rewrite /= ?big_opMS_disj_union ?big_opMS_singleton ?left_id //.
Qed.
Lemma big_opMS_opMS f g X :
......@@ -478,7 +478,7 @@ Section homomorphisms.
Proof.
intros. induction X as [|x X IH] using gmultiset_ind.
- by rewrite !big_opMS_empty monoid_homomorphism_unit.
- by rewrite !big_opMS_union !big_opMS_singleton monoid_homomorphism -IH.
- by rewrite !big_opMS_disj_union !big_opMS_singleton monoid_homomorphism -IH.
Qed.
Lemma big_opMS_commute1 `{Countable A} (h : M1 M2)
`{!WeakMonoidHomomorphism o1 o2 R h} (f : A M1) X :
......@@ -486,8 +486,8 @@ Section homomorphisms.
Proof.
intros. induction X as [|x X IH] using gmultiset_ind; [done|].
destruct (decide (X = )) as [->|].
- by rewrite !big_opMS_union !big_opMS_singleton !big_opMS_empty !right_id.
- by rewrite !big_opMS_union !big_opMS_singleton monoid_homomorphism -IH //.
- by rewrite !big_opMS_disj_union !big_opMS_singleton !big_opMS_empty !right_id.
- by rewrite !big_opMS_disj_union !big_opMS_singleton monoid_homomorphism -IH //.
Qed.
Context `{!LeibnizEquiv M2}.
......
......@@ -31,6 +31,6 @@ Lemma big_opMS_None {M : cmraT} `{Countable A} (f : A → option M) X :
Proof.
induction X as [|x X IH] using gmultiset_ind.
{ rewrite big_opMS_empty. set_solver. }
rewrite -equiv_None big_opMS_union big_opMS_singleton equiv_None op_None IH.
rewrite -equiv_None big_opMS_disj_union big_opMS_singleton equiv_None op_None IH.
set_solver.
Qed.
\ No newline at end of file
......@@ -13,10 +13,10 @@ Section gmultiset.
Instance gmultiset_valid : Valid (gmultiset K) := λ _, True.
Instance gmultiset_validN : ValidN (gmultiset K) := λ _ _, True.
Instance gmultiset_unit : Unit (gmultiset K) := ( : gmultiset K).
Instance gmultiset_op : Op (gmultiset K) := union.
Instance gmultiset_op : Op (gmultiset K) := disj_union.
Instance gmultiset_pcore : PCore (gmultiset K) := λ X, Some .
Lemma gmultiset_op_union X Y : X Y = X Y.
Lemma gmultiset_op_disj_union X Y : X Y = X Y.
Proof. done. Qed.
Lemma gmultiset_core_empty X : core X = .
Proof. done. Qed.
......@@ -24,8 +24,8 @@ Section gmultiset.
Proof.
split.
- intros [Z ->%leibniz_equiv].
rewrite gmultiset_op_union. apply gmultiset_union_subseteq_l.
- intros ->%gmultiset_union_difference. by exists (Y X).
rewrite gmultiset_op_disj_union. apply gmultiset_disj_union_subseteq_l.
- intros ->%gmultiset_disj_union_difference. by exists (Y X).
Qed.
Lemma gmultiset_ra_mixin : RAMixin (gmultiset K).
......@@ -34,8 +34,8 @@ 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_union assoc_L.
- intros X1 X2. by rewrite !gmultiset_op_union comm_L.
- 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 .
by rewrite left_id.
......@@ -47,33 +47,34 @@ Section gmultiset.
Proof. apply discrete_cmra_discrete. Qed.
Lemma gmultiset_ucmra_mixin : UcmraMixin (gmultiset K).
Proof. split. done. intros X. by rewrite gmultiset_op_union left_id_L. done. Qed.
Proof. split. done. intros X. by rewrite gmultiset_op_disj_union left_id_L. done. Qed.
Canonical Structure gmultisetUR := UcmraT (gmultiset K) gmultiset_ucmra_mixin.
Global Instance gmultiset_cancelable X : Cancelable X.
Proof.
apply: discrete_cancelable=> Y Z _ ?. fold_leibniz. by apply (inj (X )).
apply: discrete_cancelable=> Y Z _ ?. fold_leibniz. by apply (inj (X )).
Qed.
Lemma gmultiset_opM X mY : X ? mY = X default mY.
Lemma gmultiset_opM X mY : X ? mY = X default mY.
Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
Lemma gmultiset_update X Y : X ~~> Y.
Proof. done. Qed.
Lemma gmultiset_local_update_alloc X Y X' : (X,Y) ~l~> (X X', Y X').
Lemma gmultiset_local_update_alloc X Y X' : (X,Y) ~l~> (X X', Y X').
Proof.
rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
split. done. rewrite !gmultiset_op_union.
split. done. rewrite !gmultiset_op_disj_union.
by rewrite -!assoc (comm _ Z' X').
Qed.
Lemma gmultiset_local_update_dealloc X Y X' : X' X X' Y (X,Y) ~l~> (X X', Y X').
Lemma gmultiset_local_update_dealloc X Y X' :
X' X X' Y (X,Y) ~l~> (X X', Y X').
Proof.
intros ->%gmultiset_union_difference ->%gmultiset_union_difference.
intros ->%gmultiset_disj_union_difference ->%gmultiset_disj_union_difference.
rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
split. done. rewrite !gmultiset_op_union=> x.
repeat (rewrite multiplicity_difference || rewrite multiplicity_union).
split. done. rewrite !gmultiset_op_disj_union=> x.
repeat (rewrite multiplicity_difference || rewrite multiplicity_disj_union).
lia.
Qed.
End gmultiset.
......
......@@ -909,9 +909,9 @@ Section gmultiset.
Lemma big_sepMS_empty' `{!BiAffine PROP} P Φ : P [ mset] x , Φ x.
Proof. rewrite big_sepMS_empty. apply: affine. Qed.
Lemma big_sepMS_union Φ X Y :
([ mset] y X Y, Φ y) ([ mset] y X, Φ y) [ mset] y Y, Φ y.
Proof. apply big_opMS_union. Qed.
Lemma big_sepMS_disj_union Φ X Y :
([ mset] y X Y, Φ y) ([ mset] y X, Φ y) [ mset] y Y, Φ y.
Proof. apply big_opMS_disj_union. Qed.
Lemma big_sepMS_delete Φ X x :
x X ([ mset] y X, Φ y) Φ x [ mset] y X {[ x ]}, Φ y.
......
......@@ -591,10 +591,11 @@ Proof.
apply wand_elim_l', big_sepL2_app.
Qed.
Global Instance from_and_big_sepMS_union_persistent `{Countable A} (Φ : A PROP) X1 X2 :
Global Instance from_and_big_sepMS_disj_union_persistent
`{Countable A} (Φ : A PROP) X1 X2 :
( y, Persistent (Φ y))
FromAnd ([ mset] y X1 X2, Φ y) ([ mset] y X1, Φ y) ([ mset] y X2, Φ y).
Proof. intros. by rewrite /FromAnd big_sepMS_union persistent_and_sep_1. Qed.
FromAnd ([ mset] y X1 X2, Φ y) ([ mset] y X1, Φ y) ([ mset] y X2, Φ y).
Proof. intros. by rewrite /FromAnd big_sepMS_disj_union persistent_and_sep_1. Qed.
(** FromSep *)
Global Instance from_sep_sep P1 P2 : FromSep (P1 P2) P1 P2 | 100.
......@@ -649,9 +650,9 @@ Global Instance from_sep_big_sepL2_app {A B} (Φ : nat → A → B → PROP)
([ list] k y1;y2 l1'';l2'', Φ (length l1' + k) y1 y2).
Proof. rewrite /IsApp=>-> ->. apply wand_elim_l', big_sepL2_app. Qed.
Global Instance from_sep_big_sepMS_union `{Countable A} (Φ : A PROP) X1 X2 :
FromSep ([ mset] y X1 X2, Φ y) ([ mset] y X1, Φ y) ([ mset] y X2, Φ y).
Proof. by rewrite /FromSep big_sepMS_union. Qed.
Global Instance from_sep_big_sepMS_disj_union `{Countable A} (Φ : A PROP) X1 X2 :
FromSep ([ mset] y X1 X2, Φ y) ([ mset] y X1, Φ y) ([ mset] y X2, Φ y).
Proof. by rewrite /FromSep big_sepMS_disj_union. Qed.
Global Instance from_sep_bupd `{BiBUpd PROP} P Q1 Q2 :
FromSep P Q1 Q2 FromSep (|==> P) (|==> Q1) (|==> Q2).
......@@ -802,9 +803,9 @@ Global Instance into_sep_big_sepL2_cons {A B}
(Φ 0 x1 x2) ([ list] k y1;y2 l1';l2', Φ (S k) y1 y2).
Proof. rewrite /IsCons=>-> ->. by rewrite /IntoSep big_sepL2_cons. Qed.
Global Instance into_sep_big_sepMS_union `{Countable A} (Φ : A PROP) X1 X2 :
IntoSep ([ mset] y X1 X2, Φ y) ([ mset] y X1, Φ y) ([ mset] y X2, Φ y).
Proof. by rewrite /IntoSep big_sepMS_union. Qed.
Global Instance into_sep_big_sepMS_disj_union `{Countable A} (Φ : A PROP) X1 X2 :
IntoSep ([ mset] y X1 X2, Φ y) ([ mset] y X1, Φ y) ([ mset] y X2, Φ y).
Proof. by rewrite /IntoSep big_sepMS_disj_union. Qed.
(** FromOr *)
Global Instance from_or_or P1 P2 : FromOr (P1 P2) P1 P2.
......
......@@ -105,10 +105,10 @@ Global Instance frame_big_sepL2_app {A B} p (Φ : nat → A → B → PROP)
Frame p R ([ list] k y1;y2 l1;l2, Φ k y1 y2) Q.
Proof. rewrite /IsApp /Frame=>-> -> ->. apply wand_elim_l', big_sepL2_app. Qed.
Global Instance frame_big_sepMS_union `{Countable A} p (Φ : A PROP) R Q X1 X2 :
Global Instance frame_big_sepMS_disj_union `{Countable A} p (Φ : A PROP) R Q X1 X2 :
Frame p R (([ mset] y X1, Φ y) [ mset] y X2, Φ y) Q
Frame p R ([ mset] y X1 X2, Φ y) Q.
Proof. by rewrite /Frame big_sepMS_union. Qed.
Frame p R ([ mset] y X1 X2, Φ y) Q.
Proof. by rewrite /Frame big_sepMS_disj_union. Qed.
Global Instance make_and_true_l P : KnownLMakeAnd True P P.
Proof. apply left_id, _. 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