Commit fbea3aa1 authored by Robbert Krebbers's avatar Robbert Krebbers

Move modality record and instances to a separate file.

parent 25ab3a07
......@@ -101,6 +101,8 @@ theories/proofmode/notation.v
theories/proofmode/classes.v
theories/proofmode/class_instances.v
theories/proofmode/monpred.v
theories/proofmode/modalities.v
theories/proofmode/modality_instances.v
theories/tests/heap_lang.v
theories/tests/one_shot.v
theories/tests/proofmode.v
......
From stdpp Require Import nat_cancel.
From iris.bi Require Import bi tactics.
From iris.proofmode Require Export classes.
From iris.proofmode Require Export modality_instances classes.
Set Default Proof Using "Type".
Import bi.
......
From iris.bi Require Export bi.
From iris.proofmode Require Export modalities.
From stdpp Require Import namespaces.
Set Default Proof Using "Type".
Import bi.
......@@ -83,156 +84,16 @@ Arguments IntoPersistent {_} _ _%I _%I : simpl never.
Arguments into_persistent {_} _ _%I _%I {_}.
Hint Mode IntoPersistent + + ! - : typeclass_instances.
(* The `iModIntro` tactic is not tied the Iris modalities, but can be
instantiated with a variety of modalities.
In order to plug in a modality, one has to decide for both the persistent and
spatial what action should be performed upon introducing the modality:
- Introduction is only allowed when the context is empty.
- Introduction is only allowed when all hypotheses satisfy some predicate
`C : PROP → Prop` (where `C` should be a type class).
- Introduction will transform each hypotheses using a type class
`C : PROP → PROP → Prop`, where the first parameter is the input and the
second parameter is the output. Hypotheses that cannot be transformed (i.e.
for which no instance of `C` can be found) will be cleared.
- Introduction will clear the context.
- Introduction will keep the context as-if.
Formally, these actions correspond to the following inductive type: *)
Inductive modality_intro_spec (PROP1 : bi) : bi Type :=
| MIEnvIsEmpty {PROP2 : bi} : modality_intro_spec PROP1 PROP2
| MIEnvForall (C : PROP1 Prop) : modality_intro_spec PROP1 PROP1
| MIEnvTransform {PROP2 : bi} (C : PROP2 PROP1 Prop) : modality_intro_spec PROP1 PROP2
| MIEnvClear {PROP2} : modality_intro_spec PROP1 PROP2
| MIEnvId : modality_intro_spec PROP1 PROP1.
Arguments MIEnvIsEmpty {_ _}.
Arguments MIEnvForall {_} _.
Arguments MIEnvTransform {_ _} _.
Arguments MIEnvClear {_ _}.
Arguments MIEnvId {_}.
Notation MIEnvFilter C := (MIEnvTransform (TCDiag C)).
Definition modality_intro_spec_persistent {PROP1 PROP2}
(s : modality_intro_spec PROP1 PROP2) : (PROP1 PROP2) Prop :=
match s with
| MIEnvIsEmpty => λ M, True
| MIEnvForall C => λ M,
( P, C P P M ( P))
( P Q, M P M Q M (P Q))
| MIEnvTransform C => λ M,
( P Q, C P Q P M ( Q))
( P Q, M P M Q M (P Q))
| MIEnvClear => λ M, True
| MIEnvId => λ M, P, P M ( P)
end.
Definition modality_intro_spec_spatial {PROP1 PROP2}
(s : modality_intro_spec PROP1 PROP2) : (PROP1 PROP2) Prop :=
match s with
| MIEnvIsEmpty => λ M, True
| MIEnvForall C => λ M, P, C P P M P
| MIEnvTransform C => λ M, P Q, C P Q P M Q
| MIEnvClear => λ M, P, Absorbing (M P)
| MIEnvId => λ M, P, P M P
end.
(* A modality is then a record packing together the modality with the laws it
should satisfy to justify the given actions for both contexts: *)
Record modality_mixin {PROP1 PROP2 : bi} (M : PROP1 PROP2)
(pspec sspec : modality_intro_spec PROP1 PROP2) := {
modality_mixin_persistent : modality_intro_spec_persistent pspec M;
modality_mixin_spatial : modality_intro_spec_spatial sspec M;
modality_mixin_emp : emp M emp;
modality_mixin_mono P Q : (P Q) M P M Q;
modality_mixin_sep P Q : M P M Q M (P Q)
}.
Record modality (PROP1 PROP2 : bi) := Modality {
modality_car :> PROP1 PROP2;
modality_persistent_spec : modality_intro_spec PROP1 PROP2;
modality_spatial_spec : modality_intro_spec PROP1 PROP2;
modality_mixin_of :
modality_mixin modality_car modality_persistent_spec modality_spatial_spec
}.
Arguments Modality {_ _} _ {_ _} _.
Arguments modality_persistent_spec {_ _} _.
Arguments modality_spatial_spec {_ _} _.
Section modality.
Context {PROP1 PROP2} (M : modality PROP1 PROP2).
Lemma modality_persistent_transform C P Q :
modality_persistent_spec M = MIEnvTransform C C P Q P M ( Q).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_and_transform C P Q :
modality_persistent_spec M = MIEnvTransform C M P M Q M (P Q).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_spatial_transform C P Q :
modality_spatial_spec M = MIEnvTransform C C P Q P M Q.
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_spatial_clear P :
modality_spatial_spec M = MIEnvClear Absorbing (M P).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_emp : emp M emp.
Proof. eapply modality_mixin_emp, modality_mixin_of. Qed.
Lemma modality_mono P Q : (P Q) M P M Q.
Proof. eapply modality_mixin_mono, modality_mixin_of. Qed.
Lemma modality_sep P Q : M P M Q M (P Q).
Proof. eapply modality_mixin_sep, modality_mixin_of. Qed.
Global Instance modality_mono' : Proper (() ==> ()) M.
Proof. intros P Q. apply modality_mono. Qed.
Global Instance modality_flip_mono' : Proper (flip () ==> flip ()) M.
Proof. intros P Q. apply modality_mono. Qed.
Global Instance modality_proper : Proper (() ==> ()) M.
Proof. intros P Q. rewrite !equiv_spec=> -[??]; eauto using modality_mono. Qed.
End modality.
Section modality1.
Context {PROP} (M : modality PROP PROP).
Lemma modality_persistent_forall C P :
modality_persistent_spec M = MIEnvForall C C P P M ( P).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_and_forall C P Q :
modality_persistent_spec M = MIEnvForall C M P M Q M (P Q).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_persistent_id P :
modality_persistent_spec M = MIEnvId P M ( P).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_spatial_forall C P :
modality_spatial_spec M = MIEnvForall C C P P M P.
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_spatial_id P :
modality_spatial_spec M = MIEnvId P M P.
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_persistent_forall_big_and C Ps :
modality_persistent_spec M = MIEnvForall C
Forall C Ps [] Ps M ( [] Ps).
Proof.
induction 2 as [|P Ps ? _ IH]; simpl.
- by rewrite persistently_pure affinely_True_emp affinely_emp -modality_emp.
- rewrite affinely_persistently_and -modality_and_forall // -IH.
by rewrite {1}(modality_persistent_forall _ P).
Qed.
Lemma modality_spatial_forall_big_sep C Ps :
modality_spatial_spec M = MIEnvForall C
Forall C Ps [] Ps M ([] Ps).
Proof.
induction 2 as [|P Ps ? _ IH]; simpl.
- by rewrite -modality_emp.
- by rewrite -modality_sep -IH {1}(modality_spatial_forall _ P).
Qed.
End modality1.
(** The [FromModal M P Q] class is used by the [iModIntro] tactic to transform
a goal [P] into a modality [M] and proposition [Q].
The input is [P] and the outputs are [M] and [Q]. *)
The input is [P] and the outputs are [M] and [Q].
For modalities [M] that do not need to augment the proof mode environment, one
can define an instance [FromModal modality_id (M P) P]. Defining such an
only imposes the proof obligation [P ⊢ M P]. Examples of modalities that have
such an instance are [bupd], [fupd], [except_0], [monPred_relatively] and
[bi_absorbingly]. *)
  • I had to read this at least three times... so the M here is not the M down there in M Q ⊢ P, right?

    Edited by Ralf Jung
  • Also there's a typo, "Defining such an [missing: instance] only imposes the proof obligation..."

    Oh and (as usual for all these typclasses^^) the order of arguments makes no sense. M Q P would make sense as that's the order in which they appear, P M Q would make sense as that's inputs-first, but M P Q?!?

    Edited by Ralf Jung
  • Fixed both.

    W.r.t. the order of arguments, I always prefer to put things like modalities/functors/maps first so that you can easily use the definition/class/... in a curried way.

    Taking away the M, which should be first by the above principle, the order is the same as for the other From... classes.

  • See e.g. MaybeIntoLaterN where it is important that the n is first so that we can used it curried.

