(* iris/bi/sbi_unfold.v *)
From iris.bi Require Export cmra internal_eq
From iris.prelude Require Import options

Local SetDefault Proof Using "Type*".

Inductive sbi_unfold_closure_indicator:= DownClosed | NotClosed.

Class SbiUnfold`{!Sbi PROP} (clo : sbi_unfold_closure_indicator)
    (P : PROP) (Pi : nat → Prop) := {
  sbi_unfold_closed n1 n2 : clo = DownClosed → Pi n1 → n2 ≤ n1 → Pi n2;

Global HintMode SbiUnfold + + + ! - : typeclass_instances.

Lemma SbiUnfold_closed`{Sbi PROP} clo (P : PROP) Pi
    (Piclosed : ∀ n1 n2, Pi n1 → n2 ≤ n1 → Pi n2) :
  P ⊣⊢ <si_pure> SiProp Pi Piclosed → SbiUnfold clo P Pi.
Proof.
  intros HP. split; [naive_solver|]. rewrite HP.
  f_equiv. split=> n; rewrite /siProp_holds /=; naive_solver eauto with lia.
Qed.

Definition sbi_unfold_maybe_downclose(clo : sbi_unfold_closure_indicator)
    (Pi : nat → Prop) (n : nat) : Prop :=
  if clo is DownClosed then ∀ n', n' ≤ n → Pi n' else Pi n.

Lemma SbiUnfold_downclose`{Sbi PROP} clo (P : PROP) Pi :
  P ⊣⊢ <si_pure> SiProp_downclose Pi →
  SbiUnfold clo P (sbi_unfold_maybe_downclose clo Pi).
Proof.
  destruct clo; [|by split].
  intros HP. split; [naive_solver eauto with lia|]. rewrite HP.
  f_equiv. split=> n; rewrite /siProp_holds /=; naive_solver eauto with lia.
Qed.

Lemma sbi_unfold_closed_weaken`{Sbi PROP} clo (P : PROP) Pi :
  SbiUnfold DownClosed P Pi → SbiUnfold clo P Pi.
Proof. intros [??]; split; naive_solver. Qed.

Global Instancesbi_unfold_siprop clo (P : siProp) :
  SbiUnfold clo P (siProp_holds P) | 100.
Proof. apply: SbiUnfold_closed; [by eauto using siProp_closed|]. by split. Qed.

Local ArgumentssiProp_holds !_.

Local NotationSbiUnfold := (SbiUnfold (PROP:=PROP)).

Lemma sbi_unfold_entails`{!SbiUnfold DownClosed P Pi, !SbiUnfold NotClosed Q Qi} :
    (P ⊢ Q) ↔ ∀ n, Pi n → Qi n.
  Proof.
    destruct select (SbiUnfold _ P _) as [? HP].
    destruct select (SbiUnfold _ Q _) as [? HQ].
    rewrite HP HQ si_pure_entails.
    split; [intros []|split]; naive_solver eauto with lia.
  Qed.

Lemma sbi_unfold_equiv`{!SbiUnfold DownClosed P Pi, !SbiUnfold DownClosed Q Qi} :
    P ⊣⊢ Q ↔ ∀ n, Pi n ↔ Qi n.
  Proof.
    pose proof @sbi_unfold_closed_weaken.
    rewrite bi.equiv_entails !sbi_unfold_entails. naive_solver.
  Qed.

