Commit df8e3df5 authored by Robbert Krebbers's avatar Robbert Krebbers

Make `_iff` and `_alter` lemmas for invariants consistent.

They follow the pattern of `wp_wand`.
parent 92eaf4f9
......@@ -53,11 +53,10 @@ Section proofs.
iDestruct (cinv_own_valid with "H1 H2") as %[]%(exclusive_l 1%Qp).
Qed.
Lemma cinv_iff N γ P P' :
(P P') - cinv N γ P - cinv N γ P'.
Lemma cinv_iff N γ P Q : cinv N γ P - (P Q) - cinv N γ Q.
Proof.
iIntros "#HP". iApply inv_iff. iIntros "!> !>".
iSplit; iIntros "[?|$]"; iLeft; by iApply "HP".
iIntros "HI #HPQ". iApply (inv_iff with "HI"). iIntros "!> !>".
iSplit; iIntros "[?|$]"; iLeft; by iApply "HPQ".
Qed.
(*** Allocation rules. *)
......
......@@ -97,18 +97,17 @@ Section inv.
Global Instance inv_persistent N P : Persistent (inv N P).
Proof. rewrite inv_eq. apply _. Qed.
Lemma inv_alter N P Q:
inv N P - (P - Q (Q - P)) - inv N Q.
Lemma inv_alter N P Q : inv N P - (P - Q (Q - P)) - inv N Q.
Proof.
rewrite inv_eq. iIntros "#HI #Acc !>" (E H).
rewrite inv_eq. iIntros "#HI #HPQ !>" (E H).
iMod ("HI" $! E H) as "[HP Hclose]".
iDestruct ("Acc" with "HP") as "[$ HQP]".
iDestruct ("HPQ" with "HP") as "[$ HQP]".
iIntros "!> HQ". iApply "Hclose". iApply "HQP". done.
Qed.
Lemma inv_iff N P Q : (P Q) - inv N P - inv N Q.
Lemma inv_iff N P Q : inv N P - (P Q) - inv N Q.
Proof.
iIntros "#HPQ #HI". iApply (inv_alter with "HI").
iIntros "#HI #HPQ". iApply (inv_alter with "HI").
iIntros "!> !> HP". iSplitL "HP".
- by iApply "HPQ".
- iIntros "HQ". by iApply "HPQ".
......
......@@ -43,10 +43,10 @@ Section proofs.
Global Instance na_inv_persistent p N P : Persistent (na_inv p N P).
Proof. rewrite /na_inv; apply _. Qed.
Lemma na_inv_iff p N P Q : (P Q) - na_inv p N P - na_inv p N Q.
Lemma na_inv_iff p N P Q : na_inv p N P - (P Q) - na_inv p N Q.
Proof.
iIntros "#HPQ". rewrite /na_inv. iDestruct 1 as (i ?) "#Hinv".
iExists i. iSplit; first done. iApply (inv_iff with "[] Hinv").
iIntros "HI #HPQ". rewrite /na_inv. iDestruct "HI" as (i ?) "HI".
iExists i. iSplit; first done. iApply (inv_iff with "HI").
iIntros "!> !>".
iSplit; iIntros "[[? Ho]|$]"; iLeft; iFrame "Ho"; by iApply "HPQ".
Qed.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment