Library iris.proofmode.class_instances_make
IMPORTANT: Read the comment in classes_make about the "constant time"
requirements of these instances.
From iris.proofmode Require Export classes_make.
From iris.prelude Require Import options.
Import bi.
Section class_instances_make.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
From iris.prelude Require Import options.
Import bi.
Section class_instances_make.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
Affine
Global Instance bi_affine_quick_affine P : BiAffine PROP → QuickAffine P.
Proof. rewrite /QuickAffine. apply _. Qed.
Global Instance False_quick_affine : @QuickAffine PROP False.
Proof. rewrite /QuickAffine. apply _. Qed.
Global Instance emp_quick_affine : @QuickAffine PROP emp.
Proof. rewrite /QuickAffine. apply _. Qed.
Global Instance affinely_quick_affine P : QuickAffine (<affine> P).
Proof. rewrite /QuickAffine. apply _. Qed.
Global Instance intuitionistically_quick_affine P : QuickAffine (□ P).
Proof. rewrite /QuickAffine. apply _. Qed.
Proof. rewrite /QuickAffine. apply _. Qed.
Global Instance False_quick_affine : @QuickAffine PROP False.
Proof. rewrite /QuickAffine. apply _. Qed.
Global Instance emp_quick_affine : @QuickAffine PROP emp.
Proof. rewrite /QuickAffine. apply _. Qed.
Global Instance affinely_quick_affine P : QuickAffine (<affine> P).
Proof. rewrite /QuickAffine. apply _. Qed.
Global Instance intuitionistically_quick_affine P : QuickAffine (□ P).
Proof. rewrite /QuickAffine. apply _. Qed.
Absorbing
Global Instance bi_affine_quick_absorbing P : BiAffine PROP → QuickAbsorbing P.
Proof. rewrite /QuickAbsorbing. apply _. Qed.
Global Instance pure_quick_absorbing φ : @QuickAbsorbing PROP ⌜ φ ⌝.
Proof. rewrite /QuickAbsorbing. apply _. Qed.
Global Instance absorbingly_quick_absorbing P : QuickAbsorbing (<absorb> P).
Proof. rewrite /QuickAbsorbing. apply _. Qed.
Global Instance persistently_quick_absorbing P : QuickAbsorbing (<pers> P).
Proof. rewrite /QuickAbsorbing. apply _. Qed.
Proof. rewrite /QuickAbsorbing. apply _. Qed.
Global Instance pure_quick_absorbing φ : @QuickAbsorbing PROP ⌜ φ ⌝.
Proof. rewrite /QuickAbsorbing. apply _. Qed.
Global Instance absorbingly_quick_absorbing P : QuickAbsorbing (<absorb> P).
Proof. rewrite /QuickAbsorbing. apply _. Qed.
Global Instance persistently_quick_absorbing P : QuickAbsorbing (<pers> P).
Proof. rewrite /QuickAbsorbing. apply _. Qed.
Embed
Global Instance make_embed_pure {PROP'} `{!BiEmbed PROP PROP'} φ :
KnownMakeEmbed (PROP:=PROP) ⌜φ⌝ ⌜φ⌝.
Proof. apply embed_pure. Qed.
Global Instance make_embed_emp {PROP'} `{!BiEmbed PROP PROP'} `{!BiEmbedEmp PROP PROP'} :
KnownMakeEmbed (PROP:=PROP) emp emp.
Proof. apply embed_emp. Qed.
Global Instance make_embed_default {PROP'} `{!BiEmbed PROP PROP'} P :
MakeEmbed P ⎡P⎤ | 100.
Proof. by rewrite /MakeEmbed. Qed.
KnownMakeEmbed (PROP:=PROP) ⌜φ⌝ ⌜φ⌝.
Proof. apply embed_pure. Qed.
Global Instance make_embed_emp {PROP'} `{!BiEmbed PROP PROP'} `{!BiEmbedEmp PROP PROP'} :
KnownMakeEmbed (PROP:=PROP) emp emp.
Proof. apply embed_emp. Qed.
Global Instance make_embed_default {PROP'} `{!BiEmbed PROP PROP'} P :
MakeEmbed P ⎡P⎤ | 100.
Proof. by rewrite /MakeEmbed. Qed.
Sep
Global Instance make_sep_emp_l P : KnownLMakeSep emp P P.
Proof. apply left_id, _. Qed.
Global Instance make_sep_emp_r P : KnownRMakeSep P emp P.
Proof. apply right_id, _. Qed.
Global Instance make_sep_true_l P : QuickAbsorbing P → KnownLMakeSep True P P.
Proof. rewrite /QuickAbsorbing /KnownLMakeSep /MakeSep⇒ ?. by apply True_sep. Qed.
Global Instance make_sep_true_r P : QuickAbsorbing P → KnownRMakeSep P True P.
Proof. rewrite /QuickAbsorbing /KnownLMakeSep /MakeSep⇒ ?. by apply sep_True. Qed.
Global Instance make_sep_default P Q : MakeSep P Q (P ∗ Q) | 100.
Proof. by rewrite /MakeSep. Qed.
Proof. apply left_id, _. Qed.
Global Instance make_sep_emp_r P : KnownRMakeSep P emp P.
Proof. apply right_id, _. Qed.
Global Instance make_sep_true_l P : QuickAbsorbing P → KnownLMakeSep True P P.
Proof. rewrite /QuickAbsorbing /KnownLMakeSep /MakeSep⇒ ?. by apply True_sep. Qed.
Global Instance make_sep_true_r P : QuickAbsorbing P → KnownRMakeSep P True P.
Proof. rewrite /QuickAbsorbing /KnownLMakeSep /MakeSep⇒ ?. by apply sep_True. Qed.
Global Instance make_sep_default P Q : MakeSep P Q (P ∗ Q) | 100.
Proof. by rewrite /MakeSep. Qed.
And
Global Instance make_and_true_l P : KnownLMakeAnd True P P.
Proof. apply left_id, _. Qed.
Global Instance make_and_true_r P : KnownRMakeAnd P True P.
Proof. by rewrite /KnownRMakeAnd /MakeAnd right_id. Qed.
Global Instance make_and_emp_l P : QuickAffine P → KnownLMakeAnd emp P P.
Proof. apply emp_and. Qed.
Global Instance make_and_emp_r P : QuickAffine P → KnownRMakeAnd P emp P.
Proof. apply and_emp. Qed.
Global Instance make_and_false_l P : KnownLMakeAnd False P False.
Proof. apply left_absorb, _. Qed.
Global Instance make_and_false_r P : KnownRMakeAnd P False False.
Proof. by rewrite /KnownRMakeAnd /MakeAnd right_absorb. Qed.
Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
Proof. by rewrite /MakeAnd. Qed.
Proof. apply left_id, _. Qed.
Global Instance make_and_true_r P : KnownRMakeAnd P True P.
Proof. by rewrite /KnownRMakeAnd /MakeAnd right_id. Qed.
Global Instance make_and_emp_l P : QuickAffine P → KnownLMakeAnd emp P P.
Proof. apply emp_and. Qed.
Global Instance make_and_emp_r P : QuickAffine P → KnownRMakeAnd P emp P.
Proof. apply and_emp. Qed.
Global Instance make_and_false_l P : KnownLMakeAnd False P False.
Proof. apply left_absorb, _. Qed.
Global Instance make_and_false_r P : KnownRMakeAnd P False False.
Proof. by rewrite /KnownRMakeAnd /MakeAnd right_absorb. Qed.
Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
Proof. by rewrite /MakeAnd. Qed.
Or
Global Instance make_or_true_l P : KnownLMakeOr True P True.
Proof. apply left_absorb, _. Qed.
Global Instance make_or_true_r P : KnownRMakeOr P True True.
Proof. by rewrite /KnownRMakeOr /MakeOr right_absorb. Qed.
Global Instance make_or_emp_l P : QuickAffine P → KnownLMakeOr emp P emp.
Proof. apply emp_or. Qed.
Global Instance make_or_emp_r P : QuickAffine P → KnownRMakeOr P emp emp.
Proof. apply or_emp. Qed.
Global Instance make_or_false_l P : KnownLMakeOr False P P.
Proof. apply left_id, _. Qed.
Global Instance make_or_false_r P : KnownRMakeOr P False P.
Proof. by rewrite /KnownRMakeOr /MakeOr right_id. Qed.
Global Instance make_or_default P Q : MakeOr P Q (P ∨ Q) | 100.
Proof. by rewrite /MakeOr. Qed.
Proof. apply left_absorb, _. Qed.
Global Instance make_or_true_r P : KnownRMakeOr P True True.
Proof. by rewrite /KnownRMakeOr /MakeOr right_absorb. Qed.
Global Instance make_or_emp_l P : QuickAffine P → KnownLMakeOr emp P emp.
Proof. apply emp_or. Qed.
Global Instance make_or_emp_r P : QuickAffine P → KnownRMakeOr P emp emp.
Proof. apply or_emp. Qed.
Global Instance make_or_false_l P : KnownLMakeOr False P P.
Proof. apply left_id, _. Qed.
Global Instance make_or_false_r P : KnownRMakeOr P False P.
Proof. by rewrite /KnownRMakeOr /MakeOr right_id. Qed.
Global Instance make_or_default P Q : MakeOr P Q (P ∨ Q) | 100.
Proof. by rewrite /MakeOr. Qed.
Affinely
- make_affinely_affine adds no modality, but only if the argument is affine.
- make_affinely_True turns True into emp. For an affine BI this instance overlaps with make_affinely_affine, since True is affine. Since we prefer to avoid emp in goals involving affine BIs, we give make_affinely_affine a lower cost than make_affinely_True.
- make_affinely_default adds the modality. This is the default instance since it can always be used, and thus has the highest cost. (For this last point, the cost of the KnownMakeAffinely instances does not actually matter, since this is a MakeAffinely instance, i.e. an instance of a different class. What really matters is that the known_make_affinely instance has a lower cost than make_affinely_default.)
Global Instance make_affinely_affine P :
QuickAffine P → KnownMakeAffinely P P | 0.
Proof. apply affine_affinely. Qed.
Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 1.
Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp. Qed.
Global Instance make_affinely_default P : MakeAffinely P (<affine> P) | 100.
Proof. by rewrite /MakeAffinely. Qed.
Absorbingly
- make_absorbingly_absorbing adds no modality, but only if the argument is absorbing.
- make_absorbingly_emp turns emp into True. For an affine BI this instance overlaps with make_absorbingly_absorbing, since emp is absorbing. For consistency, we give this instance the same cost as make_affinely_True, but it does not really matter since goals in affine BIs typically do not contain occurrences of emp to start with.
- make_absorbingly_default adds the modality. This is the default instance since it can always be used, and thus has the highest cost. (For this last point, the cost of the KnownMakeAbsorbingly instances does not actually matter, since this is a MakeAbsorbingly instance, i.e. an instance of a different class. What really matters is that the known_make_absorbingly instance has a lower cost than make_absorbingly_default.)
Global Instance make_absorbingly_absorbing P :
QuickAbsorbing P → KnownMakeAbsorbingly P P | 0.
Proof. apply absorbing_absorbingly. Qed.
Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 1.
Proof.
by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly -absorbingly_emp_True.
Qed.
Global Instance make_absorbingly_default P : MakeAbsorbingly P (<absorb> P) | 100.
Proof. by rewrite /MakeAbsorbingly. Qed.
Persistently
Global Instance make_persistently_emp :
@KnownMakePersistently PROP emp True | 0.
Proof.
by rewrite /KnownMakePersistently /MakePersistently
-persistently_True_emp persistently_pure.
Qed.
Global Instance make_persistently_True :
@KnownMakePersistently PROP True True | 0.
Proof. by rewrite /KnownMakePersistently /MakePersistently persistently_pure. Qed.
Global Instance make_persistently_default P :
MakePersistently P (<pers> P) | 100.
Proof. by rewrite /MakePersistently. Qed.
@KnownMakePersistently PROP emp True | 0.
Proof.
by rewrite /KnownMakePersistently /MakePersistently
-persistently_True_emp persistently_pure.
Qed.
Global Instance make_persistently_True :
@KnownMakePersistently PROP True True | 0.
Proof. by rewrite /KnownMakePersistently /MakePersistently persistently_pure. Qed.
Global Instance make_persistently_default P :
MakePersistently P (<pers> P) | 100.
Proof. by rewrite /MakePersistently. Qed.
Intuitionistically
Global Instance make_intuitionistically_emp :
@KnownMakeIntuitionistically PROP emp emp | 0.
Proof.
by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
intuitionistically_emp.
Qed.
@KnownMakeIntuitionistically PROP emp emp | 0.
Proof.
by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
intuitionistically_emp.
Qed.
For affine BIs, we would prefer □ True to become True rather than emp,
so we have this instance with lower cost than the next.
Global Instance make_intuitionistically_True_affine :
BiAffine PROP →
@KnownMakeIntuitionistically PROP True True | 0.
Proof.
intros. rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
intuitionistically_True_emp True_emp //.
Qed.
Global Instance make_intuitionistically_True :
@KnownMakeIntuitionistically PROP True emp | 1.
Proof.
by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
intuitionistically_True_emp.
Qed.
Global Instance make_intuitionistically_default P :
MakeIntuitionistically P (□ P) | 100.
Proof. by rewrite /MakeIntuitionistically. Qed.
BiAffine PROP →
@KnownMakeIntuitionistically PROP True True | 0.
Proof.
intros. rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
intuitionistically_True_emp True_emp //.
Qed.
Global Instance make_intuitionistically_True :
@KnownMakeIntuitionistically PROP True emp | 1.
Proof.
by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
intuitionistically_True_emp.
Qed.
Global Instance make_intuitionistically_default P :
MakeIntuitionistically P (□ P) | 100.
Proof. by rewrite /MakeIntuitionistically. Qed.
Later
Global Instance make_laterN_true n : @KnownMakeLaterN PROP n True True | 0.
Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_True. Qed.
Global Instance make_laterN_emp `{!BiAffine PROP} n :
@KnownMakeLaterN PROP n emp emp | 0.
Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_emp. Qed.
Global Instance make_laterN_default n P : MakeLaterN n P (▷^n P) | 100.
Proof. by rewrite /MakeLaterN. Qed.
Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_True. Qed.
Global Instance make_laterN_emp `{!BiAffine PROP} n :
@KnownMakeLaterN PROP n emp emp | 0.
Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_emp. Qed.
Global Instance make_laterN_default n P : MakeLaterN n P (▷^n P) | 100.
Proof. by rewrite /MakeLaterN. Qed.
Except-0
Global Instance make_except_0_True : @KnownMakeExcept0 PROP True True.
Proof. by rewrite /KnownMakeExcept0 /MakeExcept0 except_0_True. Qed.
Global Instance make_except_0_default P : MakeExcept0 P (◇ P) | 100.
Proof. by rewrite /MakeExcept0. Qed.
End class_instances_make.
Proof. by rewrite /KnownMakeExcept0 /MakeExcept0 except_0_True. Qed.
Global Instance make_except_0_default P : MakeExcept0 P (◇ P) | 100.
Proof. by rewrite /MakeExcept0. Qed.
End class_instances_make.