Lemma sbi_unfold_emp_valid`{!SbiUnfold NotClosed Q Qi} :
    (⊢ Q) ↔ ∀ n, Qi n.
  Proof.
    destruct select (SbiUnfold _ Q _) as [? HQ].
    rewrite HQ si_pure_emp_valid /bi_emp_valid. siProp.unseal.
    split; [intros []|split]; naive_solver eauto with lia.
  Qed.

Global Instancesbi_unfold_pure clo φ : SbiUnfold clo ⌜ φ ⌝ (λ _, φ).
  Proof.
    apply: SbiUnfold_closed. rewrite -si_pure_pure. f_equiv. by siProp.unseal.
  Qed.

Global Instancesbi_unfold_internal_eq {A : ofe} clo (x y : A) :
    SbiUnfold clo (x ≡ y) (λ n, x ≡{n}≡ y).
  Proof.
    apply: SbiUnfold_closed; [by eauto using dist_le|].
    intros ?. rewrite /internal_eq. f_equiv. by siProp.unseal.
  Qed.

Global Instancesbi_unfold_internal_cmra_valid {A : cmra} clo (x : A) :
    SbiUnfold clo (✓ x) (λ n, ✓{n} x).
  Proof.
    apply: SbiUnfold_closed; [by eauto using cmra_validN_le|].
    intros ?. rewrite /internal_cmra_valid. f_equiv. by siProp.unseal.
  Qed.

Global Instancesbi_unfold_internal_included {A : cmra} clo (x y : A) :
    SbiUnfold clo (x ≼ y) (λ n, x ≼{n} y).
  Proof.
    apply: SbiUnfold_closed; [by eauto using cmra_includedN_le|].
    intros ?. rewrite /internal_included /internal_eq -si_pure_exist.
    f_equiv. by siProp.unseal.
  Qed.

Global Instancesbi_unfold_si_pure clo (Psi : siProp) Pi :
    bi.sbi_unfold.SbiUnfold clo Psi Pi →
    SbiUnfold clo (<si_pure> Psi) Pi.
  Proof. intros [? HP]. split; [done|]. by rewrite HP. Qed.

Global Instancesbi_unfold_and clo P Q Pi Qi :
    SbiUnfold clo P Pi →
    SbiUnfold clo Q Qi →
    SbiUnfold clo (P ∧ Q) (λ n, Pi n ∧ Qi n).
  Proof.
    intros [? HP] [? HQ]. split; [naive_solver|].
    rewrite HP HQ -si_pure_and. f_equiv.
    siProp.unseal. split=> n /=. destruct clo; naive_solver.
  Qed.

Global Instancesbi_unfold_sep clo P Q Pi Qi :
    SbiUnfold clo P Pi →
    SbiUnfold clo Q Qi →
    SbiUnfold clo (P ∗ Q) (λ n, Pi n ∧ Qi n).
  Proof.
    intros [? HP] [? HQ]. split; [naive_solver|].
    rewrite HP HQ -si_pure_and_sep. f_equiv.
    siProp.unseal. split=> n /=. destruct clo; naive_solver.
  Qed.

Global Instancesbi_unfold_or clo P Q Pi Qi :
    SbiUnfold DownClosed P Pi →
    SbiUnfold DownClosed Q Qi →
    SbiUnfold clo (P ∨ Q) (λ n, Pi n ∨ Qi n).
  Proof.
    intros [? HP] [? HQ]. apply: SbiUnfold_closed; [naive_solver|].
    intros ?. rewrite HP HQ -si_pure_or. f_equiv.
    split=> n /=; siProp.unseal; naive_solver.
  Qed.

Global Instancesbi_unfold_impl clo P Q Pi Qi :
    SbiUnfold DownClosed P Pi →
    SbiUnfold NotClosed Q Qi →
    SbiUnfold clo (P → Q) (sbi_unfold_maybe_downclose clo (λ n, Pi n → Qi n)).
  Proof.
    intros [? HP] [? HQ]. apply SbiUnfold_downclose.
    rewrite HP HQ -si_pure_impl. f_equiv.
    split=> n /=; siProp.unseal; naive_solver eauto with lia.
  Qed.

Global Instancesbi_unfold_wand clo P Q Pi Qi :
    SbiUnfold DownClosed P Pi →
    SbiUnfold NotClosed Q Qi →
    SbiUnfold clo (P -∗ Q) (sbi_unfold_maybe_downclose clo (λ n, Pi n → Qi n)).
  Proof.
    intros [? HP] [? HQ]. apply SbiUnfold_downclose.
    rewrite HP HQ -si_pure_impl_wand. f_equiv.
    split=> n /=; siProp.unseal; naive_solver eauto with lia.
  Qed.

Global Instancesbi_unfold_iff clo P Q Pi Qi :
    SbiUnfold DownClosed P Pi →
    SbiUnfold DownClosed Q Qi →
    SbiUnfold clo (P ↔ Q) (sbi_unfold_maybe_downclose clo (λ n, Pi n ↔ Qi n)).
  Proof.
    intros [? HP] [? HQ]. apply SbiUnfold_downclose.
    rewrite HP HQ -si_pure_iff. f_equiv.
    split=> n /=; rewrite /bi_iff; siProp.unseal; naive_solver eauto with lia.
  Qed.

Global Instancesbi_unfold_iff_wand clo P Q Pi Qi :
    SbiUnfold DownClosed P Pi →
    SbiUnfold DownClosed Q Qi →
    SbiUnfold clo (P ∗-∗ Q) (sbi_unfold_maybe_downclose clo (λ n, Pi n ↔ Qi n)).
  Proof.
    intros [? HP] [? HQ]. apply SbiUnfold_downclose.
    rewrite HP HQ -si_pure_impl_iff_wand. f_equiv.
    split=> n /=; rewrite /bi_iff; siProp.unseal; naive_solver eauto with lia.
  Qed.

Global Instancesbi_unfold_forall {A} clo (Φ : A → PROP) Φi :
    (∀ x, SbiUnfold clo (Φ x) (Φi x)) →
    SbiUnfold clo (∀ x, Φ x) (λ n, ∀ x, Φi x n).
  Proof.
    intros HΦ. split; [naive_solver|]. etrans; [f_equiv=> x; apply HΦ|].
    rewrite -si_pure_forall. f_equiv.
    split=> n /=; siProp.unseal; destruct clo; naive_solver eauto with lia.
  Qed.

Global Instancesbi_unfold_exist {A} clo (Φ : A → PROP) Φi :
    (∀ x, SbiUnfold DownClosed (Φ x) (Φi x)) →
    SbiUnfold clo (∃ x, Φ x) (λ n, ∃ x, Φi x n).
  Proof.
    intros HΦ. apply: SbiUnfold_closed; [naive_solver|].
    intros ?. etrans; [f_equiv=> x; apply HΦ|].
    rewrite -si_pure_exist. f_equiv.
    split=> n /=; siProp.unseal; destruct clo; naive_solver eauto with lia.
  Qed.

Global Instancesbi_unfold_later clo P Pi :
    SbiUnfold clo P Pi →
    SbiUnfold clo (▷ P) (λ n, match n with 0 => True | S n' => Pi n' end).
  Proof.
    intros [? HP]. split.
    { intros [] []; naive_solver eauto with lia. }
    rewrite HP -si_pure_later. f_equiv.
    split=> n /=; siProp.unseal; simpl. split.
    - destruct n; intros ? []; naive_solver eauto with lia.
    - destruct n; [done|]. intros HPi n' ?. apply (HPi (S n')); lia.
  Qed.

Local Lemmasbi_unfold_tceq `{Sbi PROP} clo (P : PROP) Pi Pi' :
  SbiUnfold clo P Pi' → TCEq Pi Pi' → SbiUnfold clo P Pi.
Proof. by intros ? ->. Qed.

Global HintExtern 0 (SbiUnfold _ (match ?x with _ => _ end) ?Pi) =>

Ltac sbi_unfold:=
  match goal with
  | |- ⊢ _ => apply sbi_unfold_emp_valid
  | |- _ ⊣⊢ _ => apply sbi_unfold_equiv
  | |- _ ⊢ _ => apply sbi_unfold_entails
  | |- _ => fail "sbi_unfold: not a BI entailment"
  end;