Support heterogeneous modalities.

theories/proofmode/class_instances.v

@@ -9,8 +9,8 @@ Section bi_modalities.
   Lemma modality_persistently_mixin :
     modality_mixin (@bi_persistently PROP) MIEnvId MIEnvClear.
   Proof.
-    split; eauto using equiv_entails_sym, persistently_intro, persistently_mono,
-      persistently_sep_2 with typeclass_instances.
+    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.
@@ -18,7 +18,7 @@ Section bi_modalities.
   Lemma modality_affinely_mixin :
     modality_mixin (@bi_affinely PROP) MIEnvId (MIEnvForall Affine).
   Proof.
-    split; eauto using equiv_entails_sym, affinely_intro, affinely_mono,
+    split; simpl; eauto using equiv_entails_sym, affinely_intro, affinely_mono,
       affinely_sep_2 with typeclass_instances.
   Qed.
   Definition modality_affinely :=
@@ -27,7 +27,7 @@ Section bi_modalities.
   Lemma modality_affinely_persistently_mixin :
     modality_mixin (λ P : PROP, □ P)%I MIEnvId MIEnvIsEmpty.
   Proof.
-    split; eauto using equiv_entails_sym, affinely_persistently_emp,
+    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.
@@ -37,8 +37,8 @@ Section bi_modalities.
   Lemma modality_plainly_mixin :
     modality_mixin (@bi_plainly PROP) (MIEnvForall Plain) MIEnvClear.
   Proof.
-    split; split_and?; eauto using equiv_entails_sym, plainly_intro, plainly_mono,
-      plainly_and, plainly_sep_2 with typeclass_instances.
+    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.
@@ -46,7 +46,8 @@ Section bi_modalities.
   Lemma modality_affinely_plainly_mixin :
     modality_mixin (λ P : PROP, ■ P)%I (MIEnvForall Plain) MIEnvIsEmpty.
   Proof.
-    split; split_and?; eauto using equiv_entails_sym, affinely_plainly_emp, affinely_intro,
+    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.
@@ -56,7 +57,7 @@ Section bi_modalities.
   Lemma modality_absorbingly_mixin :
     modality_mixin (@bi_absorbingly PROP) MIEnvId MIEnvId.
   Proof.
-    split; eauto using equiv_entails_sym, absorbingly_intro,
+    split; simpl; eauto using equiv_entails_sym, absorbingly_intro,
       absorbingly_mono, absorbingly_sep.
   Qed.
   Definition modality_absorbingly :=
@@ -69,7 +70,7 @@ Section sbi_modalities.
   Lemma modality_except_0_mixin :
     modality_mixin (@sbi_except_0 PROP) MIEnvId MIEnvId.
   Proof.
-    split; eauto using equiv_entails_sym,
+    split; simpl; eauto using equiv_entails_sym,
       except_0_intro, except_0_mono, except_0_sep.
   Qed.
   Definition modality_except_0 :=
@@ -79,8 +80,8 @@ Section sbi_modalities.
     modality_mixin (@sbi_laterN PROP n)
       (MIEnvTransform (MaybeIntoLaterN false n)) (MIEnvTransform (MaybeIntoLaterN false n)).
   Proof.
-    split; split_and?; eauto using equiv_entails_sym, laterN_intro, laterN_mono,
-      laterN_and, laterN_sep with typeclass_instances.
+    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 :=
@@ -88,13 +89,13 @@ Section sbi_modalities.
 
   Lemma modality_bupd_mixin `{BUpdFacts PROP} :
     modality_mixin (@bupd PROP _) MIEnvId MIEnvId.
-  Proof. split; eauto using bupd_intro, bupd_mono, bupd_sep. Qed.
+  Proof. split; simpl; eauto using bupd_intro, bupd_mono, bupd_sep. Qed.
   Definition modality_bupd `{BUpdFacts PROP} :=
     Modality _ modality_bupd_mixin.
 
   Lemma modality_fupd_mixin `{FUpdFacts PROP} E :
     modality_mixin (@fupd PROP _ E E) MIEnvId MIEnvId.
-  Proof. split; eauto using fupd_intro, fupd_mono, fupd_sep. Qed.
+  Proof. split; simpl; eauto using fupd_intro, fupd_mono, fupd_sep. Qed.
   Definition modality_fupd `{FUpdFacts PROP} E :=
     Modality _ (modality_fupd_mixin E).
 End sbi_modalities.

theories/proofmode/classes.v

@@ -101,86 +101,81 @@ spatial what action should be performed upon introducing the modality:
 
 Formally, these actions correspond to the following inductive type: *)
 
