Library zoo.program_logic.biglater

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

Section zoo_G.
  Context `{zoo_G : !ZooG Σ}.

  Implicit Types 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 Types 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_1 P1 P2 :
    ▶ (P1 ∨ P2) ⊢
    ▶ P1 ∨ ▶ P2.
  Lemma biglater_or_2 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_1 `{!Inhabited X} (Φ : X → iProp Σ) :
    ▶ (∃ x, Φ x) ⊢
    ∃ x, ▶ Φ x.
  Lemma biglater_exist_2 `(Φ : X → iProp Σ) :
    (∃ x, ▶ Φ x) ⊢
    ▶ ∃ x, Φ x.
  Lemma biglater_exist `{!Inhabited X} (Φ : X → iProp Σ) :
    ▶ (∃ x, Φ x) ⊣⊢
    ∃ x, ▶ Φ x.

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

  Lemma biglater_sep_1 P1 P2 :
    ▶ (P1 ∗ P2) ⊢
      ▶ P1 ∗
      ▶ P2.
  Lemma biglater_sep_2 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 Types 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 maybe_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.