modality_instances.v 2.6 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26
From iris.bi Require Import bi.
From iris.proofmode Require Export classes.
Set Default Proof Using "Type".
Import bi.

Section bi_modalities.
  Context {PROP : bi}.

  Lemma modality_persistently_mixin :
    modality_mixin (@bi_persistently PROP) MIEnvId MIEnvClear.
  Proof.
    split; simpl; eauto using equiv_entails_sym, persistently_intro,
      persistently_mono, persistently_sep_2 with typeclass_instances.
  Qed.
  Definition modality_persistently :=
    Modality _ modality_persistently_mixin.

  Lemma modality_affinely_mixin :
    modality_mixin (@bi_affinely PROP) MIEnvId (MIEnvForall Affine).
  Proof.
    split; simpl; eauto using equiv_entails_sym, affinely_intro, affinely_mono,
      affinely_sep_2 with typeclass_instances.
  Qed.
  Definition modality_affinely :=
    Modality _ modality_affinely_mixin.

27
  Lemma modality_intuitionistically_mixin :
Ralf Jung's avatar
Ralf Jung committed
28
    modality_mixin (@bi_intuitionistically PROP) MIEnvId MIEnvIsEmpty.
29
  Proof.
30 31 32
    split; simpl; eauto using equiv_entails_sym, intuitionistically_emp,
      affinely_mono, persistently_mono, intuitionistically_idemp,
      intuitionistically_sep_2 with typeclass_instances.
33
  Qed.
34 35
  Definition modality_intuitionistically :=
    Modality _ modality_intuitionistically_mixin.
36

37 38
  Lemma modality_embed_mixin `{BiEmbed PROP PROP'} :
    modality_mixin (@embed PROP PROP' _)
39 40 41
      (MIEnvTransform IntoEmbed) (MIEnvTransform IntoEmbed).
  Proof.
    split; simpl; split_and?;
Robbert Krebbers's avatar
Robbert Krebbers committed
42 43
      eauto using equiv_entails_sym, embed_emp_2, embed_sep, embed_and.
    - intros P Q. rewrite /IntoEmbed=> ->. by rewrite embed_intuitionistically_2.
44 45
    - by intros P Q ->.
  Qed.
46
  Definition modality_embed `{BiEmbed PROP PROP'} :=
47 48 49 50 51 52
    Modality _ modality_embed_mixin.
End bi_modalities.

Section sbi_modalities.
  Context {PROP : sbi}.

Robbert Krebbers's avatar
Robbert Krebbers committed
53 54 55 56 57 58 59 60 61
  Lemma modality_plainly_mixin `{BiPlainly PROP} :
    modality_mixin (@plainly PROP _) (MIEnvForall Plain) MIEnvClear.
  Proof.
    split; simpl; split_and?; eauto using equiv_entails_sym, plainly_intro,
      plainly_mono, plainly_and, plainly_sep_2 with typeclass_instances.
  Qed.
  Definition modality_plainly `{BiPlainly PROP} :=
    Modality _ modality_plainly_mixin.

62 63 64 65 66 67
  Lemma modality_laterN_mixin n :
    modality_mixin (@sbi_laterN PROP n)
      (MIEnvTransform (MaybeIntoLaterN false n)) (MIEnvTransform (MaybeIntoLaterN false n)).
  Proof.
    split; simpl; split_and?; eauto using equiv_entails_sym, laterN_intro,
      laterN_mono, laterN_and, laterN_sep with typeclass_instances.
68
    rewrite /MaybeIntoLaterN=> P Q ->. by rewrite laterN_intuitionistically_2.
69 70 71 72
  Qed.
  Definition modality_laterN n :=
    Modality _ (modality_laterN_mixin n).
End sbi_modalities.