modalities.v 6.98 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
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
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.