Skip to content

Commit 159e611

Browse files
lzy0505lzy0505
committed
Address comments
1 parent 11f4479 commit 159e611

File tree

2 files changed

+23
-32
lines changed

2 files changed

+23
-32
lines changed

‎src/Iris/BI/BigOp/BigAndMap.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -158,7 +158,7 @@ theorem bigAndM_lookup_dom {Φ : K → PROP} {m : M V} {i : K} {x : V}
158158
bigAndM_lookup h
159159

160160
@[rocq_alias big_andM_insert_2]
161-
theorem bigAndM_insert_2 {Φ : K → V → PROP} {m : M V} {i : K} {x : V} :
161+
theorem bigAndM_insert_elim {Φ : K → V → PROP} {m : M V} {i : K} {x : V} :
162162
Φ i x ∧ ([∧map] k ↦ v ∈ m, Φ k v) ⊢ [∧map] k ↦ v ∈ insert m i x, Φ k v :=
163163
match hm : get? m i with
164164
| none => (bigAndM_insert hm).2
@@ -219,7 +219,7 @@ theorem bigAndM_pure_elim {φ : K → V → Prop} {m : M V} :
219219

220220
@[rocq_alias big_andM_pure]
221221
theorem bigAndM_pure {φ : K → V → Prop} {m : M V} :
222-
([∧map] k ↦ x ∈ m, (⌜φ k x⌝ : PROP)) ⊣⊢ ⌜PartialMap.all φ m⌝ :=
222+
([∧map] k ↦ x ∈ m, ⌜φ k x⌝ : PROP) ⊣⊢ ⌜PartialMap.all φ m⌝ :=
223223
⟨bigAndM_pure_intro, bigAndM_pure_elim⟩
224224

225225
@[rocq_alias big_andM_later]
@@ -265,8 +265,8 @@ theorem bigAndM_filter {Φ : K → V → PROP} {m : M V} (p : K → V → Bool)
265265
[∧map] k ↦ x ∈ m, iprop(⌜p k x = true⌝ → Φ k x) :=
266266
(bigAndM_filter_cond p).trans <| bigOpM_proper fun {k x} _ => by
267267
match hp : p k x with
268-
| false => simp; exact equiv_iff.mpr ⟨imp_intro' <| pure_elim_l False.elim, true_intro⟩
269-
| true => simp; exact equiv_iff.mpr true_imp.symm
268+
| false => simpa using equiv_iff.mpr ⟨imp_intro' <| pure_elim_l False.elim, true_intro⟩
269+
| true => simpa using equiv_iff.mpr true_imp.symm
270270

