Library iris.program_logic.invariants

From iris.program_logic Require Import ownership.
From iris.program_logic Require Export namespaces.
From iris.proofmode Require Import pviewshifts.
Import uPred.

Derived forms and lemmas about them.

Definition inv_def {Λ Σ} (N : namespace) (P : iProp Λ Σ) : iProp Λ Σ :=
  (∃ i, ⧆■ (i ∈ nclose N ) ∧ ownI i P)%I.
Definition inv_aux : { x | x = @inv_def }. by eexists. Qed.
Definition inv {Λ Σ} := proj1_sig inv_aux Λ Σ.
Definition inv_eq : @inv = @inv_def := proj2_sig inv_aux.
Instance: Params (@inv) 3.
Typeclasses Opaque inv.

Section inv.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types i : positive.
Implicit Types N : namespace.
Implicit Types P Q R : iProp Λ Σ.
Implicit Types Φ : val Λ → iProp Λ Σ.

Global Instance inv_contractive N : Contractive (@inv Λ Σ N).
Proof.
  rewrite inv_eq⇒ n ???. apply exist_ne⇒i. by apply and_ne, ownI_contractive.
Qed.

Global Instance inv_relevant N P : RelevantP (inv N P).
Proof.
  rewrite inv_eq /inv /RelevantP. rewrite relevant_exist.
  eapply exist_mono⇒i. rewrite relevant_relevant'. auto.
Qed.
Global Instance inv_affine N P : AffineP (inv N P).
Proof.
  rewrite inv_eq /inv /AffineP. rewrite affine_exist.
  eapply exist_mono⇒i. apply affine_intro; first by apply _.
  auto.
Qed.

Lemma always_inv N P : □ inv N P ⊣⊢ inv N P.
Proof. by rewrite relevant_relevant'. Qed.

Lemma inv_alloc N E P : nclose N ⊆ E → ⧆▷ P ⊢ |={E }=> inv N P.
Proof.
  intros. rewrite -(pvs_mask_weaken N) //.
  rewrite inv_eq /inv (pvs_allocI N); last apply nclose_infinite.
  eapply pvs_mono, exist_mono. intros i. unfold ownI. rewrite ?affine_equiv.
  apply and_intro; eauto with I.
Qed.

Fairly explicit form of opening invariants

Lemma inv_open E N P :
  nclose N ⊆ E →
  inv N P ⊢ ∃ E', ⧆■ (E ∖ nclose N ⊆ E' ⊆ E ) ★
                    |={E ,E'}=> ⧆▷ P ★ ⧆(⧆▷ P ={E',E }=★ Emp ).
Proof.
  rewrite inv_eq /inv. iDestruct 1 as (i) "[% #Hi]".
  iExists (E ∖ {[ i ]}). iSplit; first (iPureIntro; set_solver).
  iPvs (pvs_openI' with "Hi") as "HP"; [set_solver..|].
  iPvsIntro. iSplitL "HP"; first done.
  iIntros "@ HP". iPvs (pvs_closeI_sep' _ _ P with "[HP]"); [set_solver|iSplit; done|set_solver|].
  done.
Qed.

Invariants can be opened around any frame-shifting assertion. This is less verbose to apply than inv_open.

Lemma inv_fsa {A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa} E N P Ψ :
  fsaV → nclose N ⊆ E →
  (inv N P ★ (▷ P -★ fsa (E ∖ nclose N) (λ a, ⧆▷ P ★ Ψ a))) ⊢ fsa E Ψ.
Proof.
  iIntros (??) "[Hinv HΨ]".
  iDestruct (inv_open E N P with "Hinv") as (E') "[% Hvs]"; first done.
  iApply (fsa_open_close E E'); auto; first set_solver.
  iPvs "Hvs" as "[HP Hvs]"; first set_solver.
  iPvsIntro. iApply (fsa_mask_weaken _ (E ∖ N)); first set_solver.
  iApply fsa_wand_r. iSplitR "Hvs"; first by (iApply "HΨ"; rewrite affine_elim).
  iIntros (v) "[HP HΨ]". rewrite affine_elim. by iPvs ("Hvs" with "HP"); first set_solver.
Qed.

Lemma inv_afsa {A} (fsa : FSA Λ Σ A) `{!AffineFrameShiftAssertion fsaV fsa} E N P Ψ :
  fsaV → nclose N ⊆ E →
  (inv N P ★ (⧆▷ P -★ fsa (E ∖ nclose N) (λ a, ⧆▷ P ★ Ψ a))) ⊢ fsa E Ψ.
Proof.
  iIntros (??) "[Hinv HΨ]".
  iDestruct (inv_open E N P with "Hinv") as (E') "[% Hvs]"; first done.
  iApply (afsa_open_close E E'); auto; first set_solver.
  iPvs "Hvs" as "[HP Hvs]"; first set_solver.
  iPvsIntro. iApply (afsa_mask_weaken _ (E ∖ N)); first set_solver.
  iApply afsa_wand_r. iSplitR "Hvs"; first by (iApply "HΨ").
  iIntros "@". iIntros (v) "[HP HΨ]".
  rewrite affine_elim. iPvs ("Hvs" with "HP"); first set_solver.
  iPvsIntro. done.
Qed.
End inv.