Please register or sign in to reply
Class FromModal {PROP1 PROP2 : bi}
(M : modality PROP1 PROP2) (P : PROP2) (Q : PROP1) :=
from_modal : M Q P.
......@@ -240,16 +101,6 @@ Arguments FromModal {_ _} _ _%I _%I : simpl never.
Arguments from_modal {_ _} _ _%I _%I {_}.
Hint Mode FromModal - + - ! - : typeclass_instances.
(** The identity modality [modality_id] can be used in combination with
[FromModal modality_id] to support introduction for modalities that enjoy
[P ⊢ M P]. This is done by defining an instance [FromModal modality_id (M P) P],
which will instruct [iModIntro] to introduce the modality without modifying the
proof mode context. Examples of such modalities are [bupd], [fupd], [except_0],
[monPred_relatively] and [bi_absorbingly]. *)
Lemma modality_id_mixin {PROP : bi} : modality_mixin (@id PROP) MIEnvId MIEnvId.
Proof. split; simpl; eauto. Qed.
Definition modality_id {PROP : bi} := Modality (@id PROP) modality_id_mixin.
Class FromAffinely {PROP : bi} (P Q : PROP) :=
from_affinely : bi_affinely Q P.
Arguments FromAffinely {_} _%I _%type_scope : simpl never.
......
From iris.bi Require Export bi.
From stdpp Require Import namespaces.
Set Default Proof Using "Type".
Import bi.
(** The `iModIntro` tactic is not tied the Iris modalities, but can be
instantiated with a variety of modalities.
In order to plug in a modality, one has to decide for both the persistent and
spatial what action should be performed upon introducing the modality:
- Introduction is only allowed when the context is empty.
- Introduction is only allowed when all hypotheses satisfy some predicate
`C : PROP → Prop` (where `C` should be a type class).
- Introduction will transform each hypotheses using a type class
`C : PROP → PROP → Prop`, where the first parameter is the input and the
second parameter is the output. Hypotheses that cannot be transformed (i.e.
for which no instance of `C` can be found) will be cleared.
- Introduction will clear the context.
- Introduction will keep the context as-if.
Formally, these actions correspond to the following inductive type: *)
Inductive modality_intro_spec (PROP1 : bi) : bi Type :=
| MIEnvIsEmpty {PROP2 : bi} : modality_intro_spec PROP1 PROP2
| MIEnvForall (C : PROP1 Prop) : modality_intro_spec PROP1 PROP1
| MIEnvTransform {PROP2 : bi} (C : PROP2 PROP1 Prop) : modality_intro_spec PROP1 PROP2
| MIEnvClear {PROP2} : modality_intro_spec PROP1 PROP2
| MIEnvId : modality_intro_spec PROP1 PROP1.
Arguments MIEnvIsEmpty {_ _}.
Arguments MIEnvForall {_} _.
Arguments MIEnvTransform {_ _} _.
Arguments MIEnvClear {_ _}.
Arguments MIEnvId {_}.
Notation MIEnvFilter C := (MIEnvTransform (TCDiag C)).
Definition modality_intro_spec_persistent {PROP1 PROP2}
(s : modality_intro_spec PROP1 PROP2) : (PROP1 PROP2) Prop :=
match s with
| MIEnvIsEmpty => λ M, True
| MIEnvForall C => λ M,
( P, C P P M ( P))
( P Q, M P M Q M (P Q))
| MIEnvTransform C => λ M,
( P Q, C P Q P M ( Q))
( P Q, M P M Q M (P Q))
| MIEnvClear => λ M, True
| MIEnvId => λ M, P, P M ( P)
end.
Definition modality_intro_spec_spatial {PROP1 PROP2}
(s : modality_intro_spec PROP1 PROP2) : (PROP1 PROP2) Prop :=
match s with
| MIEnvIsEmpty => λ M, True
| MIEnvForall C => λ M, P, C P P M P
| MIEnvTransform C => λ M, P Q, C P Q P M Q
| MIEnvClear => λ M, P, Absorbing (M P)
| MIEnvId => λ M, P, P M P
end.
(* A modality is then a record packing together the modality with the laws it
should satisfy to justify the given actions for both contexts: *)
Record modality_mixin {PROP1 PROP2 : bi} (M : PROP1 PROP2)
(pspec sspec : modality_intro_spec PROP1 PROP2) := {
modality_mixin_persistent : modality_intro_spec_persistent pspec M;
modality_mixin_spatial : modality_intro_spec_spatial sspec M;
modality_mixin_emp : emp M emp;
modality_mixin_mono P Q : (P Q) M P M Q;
modality_mixin_sep P Q : M P M Q M (P Q)
}.
Record modality (PROP1 PROP2 : bi) := Modality {
modality_car :> PROP1 PROP2;
modality_persistent_spec : modality_intro_spec PROP1 PROP2;
modality_spatial_spec : modality_intro_spec PROP1 PROP2;
modality_mixin_of :
modality_mixin modality_car modality_persistent_spec modality_spatial_spec
}.
Arguments Modality {_ _} _ {_ _} _.
Arguments modality_persistent_spec {_ _} _.
Arguments modality_spatial_spec {_ _} _.
Section modality.
Context {PROP1 PROP2} (M : modality PROP1 PROP2).
Lemma modality_persistent_transform C P Q :
modality_persistent_spec M = MIEnvTransform C C P Q P M ( Q).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_and_transform C P Q :
modality_persistent_spec M = MIEnvTransform C M P M Q M (P Q).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_spatial_transform C P Q :
modality_spatial_spec M = MIEnvTransform C C P Q P M Q.
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_spatial_clear P :
modality_spatial_spec M = MIEnvClear Absorbing (M P).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_emp : emp M emp.
Proof. eapply modality_mixin_emp, modality_mixin_of. Qed.
Lemma modality_mono P Q : (P Q) M P M Q.
Proof. eapply modality_mixin_mono, modality_mixin_of. Qed.
Lemma modality_sep P Q : M P M Q M (P Q).
Proof. eapply modality_mixin_sep, modality_mixin_of. Qed.
Global Instance modality_mono' : Proper (() ==> ()) M.
Proof. intros P Q. apply modality_mono. Qed.
Global Instance modality_flip_mono' : Proper (flip () ==> flip ()) M.
Proof. intros P Q. apply modality_mono. Qed.
Global Instance modality_proper : Proper (() ==> ()) M.
Proof. intros P Q. rewrite !equiv_spec=> -[??]; eauto using modality_mono. Qed.
End modality.
Section modality1.
Context {PROP} (M : modality PROP PROP).
Lemma modality_persistent_forall C P :
modality_persistent_spec M = MIEnvForall C C P P M ( P).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_and_forall C P Q :
modality_persistent_spec M = MIEnvForall C M P M Q M (P Q).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_persistent_id P :
modality_persistent_spec M = MIEnvId P M ( P).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_spatial_forall C P :
modality_spatial_spec M = MIEnvForall C C P P M P.
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_spatial_id P :
modality_spatial_spec M = MIEnvId P M P.
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_persistent_forall_big_and C Ps :
modality_persistent_spec M = MIEnvForall C
Forall C Ps [] Ps M ( [] Ps).
Proof.
induction 2 as [|P Ps ? _ IH]; simpl.
- by rewrite persistently_pure affinely_True_emp affinely_emp -modality_emp.
- rewrite affinely_persistently_and -modality_and_forall // -IH.
by rewrite {1}(modality_persistent_forall _ P).
Qed.
Lemma modality_spatial_forall_big_sep C Ps :
modality_spatial_spec M = MIEnvForall C
Forall C Ps [] Ps M ([] Ps).
Proof.
induction 2 as [|P Ps ? _ IH]; simpl.
- by rewrite -modality_emp.
- by rewrite -modality_sep -IH {1}(modality_spatial_forall _ P).
Qed.
End modality1.
(** The identity modality [modality_id] can be used in combination with
[FromModal modality_id] to support introduction for modalities that enjoy
[P ⊢ M P]. This is done by defining an instance [FromModal modality_id (M P) P],
which will instruct [iModIntro] to introduce the modality without modifying the
proof mode context. Examples of such modalities are [bupd], [fupd], [except_0],
[monPred_relatively] and [bi_absorbingly]. *)
Lemma modality_id_mixin {PROP : bi} : modality_mixin (@id PROP) MIEnvId MIEnvId.
Proof. split; simpl; eauto. Qed.
Definition modality_id {PROP : bi} := Modality (@id PROP) modality_id_mixin.
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.
Lemma modality_affinely_persistently_mixin :
modality_mixin (λ P : PROP, P)%I MIEnvId MIEnvIsEmpty.
Proof.
split; simpl; eauto using equiv_entails_sym, affinely_persistently_emp,
affinely_mono, persistently_mono, affinely_persistently_idemp,
affinely_persistently_sep_2 with typeclass_instances.
Qed.
Definition modality_affinely_persistently :=
Modality _ modality_affinely_persistently_mixin.
Lemma modality_plainly_mixin :
modality_mixin (@bi_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 :=
Modality _ modality_plainly_mixin.
Lemma modality_affinely_plainly_mixin :
modality_mixin (λ P : PROP, P)%I (MIEnvForall Plain) MIEnvIsEmpty.
Proof.
split; simpl; split_and?; eauto using equiv_entails_sym,
affinely_plainly_emp, affinely_intro,
plainly_intro, affinely_mono, plainly_mono, affinely_plainly_idemp,
affinely_plainly_and, affinely_plainly_sep_2 with typeclass_instances.
Qed.
Definition modality_affinely_plainly :=
Modality _ modality_affinely_plainly_mixin.
Lemma modality_embed_mixin `{BiEmbedding PROP PROP'} :
modality_mixin (@bi_embed PROP PROP' _)
(MIEnvTransform IntoEmbed) (MIEnvTransform IntoEmbed).
Proof.
split; simpl; split_and?;
eauto using equiv_entails_sym, bi_embed_emp, bi_embed_sep, bi_embed_and.
- intros P Q. rewrite /IntoEmbed=> ->.
by rewrite bi_embed_affinely bi_embed_persistently.
- by intros P Q ->.
Qed.
Definition modality_embed `{BiEmbedding PROP PROP'} :=
Modality _ modality_embed_mixin.
End bi_modalities.
Section sbi_modalities.
Context {PROP : sbi}.
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.
rewrite /MaybeIntoLaterN=> P Q ->. by rewrite laterN_affinely_persistently_2.
Qed.
Definition modality_laterN n :=
Modality _ (modality_laterN_mixin n).
End sbi_modalities.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment