(* iris/proofmode/class_instances_frame.v *)
From iris.bi Require Import telescopes
From iris.proofmode Require Import classes classes_make
From iris.prelude Require Import options
FromPure a Q φ → Frame true ⌜φ⌝ Q emp | 2
FromPure a Q φ →

Global Instanceframe_here_absorbing p R :
  QuickAbsorbing R → Frame p R R True | 0.
Proof.
  rewrite /QuickAbsorbing /Frame. intros.
  by rewrite intuitionistically_if_elim sep_elim_l.
Qed.

Global Instanceframe_here p R : Frame p R R emp | 1.
Proof. intros. by rewrite /Frame intuitionistically_if_elim sep_elim_l. Qed.

Global Instanceframe_affinely_here_absorbing p R :
  QuickAbsorbing R → Frame p (<affine> R) R True | 0.
Proof.
  rewrite /QuickAbsorbing /Frame. intros.
  rewrite intuitionistically_if_elim affinely_elim. apply sep_elim_l, _.
Qed.

Global Instanceframe_affinely_here p R : Frame p (<affine> R) R emp | 1.
Proof.
  intros. rewrite /Frame intuitionistically_if_elim affinely_elim.
  apply sep_elim_l, _.
Qed.

Global Instanceframe_here_pure_persistent a φ Q :
  FromPure a Q φ → Frame true ⌜φ⌝ Q emp | 2.
Proof.
  rewrite /FromPure /Frame /= => <-. rewrite right_id.
  by rewrite -affinely_affinely_if intuitionistically_affinely.
Qed.

Global Instanceframe_here_pure a φ Q :
  FromPure a Q φ →
  TCOr (TCEq a false) (BiAffine PROP) →
  Frame false ⌜φ⌝ Q emp | 2.
Proof.
  rewrite /FromPure /Frame => <- [->|?] /=.
  - by rewrite right_id.
  - by rewrite right_id -affinely_affinely_if affine_affinely.
Qed.

