Skip to content

Commit 06219a2

Browse files
HaleOICHaleOIC
committed
feat: clean up
1 parent cdd8b85 commit 06219a2

File tree

11 files changed

+717
-321
lines changed

11 files changed

+717
-321
lines changed

‎PORTING.md‎

Lines changed: 11 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -237,8 +237,11 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
237237
- [ ] `sbi_unfold.v`
238238
- [ ] `telescopes.v`
239239
- [ ] `updates.v`
240-
- [x] FUpd class
241-
- [ ] Big op lemmas
240+
- [x] Bupd laws
241+
- [x] Fupd basic laws
242+
- [ ] Fupd mask change laws
243+
- [ ] Fupd step derived rules
244+
- [ ] Fupd plainly general laws
242245
- [ ] `weakestpre.v`
243246
- [ ] `lib/atomic.v`
244247
- [ ] `lib/core.v`
@@ -261,6 +264,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
261264
- [ ] instances for big ops
262265
- [ ] MaybeCombineSepAs instances
263266
- [ ] CombineSepGives instances
267+
- [x] FromModal instances
264268
- [x] ElimModal instances
265269
- [ ] AddModal instances
266270
- [ ] ElimInv instances
@@ -294,11 +298,11 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
294298
- [ ] IntoLaterN
295299
- [ ] `class_instances_updates.v` (InstancesUpdates.lean)
296300
- [x] Basic instances for bupd
297-
- [ ] Basic instances for fupd
301+
- [x] Basic instances for fupd
298302
- [x] FromModal bupd
299-
- [ ] FromModal fupd
303+
- [x] FromModal fupd
300304
- [x] ElimModal bupd
301-
- [ ] ElimModal fupd
305+
- [x] ElimModal fupd
302306
- [ ] AddModal bupd
303307
- [ ] AddModal fupd
304308
- [ ] ElimAcc bupd
@@ -434,6 +438,8 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
434438
- [ ] IClearFrame
435439
- [ ] `modalities.v`
436440
- [ ] `modality_instances.v`
441+
- [ ] modality_embed
442+
- [x] others
437443
- [ ] `monpred.v`
438444
- [x] `proofmode.v` (ProofMode.lean)
439445
- [-] `reduction.v` (not necessary in Lean)

‎src/Iris/BI/Updates.lean‎

Lines changed: 143 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
/-
22
Copyright (c) 2025 Markus de Medeiros, Remy Seassau. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
4-
Authors: Markus de Medeiros, Remy Seassau
4+
Authors: Markus de Medeiros, Remy Seassau, Yunsong Yang
55
-/
66
module
77

@@ -38,29 +38,46 @@ class FUpd (PROP : Type _) where
3838
fupd : CoPset → CoPset → PROP → PROP
3939
export FUpd (fupd)
4040

41-
syntax "|={ " term " , " term " }=> " term : term
42-
syntax term "={ " term " , " term " }=∗ " term : term
43-
syntax "|={ " term " }=> " term : term
44-
syntax term "={ " term " }=∗ " term : term
41+
syntax "|={" term "," term "}=> " term : term
42+
syntax term "={" term "," term "}=∗ " term : term
43+
syntax "|={" term "}=> " term : term
44+
syntax term "={" term "}=∗ " term : term
4545

