(* iris/proofmode/class_instances_make.v *)
From iris.proofmode Require Export classes_make
From iris.prelude Require Import options

Global Instancebi_affine_quick_affine P : BiAffine PROP → QuickAffine P.
Proof. rewrite /QuickAffine. apply _. Qed.

Global InstanceFalse_quick_affine : @QuickAffine PROP False.
Proof. rewrite /QuickAffine. apply _. Qed.

Global Instanceemp_quick_affine : @QuickAffine PROP emp.
Proof. rewrite /QuickAffine. apply _. Qed.

Global Instanceaffinely_quick_affine P : QuickAffine (<affine> P).
Proof. rewrite /QuickAffine. apply _. Qed.

Global Instanceintuitionistically_quick_affine P : QuickAffine (□ P).
Proof. rewrite /QuickAffine. apply _. Qed.

Global Instancebi_affine_quick_absorbing P : BiAffine PROP → QuickAbsorbing P.
Proof. rewrite /QuickAbsorbing. apply _. Qed.

Global Instancepure_quick_absorbing φ : @QuickAbsorbing PROP ⌜ φ ⌝.
Proof. rewrite /QuickAbsorbing. apply _. Qed.

Global Instanceabsorbingly_quick_absorbing P : QuickAbsorbing (<absorb> P).
Proof. rewrite /QuickAbsorbing. apply _. Qed.

Global Instancepersistently_quick_absorbing P : QuickAbsorbing (<pers> P).
Proof. rewrite /QuickAbsorbing. apply _. Qed.

Global Instancemake_embed_pure {PROP'} `{!BiEmbed PROP PROP'} φ :
  KnownMakeEmbed (PROP:=PROP) ⌜φ⌝ ⌜φ⌝.
Proof. apply embed_pure. Qed.