271271
@[rocq_alias big_andM_union]
272272
theorem bigAndM_union [DecidableEq K] {Φ : K → V → PROP} {m₁ m₂ : M V} (hdisj : m₁ ##ₘ m₂) :

‎src/Iris/BI/BigOp/BigSepMap.lean‎

Lines changed: 19 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -235,27 +235,27 @@ theorem bigSepM_insert_acc {Φ : K → V → PROP} {m : M V} {i : K} {x : V}
235235
wand_intro <| sep_comm.1.trans bigSepM_insert_delete.2
236236

237237
@[rocq_alias big_sepM_insert_2]
238-
theorem bigSepM_insert_2 {Φ : K → V → PROP} {m : M V} {i : K} {x : V} [∀ k v, Affine (Φ k v)] :
238+
theorem bigSepM_insert_elim {Φ : K → V → PROP} {m : M V} {i : K} {x : V} [∀ k v, Affine (Φ k v)] :
239239
⊢ Φ i x -∗ ([∗map] k ↦ v ∈ m, Φ k v) -∗ [∗map] k ↦ v ∈ insert m i x, Φ k v :=
240240
entails_wand <| wand_intro <|
241241
match hm : get? m i with
242242
| none => (bigSepM_insert hm).2
243243
| some _ => (sep_mono_r ((bigSepM_delete hm).1.trans sep_elim_r)).trans bigSepM_insert_delete.2
244244

245245
@[rocq_alias big_sepM_insert_override]
246-
theorem bigSepM_insert_override {Φ : K → V → PROP} {m : M V} {i : K} {x x' : V}
246+
theorem bigSepM_insert_exist {Φ : K → V → PROP} {m : M V} {i : K} {x x' : V}
247247
(hi : get? m i = some x) (hΦ : Φ i x ≡ Φ i x') :
248248
([∗map] k ↦ v ∈ insert m i x', Φ k v) ≡ [∗map] k ↦ v ∈ m, Φ k v :=
249249
bigOpM_insert_override_equiv hi hΦ
250250

251251
@[rocq_alias big_sepM_insert_override_1]
252-
theorem bigSepM_insert_override_1 {Φ : K → V → PROP} {m : M V} {i : K} {x x' : V}
252+
theorem bigSepM_insert_exist_elim {Φ : K → V → PROP} {m : M V} {i : K} {x x' : V}
253253
(hi : get? m i = some x) (hΦ : Φ i x ⊢ Φ i x') :
254254
([∗map] k ↦ v ∈ m, Φ k v) ⊢ [∗map] k ↦ v ∈ insert m i x', Φ k v :=
255255
(bigSepM_delete hi).1.trans <| (sep_mono_l hΦ).trans bigSepM_insert_delete.2
256256

257257
@[rocq_alias big_sepM_insert_override_2]
258-
theorem bigSepM_insert_override_2 {Φ : K → V → PROP} {m : M V} {i : K} {x x' : V}
258+
theorem bigSepM_insert_exist_intro {Φ : K → V → PROP} {m : M V} {i : K} {x x' : V}
259259
(hi : get? m i = some x) (hΦ : Φ i x' ⊢ Φ i x) :
260260
([∗map] k ↦ v ∈ insert m i x', Φ k v) ⊢ [∗map] k ↦ v ∈ m, Φ k v :=
261261
bigSepM_insert_delete.1.trans <| (sep_mono_l hΦ).trans (bigSepM_delete hi).2
@@ -429,7 +429,7 @@ theorem bigSepM_union [DecidableEq K] {Φ : K → V → PROP} {m₁ m₂ : M V}
429429
equiv_iff.mp <| bigOpM_union_equiv Φ m₁ m₂ hdisj
430430

431431
@[rocq_alias big_sepM_subseteq]
432-
theorem subseteq [DecidableEq K] {Φ : K → V → PROP} {m₁ m₂ : M V}
432+
theorem bigSepM_subseteq [DecidableEq K] {Φ : K → V → PROP} {m₁ m₂ : M V}
433433
[∀ k v, Affine (Φ k v)] (h : m₂ ⊆ m₁) :
434434
([∗map] k ↦ x ∈ m₁, Φ k x) ⊢ [∗map] k ↦ x ∈ m₂, Φ k x :=
435435
(equiv_iff.mp <| bigOpM_equiv_of_perm Φ <| union_difference_cancel h).2.trans <|
@@ -446,15 +446,13 @@ theorem bigSepM_lookup_acc_impl [DecidableEq K] {Φ : K → V → PROP} {m : M V
446446
wand_intro <| sep_comm.1.trans <| (sep_mono_r <| (sep_mono_r <|
447447
bigSepM_intro (Φ := fun k v => if k = i then emp else iprop(Φ k v -∗ Ψ k v))
448448
fun {k v} hget' => ?_).trans <| (equiv_iff.mp bigSepM_sep_equiv.symm).1.trans <|
449-
bigSepM_mono fun {k v} hdel => ?_).trans <| (bigSepM_delete h).2
450-
· let hki : k ≠ i := fun heq => absurd hget' (heq ▸ (get?_delete_eq (M := M) rfl).symm ▸ nofun)
451-
simpa only [eq_false hki] using
452-
intuitionistically_elim.trans <| ((forall_elim k).trans <| forall_elim v).trans <|
453-
((and_intro (pure_intro <|
454-
(get?_delete_ne <| Ne.symm hki).symm.trans hget') .rfl).trans imp_elim_r).trans <|
455-
(and_intro (pure_intro hki) .rfl).trans imp_elim_r
456-
· let hki : k ≠ i := fun heq => absurd hdel (heq ▸ (get?_delete_eq (M := M) rfl).symm ▸ nofun)
457-
simpa only [eq_false hki] using wand_elim_r
449+
bigSepM_mono fun {k v} hget' => ?_).trans <| (bigSepM_delete h).2 <;>
450+
let hki : k ≠ i := fun heq => absurd hget' (heq ▸ (get?_delete_eq (M := M) rfl).symm ▸ nofun) <;>
451+
simp only [if_neg hki, wand_elim_r]
452+
refine
453+
intuitionistically_elim.trans <| (forall_elim k).trans <| (forall_elim v).trans <|
454+
((and_intro ?_ .rfl).trans imp_elim_r).trans <| (and_intro (pure_intro hki) .rfl).trans imp_elim_r
455+
exact pure_intro <| (get?_delete_ne <| Ne.symm hki).symm.trans hget'
458456

459457
@[rocq_alias big_sepM_sep_zip_with]
460458
theorem bigSepM_sep_zipWith {A B C : Type _}
@@ -500,11 +498,10 @@ theorem bigSepM_impl_strong [DecidableEq K]
500498
exact intuitionistically_mono <| forall_mono fun k => forall_mono fun y =>
501499
wand_mono_r <| imp_intro' <| pure_elim_l fun hget =>
502500
(and_intro (pure_intro <| heq k ▸ hget) .rfl).trans imp_elim_r
503-
exact fun k => by simp only [get?_filter]; congr 1; cases get? m₁ k <;> simp [heq k]
501+
exact fun k => by cases get? m₁ k <;> simp [get?_filter, heq k]
504502
case hemp =>
505503
exact fun m₁ => (sep_mono_r Affine.affine).trans sep_emp.1 |>.trans
506-
(equiv_iff.mp <| bigOpM_equiv_of_perm Φ fun k => by
507-
rw [get?_filter]; cases get? m₁ k with | none | some v => simp [get?_empty k]).2
504+
(equiv_iff.mp <| bigOpM_equiv_of_perm Φ fun k => by simp [get?_filter,get?_empty k]).2
508505
|>.trans sep_emp.2 |>.trans <| sep_comm.1.trans <| sep_mono_l bigSepM_empty.2
509506
case hind =>
510507
refine fun i y m₂'' hi IH m₁ => (sep_mono_r intuitionistically_sep_idem.2).trans <| sep_assoc.2.trans ?_
@@ -513,8 +510,8 @@ theorem bigSepM_impl_strong [DecidableEq K]
513510
cases hm₁i : get? m₁ i with
514511
| none =>
515512
refine (sep_mono_r <| intuitionistically_elim.trans <| (forall_elim i).trans <|
516-
(forall_elim y).trans <| by simp only [hm₁i, get?_insert_eq rfl]; exact
517-
(wand_mono_r true_imp.1).trans (emp_sep.2.trans (sep_comm.1.trans wand_elim_l))).trans ?_
513+
(forall_elim y).trans <| by simpa only [hm₁i, get?_insert_eq rfl] using
514+
(wand_mono_r true_imp.1).trans (emp_sep.2.trans (sep_comm.1.trans wand_elim_l))).trans ?_
518515
refine (sep_mono_l <| sep_mono_r <| intuitionistically_mono <| forall_mono fun k =>
519516
forall_mono fun y' => wand_mono_r <| imp_intro' <| pure_elim_l fun hget =>
520517
(and_intro (pure_intro <| (get?_insert_ne (hne_of_get hget).symm).trans hget)
@@ -523,11 +520,7 @@ theorem bigSepM_impl_strong [DecidableEq K]
523520
(sep_mono_r sep_comm.1).trans <| sep_assoc.2.trans <|
524521
(sep_mono_l <| sep_comm.1.trans (bigSepM_insert hi).2).trans ?_
525522
refine sep_mono_r (equiv_iff.mp <| bigOpM_equiv_of_perm Φ fun k => ?_).2
526-
simp [get?_filter]; cases hk : get? m₁ k with
527-
| none => simp
528-
| some v =>
529-
have hne : i ≠ k := fun h => absurd (h ▸ hk) (hm₁i.symm ▸ nofun)
530-
simp [Option.bind_some, get?_insert_ne hne]
523+
by_cases heq : i = k <;> simp_all [get?_filter, get?_insert]
531524
| some x =>
532525
refine (sep_mono_l <| sep_mono_l (bigSepM_delete hm₁i).1).trans <|
533526
(sep_mono_l sep_assoc.1).trans <| sep_assoc.1.trans <|
@@ -536,7 +529,7 @@ theorem bigSepM_impl_strong [DecidableEq K]
536529
refine (sep_mono_l <| (sep_mono_r intuitionistically_elim).trans <|
537530
(sep_mono_r <| (forall_elim i).trans <| forall_elim y).trans <| by
538531
simpa [hm₁i, get?_insert_eq rfl] using
539-
(sep_mono_r <| wand_mono_r true_imp.1).trans wand_elim_r).trans ?_
532+
(sep_mono_r <| wand_mono_r true_imp.1).trans wand_elim_r).trans ?_
540533
refine (sep_mono_r <| sep_mono_r <| intuitionistically_mono <| forall_mono fun k =>
541534
forall_mono fun y' => wand_intro <| imp_intro' <| pure_elim_l fun hget => by
542535
let hne : i ≠ k := (hne_of_get hget).symm
@@ -547,9 +540,7 @@ theorem bigSepM_impl_strong [DecidableEq K]
547540
(sep_mono_r <| IH (delete m₁ i)).trans ?_
548541
refine (sep_mono_r <| sep_mono_r (equiv_iff.mp <| bigOpM_equiv_of_perm Φ fun k => ?_).2).trans <|
549542
sep_assoc.2.trans <| sep_mono_l (bigSepM_insert hi).2
550-
simp [get?_filter]; by_cases hki : k = i
551-
· simp [hki, get?_insert_eq rfl, get?_delete_eq rfl]
552-
· simp [get?_insert_ne (Ne.symm hki), get?_delete_ne (Ne.symm hki)]
543+
by_cases hki : i = k <;> simp_all [get?_filter, get?_insert, get?_delete]
553544

554545
-- TODO: `big_sepM_kmap` and `big_sepM_map_seq` require map operations
555546
-- which are not yet available in `PartialMap`.

0 commit comments

Comments
 (0)