Library zoo.program_logic.biglater

Require Import zoo.prelude.
Require Export zoo.program_logic.wp.
Require Import zoo.diaframe.
Require Import zoo.options.

Section zoo ۰ G.
  Context `{zoo ۰ G : !ZooG Σ}.

  Implicit Type P : iProp Σ.

  Definition biglater P : iProp Σ :=
    ∃ ns ,
    ⧖ ns ∗
    ▷^(later ۰ function ns ) P.
End zoo ۰ G.

Notation "▶ P" := (
  biglater P
)(at level 20,
  right associativity
) : bi_scope.

#[local] Instance : CustomIpat "biglater" :=
  " ( %ns{} & #H⧖{_{}} & HP{} ) ".

Section zoo ۰ G.
  Context `{zoo ۰ G : !ZooG Σ}.

  Implicit Type P : iProp Σ.

  #[global] Instance biglater ｰ ne :
    NonExpansive biglater.
  #[global] Instance biglater ｰ proper :
    Proper ((≡) ==> (≡)) biglater.

  Lemma biglater ｰ intro P :
    P ⊢ |==>
    ▶ P.

  Lemma biglater ｰ mono P1 P2 :
    (P1 ⊢ P2) →
    (▶ P1 ) ⊢ ▶ P2.
  #[global] Instance biglater ｰ mono' :
    Proper ((⊢) ==> (⊢)) biglater.
  #[global] Instance biglater ｰ flip ｰ mono' :
    Proper (flip (⊢) ==> flip (⊢)) biglater.

  Lemma biglater ｰ or₁ P1 P2 :
    ▶ (P1 ∨ P2 ) ⊢
    ▶ P1 ∨ ▶ P2.
  Lemma biglater ｰ or₂ P1 P2 :
    ▶ P1 ∨ ▶ P2 ⊢
    ▶ (P1 ∨ P2 ).
  Lemma biglater ｰ or P1 P2 :
    ▶ (P1 ∨ P2 ) ⊣⊢
    ▶ P1 ∨ ▶ P2.

  Lemma biglater ｰ and P1 P2 :
    ▶ (P1 ∧ P2 ) ⊢
    ▶ P1 ∧ ▶ P2.

  Lemma biglater ｰ exist₁ `{!Inhabited X} (Φ : X → iProp Σ) :
    ▶ (∃ x , Φ x ) ⊢
    ∃ x , ▶ Φ x.
  Lemma biglater ｰ exist₂ `(Φ : X → iProp Σ) :
    (∃ x , ▶ Φ x ) ⊢
    ▶ ∃ x , Φ x.
  Lemma biglater ｰ exist `{!Inhabited X} (Φ : X → iProp Σ) :
    ▶ (∃ x , Φ x ) ⊣⊢
    ∃ x , ▶ Φ x.

  Lemma biglater ｰ ∀ `(Φ : X → iProp Σ) :
    ▶ (∀ x , Φ x ) ⊢
    ∀ x , ▶ Φ x.

  Lemma biglater ｰ sep₁ P1 P2 :
    ▶ (P1 ∗ P2 ) ⊢
      ▶ P1 ∗
      ▶ P2.
  Lemma biglater ｰ sep₂ P1 P2 :
    ▶ P1 -∗
    ▶ P2 -∗
    ▶ (P1 ∗ P2 ).
  Lemma biglater ｰ sep P1 P2 :
    ▶ (P1 ∗ P2 ) ⊣⊢
      ▶ P1 ∗
      ▶ P2.

  Lemma biglater ｰ frame ｰ l P1 P2 :
    P1 -∗
    ▶ P2 -∗
    ▶ (P1 ∗ P2 ).
  Lemma biglater ｰ frame ｰ r P1 P2 :
    ▶ P1 -∗
    P2 -∗
    ▶ (P1 ∗ P2 ).

  Lemma biglater ｰ wand ｰ l P1 P2 :
    (P1 -∗ P2 ) -∗
    (▶ P1 ) -∗
    ▶ P2.
  Lemma biglater ｰ wand ｰ r P1 P2 :
    (▶ P1 ) -∗
    (P1 -∗ P2 ) -∗
    ▶ P2.

  Lemma biglater ｰ persistently P :
    ▶ <pers > P ⊢
    <pers > ▶ P.
End zoo ۰ G.

Section zoo ۰ G.
  Context `{zoo ۰ G : !ZooG Σ}.

  Implicit Type P : iProp Σ.

  #[global] Instance into_wand ｰ biglater p q R P Q :
    IntoWand false false R P Q →
    IntoWand p q (▶ R) (▶ P) (▶ Q).
  #[global] Instance into_wand ｰ biglater ｰ args p q R P Q :
    IntoWand p false R P Q →
    IntoWand' p q R (▶ P) (▶ Q).

  #[global] Instance from_sep ｰ biglater P Q1 Q2 :
    FromSep P Q1 Q2 →
    FromSep (▶ P) (▶ Q1) (▶ Q2).

  #[global] Instance maybe_combine_sep_as ｰ biglater Q1 Q2 P progress :
    MaybeCombineSepAs Q1 Q2 P progress →
    MaybeCombineSepAs (▶ Q1) (▶ Q2) (▶ P) progress.

  #[global] Instance combine_sep_gives ｰ biglater Q1 Q2 P :
    CombineSepGives Q1 Q2 P →
    CombineSepGives (▶ Q1) (▶ Q2) (▶ P).

  #[global] Instance into_and ｰ biglater P Q1 Q2 :
    IntoAnd false P Q1 Q2 →
    IntoAnd false (▶ P) (▶ Q1) (▶ Q2).

  #[global] Instance into_sep ｰ biglater P Q1 Q2 :
    IntoSep P Q1 Q2 →
    IntoSep (▶ P) (▶ Q1) (▶ Q2).

  #[global] Instance from_or ｰ biglater P Q1 Q2 :
    FromOr P Q1 Q2 →
    FromOr (▶ P) (▶ Q1) (▶ Q2).

  #[global] Instance into_or ｰ biglater P Q1 Q2 :
    IntoOr P Q1 Q2 →
    IntoOr (▶ P) (▶ Q1) (▶ Q2).

  #[global] Instance from_exist ｰ biglater {X} P (Φ : X → iProp Σ) :
    FromExist P Φ →
    FromExist (▶ P) (λ x, ▶ Φ x)%I.

  #[global] Instance into_exist ｰ biglater {X} P (Φ : X → iProp Σ) name :
    IntoExist P Φ name →
    Inhabited X →
    IntoExist (▶ P) (λ a, ▶ (Φ a ))%I name.

  #[global] Instance into_forall ｰ biglater {X} P (Φ : X → iProp Σ) :
    IntoForall P Φ →
    IntoForall (▶ P) (λ x, ▶ Φ x)%I.

  #[global] Instance frame ｰ biglater p R P Q :
    Frame p R P Q →
    Frame p R (▶ P) (▶ Q)
  | 2.

  #[global] Instance biglater ｰ strong_modality :
    ModalityStrongMono biglater.
End zoo ۰ G.