Commit 7a260d80 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump std++ (multiset singleton).

parent 823d3357
......@@ -14,7 +14,7 @@ iris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_lo
depends: [
"coq" { (>= "8.12" & < "8.14~") | (= "dev") }
"coq-stdpp" { (= "dev.2021-04-08.1.5843163b") | (= "dev") }
"coq-stdpp" { (= "dev.2021-04-20.2.03290b88") | (= "dev") }
]
build: ["./make-package" "iris" "-j%{jobs}%"]
......
......@@ -630,13 +630,13 @@ Section gmultiset.
([^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_eq /big_opMS_def gmultiset_elements_disj_union big_opL_app. Qed.
Lemma big_opMS_singleton f x : ([^o mset] y {[ x ]}, f y) f x.
Lemma big_opMS_singleton f x : ([^o mset] y {[+ x +]}, f y) f x.
Proof.
intros. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_singleton /= right_id.
Qed.
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.
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_disj_union.
by rewrite -gmultiset_disj_union_difference'.
......
......@@ -86,7 +86,7 @@ Section gmultiset.
Qed.
Lemma big_opMS_singletons X :
([^op mset] x X, {[ x ]}) = X.
([^op mset] x X, {[+ x +]}) = X.
Proof.
induction X as [|x X IH] using gmultiset_ind.
- rewrite big_opMS_empty. done.
......
......@@ -2053,7 +2053,7 @@ Section gmultiset.
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.
x X ([ mset] y X, Φ y) Φ x [ mset] y X {[+ x +]}, Φ y.
Proof. apply big_opMS_delete. Qed.
Lemma big_sepMS_elem_of Φ X x `{!Absorbing (Φ x)} :
......@@ -2067,7 +2067,7 @@ Section gmultiset.
intros. rewrite big_sepMS_delete //. by apply sep_mono_r, wand_intro_l.
Qed.
Lemma big_sepMS_singleton Φ x : ([ mset] y {[ x ]}, Φ y) Φ x.
Lemma big_sepMS_singleton Φ x : ([ mset] y {[+ x +]}, Φ y) Φ x.
Proof. apply big_opMS_singleton. Qed.
Lemma big_sepMS_sep Φ Ψ X :
......@@ -2155,7 +2155,7 @@ Section gmultiset.
Φ x
(* we reobtain the bigop for a predicate [Ψ] selected by the user *)
Ψ,
( y, y X {[ x ]} Φ y - Ψ y) -
( y, y X {[+ x +]} Φ y - Ψ y) -
Ψ x -
[ mset] y X, Ψ y.
Proof.
......
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