Skip to content

Commit e92ba09

Browse files
suhrsuhr
committed
Add Local Updates
1 parent bd29ca4 commit e92ba09

1 file changed

Lines changed: 294 additions & 0 deletions

File tree

‎src/Iris/Algebra/LocalUpdates.lean‎

Lines changed: 294 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,294 @@
1+
/-
2+
Copyright (c) 2025 Сухарик. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Сухарик (@suhr)
5+
-/
6+
import Iris.Algebra.CMRA
7+
8+
namespace Iris
9+
10+
def LocalUpdate {α: Type}[CMRA α] (x y: α × α) :=
11+
∀n mz, ✓{n} x.1 → x.1 ≡{n}≡ x.2 •? mz → ✓{n} y.1 ∧ y.1 ≡{n}≡ y.2 •? mz
12+
13+
infixr:50 " ~l~> " => LocalUpdate
14+
15+
namespace LocalUpdate
16+
17+
section CMRA
18+
variable [cmr: CMRA α]
19+
20+
-- Global Instance local_update_proper :
21+
-- Proper ((≡) ==> (≡) ==> iff) (@local_update SI A).
22+
-- Proof. unfold local_update. by repeat intro; setoid_subst. Qed.
23+
24+
theorem local_update_id (x: α × α): x ~l~> x := fun _ _ vx e => ⟨vx, e⟩
25+
26+
theorem local_update_left_eqv {x y: α × α} (z: α × α) (h: x ≡ y) : x ~l~> z → y ~l~> z :=
27+
fun u => fun n mw v e =>
28+
have e1: x.fst ≡{n}≡ y.fst := (OFE.equiv_fst h).dist
29+
have := calc
30+
x.fst ≡{n}≡ y.fst := e1
31+
y.fst ≡{n}≡ y.snd •? mw := e
32+
y.snd •? mw ≡{n}≡ x.snd •? mw := CMRA.opM_left_dist mw (OFE.equiv_snd h).dist.symm
33+
u n mw ((OFE.Dist.validN e1.symm).mp v) this
34+
35+
theorem local_update_right_eqv (x: α × α) {y z: α × α} (h: y ≡ z): x ~l~> y → x ~l~> z :=
36+
fun u => fun n mw v e =>
37+
let ⟨vy, e⟩ := u n mw v e
38+
have e1: y.fst ≡{n}≡ z.fst := OFE.dist_fst (OFE.Equiv.dist h)
39+
have := calc
40+
z.fst ≡{n}≡ y.fst := e1.symm
41+
_ ≡{n}≡ y.snd •? mw := e
42+
_ ≡{n}≡ z.snd •? mw := CMRA.opM_left_dist mw $ OFE.dist_snd (OFE.Equiv.dist h)
43+
⟨(OFE.Dist.validN e1).mp vy, this⟩
44+
45+
-- Global Instance local_update_preorder : PreOrder (@local_update SI A).
46+
-- Proof. split; unfold local_update; red; naive_solver. Qed.
47+
48+
theorem exclusive_local_update {y: α}[CMRA.Exclusive y](x x': α)(vx': ✓ x'): (x,y) ~l~> (x', x') :=
49+
fun n mz vx e =>
50+
have : mz = none := CMRA.none_of_excl_valid_op ((OFE.Dist.validN e).mp vx)
51+
have : x' ≡{n}≡ x' •? mz := calc
52+
x' ≡{n}≡ x' := OFE.Dist.of_eq rfl
53+
_ = x' •? mz := by rw[this]; rfl
54+
⟨vx'.validN, this⟩
55+
56+
theorem op_local_update (x y z : α) (h : ∀ n, ✓{n} x → ✓{n} (z • x)) : (x, y) ~l~> (z • x, z • y) :=
57+
fun n mz vx (e : x ≡{n}≡ y •? mz) =>
58+
have g1 : ✓{n} (z • x) := h n vx
59+
have g2 := calc
60+
(z • x) ≡{n}≡ z • (y •? mz) := CMRA.op_right_dist z e
61+
_ ≡{n}≡ (z • y) •? mz := OFE.Dist.symm (CMRA.op_opM_assoc_dist z y mz)
62+
⟨g1, g2⟩
63+
64+
theorem op_local_update_discrete [CMRA.Discrete α] (x y z : α)
65+
(h : ✓ x → ✓ (z • x)) : (x, y) ~l~> (z • x, z • y) :=
66+
fun n mz vx e =>
67+
have this n (vx: ✓{n} x): ✓{n} (z • x) :=
68+
CMRA.Valid.validN (h ((CMRA.valid_iff_validN' n).mpr vx))
69+
op_local_update x y z this n mz vx e
70+
71+
theorem op_local_update_frame (x y x' y' yf : α)
72+
(h : (x, y) ~l~> (x', y')) : (x, y • yf) ~l~> (x', y' • yf) :=
73+
fun n mz vx e =>
74+
have := h n (some yf • mz) vx
75+
have := calc
76+
x ≡{n}≡ (y • yf) •? mz := e
77+
_ ≡{n}≡ y •? (some yf • mz) := CMRA.op_some_opM_assoc_dist y yf mz
78+
have u := h n (some yf • mz) vx this
79+
have := calc
80+
x' ≡{n}≡ y' •? (some yf • mz) := u.2
81+
_ ≡{n}≡ (y' • yf) •? mz := (CMRA.op_some_opM_assoc_dist y' yf mz).symm
82+
⟨u.1, this⟩
83+
84+
theorem cancel_local_update (x y z : α) [CMRA.Cancelable x] : (x • y, x • z) ~l~> (y, z) :=
85+
fun _ _ vx e => ⟨CMRA.validN_op_right vx, CMRA.op_opM_cancel_dist vx e⟩
86+
87+
theorem replace_local_update (x y : α) [CMRA.IdFree x] (h : ✓ y) : (x, x) ~l~> (y, y) :=
88+
fun _ mz vx e =>
89+
match mz with
90+
| none => ⟨CMRA.Valid.validN h, OFE.Dist.symm (OFE.Dist.of_eq rfl)⟩
91+
| some _ => absurd e.symm (CMRA.id_freeN_r vx)
92+
93+
theorem core_id_local_update (x y z : α) [CMRA.CoreId y] (inc : y ≼ x) : (x, z) ~l~> (x, z • y) :=
94+
fun n mz vx e =>
95+
have g: x ≡{n}≡ (z • y) •? mz :=
96+
suffices h: y • x ≡{n}≡ (z • y) •? mz
97+
from (CMRA.op_core_right_of_inc inc).symm.dist.trans h
98+
match mz with
99+
| none =>
100+
calc
101+
y • x ≡{n}≡ y • z := CMRA.op_right_dist y e
102+
_ ≡{n}≡ z • y := CMRA.op_commN
103+
| some w =>
104+
calc
105+
y • x ≡{n}≡ y • (z • w) := CMRA.op_right_dist y e
106+
_ ≡{n}≡ (y • z) • w := CMRA.op_assocN
107+
_ ≡{n}≡ (z • y) • w := CMRA.op_left_dist w (CMRA.op_commN)
108+
⟨vx, g⟩
109+
110+
theorem local_update_discrete [CMRA.Discrete α] (x y x' y' : α) :
111+
(x, y) ~l~> (x', y') ↔ ∀ mz, ✓ x → x ≡ y •? mz → (✓ x' ∧ x' ≡ y' •? mz) :=
112+
Iff.intro
113+
(fun h mz vx e =>
114+
have ⟨vx', e⟩ := h 0 mz vx.validN e.dist
115+
⟨CMRA.Discrete.discrete_valid vx', OFE.discrete_0 e⟩)
116+
(fun h n mz vx e =>
117+
have ⟨vx', e'⟩ := h mz ((CMRA.valid_iff_validN' n).mpr vx) (OFE.discrete_n e)
118+
⟨CMRA.Valid.validN vx', e'.dist⟩)
119+
120+
theorem local_update_valid0 (x y x' y' : α)
121+
(h: ✓{0} x → ✓{0} y → some y ≼{0} some x → (x, y) ~l~> (x', y')) :
122+
(x, y) ~l~> (x', y') :=
123+
fun n mz vx e =>
124+
have v0y: ✓{0} y := CMRA.valid0_of_validN $ CMRA.validN_opM ((OFE.Dist.validN e).mp vx)
125+
have: some y ≼{0} some x := CMRA.inc0_of_incN (CMRA.some_inc_some_of_dist_opM e)
126+
have: (x, y) ~l~> (x', y') := h (CMRA.valid0_of_validN vx) v0y this
127+
this n mz vx e
128+
129+
theorem local_update_valid [CMRA.Discrete α] (x y x' y' : α)
130+
(h: ✓ x → ✓ y → some y ≼ some x → (x, y) ~l~> (x', y')) : (x, y) ~l~> (x', y') :=
131+
have h0 vx0 vy0 mz: (x, y) ~l~> (x', y') :=
132+
h (CMRA.discrete_valid vx0) (CMRA.discrete_valid vy0) ((CMRA.inc_iff_incN 0).mpr mz)
133+
local_update_valid0 x y x' y' h0
134+
135+
theorem local_update_total_valid0 [CMRA.IsTotal α] (x y x' y' : α)
136+
(h: ✓{0} x → ✓{0} y → y ≼{0} x → (x, y) ~l~> (x', y')) : (x, y) ~l~> (x', y') :=
137+
have h0 (vx0: ✓{0} x) (vy0: ✓{0} y) (mz : some y ≼{0} some x) : (x, y) ~l~> (x', y') :=
138+
h vx0 vy0 (CMRA.incN_of_some_incN_some mz)
139+
local_update_valid0 x y x' y' h0
140+
141+
theorem local_update_total_valid [CMRA.IsTotal α] [CMRA.Discrete α] (x y x' y' : α)
142+
(h: ✓ x → ✓ y → y ≼ x → (x, y) ~l~> (x', y')) : (x, y) ~l~> (x', y') :=
143+
have hs vx vy inc : (x, y) ~l~> (x', y') := h vx vy (CMRA.inc_of_some_inc_some inc)
144+
local_update_valid x y x' y' hs
145+
end CMRA
146+
147+
section updates_unital
148+
variable [UCMRA α]
149+
150+
theorem local_update_unital (x y x' y' : α) :
151+
(x, y) ~l~> (x', y') ↔ ∀ n z, ✓{n} x → x ≡{n}≡ y • z → (✓{n} x' ∧ x' ≡{n}≡ y' • z) where
152+
mp h n z := h n (some z)
153+
mpr h n mz vx e :=
154+
match mz with
155+
| none =>
156+
have := h n UCMRA.unit vx (e.trans (CMRA.unit_right_id_dist y).symm)
157+
⟨this.left, this.right.trans (CMRA.unit_right_id_dist y')⟩
158+
| some z => h n z vx e
159+
160+
theorem local_update_unital_discrete [CMRA.Discrete α] (x y x' y' : α) :
161+
(x, y) ~l~> (x', y') ↔ ∀ z, ✓ x → x ≡ y • z → (✓ x' ∧ x' ≡ y' • z) where
162+
mp h z vx e :=
163+
have ⟨vx', e'⟩ := h 0 (some z) (CMRA.Valid.validN vx) e.dist
164+
⟨CMRA.discrete_valid vx', OFE.discrete_0 e'⟩
165+
mpr h :=
166+
have h' n z vnx e : (✓{n} x' ∧ x' ≡{n}≡ y' • z) :=
167+
have ⟨vx', e'⟩ := h z ((CMRA.valid_iff_validN' n).mpr vnx) (OFE.discrete_n e)
168+
⟨CMRA.Valid.validN vx', OFE.Equiv.dist e'⟩
169+
(local_update_unital x y x' y').mpr h'
170+
171+
theorem cancel_local_update_unit (x y : α) [CMRA.Cancelable x] :
172+
(x • y, x) ~l~> (y, UCMRA.unit) :=
173+
have e : (x • y, x • UCMRA.unit) ≡ (x • y, x) :=
174+
OFE.equiv_prod_ext OFE.Equiv.rfl (CMRA.unit_right_id)
175+
local_update_left_eqv _ e (cancel_local_update x y UCMRA.unit)
176+
177+
end updates_unital
178+
179+
section updates_unit
180+
181+
theorem unit_local_update (x y x' y' : Unit) : (x, y) ~l~> (x', y') :=
182+
match x, y, x', y' with
183+
| .unit, .unit, .unit, .unit => local_update_id ((), ())
184+
185+
end updates_unit
186+
187+
section updates_discrete_fun
188+
189+
theorem discrete_fun_local_update {α : Type} (β : α → Type _) [∀ x, UCMRA (β x)]
190+
(f g f' g' : ∀ x, β x) (h : ∀ x : α, (f x, g x) ~l~> (f' x, g' x))
191+
: (f, g) ~l~> (f', g') :=
192+
fun n mz vx e =>
193+
have g₁ : ✓{n} f' := fun x =>
194+
match mz with
195+
| .none => (h x n .none (vx x) (e x)).left
196+
| .some z => (h x n (.some (z x)) (vx x) (e x)).left
197+
have g₂ : f' ≡{n}≡ g' •? mz := fun x =>
198+
match mz with
199+
| .none => (h x n .none (vx x) (e x)).right
200+
| .some z => (h x n (.some (z x)) (vx x) (e x)).right
201+
⟨g₁, g₂⟩
202+
203+
end updates_discrete_fun
204+
205+
section updates_product
206+
variable [CMRA α] [CMRA β]
207+
208+
theorem prod_local_update
209+
{x y x' y' : α × β} (hl: (x.1, y.1) ~l~> (x'.1, y'.1)) (hr: (x.2, y.2) ~l~> (x'.2, y'.2))
210+
: (x, y) ~l~> (x', y') :=
211+
fun n mz vx e =>
212+
match mz with
213+
| .none =>
214+
have ⟨v₁, e₁⟩ := hl n .none vx.left e.left
215+
have ⟨v₂, e₂⟩ := hr n .none vx.right e.right
216+
⟨⟨v₁, v₂⟩, ⟨e₁, e₂⟩⟩
217+
| .some z =>
218+
have ⟨v₁, e₁⟩ := hl n (.some z.fst) vx.left e.left
219+
have ⟨v₂, e₂⟩ := hr n (.some z.snd) vx.right e.right
220+
⟨⟨v₁, v₂⟩, ⟨e₁, e₂⟩⟩
221+
222+
theorem prod_local_update'
223+
{x1 y1 x1' y1' : α} {x2 y2 x2' y2' : β}
224+
(hl: (x1, y1) ~l~> (x1', y1')) (hr: (x2, y2) ~l~> (x2', y2'))
225+
: ((x1, x2), (y1, y2)) ~l~> ((x1', x2'), (y1', y2')) :=
226+
prod_local_update hl hr
227+
228+
theorem prod_local_update_1
229+
(x1 y1 x1' y1' : α) (x2 y2 : β) (h: (x1, y1) ~l~> (x1', y1'))
230+
: ((x1, x2), (y1, y2)) ~l~> ((x1', x2), (y1', y2)) :=
231+
prod_local_update' h (local_update_id (x2, y2))
232+
233+
theorem prod_local_update_2
234+
(x1 y1 : α) (x2 y2 x2' y2' : β) (h: (x2, y2) ~l~> (x2', y2'))
235+
: ((x1, x2), (y1, y2)) ~l~> ((x1, x2'), (y1, y2')) :=
236+
prod_local_update' (local_update_id (x1, y1)) h
237+
238+
end updates_product
239+
240+
section updates_option
241+
theorem option_local_update {α : Type} [CMRA α]
242+
{x y x' y' : α} (h: (x, y) ~l~> (x', y')) : (some x, some y) ~l~> (some x', some y') :=
243+
fun n mz vx e =>
244+
match mz with
245+
| .none => h n .none vx e
246+
| .some .none => have ⟨vx, e⟩ := h n .none vx e; ⟨vx, e⟩
247+
| .some (.some z) => have ⟨vx, e⟩ := h n (.some z) vx e; ⟨vx, e⟩
248+
249+
theorem option_local_update_none {α : Type} [UCMRA α]
250+
{x x' y' : α} (h: (x, UCMRA.unit) ~l~> (x', y')): (some x, none) ~l~> (some x', some y') :=
251+
fun n mz vx e =>
252+
match mz with
253+
| .none => False.elim e
254+
| .some .none => False.elim e
255+
| .some (.some z) =>
256+
have e: x ≡{n}≡ z := e
257+
have ⟨vx, e⟩ := h n (.some z) vx (e.trans (CMRA.unit_left_id_dist z).symm)
258+
⟨vx, e⟩
259+
260+
theorem alloc_option_local_update {α : Type} [CMRA α]
261+
{x : α} (y : Option α) (vx: ✓ x): (none, y) ~l~> (some x, some x) :=
262+
fun n mz _ e =>
263+
match mz with
264+
| .none => ⟨CMRA.Valid.validN vx, OFE.Dist.of_eq rfl⟩
265+
| .some .none => ⟨CMRA.Valid.validN vx, OFE.Dist.of_eq rfl⟩
266+
| .some (.some z) =>
267+
have ⟨_, hw⟩ := CMRA.exists_op_some_dist_some (n := n) y z
268+
False.elim (e.trans hw)
269+
270+
theorem delete_option_local_update {α : Type} [CMRA α]
271+
(x : Option α) (y : α) [CMRA.Exclusive y] :
272+
(x, some y) ~l~> (none, none) :=
273+
fun n mz vx e =>
274+
match mz with
275+
| .none => ⟨True.intro, OFE.Dist.of_eq rfl⟩
276+
| .some .none => ⟨True.intro, OFE.Dist.of_eq rfl⟩
277+
| .some (.some z) =>
278+
have : ✓{n} some y • some z := (OFE.Dist.validN e).mp vx
279+
absurd this not_valid_some_exclN_op_left
280+
281+
theorem delete_option_local_update_cancelable {α : Type} [CMRA α]
282+
(mx : Option α) [CMRA.Cancelable mx] : (mx, mx) ~l~> (none, none) :=
283+
fun n mz vx e =>
284+
match mz with
285+
| .none => ⟨True.intro, OFE.Dist.of_eq rfl⟩
286+
| .some .none => ⟨True.intro, OFE.Dist.of_eq rfl⟩
287+
| .some (.some z) =>
288+
have : CMRA.unit ≡{n}≡ some z :=
289+
CMRA.cancelableN (validN_op_unit vx) ((CMRA.unit_right_id_dist mx).trans e)
290+
⟨True.intro, this⟩
291+
292+
end updates_option
293+
294+
end LocalUpdate

0 commit comments

Comments
 (0)