Global Instancemake_embed_emp {PROP'} `{!BiEmbed PROP PROP'} `{!BiEmbedEmp PROP PROP'} :
  KnownMakeEmbed (PROP:=PROP) emp emp.
Proof. apply embed_emp. Qed.

Global Instancemake_embed_default {PROP'} `{!BiEmbed PROP PROP'} P :
  MakeEmbed P ⎡P⎤ | 100.
Proof. by rewrite /MakeEmbed. Qed.

Global Instancemake_sep_emp_l P : KnownLMakeSep emp P P.
Proof. apply left_id, _. Qed.

Global Instancemake_sep_emp_r P : KnownRMakeSep P emp P.
Proof. apply right_id, _. Qed.

Global Instancemake_sep_true_l P : QuickAbsorbing P → KnownLMakeSep True P P.
Proof. rewrite /QuickAbsorbing /KnownLMakeSep /MakeSep=> ?. by apply True_sep. Qed.

Global Instancemake_sep_true_r P : QuickAbsorbing P →  KnownRMakeSep P True P.
Proof. rewrite /QuickAbsorbing /KnownLMakeSep /MakeSep=> ?. by apply sep_True. Qed.

Global Instancemake_sep_default P Q : MakeSep P Q (P ∗ Q) | 100.
Proof. by rewrite /MakeSep. Qed.

Global Instancemake_and_true_l P : KnownLMakeAnd True P P.
Proof. apply left_id, _. Qed.

Global Instancemake_and_true_r P : KnownRMakeAnd P True P.
Proof. by rewrite /KnownRMakeAnd /MakeAnd right_id. Qed.

Global Instancemake_and_emp_l P : QuickAffine P → KnownLMakeAnd emp P P.
Proof. apply emp_and. Qed.

Global Instancemake_and_emp_r P : QuickAffine P → KnownRMakeAnd P emp P.
Proof. apply and_emp. Qed.

Global Instancemake_and_false_l P : KnownLMakeAnd False P False.
Proof. apply left_absorb, _. Qed.

Global Instancemake_and_false_r P : KnownRMakeAnd P False False.
Proof. by rewrite /KnownRMakeAnd /MakeAnd right_absorb. Qed.

Global Instancemake_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
Proof. by rewrite /MakeAnd. Qed.

Global Instancemake_or_true_l P : KnownLMakeOr True P True.
Proof. apply left_absorb, _. Qed.

Global Instancemake_or_true_r P : KnownRMakeOr P True True.
Proof. by rewrite /KnownRMakeOr /MakeOr right_absorb. Qed.

Global Instancemake_or_emp_l P : QuickAffine P → KnownLMakeOr emp P emp.
Proof. apply emp_or. Qed.

Global Instancemake_or_emp_r P : QuickAffine P → KnownRMakeOr P emp emp.
Proof. apply or_emp. Qed.

Global Instancemake_or_false_l P : KnownLMakeOr False P P.
Proof. apply left_id, _. Qed.

Global Instancemake_or_false_r P : KnownRMakeOr P False P.
Proof. by rewrite /KnownRMakeOr /MakeOr right_id. Qed.

Global Instancemake_or_default P Q : MakeOr P Q (P ∨ Q) | 100.
Proof. by rewrite /MakeOr. Qed.

Global Instancemake_affinely_affine P :
  QuickAffine P → KnownMakeAffinely P P | 0.
Proof. apply affine_affinely. Qed.

Global Instancemake_affinely_True : @KnownMakeAffinely PROP True emp | 1.
Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp. Qed.

Global Instancemake_affinely_default P : MakeAffinely P (<affine> P) | 100.
Proof. by rewrite /MakeAffinely. Qed.

Global Instancemake_absorbingly_absorbing P :
  QuickAbsorbing P → KnownMakeAbsorbingly P P | 0.
Proof. apply absorbing_absorbingly. Qed.

Global Instancemake_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 1.
Proof.
  by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly -absorbingly_emp_True.
Qed.

Global Instancemake_absorbingly_default P : MakeAbsorbingly P (<absorb> P) | 100.
Proof. by rewrite /MakeAbsorbingly. Qed.

Global Instancemake_persistently_emp :
  @KnownMakePersistently PROP emp True | 0.
Proof.
  by rewrite /KnownMakePersistently /MakePersistently
     -persistently_True_emp persistently_pure.
Qed.

Global Instancemake_persistently_True :
  @KnownMakePersistently PROP True True | 0.
Proof. by rewrite /KnownMakePersistently /MakePersistently persistently_pure. Qed.

Global Instancemake_persistently_default P :
  MakePersistently P (<pers> P) | 100.
Proof. by rewrite /MakePersistently. Qed.

Global Instancemake_intuitionistically_emp :
  @KnownMakeIntuitionistically PROP emp emp | 0.
Proof.
  by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
    intuitionistically_emp.
Qed.

Global Instancemake_intuitionistically_True_affine :
  BiAffine PROP →
  @KnownMakeIntuitionistically PROP True True | 0.
Proof.
  intros. rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
    intuitionistically_True_emp True_emp //.
Qed.

Global Instancemake_intuitionistically_True :
  @KnownMakeIntuitionistically PROP True emp | 1.
Proof.
  by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
    intuitionistically_True_emp.
Qed.

Global Instancemake_intuitionistically_default P :
  MakeIntuitionistically P (□ P) | 100.
Proof. by rewrite /MakeIntuitionistically. Qed.

Global Instancemake_laterN_true n : @KnownMakeLaterN PROP n True True | 0.
Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_True. Qed.

Global Instancemake_laterN_emp `{!BiAffine PROP} n :
  @KnownMakeLaterN PROP n emp emp | 0.
Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_emp. Qed.

Global Instancemake_laterN_default n P : MakeLaterN n P (▷^n P) | 100.
Proof. by rewrite /MakeLaterN. Qed.

Global Instancemake_except_0_True : @KnownMakeExcept0 PROP True True.
Proof. by rewrite /KnownMakeExcept0 /MakeExcept0 except_0_True. Qed.

Global Instancemake_except_0_default P : MakeExcept0 P (◇ P) | 100.
Proof. by rewrite /MakeExcept0. Qed.