Library iris.proofmode.invariants

From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export pviewshifts.
From iris.program_logic Require Export invariants.
Import uPred.

Section invariants.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types N : namespace.
Implicit Types P Q R : iProp Λ Σ.

Lemma tac_inv_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E N i j p P Q Φ :
  IsFSA Q E fsa fsaV Φ →
  fsaV → nclose N ⊆ E → envs_lookup j Δ = Some (p, inv N P) →
  envs_app false (Esnoc Enil i (▷ P)) Δ = Some Δ' →
  (Δ' ⊢ fsa (E ∖ nclose N) (λ a, ⧆▷ P ★ Φ a)) → Δ ⊢ Q.
Proof.
  intros ????? HΔ'. rewrite (is_fsa Q) -(inv_fsa fsa _ _ P) //.
  rewrite envs_lookup_relevant_sound'; eauto.
  rewrite relevant_elim. eapply sep_mono. auto.
  rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'.
Qed.

Lemma tac_inv_afsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E N i j p P Q Φ :
  IsAFSA Q E fsa fsaV Φ →
  fsaV → nclose N ⊆ E → envs_lookup j Δ = Some (p, inv N P) →
  envs_app false (Esnoc Enil i (⧆▷ P)) Δ = Some Δ' →
  (Δ' ⊢ fsa (E ∖ nclose N) (λ a, ⧆▷ P ★ Φ a)) → Δ ⊢ Q.
Proof.
  intros ????? HΔ'. rewrite (is_afsa Q) -(inv_afsa fsa _ _ P) //.
  rewrite envs_lookup_relevant_sound'; eauto.
  rewrite relevant_elim. eapply sep_mono. auto.
  rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'.
Qed.


End invariants.

Tactic Notation "iInvCore" constr(N) "as" constr(H) :=
  
  (eapply tac_inv_afsa with _ _ _ _ _ H N _ _ _;
    [let P := match goal with |- IsAFSA ?P _ _ _ _ ⇒ P end in
     apply _ || fail "iInv: cannot viewshift in goal" P
    |try fast_done
    |done || eauto with ndisj
    | env_cbv; reflexivity || fail "iInv: invariant not found"
    | env_cbv; reflexivity || fail "iOpenInv: invariant not found"
    |simpl ]).

Tactic Notation "iInv" constr(N) "as" constr(pat) :=
  let H := iFresh in iInvCore N as H; last iDestruct H as pat.
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1) ")"
    constr(pat) :=
  let H := iFresh in iInvCore N as H; last iDestruct H as (x1) pat.
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) ")" constr(pat) :=
  let H := iFresh in iInvCore N as H; last iDestruct H as (x1 x2) pat.
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
  let H := iFresh in iInvCore N as H; last iDestruct H as (x1 x2 x3) pat.
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
    constr(pat) :=
  let H := iFresh in iInvCore N as H; last iDestruct H as (x1 x2 x3 x4) pat.