(* iris/bi/interface.v *)
From iris.algebra Require Export ofe stepindex_finite
From iris.bi Require Export notation
From iris.prelude Require Import options

Local SetPrimitive Projections.

Local Infix"⊢" := bi_entails.

Local Notation"'emp'" := bi_emp : bi_scope.

Local Notation"'True'" := (bi_pure True) : bi_scope.

Local Notation"'False'" := (bi_pure False) : bi_scope.

Local Notation"'⌜' φ '⌝'" := (bi_pure φ%type%stdpp) : bi_scope.

Local Infix"∧" := bi_and : bi_scope.

Local Infix"∨" := bi_or : bi_scope.

Local Infix"→" := bi_impl : bi_scope.

Local Notation"∀ x .. y , P" :=
    (bi_forall _ (λ x, .. (bi_forall _ (λ y, P%I)) ..)) : bi_scope.

Local Notation"∃ x .. y , P" :=
    (bi_exist _ (λ x, .. (bi_exist _ (λ y, P%I)) ..)) : bi_scope.

Local Infix"∗" := bi_sep : bi_scope.

Local Infix"-∗" := bi_wand : bi_scope.

Record BiMixin:= {
    bi_mixin_entails_po : PreOrder bi_entails;
    bi_mixin_equiv_entails P Q : (P ≡ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P);

Local Notation"'<pers>' P" := (bi_persistently P) : bi_scope.

Record BiPersistentlyMixin:= {
    bi_mixin_persistently_ne : NonExpansive bi_persistently;

Lemma bi_persistently_mixin_discrete:
    (∀ n (P Q : PROP), P ≡{n}≡ Q → P ≡ Q) →
    (∀ {A} (Φ : A → PROP), (emp ⊢ ∃ x, Φ x) → ∃ x, emp ⊢ Φ x) →
    (∀ P : PROP, (<pers> P)%I = ⌜ emp ⊢ P ⌝%I) →
    BiMixin →
    BiPersistentlyMixin.
  Proof.
    intros Hdiscrete Hex Hpers Hbi. pose proof (bi_mixin_entails_po Hbi).
    split.
    -
      intros n P Q [HPQ HQP]%Hdiscrete%(bi_mixin_equiv_entails Hbi).
      rewrite !Hpers. apply (bi_mixin_pure_ne Hbi). split=> ?; by etrans.
    -
      intros P Q HPQ. rewrite !Hpers. apply (bi_mixin_pure_elim' Hbi)=> ?.
      apply (bi_mixin_pure_intro Hbi). by trans P.
    -
      intros P. rewrite !Hpers. apply (bi_mixin_pure_elim' Hbi)=> ?.
      by do 2 apply (bi_mixin_pure_intro Hbi).
    -
      rewrite Hpers. by apply (bi_mixin_pure_intro Hbi).
    -
      intros P Q. rewrite !Hpers.
      apply (bi_mixin_impl_elim_l' Hbi). apply (bi_mixin_pure_elim' Hbi)=> ?.
      apply (bi_mixin_impl_intro_r Hbi).
      etrans; [apply (bi_mixin_and_elim_r Hbi)|].
      apply (bi_mixin_pure_elim' Hbi)=> ?.
      apply (bi_mixin_pure_intro Hbi). by apply (bi_mixin_and_intro Hbi).
    -
      intros A Φ. rewrite !Hpers. apply (bi_mixin_pure_elim' Hbi)=> /Hex [x ?].
      etrans; [|apply (bi_mixin_exist_intro Hbi x)]; simpl.
      rewrite Hpers. by apply (bi_mixin_pure_intro Hbi).
    -
      intros P Q. rewrite !Hpers.
      apply (bi_mixin_wand_elim_l' Hbi). apply (bi_mixin_pure_elim' Hbi)=> ?.
      apply (bi_mixin_wand_intro_r Hbi). by apply (bi_mixin_pure_intro Hbi).
    -
      intros
...

Local Notation"▷ P" := (bi_later P) : bi_scope.

Record BiLaterMixin:= {
    bi_mixin_later_ne : NonExpansive bi_later;
    bi_mixin_later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q;
    bi_mixin_later_intro P : P ⊢ ▷ P;
    bi_mixin_later_forall_2 {A} (Φ : A → PROP) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a;
    bi_mixin_later_exist_false {A} (Φ : A → PROP) :
      (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a);
    bi_mixin_later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q;
    bi_mixin_later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q);
    bi_mixin_later_persistently_1 P : ▷ <pers> P ⊢ <pers> ▷ P;
    bi_mixin_later_persistently_2 P : <pers> ▷ P ⊢ ▷ <pers> P;

Lemma bi_later_mixin_id:
    (∀ (P : PROP), (▷ P)%I = P) →
    BiMixin → BiLaterMixin.
  Proof.
    intros Hlater Hbi. pose proof (bi_mixin_entails_po Hbi).
    split; repeat intro; rewrite ?Hlater //.
    - apply (bi_mixin_forall_intro Hbi)=> a.
      etrans; [apply (bi_mixin_forall_elim Hbi a)|]. by rewrite Hlater.
    - etrans; [|apply (bi_mixin_or_intro_r Hbi)].
      apply (bi_mixin_exist_elim Hbi)=> a.
      etrans; [|apply (bi_mixin_exist_intro Hbi a)]. by rewrite /= Hlater.
    - etrans; [|apply (bi_mixin_or_intro_r Hbi)].
      apply (bi_mixin_impl_intro_r Hbi), (bi_mixin_and_elim_l Hbi).
  Qed.

Structure bi:= Bi {
  bi_car :> Type@{Logic};
  bi_dist : Dist bi_car;
  bi_equiv : Equiv bi_car;
  bi_entails : bi_car → bi_car → Prop;
  bi_emp : bi_car;
  bi_pure : Prop → bi_car;
  bi_and : bi_car → bi_car → bi_car;
  bi_or : bi_car → bi_car → bi_car;
  bi_impl : bi_car → bi_car → bi_car;
  bi_forall : ∀ A : Type@{Quant}, (A → bi_car) → bi_car;
  bi_exist : ∀ A : Type@{Quant}, (A → bi_car) → bi_car;
  bi_sep : bi_car → bi_car → bi_car;
  bi_wand : bi_car → bi_car → bi_car;
  bi_persistently : bi_car → bi_car;
  bi_later : bi_car → bi_car;
  bi_ofe_mixin : OfeMixin bi_car;
  bi_cofe_aux : Cofe (Ofe bi_car bi_ofe_mixin);
  bi_bi_mixin : BiMixin bi_entails bi_emp bi_pure bi_and bi_or bi_impl bi_forall
                        bi_exist bi_sep bi_wand;
  bi_bi_persistently_mixin :
    BiPersistentlyMixin bi_entails bi_emp bi_and bi_exist bi_sep bi_persistently;
  bi_bi_later_mixin : BiLaterMixin bi_entails bi_pure bi_or bi_impl
                                   bi_forall bi_exist bi_sep bi_persistently bi_later;
}.
Bind Scope bi_scope with bi_car.

Coercion bi_ofeO(PROP : bi) : ofe := Ofe PROP (bi_ofe_mixin PROP).
Canonical Structure bi_ofeO.

Global Instancebi_cofe (PROP : bi) : Cofe PROP := bi_cofe_aux PROP.

Global Instance: Params (@bi_entails) 1 := {}.

Global Instance: Params (@bi_emp) 1 := {}.

Global Instance: Params (@bi_pure) 1 := {}.

Global Instance: Params (@bi_and) 1 := {}.

Global Instance: Params (@bi_or) 1 := {}.

Global Instance: Params (@bi_impl) 1 := {}.

Global Instance: Params (@bi_forall) 2 := {}.

Global Instance: Params (@bi_exist) 2 := {}.

Global Instance: Params (@bi_sep) 1 := {}.

Global Instance: Params (@bi_wand) 1 := {}.

Global Instance: Params (@bi_persistently) 1 := {}.

Global Instance: Params (@bi_later) 1  := {}.

Global Argumentsbi_car : simpl never.

Global Argumentsbi_dist : simpl never.

Global Argumentsbi_equiv : simpl never.

Global Argumentsbi_entails {PROP} _ _ : simpl never, rename.

Global Argumentsbi_emp {PROP} : simpl never, rename.

Global Argumentsbi_pure {PROP} _%_stdpp : simpl never, rename.

Global Argumentsbi_and {PROP} _ _ : simpl never, rename.

Global Argumentsbi_or {PROP} _ _ : simpl never, rename.

Global Argumentsbi_impl {PROP} _ _ : simpl never, rename.

Global Argumentsbi_forall {PROP _} _%_I : simpl never, rename.

Global Argumentsbi_exist {PROP _} _%_I : simpl never, rename.

Global Argumentsbi_sep {PROP} _ _ : simpl never, rename.

Global Argumentsbi_wand {PROP} _ _ : simpl never, rename.

Global Argumentsbi_persistently {PROP} _ : simpl never, rename.

Global Argumentsbi_later {PROP} _ : simpl never, rename.

Global HintExtern 0 (bi_entails _ _) => reflexivity : core.

Global Instancebi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) | 170 := {}.

Global Instancebi_inhabited {PROP : bi} : Inhabited PROP := populate (bi_pure True).

Definition bi_emp_valid{PROP : bi} (P : PROP) : Prop := emp ⊢ P.

Global Argumentsbi_emp_valid {_} _%_I : simpl never.

Global TypeclassesOpaque bi_emp_valid.

Global Instanceentails_po : PreOrder (@bi_entails PROP).
Proof. eapply bi_mixin_entails_po, bi_bi_mixin. Qed.

Lemma equiv_entailsP Q : P ≡ Q ↔ (P ⊢ Q) ∧ (Q ⊢ P).
Proof. eapply bi_mixin_equiv_entails, bi_bi_mixin. Qed.

Global Instancepure_ne n : Proper (iff ==> dist n) (@bi_pure PROP).
Proof. eapply bi_mixin_pure_ne, bi_bi_mixin. Qed.

Global Instanceand_ne : NonExpansive2 (@bi_and PROP).
Proof. eapply bi_mixin_and_ne, bi_bi_mixin. Qed.

Global Instanceor_ne : NonExpansive2 (@bi_or PROP).
Proof. eapply bi_mixin_or_ne, bi_bi_mixin. Qed.

Global Instanceimpl_ne : NonExpansive2 (@bi_impl PROP).
Proof. eapply bi_mixin_impl_ne, bi_bi_mixin. Qed.

Global Instanceforall_ne A n :
  Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_forall PROP A).
Proof. eapply bi_mixin_forall_ne, bi_bi_mixin. Qed.

Global Instanceexist_ne A n :
  Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_exist PROP A).
Proof. eapply bi_mixin_exist_ne, bi_bi_mixin. Qed.

Global Instancesep_ne : NonExpansive2 (@bi_sep PROP).
Proof. eapply bi_mixin_sep_ne, bi_bi_mixin. Qed.

Global Instancewand_ne : NonExpansive2 (@bi_wand PROP).
Proof. eapply bi_mixin_wand_ne, bi_bi_mixin. Qed.

Global Instancepersistently_ne : NonExpansive (@bi_persistently PROP).
Proof. eapply bi_mixin_persistently_ne, bi_bi_persistently_mixin. Qed.

Lemma pure_intro(φ : Prop) P : φ → P ⊢ ⌜ φ ⌝.
Proof. eapply bi_mixin_pure_intro, bi_bi_mixin. Qed.

Lemma pure_elim'(φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P.
Proof. eapply bi_mixin_pure_elim', bi_bi_mixin. Qed.

Lemma and_elim_lP Q : P ∧ Q ⊢ P.
Proof. eapply bi_mixin_and_elim_l, bi_bi_mixin. Qed.

Lemma and_elim_rP Q : P ∧ Q ⊢ Q.
Proof. eapply bi_mixin_and_elim_r, bi_bi_mixin. Qed.

Lemma and_introP Q R : (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R.
Proof. eapply bi_mixin_and_intro, bi_bi_mixin. Qed.

Lemma or_intro_lP Q : P ⊢ P ∨ Q.
Proof. eapply bi_mixin_or_intro_l, bi_bi_mixin. Qed.

Lemma or_intro_rP Q : Q ⊢ P ∨ Q.
Proof. eapply bi_mixin_or_intro_r, bi_bi_mixin. Qed.

Lemma or_elimP Q R : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R.
Proof. eapply bi_mixin_or_elim, bi_bi_mixin. Qed.

Lemma impl_intro_rP Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R.
Proof. eapply bi_mixin_impl_intro_r, bi_bi_mixin. Qed.

Lemma impl_elim_l'P Q R : (P ⊢ Q → R) → P ∧ Q ⊢ R.
Proof. eapply bi_mixin_impl_elim_l', bi_bi_mixin. Qed.

Lemma forall_intro{A} P (Ψ : A → PROP) : (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a.
Proof. eapply bi_mixin_forall_intro, bi_bi_mixin. Qed.

Lemma forall_elim{A} {Ψ : A → PROP} a : (∀ a, Ψ a) ⊢ Ψ a.
Proof. eapply (bi_mixin_forall_elim bi_entails), bi_bi_mixin. Qed.

Lemma exist_intro{A} {Ψ : A → PROP} a : Ψ a ⊢ ∃ a, Ψ a.
Proof. eapply bi_mixin_exist_intro, bi_bi_mixin. Qed.

Lemma exist_elim{A} (Φ : A → PROP) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q.
Proof. eapply bi_mixin_exist_elim, bi_bi_mixin. Qed.

Lemma sep_monoP P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q'.
Proof. eapply bi_mixin_sep_mono, bi_bi_mixin. Qed.

Lemma emp_sep_1P : P ⊢ emp ∗ P.
Proof. eapply bi_mixin_emp_sep_1, bi_bi_mixin. Qed.

Lemma emp_sep_2P : emp ∗ P ⊢ P.
Proof. eapply bi_mixin_emp_sep_2, bi_bi_mixin. Qed.

Lemma sep_comm'P Q : P ∗ Q ⊢ Q ∗ P.
Proof. eapply (bi_mixin_sep_comm' bi_entails), bi_bi_mixin. Qed.

Lemma sep_assoc'P Q R : (P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R).
Proof. eapply bi_mixin_sep_assoc', bi_bi_mixin. Qed.

Lemma wand_intro_rP Q R : (P ∗ Q ⊢ R) → P ⊢ Q -∗ R.
Proof. eapply bi_mixin_wand_intro_r, bi_bi_mixin. Qed.

Lemma wand_elim_l'P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R.
Proof. eapply bi_mixin_wand_elim_l', bi_bi_mixin. Qed.

Lemma persistently_monoP Q : (P ⊢ Q) → <pers> P ⊢ <pers> Q.
Proof. eapply bi_mixin_persistently_mono, bi_bi_persistently_mixin. Qed.

Lemma persistently_idemp_2P : <pers> P ⊢ <pers> <pers> P.
Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_persistently_mixin. Qed.

Lemma persistently_emp_2: emp ⊢@{PROP} <pers> emp.
Proof. eapply bi_mixin_persistently_emp_2, bi_bi_persistently_mixin. Qed.

Lemma persistently_and_2(P Q : PROP) :
  ((<pers> P) ∧ (<pers> Q)) ⊢ <pers> (P ∧ Q).
Proof. eapply bi_mixin_persistently_and_2, bi_bi_persistently_mixin. Qed.

Lemma persistently_exist_1{A} (Ψ : A → PROP) :
  <pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a).
Proof. eapply bi_mixin_persistently_exist_1, bi_bi_persistently_mixin. Qed.

Lemma persistently_absorbingP Q : <pers> P ∗ Q ⊢ <pers> P.
Proof.
  eapply (bi_mixin_persistently_absorbing bi_entails), bi_bi_persistently_mixin.
Qed.

Lemma persistently_and_sep_elimP Q : <pers> P ∧ Q ⊢ P ∗ Q.
Proof.
  eapply (bi_mixin_persistently_and_sep_elim bi_entails), bi_bi_persistently_mixin.
Qed.

Global Instancelater_ne : NonExpansive (@bi_later PROP).
Proof. eapply bi_mixin_later_ne, bi_bi_later_mixin. Qed.

Lemma later_monoP Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
Proof. eapply bi_mixin_later_mono, bi_bi_later_mixin. Qed.

Lemma later_introP : P ⊢ ▷ P.
Proof. eapply bi_mixin_later_intro, bi_bi_later_mixin. Qed.

Lemma later_forall_2{A} (Φ : A → PROP) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a.
Proof. eapply bi_mixin_later_forall_2, bi_bi_later_mixin. Qed.

Lemma later_exist_false{A} (Φ : A → PROP) :
  (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a).
Proof. eapply bi_mixin_later_exist_false, bi_bi_later_mixin. Qed.

Lemma later_sep_1P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q.
Proof. eapply bi_mixin_later_sep_1, bi_bi_later_mixin. Qed.

Lemma later_sep_2P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q).
Proof. eapply bi_mixin_later_sep_2, bi_bi_later_mixin. Qed.

Lemma later_persistently_1P : ▷ <pers> P ⊢ <pers> ▷ P.
Proof. eapply (bi_mixin_later_persistently_1 bi_entails), bi_bi_later_mixin. Qed.

Lemma later_persistently_2P : <pers> ▷ P ⊢ ▷ <pers> P.
Proof. eapply (bi_mixin_later_persistently_2 bi_entails), bi_bi_later_mixin. Qed.

Lemma later_false_emP : ▷ P ⊢ ▷ False ∨ (▷ False → P).
Proof. eapply bi_mixin_later_false_em, bi_bi_later_mixin. Qed.