Library iris.proofmode.pstepshifts

From iris.proofmode Require Import coq_tactics spec_patterns pviewshifts.
From iris.proofmode Require Export tactics.
From iris.program_logic Require Export pviewshifts pstepshifts.
Import uPred.

Section psvs.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q : iProp Λ Σ.

Global Instance or_split_psvs E1 E2 P Q1 Q2 :
  FromOr P Q1 Q2 → FromOr (|={E1,E2}=>> P) (|={E1,E2}=>> Q1) (|={E1,E2}=>> Q2).
Proof. rewrite /FromOr=><-. apply or_elim; apply psvs_mono; auto with I. Qed.
Global Instance exists_split_psvs {A} E1 E2 P (Φ : A → iProp Λ Σ) :
  FromExist P Φ → FromExist (|={E1,E2}=>> P) (λ a, |={E1,E2}=>> Φ a)%I.
Proof.
  rewrite /FromExist=><-. apply exist_elim⇒ a. by rewrite -(exist_intro a).
Qed.
Global Instance aframe_psvs E1 E2 R P Q :
  AffineP R →
  Frame R P Q →
  Frame R (|={E1,E2}=>> P) (|={E1,E2}=>> Q)%I.
Proof. rewrite /Frame⇒ HA <-. rewrite -(affine_affine R). by rewrite psvs_frame_l. Qed.

Global Instance fsa_split_psvs E P :
  IsAFSA (|={E}=>> P)%I E psvs_fsa True (λ _, P).
Proof. split. done. apply _. Qed.

Lemma tac_psvs_elim Δ Δ' E1 E2 E3 i p P Q :
  envs_lookup i Δ = Some (p, |={E1,E2}=>> P)%I →
  envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' →
  (envs_delete i p Δ ⊢ ⧆ (envs_delete i p Δ)) →
  E2 ⊆ E1 ∪ E3 →
  (Δ' ⊢ (|={E2,E3}=> Q)) → Δ ⊢ |={E1,E3}=>> Q.
Proof.
  intros ?? Haff ? HQ. rewrite envs_replace_sound_affine //; simpl. destruct p.
  - rewrite relevant_elim right_id psvs_frame_r affine_elim wand_elim_r HQ psvs_pvs //=.
  - by rewrite right_id psvs_frame_r affine_elim wand_elim_r HQ psvs_pvs.
Qed.

Lemma tac_psvs_timeless Δ Δ' E1 E2 i P Q :
  envs_lookup i Δ = Some (false, ▷ P)%I → TimelessP P →
  envs_simple_replace i false (Esnoc Enil i P) Δ = Some Δ' →
  (Δ' ⊢ |={E1,E2}=>> Q) → Δ ⊢ (|={E1,E2}=>> Q).
Proof.
  intros ??? HQ.
  etransitivity; last apply (pvs_psvs E1 E1 E2); last set_solver.
  eapply tac_pvs_timeless; eauto.
Qed.

End psvs.

Tactic Notation "iPsvsCore" constr(H) :=
  match goal with
  | |- _ ⊢ |={_,_}=>> _ ⇒
    eapply tac_psvs_elim with _ _ H _ _;
      [env_cbv; reflexivity || fail "iPsvs:" H "not found"
      |env_cbv; reflexivity
      |env_cbv; apply affine_intro; first apply _; auto || fail "iPsvs: couldn't prove ctxt affine."
      |try (rewrite (idemp_L (∪)); reflexivity)|]
  end.

Tactic Notation "iPsvsCore" constr(H) constr(HP) :=
  match goal with
  | |- _ ⊢ |={_,_}=>> _ ⇒
    eapply tac_psvs_elim with _ _ H _ HP;
      [env_cbv; reflexivity || fail "iPsvs:" H "not found"
      |env_cbv; reflexivity
      |env_cbv; apply affine_intro; first apply _; auto || fail "iPsvs: couldn't prove ctxt affine."
      |try (rewrite (idemp_L (∪)); reflexivity)|]
  end.

Tactic Notation "iPsvs" open_constr(lem) :=
  iDestructCore lem as (fun H ⇒ iPsvsCore H; last iDestruct H as "?").