From 24e30b43739d800cb544cbdc0178fbb8b325ecb0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 29 Oct 2017 14:55:56 +0100
Subject: [PATCH] fix for latest Iris
---
theories/base/at_cas.v | 2 +-
theories/base/at_fai.v | 2 +-
theories/base/at_shared.v | 2 +-
theories/base/at_write.v | 2 +-
theories/examples/circ_buffer.v | 8 ++++----
theories/examples/nat_tokens.v | 10 +++++-----
theories/examples/rcu.v | 2 +-
theories/examples/ticket_lock.v | 2 +-
theories/gps/shared.v | 2 +-
theories/lang/blocks.v | 2 +-
theories/rsl/rsl.v | 2 +-
theories/rsl/rsl_sts.v | 6 +++---
theories/viewpred/viewpred.v | 2 +-
13 files changed, 22 insertions(+), 22 deletions(-)
diff --git a/theories/base/at_cas.v b/theories/base/at_cas.v
index c6df7645..c1b20371 100644
--- a/theories/base/at_cas.v
+++ b/theories/base/at_cas.v
@@ -11,7 +11,7 @@ Lemma f_CAS `{fG : !foundationG Σ} π V l h (v_r v_w: Z):
∗ ( ⌜b = true⌝ ∗ ⌜v = v_r⌝
∗ ⌜value_at h' V' (VInj v_w)⌝
∗ ⌜h' ≡ {[VInj v_w, V']} ∪ h⌝
- ∗ ⌜h ⊥ {[VInj v_w, V']}⌝
+ ∗ ⌜h ## {[VInj v_w, V']}⌝
∗ ⌜init l h'⌝
∗ ⌜adj_opt (V1 !! l) (V' !! l)⌝
∗ ⌜no_adj_right l h V1⌝
diff --git a/theories/base/at_fai.v b/theories/base/at_fai.v
index 7c63dfe9..1f345495 100644
--- a/theories/base/at_fai.v
+++ b/theories/base/at_fai.v
@@ -11,7 +11,7 @@ Lemma f_FAI `{fG : !foundationG Σ} C π V l h:
∗ ⌜v' = (v + 1) `mod` Z.pos C⌝%Z
∗ ⌜value_at h' V' (VInj v')⌝
∗ ⌜h' ≡ {[VInj v', V']} ∪ h⌝
- ∗ ⌜h ⊥ {[VInj v', V']}⌝
+ ∗ ⌜h ## {[VInj v', V']}⌝
∗ ⌜init l h'⌝
∗ ⌜adj_opt (V1 !! l) (V' !! l)⌝
∗ ⌜no_adj_right l h V1⌝ }}}.
diff --git a/theories/base/at_shared.v b/theories/base/at_shared.v
index 4f2aacce..bdfdcbf9 100644
--- a/theories/base/at_shared.v
+++ b/theories/base/at_shared.v
@@ -22,7 +22,7 @@ Lemma write_at_update_hist ς ς' (V: View) h t l v (m: message)
(VInj v, mview m) ∈ h'
∧ h' ≡ map_vt (hist_from (mem ς') l t)
∧ h' ≡ {[VInj v, mview m]} ∪ h
- ∧ h ⊥ {[VInj v, mview m]}.
+ ∧ h ## {[VInj v, mview m]}.
Proof.
destruct Safe as [v' [V_l [Hv'1 Hv'2]]].
assert (t ⊑ mtime m).
diff --git a/theories/base/at_write.v b/theories/base/at_write.v
index 626ec95f..eaf25691 100644
--- a/theories/base/at_write.v
+++ b/theories/base/at_write.v
@@ -7,7 +7,7 @@ Lemma f_write_at `{fG : !foundationG Σ} π V_l l h v:
⌜V_l ⊑ V'⌝ ∗ Seen π V'
∗ Hist l h' ∗ ⌜init_local h' V'⌝ ∗ ⌜init l h'⌝
∗ ⌜h' ≡ {[VInj v, V']} ∪ h⌝
- ∗ ⌜h ⊥ {[VInj v, V']}⌝
+ ∗ ⌜h ## {[VInj v, V']}⌝
∗ ⌜value_at h' V' (VInj v)⌝}}}.
Proof.
iIntros (Φ) "(#I & Seen & Hist & %) Post".
diff --git a/theories/examples/circ_buffer.v b/theories/examples/circ_buffer.v
index e7380fcc..e25d4e1d 100644
--- a/theories/examples/circ_buffer.v
+++ b/theories/examples/circ_buffer.v
@@ -101,7 +101,7 @@ Section CircBuffer.
iIntros "Toks".
rewrite /pToks_from /pTok. rewrite -own_op pair_op.
rewrite !/op !/cmra_op /=.
- case (decide ({[Pos.of_succ_nat i]} ⊥ coPset_from_ex (S i))) => [_|ND];
+ case (decide ({[Pos.of_succ_nat i]} ## coPset_from_ex (S i))) => [_|ND];
last first.
{ exfalso. apply ND, coPset_from_disjoint. }
iApply (own_mono with "Toks"). apply prod_included.
@@ -113,7 +113,7 @@ Section CircBuffer.
Proof.
iIntros "Toks".
rewrite -own_op pair_op !/op !/cmra_op /=.
- case (decide ({[Pos.of_succ_nat i]} ⊥ coPset_from_ex (S i))) => [_|ND];
+ case (decide ({[Pos.of_succ_nat i]} ## coPset_from_ex (S i))) => [_|ND];
last first.
{ exfalso. apply ND, coPset_from_disjoint. }
iApply (own_mono with "Toks"). apply prod_included.
@@ -126,9 +126,9 @@ Section CircBuffer.
Proof.
iIntros "Toks".
rewrite -own_op pair_op !/op !/cmra_op /= /ucmra_op /=.
- case (decide (coPset_from_ex i ⊥ ∅)) =>[_|ND]; last first.
+ case (decide (coPset_from_ex i ## ∅)) =>[_|ND]; last first.
{ exfalso. apply ND. set_solver+. }
- case (decide (∅ ⊥ coPset_from_ex i)) =>[_|ND]; last first.
+ case (decide (∅ ## coPset_from_ex i)) =>[_|ND]; last first.
{ exfalso. apply ND. set_solver+. }
iApply (own_mono with "Toks"). apply prod_included.
rewrite /= !coPset_disj_included. set_solver+.
diff --git a/theories/examples/nat_tokens.v b/theories/examples/nat_tokens.v
index c1ffb814..c3611e78 100644
--- a/theories/examples/nat_tokens.v
+++ b/theories/examples/nat_tokens.v
@@ -36,7 +36,7 @@ Proof.
Qed.
Lemma coPset_from_disjoint i:
- {[Pos.of_succ_nat i]} ⊥ coPset_from_ex (S i).
+ {[Pos.of_succ_nat i]} ## coPset_from_ex (S i).
Proof.
apply disjoint_singleton_l. rewrite coPset_from_ex_gt SuccNat2Pos.id_succ. lia.
Qed.
@@ -57,7 +57,7 @@ Proof.
Qed.
Lemma coPset_of_gset_difference_union (X Y Z: gset positive)
- (Disj: Y ⊥ Z) (Sub: Y ⊆ X):
+ (Disj: Y ## Z) (Sub: Y ⊆ X):
coPset.of_gset (X ∖ Z) = coPset.of_gset (X ∖ (Y ∪ Z)) ∪ coPset.of_gset Y.
Proof.
apply leibniz_equiv. move => x.
@@ -71,14 +71,14 @@ Proof.
Qed.
Lemma coPset_of_gset_difference_disjoint (X Y Z: gset positive):
- coPset.of_gset (X ∖ (Y ∪ Z)) ⊥ coPset.of_gset Y.
+ coPset.of_gset (X ∖ (Y ∪ Z)) ## coPset.of_gset Y.
Proof.
rewrite elem_of_disjoint.
move => x. rewrite !coPset.elem_of_of_gset elem_of_difference elem_of_union.
set_solver.
Qed.
-Lemma coPset_of_gset_top_difference (X Y: gset positive) (Disj: X ⊥ Y):
+Lemma coPset_of_gset_top_difference (X Y: gset positive) (Disj: X ## Y):
⊤ ∖ coPset.of_gset X = (⊤ ∖ coPset.of_gset (Y ∪ X)) ∪ coPset.of_gset Y.
Proof.
apply leibniz_equiv. move => x.
@@ -90,7 +90,7 @@ Proof.
Qed.
Lemma coPset_of_gset_top_disjoint (X Y: gset positive):
- (⊤ ∖ coPset.of_gset (Y ∪ X)) ⊥ coPset.of_gset Y.
+ (⊤ ∖ coPset.of_gset (Y ∪ X)) ## coPset.of_gset Y.
Proof.
rewrite elem_of_disjoint.
move => x. rewrite elem_of_difference coPset_of_gset_union. set_solver.
diff --git a/theories/examples/rcu.v b/theories/examples/rcu.v
index f8195933..b2add99b 100644
--- a/theories/examples/rcu.v
+++ b/theories/examples/rcu.v
@@ -353,7 +353,7 @@ Section RCU.
⊢ own γ {[ t := CoPset (⊤ ∖ coPset.of_gset Y) ]}
∗ own γ {[ t := CoPset $ coPset.of_gset (Y ∖ X) ]}.
Proof.
- have Hj: (X ⊥ Y ∖ X) by set_solver+.
+ have Hj: (X ## Y ∖ X) by set_solver+.
rewrite (coPset_of_gset_top_difference _ _ Hj) -coPset_disj_union;
last apply coPset_of_gset_top_disjoint.
rewrite (union_comm_L (Y ∖ X)) -union_difference_L; last auto.
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 5d2715bd..4d3dca20 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -367,7 +367,7 @@ Section TicketLock.
Proof.
iIntros "Perms". rewrite -own_op pair_op.
rewrite !/op /cmra_op /=.
- case (decide ({[Pos.of_succ_nat t]} ⊥ coPset_from_ex (S t))) => [_|ND];
+ case (decide ({[Pos.of_succ_nat t]} ## coPset_from_ex (S t))) => [_|ND];
last first.
{ exfalso. apply ND, coPset_from_disjoint. }
iApply (own_mono with "Perms"). apply prod_included.
diff --git a/theories/gps/shared.v b/theories/gps/shared.v
index c27359dd..d4873062 100644
--- a/theories/gps/shared.v
+++ b/theories/gps/shared.v
@@ -189,7 +189,7 @@ Section Setup.
Persistent (PrtSeen γ s V) := _.
Lemma StateInjection_insert s v V h ζ
- (Cons: Consistent ζ h) (SI: StateInjection ζ) (HDisj: h ⊥ {[VInj v,V]})
+ (Cons: Consistent ζ h) (SI: StateInjection ζ) (HDisj: h ## {[VInj v,V]})
: StateInjection ({[s, (v, V)]} ∪ ζ).
Proof.
move => e1 e2 /elem_of_union [/elem_of_singleton ->| In1]
diff --git a/theories/lang/blocks.v b/theories/lang/blocks.v
index 2aec0036..922d36b3 100644
--- a/theories/lang/blocks.v
+++ b/theories/lang/blocks.v
@@ -54,7 +54,7 @@ Section GHist.
Lemma gblock_ends_ins_update x h p
(OK: hTime_ok x ({[p]} ∪ h))
- (Fresh: h ⊥ {[p]})
+ (Fresh: h ## {[p]})
: gblock_ends_ins x h p (gblock_ends x h) (gblock_ends x ({[p]} ∪ h)).
Proof.
apply block_ends_ins.
diff --git a/theories/rsl/rsl.v b/theories/rsl/rsl.v
index a790e4a5..0886f1b8 100644
--- a/theories/rsl/rsl.v
+++ b/theories/rsl/rsl.v
@@ -121,7 +121,7 @@ Instance InitRaw_persistent V jγ : Persistent (InitRaw V jγ) := _.
Lemma big_sepS_gblock_ends_ins_update
l (h: History) p0 (Ψ: Val * View → iProp)
- (Disj: (h ⊥ {[p0]})%C)
+ (Disj: (h ## {[p0]})%C)
(GB: gblock_ends_ins l h p0 (gblock_ends l h) (gblock_ends l ({[p0]} ∪ h)))
: Ψ p0 ∗ ([∗ set] p ∈ gblock_ends l h, Ψ p)
⊢ ([∗ set] p ∈ gblock_ends l ({[p0]} ∪ h), Ψ p).
diff --git a/theories/rsl/rsl_sts.v b/theories/rsl/rsl_sts.v
index da40162b..eca760c2 100644
--- a/theories/rsl/rsl_sts.v
+++ b/theories/rsl/rsl_sts.v
@@ -295,15 +295,15 @@ Proof.
Qed.
(** Properties of split **)
-Lemma tok_disj_state_singleton s i: i ∈ rISet2 s → sts.tok s ⊥ {[Change i]}.
+Lemma tok_disj_state_singleton s i: i ∈ rISet2 s → sts.tok s ## {[Change i]}.
Proof. abstract set_solver. Qed.
Lemma state_ISet_split_token_disj_1 i1 i2 i s:
- sts.tok (state_ISet_split i1 i2 i s) ⊥ {[Change i1]}.
+ sts.tok (state_ISet_split i1 i2 i s) ## {[Change i1]}.
Proof. apply tok_disj_state_singleton. destruct s; abstract set_solver+. Qed.
Lemma state_ISet_split_token_disj_2 i1 i2 i s:
- sts.tok (state_ISet_split i1 i2 i s) ⊥ {[Change i2]}.
+ sts.tok (state_ISet_split i1 i2 i s) ## {[Change i2]}.
Proof. apply tok_disj_state_singleton. destruct s; abstract set_solver+. Qed.
Lemma state_ISet_split_included_1 i1 i2 i s:
diff --git a/theories/viewpred/viewpred.v b/theories/viewpred/viewpred.v
index 9a12a775..8b1f587a 100644
--- a/theories/viewpred/viewpred.v
+++ b/theories/viewpred/viewpred.v
@@ -286,7 +286,7 @@ Notation "∀ x .. y , P" := (vPred_forall (λ x, .. (vPred_forall (λ y, P%VP))
Notation "∃ x .. y , P" := (vPred_exists (λ x, .. (vPred_exists (λ y, P%VP)) ..)) : vPred_scope.
Notation "P ∗ Q" := (vPred_sep P Q) : vPred_scope.
Notation "x = y" := (vPred_pure (x%C%type = y%C%type)) : vPred_scope.
-Notation "x ⊥ y" := (vPred_pure (x%C%type ⊥ y%C%type)) : vPred_scope.
+Notation "x ## y" := (vPred_pure (x%C%type ## y%C%type)) : vPred_scope.
Notation "'False'" := (vPred_pure False) : vPred_scope.
Notation "'True'" := (vPred_pure True) : vPred_scope.
Infix "∧" := vPred_and : vPred_scope.
--
GitLab