4646
macro_rules
47-
| `(iprop(|={ $E1 , $E2 }=> $P)) => ``(FUpd.fupd $E1 $E2 iprop($P))
48-
| `(iprop($P ={ $E1 , $E2 }=∗ $Q)) => ``(BIBase.wand iprop($P) (FUpd.fupd $E1 $E2 iprop($Q)))
49-
| `(iprop(|={ $E1 }=> $P)) => ``(FUpd.fupd $E1 $E1 iprop($P))
50-
| `(iprop($P ={ $E1 }=∗ $Q)) => ``(BIBase.wand iprop($P) (FUpd.fupd $E1 $E1 iprop($Q)))
47+
| `(iprop(|={$E1,$E2}=> $P)) => ``(FUpd.fupd $E1 $E2 iprop($P))
48+
| `(iprop($P ={$E1,$E2}=∗ $Q)) => ``(BIBase.wand iprop($P) (FUpd.fupd $E1 $E2 iprop($Q)))
49+
| `(iprop(|={$E1}=> $P)) => ``(FUpd.fupd $E1 $E1 iprop($P))
50+
| `(iprop($P ={$E1}=∗ $Q)) => ``(BIBase.wand iprop($P) (FUpd.fupd $E1 $E1 iprop($Q)))
51+
52+
delab_rule FUpd.fupd
53+
| `($_ $E1 $E2 $P) => do
54+
let P ← Iris.BI.unpackIprop P
55+
if E1 == E2 then ``(iprop(|={$E1}=> $P))
56+
else ``(iprop(|={$E1,$E2}=> $P))
57+
58+
syntax "|={" term "}[" term "]▷=> " term : term
59+
syntax term "={" term "}[" term "]▷=∗ " term : term
60+
syntax "|={" term "}▷=> " term : term
61+
syntax term "={" term "}▷=∗ " term : term
62+
63+
macro_rules
64+
| `(iprop(|={$E1}[$E2]▷=> $P)) => ``(iprop(|={$E1,$E2}=> ▷ (|={$E2,$E1}=> iprop($P))))
65+
| `(iprop($P ={$E1}[$E2]▷=∗ $Q)) => ``(iprop(iprop($P) -∗ |={$E1}[$E2]▷=> iprop($Q)))
66+
| `(iprop(|={$E1}▷=> $P)) => ``(iprop(|={$E1}[$E1]▷=> iprop($P)))
67+
| `(iprop($P ={$E1}▷=∗ $Q)) => ``(iprop(iprop($P) ={$E1}[$E1]▷=∗ iprop($Q)))
5168

5269
-- Delab rules
5370

54-
syntax "|={ " term " }[ " term " ]▷=> " term : term
55-
syntax term "={ " term " }[ " term " ]▷=∗ " term : term
56-
syntax "|={ " term " }▷=> " term : term
57-
syntax term "={ " term " }▷=∗ " term : term
71+
syntax "|={" term "}[" term "]▷^" term "=> " term : term
72+
syntax term "={" term "}[" term "]▷^" term "=∗ " term : term
73+
syntax "|={" term "}▷^" term "=> " term : term
74+
syntax term "={" term "}▷^" term "=∗ " term : term
5875

5976
macro_rules
60-
| `(iprop(|={ $E1 }[ $E2 ]▷=> $P)) => ``(iprop(|={$E1, $E2}=> ▷ (|={ $E2, $E1 }=> iprop($P))))
61-
| `(iprop($P ={ $E1 }[ $E2 ]▷=∗ $Q)) => ``(iprop(iprop($P) -∗ |={$E1}[$E2]▷=> iprop($Q)))
62-
| `(iprop(|={ $E1 }▷=> $P)) => ``(iprop(|={$E1}[$E1]▷=> iprop($P)))
63-
| `(iprop($P ={ $E1 }▷=∗ $Q)) => ``(iprop(iprop($P) ={$E1}[$E1]▷=∗ iprop($Q)))
77+
| `(iprop(|={$E1}[$E2]▷^$n=> $P)) => ``(iprop(|={$E1,$E2}=> ▷^[$n] (|={$E2,$E1}=> iprop($P))))
78+
| `(iprop($P ={$E1}[$E2]▷^$n=∗ $Q)) => ``(iprop(iprop($P) -∗ |={$E1}[$E2]▷^$n=> iprop($Q)))
79+
| `(iprop(|={$E1}▷^$n=> $P)) => ``(iprop(|={$E1}[$E1]▷^$n=> iprop($P)))
80+
| `(iprop($P ={$E1}▷^$n=∗ $Q)) => ``(iprop(iprop($P) ={$E1}[$E1]▷^$n=∗ iprop($Q)))
6481

6582
-- Delab rules
6683

@@ -79,26 +96,26 @@ macro_rules
7996

8097
class BIUpdate (PROP : Type _) [BI PROP] extends BUpd PROP where
8198
[bupd_ne : OFE.NonExpansive (BUpd.bupd (PROP := PROP))]
82-
intro {P : PROP} : iprop(P ⊢ |==> P)
83-
mono {P Q : PROP} : iprop(P ⊢ Q) → iprop(|==> P ⊢ |==> Q)
84-
trans {P : PROP} : iprop(|==> |==> P ⊢ |==> P)
85-
frame_r {P R : PROP} : iprop((|==> P) ∗ R ⊢ |==> (P ∗ R))
99+
intro {P : PROP} : P ⊢ |==> P
100+
mono {P Q : PROP} : (P ⊢ Q) → |==> P ⊢ |==> Q
101+
trans {P : PROP} : |==> |==> P ⊢ |==> P
102+
frame_r {P R : PROP} : (|==> P) ∗ R ⊢ |==> (P ∗ R)
86103

87104
class BIFUpdate (PROP : Type _) [BI PROP] extends FUpd PROP where
88105
[ne {E1 E2 : CoPset} : OFE.NonExpansive (FUpd.fupd E1 E2 (PROP := PROP))]
89-
subset {E1 E2 : CoPset} : Subset E2 E1 → ⊢ |={E1, E2}=> |={E2, E1}=> (emp : PROP)
90-
except0 {E1 E2 : CoPset} (P : PROP) : (◇ |={E1, E2}=> P) ⊢ |={E1, E2}=> P
91-
trans {E1 E2 E3 : CoPset} (P : PROP) : (|={E1, E2}=> |={E2, E3}=> P) ⊢ |={E1, E3}=> P
92-
mask_frame_r' {E1 E2 Ef : CoPset} (P : PROP) :
93-
E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ⊢ |={CoPset.union E1 Ef, CoPset.union E2 Ef}=> P
94-
frame_r {E1 E2 : CoPset} (P R : PROP) :
95-
iprop((|={E1, E2}=> P) ∗ R ⊢ |={E1, E2}=> P ∗ R)
106+
subset {E1 E2 : CoPset} : E2 ⊆ E1 → ⊢ |={E1,E2}=> |={E2,E1}=> (emp : PROP)
107+
except0 {E1 E2 : CoPset} {P : PROP} : (◇ |={E1,E2}=> P) ⊢ |={E1,E2}=> P
108+
mono {E1 E2 : CoPset} {P Q : PROP} : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q
109+
trans {E1 E2 E3 : CoPset} {P : PROP} : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P
110+
mask_frame_r' {E1 E2 Ef : CoPset} {P : PROP} :
111+
E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}=> P
112+
frame_r {E1 E2 : CoPset} {P R : PROP} : (|={E1,E2}=> P) ∗ R ⊢ |={E1,E2}=> P ∗ R
96113

97114
class BIUpdateFUpdate (PROP : Type _) [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] where
98-
fupd_of_bupd {P : PROP} {E : CoPset} : iprop(⊢ |==> P) → iprop(⊢ |={E}=> P)
115+
fupd_of_bupd {P : PROP} {E : CoPset} : (|==> P) ⊢ |={E}=> P
99116

100117
class BIBUpdatePlainly (PROP : Type _) [BI PROP] [BIUpdate PROP] [Sbi PROP] where
101-
bupd_plainly {P : PROP} : iprop((|==> ■ P)) ⊢ P
118+
bupd_plainly {P : PROP} : (|==> ■ P) ⊢ P
102119

103120
class BIFUpdatePlainly (PROP : Type _) [BI PROP] [BIFUpdate PROP] [Sbi PROP] where
104121
fupd_plainly_keep_l (E E' : CoPset) (P R : PROP) : (R ={E,E'}=∗ ■ P) ∗ R ⊢ |={E}=> P ∗ R
@@ -112,38 +129,38 @@ variable [BI PROP] [BIUpdate PROP]
112129

113130
open BIUpdate
114131

115-
theorem bupd_frame_l {P Q : PROP} : iprop(P ∗ |==> Q ⊢ |==> (P ∗ Q)) :=
132+
theorem bupd_frame_l {P Q : PROP} : P ∗ |==> Q ⊢ |==> (P ∗ Q) :=
116133
sep_symm.trans <| frame_r.trans <| mono sep_symm
117134

118-
theorem bupd_frame_r {P Q : PROP} : iprop(|==> P ∗ Q ⊢ |==> (P ∗ Q)) :=
135+
theorem bupd_frame_r {P Q : PROP} : |==> P ∗ Q ⊢ |==> (P ∗ Q) :=
119136
frame_r
120137

121-
theorem bupd_wand_l {P Q : PROP} : iprop((P -∗ Q) ∗ (|==> P) ⊢ |==> Q) :=
138+
theorem bupd_wand_l {P Q : PROP} : (P -∗ Q) ∗ (|==> P) ⊢ |==> Q :=
122139
bupd_frame_l.trans <| mono <| wand_elim .rfl
123140

124-
theorem bupd_wand_r {P Q : PROP} : iprop((|==> P) ∗ (P -∗ Q) ⊢ |==> Q) :=
141+
theorem bupd_wand_r {P Q : PROP} : (|==> P) ∗ (P -∗ Q) ⊢ |==> Q :=
125142
sep_symm.trans bupd_wand_l
126143

127-
theorem bupd_sep {P Q : PROP} : iprop((|==> P) ∗ (|==> Q) ⊢ |==> (P ∗ Q)) :=
144+
theorem bupd_sep {P Q : PROP} : (|==> P) ∗ (|==> Q) ⊢ |==> (P ∗ Q) :=
128145
bupd_frame_l.trans <| (mono <| frame_r).trans BIUpdate.trans
129146

130-
theorem bupd_idem {P : PROP} : iprop((|==> |==> P) ⊣⊢ |==> P) :=
147+
theorem bupd_idem {P : PROP} : (|==> |==> P) ⊣⊢ |==> P :=
131148
⟨BIUpdate.trans, BIUpdate.intro⟩
132149

133-
theorem bupd_or {P Q: PROP} : iprop((|==> P) ∨ (|==> Q) ⊢ |==> (P ∨ Q)) :=
150+
theorem bupd_or {P Q: PROP} : (|==> P) ∨ (|==> Q) ⊢ |==> (P ∨ Q) :=
134151
or_elim (mono or_intro_l) (mono or_intro_r)
135152

136-
theorem bupd_and {P Q : PROP} : iprop((|==> (P ∧ Q)) ⊢ (|==> P) ∧ (|==> Q)) :=
153+
theorem bupd_and {P Q : PROP} : (|==> (P ∧ Q)) ⊢ (|==> P) ∧ (|==> Q) :=
137154
and_intro (mono and_elim_l) (mono and_elim_r)
138155

139156
theorem bupd_exist {Φ : A → PROP} : (∃ x : A, |==> Φ x) ⊢ |==> ∃ x : A, Φ x :=
140157
exists_elim (mono <| exists_intro ·)
141158

142159
theorem bupd_forall {Φ : A → PROP} :
143-
iprop(|==> «forall» fun x : A => Φ x) ⊢ «forall» fun x : A => iprop(|==> Φ x) :=
160+
(|==> «forall» fun x : A => Φ x) ⊢ «forall» fun x : A => iprop(|==> Φ x) :=
144161
forall_intro (mono <| forall_elim ·)
145162

146-
theorem bupd_except0 {P : PROP} : iprop(◇ (|==> P) ⊢ (|==> ◇ P)) :=
163+
theorem bupd_except0 {P : PROP} : ◇ (|==> P) ⊢ (|==> ◇ P) :=
147164
or_elim (or_intro_l.trans intro) (mono or_intro_r)
148165

149166
instance {P : PROP} [Absorbing P] : Absorbing iprop(|==> P) :=
@@ -170,3 +187,89 @@ instance {P : PROP} [Plain P] : Plain iprop(|==> P) :=
170187
⟨(mono Plain.plain).trans <| (bupd_elim).trans <| plainly_mono intro⟩
171188

172189
end BUpdPlainlyLaws
190+
191+
section FUpdLaws
192+
193+
variable [BI PROP] [BIFUpdate PROP]
194+
195+
open BIFUpdate
196+
197+
theorem fupd_mask_intro_subseteq {E1 E2 : CoPset} {P : PROP} : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P :=
198+
λ h => (emp_sep.2.trans <| sep_mono_l <| subset h).trans <|
199+
frame_r.trans <| mono <| frame_r.trans <| mono emp_sep.1
200+
201+
theorem fupd_intro {E : CoPset} {P : PROP} : P ⊢ |={E}=> P :=
202+
(fupd_mask_intro_subseteq λ _ => id).trans trans
203+
204+
-- Introduction lemma for a mask-chaging fupd
205+
theorem fupd_mask_intro {E1 E2 : CoPset} {P : PROP} :
206+
E2 ⊆ E1 → ((|={E2,E1}=> emp) -∗ P) ⊢ |={E1,E2}=> P :=
207+
λ h => (wand_mono_r fupd_intro).trans <|
208+
(emp_sep.2.trans <| sep_mono_l <| subset h).trans <|
209+
frame_r.trans <| (mono wand_elim_r).trans trans
210+
211+
theorem fupd_mask_intro_discard {E1 E2 : CoPset} {P : PROP} [Absorbing P] : E2 ⊆ E1 → P ⊢ |={E1,E2}=> P :=
212+
λ h => (wand_intro' sep_elim_r).trans <| fupd_mask_intro h
213+
214+
theorem fupd_elim {E1 E2 E3 : CoPset} {P Q : PROP} : (Q ⊢ |={E2,E3}=> P) → (|={E1,E2}=> Q) ⊢ |={E1,E3}=> P :=
215+
λ h => (mono h).trans trans
216+
217+
theorem fupd_frame_l {E1 E2 : CoPset} {P Q : PROP} : P ∗ (|={E1,E2}=> Q) ⊢ |={E1,E2}=> P ∗ Q :=
218+
sep_symm.trans <| frame_r.trans <| mono sep_symm
219+
220+
theorem fupd_frame_r {E1 E2 : CoPset} {P Q : PROP} : (|={E1,E2}=> P) ∗ Q ⊢ |={E1,E2}=> P ∗ Q :=
221+
frame_r
222+
223+
theorem fupd_wand_l {E1 E2 : CoPset} {P Q : PROP} : (P -∗ Q) ∗ (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q :=
224+
fupd_frame_l.trans <| mono <| wand_elim .rfl
225+
226+
theorem fupd_wand_r {E1 E2 : CoPset} {P Q : PROP} : (|={E1,E2}=> P) ∗ (P -∗ Q) ⊢ |={E1,E2}=> Q :=
227+
sep_symm.trans fupd_wand_l
228+
229+
theorem fupd_sep {E : CoPset} {P Q : PROP} : (|={E}=> P) ∗ (|={E}=> Q) ⊢ |={E}=> P ∗ Q :=
230+
fupd_frame_l.trans <| (mono frame_r).trans trans
231+
232+
theorem fupd_idem {E : CoPset} {P : PROP} : (|={E}=> |={E}=> P) ⊣⊢ |={E}=> P := ⟨trans, fupd_intro⟩
233+
234+
theorem fupd_or {E1 E2 : CoPset} {P Q : PROP} : (|={E1,E2}=> P) ∨ (|={E1,E2}=> Q) ⊢ |={E1,E2}=> P ∨ Q :=
235+
or_elim (mono or_intro_l) (mono or_intro_r)
236+
237+
theorem fupd_and {E1 E2 : CoPset} {P Q : PROP} : (|={E1,E2}=> P ∧ Q) ⊢ (|={E1,E2}=> P) ∧ (|={E1,E2}=> Q) :=
238+
and_intro (mono and_elim_l) (mono and_elim_r)
239+
240+
theorem fupd_exist {E1 E2 : CoPset} {Φ : A → PROP} : (∃ a : A, |={E1,E2}=> Φ a) ⊢ |={E1,E2}=> ∃ a : A, Φ a :=
241+
exists_elim (mono <| exists_intro ·)
242+
243+
theorem fupd_forall {E1 E2 : CoPset} {Φ : A → PROP} :
244+
(|={E1,E2}=> «forall» λ a : A => Φ a) ⊢ «forall» λ a : A => iprop(|={E1,E2}=> Φ a) :=
245+
forall_intro (mono <| forall_elim ·)
246+
247+
theorem fupd_except0 {E1 E2 : CoPset} {P : PROP} : (◇ |={E1,E2}=> P) ⊢ |={E1,E2}=> ◇ P :=
248+
except0.trans (mono except0_intro)
249+
250+
instance {E1 E2 : CoPset} {P : PROP} [Absorbing P] : Absorbing iprop(|={E1,E2}=> P) :=
251+
⟨fupd_frame_l.trans <| mono sep_elim_r⟩
252+
253+
theorem fupd_mask_frame_r {E1 E2 Ef : CoPset} {P : PROP} :
254+
E1 ## Ef → (|={E1,E2}=> P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}=> P :=
255+
λ h => (mono <| imp_intro' and_elim_r).trans <| mask_frame_r' h
256+
257+
-- TODO: the following theorems can be proved only with CoPSet extensional-equality
258+
-- theorem fupd_mask_frame {E E' E1 E2 : CoPset} {P : PROP} :
259+
-- E1 ⊆ E → (|={E1,E2}=> |={E2 ∪ (E \ E1),E'}=> P) ⊢ |={E,E'}=> P := sorry
260+
261+
-- theorem fupd_mask_frame_acc {E E' E1 E2 : CoPset} {P Q : PROP}:
262+
-- E1 ⊆ E →
263+
-- (|={E1,E1 \ E2}=> Q) ⊢
264+
-- (Q -∗ |={E \ E2,E'}=> (∀ R, (|={E1 \ E2,E1}=> R) -∗ |={E \ E2,E}=> R) -∗ P) -∗
265+
-- (|={E,E'}=> P) := sorry
266+
267+
-- theorem fupd_mask_mono {E1 E2 : CoPset} {P : PROP} :
268+
-- E1 ⊆ E2 → (|={E1}=> P) ⊢ |={E2}=> P := sorry
269+
270+
-- theorem fupd_mask_subseteq_emptyset_difference {E1 E2 : CoPset} :
271+
-- E2 ⊆ E1 → ⊢ |={E1,E2}=> |={∅,E1\E2}=> (emp: PROP) := sorry
272+
273+
-- theorem fupd_trans_frame {E1 E2 E3 : CoPset} {P Q : PROP} : ((Q ={E2,E3}=∗ emp) ∗ |={E1,E2}=> (Q ∗ P)) ⊢ |={E1,E3}=> P := sorry
274+
275+
end FUpdLaws

‎src/Iris/Examples/Proofs.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ open Iris.BI
1616
theorem proof_example_1 [BI PROP] (P Q R : PROP) (Φ : α → PROP) :
1717
P ∗ Q ∗ □ R ⊢ □ (R -∗ ∃ x, Φ x) -∗ ∃ x, Φ x ∗ P ∗ Q
1818
:= by
19-
iintro ⟨HP, HQ, □HR⟩ □HRΦ
19+
iintro ⟨HP, HQ, #HR⟩ #HRΦ
2020
ihave HΦ := HRΦ $$ HR
2121
icases HΦ with ⟨%x, _HΦ⟩
2222
iexists x

0 commit comments

Comments
 (0)