Commit 6bf5566f authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Replace some uses of `set_solver` by `multiset_solver`.

parent 0ff8f186
......@@ -14,7 +14,7 @@ iris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_lo
depends: [
"coq" { (>= "8.11" & < "8.14~") | (= "dev") }
"coq-stdpp" { (= "dev.2021-03-11.0.6d001c9d") | (= "dev") }
"coq-stdpp" { (= "dev.2021-03-13.0.7fdaea0f") | (= "dev") }
]
build: ["./make-package" "iris" "-j%{jobs}%"]
......
......@@ -30,7 +30,7 @@ Lemma big_opMS_None {M : cmra} `{Countable A} (f : A → option M) X :
([^op mset] x X, f x) = None x, x X f x = None.
Proof.
induction X as [|x X IH] using gmultiset_ind.
{ rewrite big_opMS_empty. set_solver. }
{ rewrite big_opMS_empty. multiset_solver. }
rewrite -equiv_None big_opMS_disj_union big_opMS_singleton equiv_None op_None IH.
set_solver.
multiset_solver.
Qed.
......@@ -2103,11 +2103,11 @@ Section gmultiset.
{ by rewrite (affine ( _)%I) big_sepMS_empty. }
rewrite intuitionistically_sep_dup big_sepMS_disj_union.
rewrite big_sepMS_singleton. f_equiv.
- rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
- rewrite (forall_elim x) pure_True ?True_impl; last multiset_solver.
by rewrite intuitionistically_elim.
- rewrite -IH. f_equiv. apply forall_mono=> y.
apply impl_intro_l, pure_elim_l=> ?.
by rewrite pure_True ?True_impl; last set_solver.
by rewrite pure_True ?True_impl; last multiset_solver.
Qed.
Lemma big_sepMS_forall `{BiAffine PROP} Φ X :
......
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