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 P Q Φ :
  IsFSA Q E fsa fsaV Φ →
  fsaV → nclose N ⊆ E → (of_envs Δ ⊢ 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 // -always_and_sep_l. apply and_intro; first done.
  rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'.
Qed.

Lemma tac_inv_fsa_timeless {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E N i P Q Φ :
  IsFSA Q E fsa fsaV Φ →
  fsaV → nclose N ⊆ E → (of_envs Δ ⊢ inv N P) → TimelessP 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 // -always_and_sep_l. apply and_intro, wand_intro_l; first done.
  trans (|={E ∖ N}=> P ★ Δ)%I; first by rewrite pvs_timeless pvs_frame_r.
  apply (fsa_strip_pvs _).
  rewrite envs_app_sound //; simpl. rewrite right_id HΔ' wand_elim_r.
  apply: fsa_mono=> v. by rewrite -later_intro.
Qed.
End invariants.

Tactic Notation "iInvCore" constr(N) "as" constr(H) :=
  eapply tac_inv_fsa with _ _ _ _ N H _ _;
    [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
     apply _ || fail "iInv: cannot viewshift in goal" P
    |trivial with fsaV
    |solve_ndisj
    |iAssumption || fail "iInv: invariant" N "not found"
    |env_cbv; reflexivity
    |simpl (* get rid of FSAs *)].

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.

Tactic Notation "iInvCore>" constr(N) "as" constr(H) :=
  eapply tac_inv_fsa_timeless with _ _ _ _ N H _ _;
    [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
     apply _ || fail "iInv: cannot viewshift in goal" P
    |trivial with fsaV
    |solve_ndisj
    |iAssumption || fail "iOpenInv: invariant" N "not found"
    |let P := match goal with |- TimelessP ?P => P end in
     apply _ || fail "iInv:" P "not timeless"
    |env_cbv; reflexivity
    |simpl (* get rid of FSAs *)].

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.