diff --git a/opam b/opam
index cbd9717c84b4345dca9cefe30ab5390e20491498..bbb3ed13c448239b3c99721e769a7b8027fd0359 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
depends: [
- "coq-iris" { (= "dev.2020-09-14.5.5d04e9aa") | (= "dev") }
+ "coq-iris" { (= "dev.2020-09-30.0.fe735a96") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index 41ce7c939b7151a2de13a71763658e2adad579d1..444c7fb8f7b1d02da3d593df05c03c5c0c7852d5 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -64,7 +64,7 @@ Section rules.
Proof.
iIntros "Hn Hm".
by iDestruct (own_valid_2 with "Hn Hm")
- as %[?%max_nat_included _]%auth_both_valid.
+ as %[?%max_nat_included _]%auth_both_valid_discrete.
Qed.
Lemma same_size (n m : nat) :
@@ -153,7 +153,7 @@ Section proof.
iModIntro. iExists _. iFrame. iNext. iIntros "Hs1'".
rel_load_r. rel_pure_r. rel_pure_r.
iDestruct (own_valid_2 with "Ha Hn")
- as %[?%max_nat_included _]%auth_both_valid; simpl in *.
+ as %[?%max_nat_included _]%auth_both_valid_discrete; simpl in *.
rel_op_l. rel_op_r. rewrite bool_decide_true; last lia.
rel_pure_r. rel_load_r. rel_op_r.
iMod ("Hcl" with "[Ha Hs1' Hs2' Htbl1' Htbl2' Hls]") as "_".
@@ -190,7 +190,7 @@ Section proof.
iInv sizeN as (m ls) "(Ha & Hs1' & >Hs2' & >Htbl1' & >Htbl2' & Hls)" "Hcl".
iModIntro. iExists _. iFrame. iNext. iIntros "Hs1'".
iDestruct (own_valid_2 with "Ha Hn")
- as %[?%max_nat_included _]%auth_both_valid; simpl in *.
+ as %[?%max_nat_included _]%auth_both_valid_discrete; simpl in *.
iMod ("Hcl" with "[Ha Hs1' Hs2' Htbl1' Htbl2' Hls]") as "_".
{ iNext. iExists _,_. by iFrame. }
clear ls. repeat rel_pure_l.
diff --git a/theories/experimental/helping/helping_stack.v b/theories/experimental/helping/helping_stack.v
index 42121a71fd50808ffc39c9cf1b45f48a2151573e..fa5138f3a1ba711090d744fa6f6d874c94068796 100644
--- a/theories/experimental/helping/helping_stack.v
+++ b/theories/experimental/helping/helping_stack.v
@@ -132,7 +132,7 @@ Section offerReg_rules.
Proof.
iIntros "HN Hfrag".
iDestruct (own_valid_2 with "HN Hfrag") as %Hfoo.
- apply auth_both_valid in Hfoo.
+ apply auth_both_valid_discrete in Hfoo.
simpl in Hfoo. destruct Hfoo as [Hfoo _].
iAssert (⌜✓ ((to_offer_reg N) !! o)âŒ)%I as %Hvalid.
{ iDestruct (own_valid with "HN") as %HNvalid.
diff --git a/theories/experimental/helping/helping_wrapper.v b/theories/experimental/helping/helping_wrapper.v
index b29f084ee3af2c0d097bdc27e08b4f9e315c7520..b197ef2d6da45de0e9030863d557fb379bcacb18 100644
--- a/theories/experimental/helping/helping_wrapper.v
+++ b/theories/experimental/helping/helping_wrapper.v
@@ -95,7 +95,7 @@ Section offerReg_rules.
Proof.
iIntros "HN Hfrag".
iDestruct (own_valid_2 with "HN Hfrag") as %Hfoo.
- apply auth_both_valid in Hfoo.
+ apply auth_both_valid_discrete in Hfoo.
simpl in Hfoo. destruct Hfoo as [Hfoo _].
iAssert (⌜✓ ((to_offer_reg N) !! o)âŒ)%I as %Hvalid.
{ iDestruct (own_valid with "HN") as %HNvalid.
diff --git a/theories/experimental/hocap/counter.v b/theories/experimental/hocap/counter.v
index 26736ca1d65759db6fe5ce2fcfd0aef1db7868ed..a0093c010cdc7c68766a7466e20cfdca0c39ed3a 100644
--- a/theories/experimental/hocap/counter.v
+++ b/theories/experimental/hocap/counter.v
@@ -48,7 +48,7 @@ Section cnt_model.
rewrite /cnt_auth /cnt.
iMod (own_alloc (â— (Some (1%Qp, to_agree n))â‹…
◯ (Some (1%Qp, to_agree n)))) as (γ) "H".
- { apply auth_both_valid. split; done. }
+ { apply auth_both_valid_discrete. split; done. }
iModIntro. iExists γ. by rewrite -own_op.
Qed.
@@ -80,7 +80,7 @@ Section cnt_model.
apply bi.wand_intro_r. rewrite /cnt /cnt_auth - !own_op.
iIntros "H". iDestruct (own_valid with "H") as %Hfoo.
iPureIntro; revert Hfoo.
- rewrite auth_both_valid.
+ rewrite auth_both_valid_discrete.
intros [[_ foo%to_agree_included]%Some_pair_included_total_2 _].
by unfold_leibniz.
Qed.
diff --git a/theories/logic/adequacy.v b/theories/logic/adequacy.v
index 1f5ffc3b813b6cac07372389dcdf6dca6597b9fc..6c1a741329421c333e28f16cb20d746548204dd9 100644
--- a/theories/logic/adequacy.v
+++ b/theories/logic/adequacy.v
@@ -29,7 +29,7 @@ Proof.
iMod (own_alloc (◠(to_tpool [e'], to_gen_heap (heap σ))
⋅ ◯ ((to_tpool [e'] : tpoolUR, ∅) : cfgUR)))
as (γc) "[Hcfg1 Hcfg2]".
- { apply auth_both_valid. split=>//.
+ { apply auth_both_valid_discrete. split=>//.
- apply prod_included. split=>///=.
apply: ucmra_unit_least.
- split=>//. apply to_tpool_valid. apply to_gen_heap_valid. }
@@ -52,7 +52,7 @@ Proof.
iInv specN as (tp σ') ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
rewrite tpool_mapsto_eq /tpool_mapsto_def /=.
iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
- move: Hvalid=> /auth_both_valid
+ move: Hvalid=> /auth_both_valid_discrete
[/prod_included [/tpool_singleton_included Hv2 _] _].
destruct tp as [|? tp']; simplify_eq/=.
iMod ("Hclose" with "[-]") as "_".
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index be1abfca329b4137f65afff93861039361b7e5e2..9c70f1bbb15c5ee4511f24946546177370fa3187 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -65,7 +65,7 @@ Section rules.
iInv specN as (tp σ) ">[Hown Hrtc]" "Hclose".
iDestruct "Hrtc" as %Hrtc.
iDestruct (own_valid_2 with "Hown Hj")
- as %[[Htpj%tpool_singleton_included' _]%prod_included ?]%auth_both_valid.
+ as %[[Htpj%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ eapply auth_update, prod_local_update_1.
by eapply (singleton_local_update _ j (Excl (fill K e))),
@@ -110,7 +110,7 @@ Section rules.
iDestruct "Hinv" as (Ï) "Hinv".
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj")
- as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid.
+ as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete.
destruct (exist_fresh (used_proph_id σ)) as [p Hp].
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1,
@@ -131,7 +131,7 @@ Section rules.
iDestruct "Hinv" as (Ï) "Hinv".
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj")
- as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid.
+ as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1,
singleton_local_update, (exclusive_local_update _ (Excl (fill K #()))). }
@@ -153,7 +153,7 @@ Section rules.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
destruct (exist_fresh (dom (gset loc) (heap σ))) as [l Hl%not_elem_of_dom].
iDestruct (own_valid_2 with "Hown Hj")
- as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid.
+ as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1,
singleton_local_update, (exclusive_local_update _ (Excl (fill K (#l)%E))). }
@@ -181,9 +181,9 @@ Section rules.
rewrite heapS_mapsto_eq /heapS_mapsto_def /=.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj")
- as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid.
+ as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete.
iDestruct (own_valid_2 with "Hown Hl")
- as %[[? ?%gen_heap_singleton_included]%prod_included ?]%auth_both_valid.
+ as %[[? ?%gen_heap_singleton_included]%prod_included ?]%auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, singleton_local_update,
(exclusive_local_update _ (Excl (fill K (of_val v)))). }
@@ -205,9 +205,9 @@ Section rules.
rewrite heapS_mapsto_eq /heapS_mapsto_def /=.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj")
- as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid.
+ as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete.
iDestruct (own_valid_2 with "Hown Hl")
- as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_both_valid.
+ as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, singleton_local_update,
(exclusive_local_update _ (Excl (fill K #()))). }
@@ -239,9 +239,9 @@ Section rules.
iDestruct "Hinv" as (Ï) "Hinv".
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj")
- as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid.
+ as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete.
iDestruct (own_valid_2 with "Hown Hl")
- as %[[_ ?%gen_heap_singleton_included]%prod_included _]%auth_both_valid.
+ as %[[_ ?%gen_heap_singleton_included]%prod_included _]%auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, singleton_local_update,
(exclusive_local_update _ (Excl (fill K (_, #false)%V))). }
@@ -266,9 +266,9 @@ Section rules.
iDestruct "Hinv" as (Ï) "Hinv".
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj")
- as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid.
+ as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete.
iDestruct (own_valid_2 with "Hown Hl")
- as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_both_valid.
+ as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, singleton_local_update,
(exclusive_local_update _ (Excl (fill K (_, #true)%V))). }
@@ -297,9 +297,9 @@ Section rules.
iDestruct "Hinv" as (Ï) "Hinv".
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj")
- as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid.
+ as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete.
iDestruct (own_valid_2 with "Hown Hl")
- as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_both_valid.
+ as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, singleton_local_update,
(exclusive_local_update _ (Excl (fill K (# i1)))). }
@@ -326,7 +326,7 @@ Section rules.
iDestruct "Hspec" as (Ï) "Hspec".
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj")
- as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid.
+ as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete.
assert (j < length tp) by eauto using lookup_lt_Some.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1,
diff --git a/theories/prelude/bijections.v b/theories/prelude/bijections.v
index 139c401a11b8582b3f8fb5b0b10766eb38350530..fd0f7243fc5302d4c63e66ff647fe2f9432711ed 100644
--- a/theories/prelude/bijections.v
+++ b/theories/prelude/bijections.v
@@ -116,8 +116,8 @@ Section logic.
Proof.
iIntros "HL H1 H2". rewrite BIJ_eq /BIJ_def inBij_eq /inBij_def.
iDestruct "HL" as "[HL HL1]"; iDestruct "HL1" as %HL.
- iDestruct (own_valid_2 with "HL H1") as %Hv1%auth_both_valid.
- iDestruct (own_valid_2 with "HL H2") as %Hv2%auth_both_valid.
+ iDestruct (own_valid_2 with "HL H1") as %Hv1%auth_both_valid_discrete.
+ iDestruct (own_valid_2 with "HL H2") as %Hv2%auth_both_valid_discrete.
iPureIntro.
destruct Hv1 as [Hv1 _]; destruct Hv2 as [Hv2 _].
apply gset_included, elem_of_subseteq_singleton in Hv1;