Commit e1ef66ef by Robbert Krebbers

Some box/slice renaming.

parent 6923de66
Pipeline #3127 passed with stage
in 10 minutes and 29 seconds
 ... @@ -89,7 +89,7 @@ Proof. ... @@ -89,7 +89,7 @@ Proof. - by rewrite big_sepM_empty. - by rewrite big_sepM_empty. Qed. Qed. Lemma box_insert_empty Q E f P : Lemma slice_insert_empty Q E f P : ▷ box N f P ={E}=∗ ∃ γ, ⌜f !! γ = None⌝ ∗ ▷ box N f P ={E}=∗ ∃ γ, ⌜f !! γ = None⌝ ∗ slice N γ Q ∗ ▷ box N (<[γ:=false]> f) (Q ∗ P). slice N γ Q ∗ ▷ box N (<[γ:=false]> f) (Q ∗ P). Proof. Proof. ... @@ -108,7 +108,7 @@ Proof. ... @@ -108,7 +108,7 @@ Proof. iFrame; eauto. iFrame; eauto. Qed. Qed. Lemma box_delete_empty E f P Q γ : Lemma slice_delete_empty E f P Q γ : ↑N ⊆ E → ↑N ⊆ E → f !! γ = Some false → f !! γ = Some false → slice N γ Q -∗ ▷ box N f P ={E}=∗ ∃ P', slice N γ Q -∗ ▷ box N f P ={E}=∗ ∃ P', ... @@ -128,7 +128,7 @@ Proof. ... @@ -128,7 +128,7 @@ Proof. - iExists Φ; eauto. - iExists Φ; eauto. Qed. Qed. Lemma box_fill E f γ P Q : Lemma slice_fill E f γ P Q : ↑N ⊆ E → ↑N ⊆ E → f !! γ = Some false → f !! γ = Some false → slice N γ Q -∗ ▷ Q -∗ ▷ box N f P ={E}=∗ ▷ box N (<[γ:=true]> f) P. slice N γ Q -∗ ▷ Q -∗ ▷ box N f P ={E}=∗ ▷ box N (<[γ:=true]> f) P. ... @@ -147,7 +147,7 @@ Proof. ... @@ -147,7 +147,7 @@ Proof. iFrame; eauto. iFrame; eauto. Qed. Qed. Lemma box_empty E f P Q γ : Lemma slice_empty E f P Q γ : ↑N ⊆ E → ↑N ⊆ E → f !! γ = Some true → f !! γ = Some true → slice N γ Q -∗ ▷ box N f P ={E}=∗ ▷ Q ∗ ▷ box N (<[γ:=false]> f) P. slice N γ Q -∗ ▷ box N f P ={E}=∗ ▷ Q ∗ ▷ box N (<[γ:=false]> f) P. ... @@ -167,31 +167,31 @@ Proof. ... @@ -167,31 +167,31 @@ Proof. iFrame; eauto. iFrame; eauto. Qed. Qed. Lemma box_insert_full Q E f P : Lemma slice_insert_full Q E f P : ↑N ⊆ E → ↑N ⊆ E → ▷ Q -∗ ▷ box N f P ={E}=∗ ∃ γ, ⌜f !! γ = None⌝ ∗ ▷ Q -∗ ▷ box N f P ={E}=∗ ∃ γ, ⌜f !! γ = None⌝ ∗ slice N γ Q ∗ ▷ box N (<[γ:=true]> f) (Q ∗ P). slice N γ Q ∗ ▷ box N (<[γ:=true]> f) (Q ∗ P). Proof. Proof. iIntros (?) "HQ Hbox". iIntros (?) "HQ Hbox". iMod (box_insert_empty with "Hbox") as (γ) "(% & #Hslice & Hbox)". iMod (slice_insert_empty with "Hbox") as (γ) "(% & #Hslice & Hbox)". iExists γ. iFrame "%#". iMod (box_fill with "Hslice HQ Hbox"); first done. iExists γ. iFrame "%#". iMod (slice_fill with "Hslice HQ Hbox"); first done. by apply lookup_insert. by rewrite insert_insert. by apply lookup_insert. by rewrite insert_insert. Qed. Qed. Lemma box_delete_full E f P Q γ : Lemma slice_delete_full E f P Q γ : ↑N ⊆ E → ↑N ⊆ E → f !! γ = Some true → f !! γ = Some true → slice N γ Q -∗ ▷ box N f P ={E}=∗ slice N γ Q -∗ ▷ box N f P ={E}=∗ ∃ P', ▷ Q ∗ ▷ ▷ (P ≡ (Q ∗ P')) ∗ ▷ box N (delete γ f) P'. ∃ P', ▷ Q ∗ ▷ ▷ (P ≡ (Q ∗ P')) ∗ ▷ box N (delete γ f) P'. Proof. Proof. iIntros (??) "#Hslice Hbox". iIntros (??) "#Hslice Hbox". iMod (box_empty with "Hslice Hbox") as "[\$ Hbox]"; try done. iMod (slice_empty with "Hslice Hbox") as "[\$ Hbox]"; try done. iMod (box_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]". iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; first done. done. by apply lookup_insert. { by apply lookup_insert. } iExists P'. iFrame. rewrite -insert_delete delete_insert ?lookup_delete //. iExists P'. iFrame. rewrite -insert_delete delete_insert ?lookup_delete //. Qed. Qed. Lemma box_fill_all E f P : Lemma box_fill E f P : ↑N ⊆ E → ↑N ⊆ E → box N f P -∗ ▷ P ={E}=∗ box N (const true <\$> f) P. box N f P -∗ ▷ P ={E}=∗ box N (const true <\$> f) P. Proof. Proof. ... @@ -208,7 +208,7 @@ Proof. ... @@ -208,7 +208,7 @@ Proof. iApply "Hclose". iNext; iExists true. by iFrame. iApply "Hclose". iNext; iExists true. by iFrame. Qed. Qed. Lemma box_empty_all E f P : Lemma box_empty E f P : ↑N ⊆ E → ↑N ⊆ E → map_Forall (λ _, (true =)) f → map_Forall (λ _, (true =)) f → box N f P ={E}=∗ ▷ P ∗ box N (const false <\$> f) P. box N f P ={E}=∗ ▷ P ∗ box N (const false <\$> f) P. ... @@ -230,50 +230,50 @@ Proof. ... @@ -230,50 +230,50 @@ Proof. - iExists Φ; iSplit; by rewrite big_sepM_fmap. - iExists Φ; iSplit; by rewrite big_sepM_fmap. Qed. Qed. Lemma box_split E f P Q1 Q2 γ b : Lemma slice_split E f P Q1 Q2 γ b : ↑N ⊆ E → f !! γ = Some b → ↑N ⊆ E → f !! γ = Some b → slice N γ (Q1 ∗ Q2) -∗ ▷ box N f P ={E}=∗ ∃ γ1 γ2, slice N γ (Q1 ∗ Q2) -∗ ▷ box N f P ={E}=∗ ∃ γ1 γ2, ⌜delete γ f !! γ1 = None⌝ ∗ ⌜delete γ f !! γ2 = None⌝ ∗ ⌜γ1 ≠ γ2⌝ ∗ ⌜delete γ f !! γ1 = None⌝ ∗ ⌜delete γ f !! γ2 = None⌝ ∗ ⌜γ1 ≠ γ2⌝ ∗ slice N γ1 Q1 ∗ slice N γ2 Q2 ∗ ▷ box N (<[γ2 := b]>(<[γ1 := b]>(delete γ f))) P. slice N γ1 Q1 ∗ slice N γ2 Q2 ∗ ▷ box N (<[γ2 := b]>(<[γ1 := b]>(delete γ f))) P. Proof. Proof. iIntros (??) "#Hslice Hbox". destruct b. iIntros (??) "#Hslice Hbox". destruct b. - iMod (box_delete_full with "Hslice Hbox") as (P') "([HQ1 HQ2] & Heq & Hbox)"; try done. - iMod (slice_delete_full with "Hslice Hbox") as (P') "([HQ1 HQ2] & Heq & Hbox)"; try done. iMod (box_insert_full Q1 with "HQ1 Hbox") as (γ1) "(% & #Hslice1 & Hbox)". done. iMod (slice_insert_full Q1 with "HQ1 Hbox") as (γ1) "(% & #Hslice1 & Hbox)"; first done. iMod (box_insert_full Q2 with "HQ2 Hbox") as (γ2) "(% & #Hslice2 & Hbox)". done. iMod (slice_insert_full Q2 with "HQ2 Hbox") as (γ2) "(% & #Hslice2 & Hbox)"; first done. iExists γ1, γ2. iFrame "%#". iModIntro. iSplit; last iSplit; try iPureIntro. iExists γ1, γ2. iFrame "%#". iModIntro. iSplit; last iSplit; try iPureIntro. { by eapply lookup_insert_None. } { by eapply lookup_insert_None. } { by apply (lookup_insert_None (delete γ f) γ1 γ2 true). } { by apply (lookup_insert_None (delete γ f) γ1 γ2 true). } iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto]. iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto]. iNext. iRewrite "Heq". iPureIntro. rewrite assoc. f_equiv. by rewrite comm. done. iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2). - iMod (box_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done. - iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done. iMod (box_insert_empty Q1 with "Hbox") as (γ1) "(% & #Hslice1 & Hbox)". iMod (slice_insert_empty Q1 with "Hbox") as (γ1) "(% & #Hslice1 & Hbox)". iMod (box_insert_empty Q2 with "Hbox") as (γ2) "(% & #Hslice2 & Hbox)". iMod (slice_insert_empty Q2 with "Hbox") as (γ2) "(% & #Hslice2 & Hbox)". iExists γ1, γ2. iFrame "%#". iModIntro. iSplit; last iSplit; try iPureIntro. iExists γ1, γ2. iFrame "%#". iModIntro. iSplit; last iSplit; try iPureIntro. { by eapply lookup_insert_None. } { by eapply lookup_insert_None. } { by apply (lookup_insert_None (delete γ f) γ1 γ2 false). } { by apply (lookup_insert_None (delete γ f) γ1 γ2 false). } iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto]. iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto]. iNext. iRewrite "Heq". iPureIntro. rewrite assoc. f_equiv. by rewrite comm. done. iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2). Qed. Qed. Lemma box_combine E f P Q1 Q2 γ1 γ2 b : Lemma slice_combine E f P Q1 Q2 γ1 γ2 b : ↑N ⊆ E → γ1 ≠ γ2 → f !! γ1 = Some b → f !! γ2 = Some b → ↑N ⊆ E → γ1 ≠ γ2 → f !! γ1 = Some b → f !! γ2 = Some b → slice N γ1 Q1 -∗ slice N γ2 Q2 -∗ ▷ box N f P ={E}=∗ ∃ γ, slice N γ1 Q1 -∗ slice N γ2 Q2 -∗ ▷ box N f P ={E}=∗ ∃ γ, ⌜delete γ2 (delete γ1 f) !! γ = None⌝ ∗ slice N γ (Q1 ∗ Q2) ∗ ⌜delete γ2 (delete γ1 f) !! γ = None⌝ ∗ slice N γ (Q1 ∗ Q2) ∗ ▷ box N (<[γ := b]>(delete γ2 (delete γ1 f))) P. ▷ box N (<[γ := b]>(delete γ2 (delete γ1 f))) P. Proof. Proof. iIntros (????) "#Hslice1 #Hslice2 Hbox". destruct b. iIntros (????) "#Hslice1 #Hslice2 Hbox". destruct b. - iMod (box_delete_full with "Hslice1 Hbox") as (P1) "(HQ1 & Heq1 & Hbox)"; try done. - iMod (slice_delete_full with "Hslice1 Hbox") as (P1) "(HQ1 & Heq1 & Hbox)"; try done. iMod (box_delete_full with "Hslice2 Hbox") as (P2) "(HQ2 & Heq2 & Hbox)". iMod (slice_delete_full with "Hslice2 Hbox") as (P2) "(HQ2 & Heq2 & Hbox)"; first done. done. by simplify_map_eq. { by simplify_map_eq. } iMod (box_insert_full (Q1 ∗ Q2)%I with "[\$HQ1 \$HQ2] Hbox") iMod (slice_insert_full (Q1 ∗ Q2)%I with "[\$HQ1 \$HQ2] Hbox") as (γ) "(% & #Hslice & Hbox)". done. as (γ) "(% & #Hslice & Hbox)"; first done. iExists γ. iFrame "%#". iModIntro. iNext. iExists γ. iFrame "%#". iModIntro. iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto]. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto]. iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc. iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc. - iMod (box_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done. - iMod (slice_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done. iMod (box_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)". iMod (slice_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)"; first done. done. by simplify_map_eq. { by simplify_map_eq. } iMod (box_insert_empty (Q1 ∗ Q2)%I with "Hbox") as (γ) "(% & #Hslice & Hbox)". iMod (slice_insert_empty (Q1 ∗ Q2)%I with "Hbox") as (γ) "(% & #Hslice & Hbox)". iExists γ. iFrame "%#". iModIntro. iNext. iExists γ. iFrame "%#". iModIntro. iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto]. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto]. iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc. iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc. ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!