Commit 8f5438b8 by Robbert Krebbers

### Make invariants closed under logical equivalence.

`This partially solves #112.`
parent 59fbe96b
 ... @@ -7,7 +7,7 @@ Import uPred. ... @@ -7,7 +7,7 @@ Import uPred. (** Derived forms and lemmas about them. *) (** Derived forms and lemmas about them. *) Definition inv_def `{invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ := Definition inv_def `{invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ := (∃ i, ⌜i ∈ (↑N:coPset)⌝ ∧ ownI i P)%I. (∃ i P', ⌜i ∈ (↑N:coPset)⌝ ∧ ▷ □ (P' ↔ P) ∧ ownI i P')%I. Definition inv_aux : seal (@inv_def). by eexists. Qed. Definition inv_aux : seal (@inv_def). by eexists. Qed. Definition inv {Σ i} := unseal inv_aux Σ i. Definition inv {Σ i} := unseal inv_aux Σ i. Definition inv_eq : @inv = @inv_def := seal_eq inv_aux. Definition inv_eq : @inv = @inv_def := seal_eq inv_aux. ... @@ -21,19 +21,25 @@ Implicit Types N : namespace. ... @@ -21,19 +21,25 @@ Implicit Types N : namespace. Implicit Types P Q R : iProp Σ. Implicit Types P Q R : iProp Σ. Global Instance inv_contractive N : Contractive (inv N). Global Instance inv_contractive N : Contractive (inv N). Proof. Proof. rewrite inv_eq. solve_contractive. Qed. rewrite inv_eq=> n ???. apply exist_ne=>i. by apply and_ne, ownI_contractive. Qed. Global Instance inv_ne N : NonExpansive (inv N). Global Instance inv_ne N : NonExpansive (inv N). Proof. apply contractive_ne, _. Qed. Proof. apply contractive_ne, _. Qed. Global Instance inv_Proper N : Proper ((⊣⊢) ==> (⊣⊢)) (inv N). Global Instance inv_proper N : Proper ((⊣⊢) ==> (⊣⊢)) (inv N). Proof. apply ne_proper, _. Qed. Proof. apply ne_proper, _. Qed. Global Instance inv_persistent N P : Persistent (inv N P). Global Instance inv_persistent N P : Persistent (inv N P). Proof. rewrite inv_eq /inv; apply _. Qed. Proof. rewrite inv_eq /inv; apply _. Qed. Lemma inv_iff N P Q : ▷ □ (P ↔ Q) -∗ inv N P -∗ inv N Q. Proof. iIntros "#HPQ". rewrite inv_eq. iDestruct 1 as (i P') "(?&#HP&?)". iExists i, P'. iFrame. iNext; iAlways; iSplit. - iIntros "HP'". iApply "HPQ". by iApply "HP". - iIntros "HQ". iApply "HP". by iApply "HPQ". Qed. Lemma fresh_inv_name (E : gset positive) N : ∃ i, i ∉ E ∧ i ∈ (↑N:coPset). Lemma fresh_inv_name (E : gset positive) N : ∃ i, i ∉ E ∧ i ∈ (↑N:coPset). Proof. Proof. exists (coPpick (↑ N ∖ coPset.of_gset E)). exists (coPpick (↑ N ∖ coPset.of_gset E)). ... @@ -48,6 +54,7 @@ Proof. ... @@ -48,6 +54,7 @@ Proof. rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros "HP [Hw \$]". rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros "HP [Hw \$]". iMod (ownI_alloc (∈ (↑N : coPset)) P with "[\$HP \$Hw]") iMod (ownI_alloc (∈ (↑N : coPset)) P with "[\$HP \$Hw]") as (i ?) "[\$ ?]"; auto using fresh_inv_name. as (i ?) "[\$ ?]"; auto using fresh_inv_name. do 2 iModIntro. iExists i, P. rewrite -(iff_refl True). auto. Qed. Qed. Lemma inv_alloc_open N E P : Lemma inv_alloc_open N E P : ... @@ -61,7 +68,9 @@ Proof. ... @@ -61,7 +68,9 @@ Proof. { rewrite -?ownE_op; [|set_solver..]. { rewrite -?ownE_op; [|set_solver..]. rewrite assoc_L -!union_difference_L //. set_solver. } rewrite assoc_L -!union_difference_L //. set_solver. } do 2 iModIntro. iFrame "HE\N". iSplitL "Hw HEi"; first by iApply "Hw". do 2 iModIntro. iFrame "HE\N". iSplitL "Hw HEi"; first by iApply "Hw". iSplitL "Hi"; first by eauto. iIntros "HP [Hw HE\N]". iSplitL "Hi". { iExists i, P. rewrite -(iff_refl True). auto. } iIntros "HP [Hw HE\N]". iDestruct (ownI_close with "[\$Hw \$Hi \$HP \$HD]") as "[\$ HEi]". iDestruct (ownI_close with "[\$Hw \$Hi \$HP \$HD]") as "[\$ HEi]". do 2 iModIntro. iSplitL; [|done]. do 2 iModIntro. iSplitL; [|done]. iCombine "HEi" "HEN\i" as "HEN"; iCombine "HEN" "HE\N" as "HE". iCombine "HEi" "HEN\i" as "HEN"; iCombine "HEN" "HE\N" as "HE". ... @@ -72,13 +81,16 @@ Qed. ... @@ -72,13 +81,16 @@ Qed. Lemma inv_open E N P : Lemma inv_open E N P : ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ ▷ P ∗ (▷ P ={E∖↑N,E}=∗ True). ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ ▷ P ∗ (▷ P ={E∖↑N,E}=∗ True). Proof. Proof. rewrite inv_eq /inv_def fupd_eq /fupd_def; iDestruct 1 as (i) "[Hi #HiP]". rewrite inv_eq /inv_def fupd_eq /fupd_def. iDestruct 1 as (i P') "(Hi & #HP' & #HiP)". iDestruct "Hi" as % ?%elem_of_subseteq_singleton. iDestruct "Hi" as % ?%elem_of_subseteq_singleton. rewrite {1 4}(union_difference_L (↑ N) E) // ownE_op; last set_solver. rewrite {1 4}(union_difference_L (↑ N) E) // ownE_op; last set_solver. rewrite {1 5}(union_difference_L {[ i ]} (↑ N)) // ownE_op; last set_solver. rewrite {1 5}(union_difference_L {[ i ]} (↑ N)) // ownE_op; last set_solver. iIntros "(Hw & [HE \$] & \$) !> !>". iIntros "(Hw & [HE \$] & \$) !> !>". iDestruct (ownI_open i P with "[\$Hw \$HE \$HiP]") as "(\$ & \$ & HD)". iDestruct (ownI_open i with "[\$Hw \$HE \$HiP]") as "(\$ & HP & HD)". iIntros "HP [Hw \$] !> !>". iApply ownI_close; by iFrame. iDestruct ("HP'" with "HP") as "\$". iIntros "HP [Hw \$] !> !>". iApply (ownI_close _ P'). iFrame "HD Hw HiP". iApply "HP'". iFrame. Qed. Qed. Lemma inv_open_timeless E N P `{!Timeless P} : Lemma inv_open_timeless E N P `{!Timeless P} : ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!