-Inductive modality_intro_spec (PROP : bi) :=
-  | MIEnvIsEmpty
-  | MIEnvForall (C : PROP → Prop)
-  | MIEnvTransform (C : PROP → PROP → Prop)
-  | MIEnvClear
-  | MIEnvId.
-Arguments MIEnvIsEmpty {_}.
+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 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 {PROP : bi} (M : PROP → PROP)
-    (pspec sspec : modality_intro_spec PROP) := {
-  modality_mixin_persistent :
-    match pspec with
-    | MIEnvIsEmpty => True
-    | MIEnvForall C => (∀ P, C P → □ P ⊢ M (□ P)) ∧ (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q))
-    | MIEnvTransform C => (∀ P Q, C P Q → □ P ⊢ M (□ Q)) ∧ (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q))
-    | MIEnvClear => True
-    | MIEnvId => ∀ P, □ P ⊢ M (□ P)
-    end;
-  modality_mixin_spatial :
-    match sspec with
-    | MIEnvIsEmpty => True
-    | MIEnvForall C => ∀ P, C P → P ⊢ M P
-    | MIEnvTransform C => (∀ P Q, C P Q → P ⊢ M Q)
-    | MIEnvClear => ∀ P, Absorbing (M P)
-    | MIEnvId => ∀ P, P ⊢ M P
-    end;
+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 (PROP : bi) := Modality {
-  modality_car :> PROP → PROP;
-  modality_persistent_spec : modality_intro_spec PROP;
-  modality_spatial_spec : modality_intro_spec PROP;
+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 {_} _.
+Arguments Modality {_ _} _ {_ _} _.
+Arguments modality_persistent_spec {_ _} _.
+Arguments modality_spatial_spec {_ _} _.
 
 Section modality.
-  Context {PROP} (M : modality PROP).
+  Context {PROP1 PROP2} (M : modality PROP1 PROP2).
 
-  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_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_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_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_spatial_id P :
-    modality_spatial_spec M = MIEnvId → P ⊢ M P.
-  Proof. destruct M as [??? []]; naive_solver. Qed.
 
   Lemma modality_emp : emp ⊢ M emp.
   Proof. eapply modality_mixin_emp, modality_mixin_of. Qed.
@@ -194,6 +189,26 @@ Section modality.
   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 →
@@ -212,13 +227,14 @@ Section modality.
     - by rewrite -modality_emp.
     - by rewrite -modality_sep -IH {1}(modality_spatial_forall _ P).
   Qed.
-End modality.
+End modality1.
 
-Class FromModal {PROP : bi} (M : modality PROP) (P Q : PROP) :=
+Class FromModal {PROP1 PROP2 : bi}
+    (M : modality PROP1 PROP2) (P : PROP2) (Q : PROP1) :=
   from_modal : M Q ⊢ P.
-Arguments FromModal {_} _ _%I _%I : simpl never.
-Arguments from_modal {_} _ _%I _%I {_}.
-Hint Mode FromModal + - ! - : typeclass_instances.
+Arguments FromModal {_ _} _ _%I _%I : simpl never.
+Arguments from_modal {_ _} _ _%I _%I {_}.
+Hint Mode FromModal - + - ! - : typeclass_instances.
 
 Class FromAffinely {PROP : bi} (P Q : PROP) :=
   from_affinely : bi_affinely Q ⊢ P.

theories/proofmode/monpred.v

@@ -21,7 +21,8 @@ Section modalities.
     modality_mixin (@monPred_absolutely I PROP)
       (MIEnvFilter Absolute) (MIEnvFilter Absolute).
   Proof.
-    split; split_and?; intros; try match goal with H : TCDiag _ _ _ |- _ => destruct H end;
+    split; simpl; split_and?; intros;
+      try match goal with H : TCDiag _ _ _ |- _ => destruct H end;
       eauto using bi.equiv_entails_sym, absolute_absolutely,
         monPred_absolutely_mono, monPred_absolutely_and,
         monPred_absolutely_sep_2 with typeclass_instances.

theories/proofmode/tactics.v

@@ -967,25 +967,21 @@ Tactic Notation "iModIntro":=
   eapply tac_modal_intro;
     [apply _  ||
      fail "iModIntro: the goal is not a modality"
-    |hnf; env_cbv;
-     apply _ ||
-     lazymatch goal with
-     | |- TCAnd (TCForall ?C _) _ => fail "iModIntro: persistent context does not satisfy" C
-     | |- TCAnd (TCEq _ Enil) _ => fail "iModIntro: persistent context is non-empty"
+    |apply _ ||
+     let s := lazymatch goal with |- IntoModalPersistentEnv _ _ _ ?s => s end in
+     lazymatch eval hnf in s with
+     | MIEnvForall ?C => fail "iModIntro: persistent context does not satisfy" C
+     | MIEnvIsEmpty => fail "iModIntro: persistent context is non-empty"
      end
-    |hnf; env_cbv;
-     lazymatch goal with
-     | |- ∃ _, TransformSpatialEnv _ _ _ _ _ ∧ _ =>
-        eexists; split;
-          [apply _
-          |apply _ || fail "iModIntro: cannot filter spatial context when goal is not absorbing"]
-     | |- TCAnd (TCForall ?C _) _ =>
-        apply _ || fail "iModIntro: spatial context does not satisfy" C
-     | |- TCAnd (TCEq _ Enil) _ =>
-        apply _ || fail "iModIntro: spatial context is non-empty"
-     | |- _ => apply _
+    |apply _ ||
+     let s := lazymatch goal with |- IntoModalPersistentEnv _ _ _ ?s => s end in
+     lazymatch eval hnf in s with
+     | MIEnvForall ?C => fail "iModIntro: spatial context does not satisfy" C
+     | MIEnvIsEmpty => fail "iModIntro: spatial context is non-empty"
      end
-    |env_cbv].
+    |env_cbv; apply _ ||
+     fail "iModIntro: cannot filter spatial context when goal is not absorbing"
+    |].
 Tactic Notation "iAlways" := iModIntro.
 
 (** * Later *)