Global Instanceframe_embed `{!BiEmbed PROP PROP'} p P Q (Q' : PROP') R :
  Frame p R P Q → MakeEmbed Q Q' →
  Frame p ⎡R⎤ ⎡P⎤ Q' | 2.
Proof.
  rewrite /Frame /MakeEmbed => <- <-.
  rewrite embed_sep embed_intuitionistically_if_2 => //.
Qed.

Global Instanceframe_pure_embed `{!BiEmbed PROP PROP'} p P Q (Q' : PROP') φ :
  Frame p ⌜φ⌝ P Q → MakeEmbed Q Q' →
  Frame p ⌜φ⌝ ⎡P⎤ Q' | 2.
Proof. rewrite /Frame /MakeEmbed -embed_pure. apply (frame_embed p P Q). Qed.

Global Instanceframe_sep_persistent_l progress R P1 P2 Q1 Q2 Q' :
  Frame true R P1 Q1 →
  MaybeFrame true R P2 Q2 progress →
  MakeSep Q1 Q2 Q' →
  Frame true R (P1 ∗ P2) Q' | 9.
Proof.
  rewrite /Frame /MaybeFrame' /MakeSep /= => <- [<-] <-.
  rewrite {1}(intuitionistically_sep_dup R).
  by rewrite !assoc -(assoc _ _ _ Q1) -(comm _ Q1) assoc -(comm _ Q1).
Qed.

Global Instanceframe_sep_l R P1 P2 Q Q' :
  Frame false R P1 Q → MakeSep Q P2 Q' → Frame false R (P1 ∗ P2) Q' | 9.
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.

Global Instanceframe_sep_r p R P1 P2 Q Q' :
  Frame p R P2 Q → MakeSep P1 Q Q' → Frame p R (P1 ∗ P2) Q' | 10.
Proof.
  rewrite /Frame /MakeSep => <- <-. by rewrite assoc -(comm _ P1) assoc.
Qed.

Global Instanceframe_big_sepL_cons {A} p (Φ : nat → A → PROP) R Q l x l' :
  IsCons l x l' →
  Frame p R (Φ 0 x ∗ [∗ list] k ↦ y ∈ l', Φ (S k) y) Q →
  Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q | 2.
Proof. rewrite /IsCons=>->. by rewrite /Frame big_sepL_cons. Qed.

Global Instanceframe_big_sepL_app {A} p (Φ : nat → A → PROP) R Q l l1 l2 :
  IsApp l l1 l2 →
  Frame p R (([∗ list] k ↦ y ∈ l1, Φ k y) ∗
           [∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y) Q →
  Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q | 2.
Proof. rewrite /IsApp=>->. by rewrite /Frame big_sepL_app. Qed.

Global Instanceframe_big_sepL2_cons {A B} p (Φ : nat → A → B → PROP)
    R Q l1 x1 l1' l2 x2 l2' :
  IsCons l1 x1 l1' → IsCons l2 x2 l2' →
  Frame p R (Φ 0 x1 x2 ∗ [∗ list] k ↦ y1;y2 ∈ l1';l2', Φ (S k) y1 y2) Q →
  Frame p R ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) Q.
Proof. rewrite /IsCons=>-> ->. by rewrite /Frame big_sepL2_cons. Qed.

Global Instanceframe_big_sepL2_app {A B} p (Φ : nat → A → B → PROP)
    R Q l1 l1' l1'' l2 l2' l2'' :
  IsApp l1 l1' l1'' → IsApp l2 l2' l2'' →
  Frame p R (([∗ list] k ↦ y1;y2 ∈ l1';l2', Φ k y1 y2) ∗
           [∗ list] k ↦ y1;y2 ∈ l1'';l2'', Φ (length l1' + k) y1 y2) Q →
  Frame p R ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) Q.
Proof. rewrite /IsApp /Frame=>-> -> ->. apply wand_elim_l', big_sepL2_app. Qed.

Global Instanceframe_big_sepMS_disj_union `{Countable A} p (Φ : A → PROP) R Q X X1 X2 :
  IsDisjUnion X X1 X2 ->
  Frame p R (([∗ mset] y ∈ X1, Φ y) ∗ [∗ mset] y ∈ X2, Φ y) Q →
  Frame p R ([∗ mset] y ∈ X, Φ y) Q | 2.
Proof. rewrite /IsDisjUnion=>->. by rewrite /Frame big_sepMS_disj_union. Qed.

Global Instanceframe_and p progress1 progress2 R P1 P2 Q1 Q2 Q' :
  MaybeFrame p R P1 Q1 progress1 →
  MaybeFrame p R P2 Q2 progress2 →

Global Instanceframe_or_spatial progress1 progress2 R P1 P2 Q1 Q2 Q :
  MaybeFrame false R P1 Q1 progress1 →
  MaybeFrame false R P2 Q2 progress2 →

Global Instanceframe_or_persistent progress1 progress2 R P1 P2 Q1 Q2 Q :
  MaybeFrame true R P1 Q1 progress1 →
  MaybeFrame true R P2 Q2 progress2 →

Global Instanceframe_wand p R P1 P2 Q2 :
  (FrameInstantiateExistDisabled → Frame p R P2 Q2) →
  Frame p R (P1 -∗ P2) (P1 -∗ Q2) | 2.
Proof.
  rewrite /Frame=> /(_ ltac:(constructor)) ?. apply wand_intro_l.
  by rewrite assoc (comm _ P1) -assoc wand_elim_r.
Qed.

Global Instanceframe_affinely p R P Q Q' :
  TCOr (TCEq p true) (QuickAffine R) →
  Frame p R P Q → MakeAffinely Q Q' →
  Frame p R (<affine> P) Q'.
Proof.
  rewrite /QuickAffine /Frame /MakeAffinely=> -[->|?] <- <- /=;
    by rewrite -{1}(affine_affinely (_ R)) affinely_sep_2.
Qed.

Global Instanceframe_intuitionistically R P Q Q' :
  Frame true R P Q → MakeIntuitionistically Q Q' →
  Frame true R (□ P) Q' | 2.
Proof.
  rewrite /Frame /MakeIntuitionistically=> <- <- /=.
  rewrite -intuitionistically_sep_2 intuitionistically_idemp //.
Qed.

Global Instanceframe_absorbingly p R P Q Q' :
  Frame p R P Q → MakeAbsorbingly Q Q' →
  Frame p R (<absorb> P) Q' | 2.
Proof.
  rewrite /Frame /MakeAbsorbingly=> <- <- /=. by rewrite absorbingly_sep_r.
Qed.

Global Instanceframe_persistently R P Q Q' :
  Frame true R P Q → MakePersistently Q Q' →
  Frame true R (<pers> P) Q' | 2.
Proof.
  rewrite /Frame /MakePersistently=> <- <- /=.
  rewrite -persistently_and_intuitionistically_sep_l.
  by rewrite -persistently_sep_2 -persistently_and_sep_l_1
    persistently_affinely_elim persistently_idemp.
Qed.

Local Lemmaframe_exist_helper {A} p R (Φ : A → PROP)
    {C} (g : C → A) (Ψ : C → PROP) :
  (∀ c, Frame p R (Φ $ g c) (Ψ c)) →
  Frame p R (∃ a, Φ a) (∃ c, Ψ c).
Proof.
  rewrite /Frame=> HΨ. rewrite sep_exist_l.
  apply bi.exist_elim=> c. rewrite HΨ. apply exist_intro.
Qed.

Inductive GatherEvarsEq{A} (x : A) : A → Prop :=
  GatherEvarsEq_refl : GatherEvarsEq x x.
Existing Class GatherEvarsEq.

Global ExistingInstance Build_FrameExistRequirements.

Inductive TCCbnTele{A} (x : A) : A → Prop :=
  TCCbnTele_refl : TCCbnTele x x.
Existing Class TCCbnTele.

Global HintMode TCCbnTele ! - - : typeclass_instances.

Global Instanceframe_exist {A} p R (Φ : A → PROP)
    (TT : tele) (g : TT → A) (Ψ : TT → PROP) Q :
  FrameInstantiateExistEnabled →
  (∀ c, FrameExistRequirements p R Φ (g c) (Ψ c)) →
  TCCbnTele (∃.. c, Ψ c)%I Q →
  Frame p R (∃ a, Φ a) Q.
Proof.
  move=> _ H <-. rewrite /Frame bi_texist_exist.
  eapply frame_exist_helper=> c.
  by specialize (H c) as [a G HG -> ->].
Qed.

Global Instanceframe_exist_no_instantiate {A} p R (Φ Ψ : A → PROP) :
  FrameInstantiateExistDisabled →
  (∀ a, Frame p R (Φ a) (Ψ a)) →
  Frame p R (∃ a, Φ a) (∃ a, Ψ a).
Proof. move=> _ H. eapply frame_exist_helper, H. Qed.

Global Instanceframe_texist {TT : tele} p R (Φ Ψ : TT → PROP) :
  (∀ x, Frame p R (Φ x) (Ψ x)) → Frame p R (∃.. x, Φ x) (∃.. x, Ψ x) | 2.
Proof. rewrite /Frame !bi_texist_exist. apply frame_exist_helper. Qed.

Global Instanceframe_forall {A} p R (Φ Ψ : A → PROP) :
  (FrameInstantiateExistDisabled → ∀ a, Frame p R (Φ a) (Ψ a)) →
  Frame p R (∀ x, Φ x) (∀ x, Ψ x) | 2.
Proof.
  rewrite /Frame=> /(_ ltac:(constructor)) ?.
  by rewrite sep_forall_l; apply forall_mono.
Qed.

Global Instanceframe_tforall {TT : tele} p R (Φ Ψ : TT → PROP) :
  (FrameInstantiateExistDisabled → (∀ x, Frame p R (Φ x) (Ψ x))) →
  Frame p R (∀.. x, Φ x) (∀.. x, Ψ x) | 2.
Proof. rewrite /Frame !bi_tforall_forall. apply frame_forall. Qed.

Global Instanceframe_impl_persistent R P1 P2 Q2 :
  (FrameInstantiateExistDisabled → Frame true R P2 Q2) →
  Frame true R (P1 → P2) (P1 → Q2) | 2.
Proof.
  rewrite /Frame /= => /(_ ltac:(constructor)) ?. apply impl_intro_l.
  by rewrite -persistently_and_intuitionistically_sep_l assoc (comm _ P1) -assoc impl_elim_r
             persistently_and_intuitionistically_sep_l.
Qed.

Global Instanceframe_impl R P1 P2 Q2 :
  Persistent P1 → QuickAbsorbing P1 →
  (FrameInstantiateExistDisabled → Frame false R P2 Q2) →
  Frame false R (P1 → P2) (P1 → Q2).
Proof.
  rewrite /Frame /QuickAbsorbing /==> ?? /(_ ltac:(constructor)) ?.
  apply impl_intro_l.
  rewrite {1}(persistent P1) persistently_and_intuitionistically_sep_l assoc.
  rewrite (comm _ (□ P1)%I) -assoc -persistently_and_intuitionistically_sep_l.
  rewrite persistently_elim impl_elim_r //.
Qed.

Global Instanceframe_eq_embed `{!BiEmbed PROP PROP', !Sbi PROP,
    !Sbi PROP', !BiEmbedSbi PROP PROP'}
    p P Q (Q' : PROP') {A : ofe} (a b : A) :
  Frame p (a ≡ b) P Q → MakeEmbed Q Q' →
  Frame p (a ≡ b) ⎡P⎤ Q'.
Proof. rewrite /Frame /MakeEmbed -embed_internal_eq. apply (frame_embed p P Q). Qed.

Global Instanceframe_later p R R' P Q Q' :
  TCNoBackTrack (MaybeIntoLaterN true 1 R' R) →
  Frame p R P Q → MakeLaterN 1 Q Q' →
  Frame p R' (▷ P) Q'.
Proof.
  rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
  by rewrite later_intuitionistically_if_2 later_sep.
Qed.

Global Instanceframe_laterN p n R R' P Q Q' :
  TCNoBackTrack (MaybeIntoLaterN true n R' R) →
  Frame p R P Q → MakeLaterN n Q Q' →
  Frame p R' (▷^n P) Q'.
Proof.
  rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
  by rewrite laterN_intuitionistically_if_2 laterN_sep.
Qed.

Global Instanceframe_bupd `{!BiBUpd PROP} p R P Q :
  Frame p R P Q → Frame p R (|==> P) (|==> Q) | 2.
Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.

Global Instanceframe_fupd `{!BiFUpd PROP} p E1 E2 R P Q :
  Frame p R P Q → Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 2.
Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.

Global Instanceframe_except_0 p R P Q Q' :
  Frame p R P Q → MakeExcept0 Q Q' →
  Frame p R (◇ P) Q' | 2.
Proof.
  rewrite /Frame /MakeExcept0=><- <-.
  by rewrite except_0_sep -(except_0_intro (□?p R)).
Qed.

Ltac solve_gather_evars_eq:=
  lazymatch goal with
  | |- GatherEvarsEq ?a (?g ?c) =>
    let rec retcon_tele T arg :=

Global HintExtern 0 (GatherEvarsEq _ _) =>
  solve_gather_evars_eq : typeclass_instances.

Global HintExtern 0 (TCCbnTele _ _) =>
  cbn [bi_texist tele_fold tele_bind tele_arg_head tele_arg_tail];
  notypeclasses refine (TCCbnTele_refl _) : typeclass_instances.