classes.v 12.6 KB
Newer Older
1
From iris.base_logic Require Export base_logic.
2
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Oops!    
Robbert Krebbers committed
3
4
Import uPred.

5
6
7
8
9
10
11
12
13
14
(* The Or class is useful for efficiency: instead of having two instances
[P → Q1 → R] and [P → Q2 → R] we could have one instance [P → Or Q1 Q2 → R],
which avoids the need to derive [P] twice. *)
Inductive Or (P1 P2 : Type) :=
  | Or_l : P1  Or P1 P2
  | Or_r : P2  Or P1 P2.
Existing Class Or.
Existing Instance Or_l | 9.
Existing Instance Or_r | 10.

15
16
17
Class FromAssumption {M} (p : bool) (P Q : uPred M) :=
  from_assumption : ?p P  Q.
Arguments from_assumption {_} _ _ _ {_}.
18
(* No need to restrict Hint Mode, we have a default instance that will persistently
19
20
be used in case of evars *)
Hint Mode FromAssumption + + - - : typeclass_instances.
21
22
23
24
25

Class IntoPure {M} (P : uPred M) (φ : Prop) := into_pure : P  ⌜φ⌝.
Arguments into_pure {_} _ _ {_}.
Hint Mode IntoPure + ! - : typeclass_instances.

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
(* [IntoPureT] is a variant of [IntoPure] with the argument in [Type] to avoid
some shortcoming of unification in Coq's type class search. An example where we
use this workaround is to repair the following instance:

  Global Instance into_exist_and_pure P Q (φ : Prop) :
    IntoPure P φ → IntoExist (P ∧ Q) (λ _ : φ, Q).

Coq is unable to use this instance: [class_apply] -- which is used by type class
search -- fails with the error that it cannot unify [Prop] and [Type]. This is
probably caused because [class_apply] uses an ancient unification algorith. The
[refine] tactic -- which uses a better unification algorithm -- succeeds to
apply the above instance.

Since we do not want to define [Hint Extern] declarations using [refine] for
any instance like [into_exist_and_pure], we factor this out in the class
[IntoPureT]. This way, we only have to declare a [Hint Extern] using [refine]
once, and use [IntoPureT] in any instance like [into_exist_and_pure].

TODO: Report this as a Coq bug, or wait for https://github.com/coq/coq/pull/991
to be finished and merged someday. *)
Class IntoPureT {M} (P : uPred M) (φ : Type) :=
  into_pureT :  ψ : Prop, φ = ψ  IntoPure P ψ.
Lemma into_pureT_hint {M} (P : uPred M) (φ : Prop) : IntoPure P φ  IntoPureT P φ.
Proof. by exists φ. Qed.
Hint Extern 0 (IntoPureT _ _) =>
  notypeclasses refine (into_pureT_hint _ _ _) : typeclass_instances.

53
54
55
56
Class FromPure {M} (P : uPred M) (φ : Prop) := from_pure : ⌜φ⌝  P.
Arguments from_pure {_} _ _ {_}.
Hint Mode FromPure + ! - : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
57
58
59
60
61
62
63
Class FromPureT {M} (P : uPred M) (φ : Type) :=
  from_pureT :  ψ : Prop, φ = ψ  FromPure P ψ.
Lemma from_pureT_hint {M} (P : uPred M) (φ : Prop) : FromPure P φ  FromPureT P φ.
Proof. by exists φ. Qed.
Hint Extern 0 (FromPureT _ _) =>
  notypeclasses refine (from_pureT_hint _ _ _) : typeclass_instances.

64
65
66
67
68
Class IntoInternalEq {M} {A : ofeT} (P : uPred M) (x y : A) :=
  into_internal_eq : P  x  y.
Arguments into_internal_eq {_ _} _ _ _ {_}.
Hint Mode IntoInternalEq + - ! - - : typeclass_instances.

69
70
71
72
Class IntoPersistent {M} (p : bool) (P Q : uPred M) :=
  into_persistent : ?p P   Q.
Arguments into_persistent {_} _ _ _ {_}.
Hint Mode IntoPersistent + + ! - : typeclass_instances.
73

74
75
76
77
78
Class FromAlways {M} (p : bool) (P Q : uPred M) :=
  from_always : (if p then  Q else  Q)  P.
Arguments from_always {_} _ _ _ {_}.
Hint Mode FromAlways + - ! - : typeclass_instances.

79
80
81
82
83
84
85
86
87
88
89
90
91
92
(* The class [IntoLaterN] has only two instances:

- The default instance [IntoLaterN n P P], i.e. [▷^n P -∗ P]
- The instance [IntoLaterN' n P Q → IntoLaterN n P Q], where [IntoLaterN']
  is identical to [IntoLaterN], but computationally is supposed to make
  progress, i.e. its instances should actually strip a later.

The point of using the auxilary class [IntoLaterN'] is to ensure that the
default instance is not applied deeply in the term, which may cause in too many
definitions being unfolded (see issue #55).

For binary connectives we have the following instances:

<<
Robbert Krebbers's avatar
Robbert Krebbers committed
93
94
95
IntoLaterN' n P P'       IntoLaterN n Q Q'
------------------------------------------
     IntoLaterN' n (P /\ Q) (P' /\ Q')
96
97


Robbert Krebbers's avatar
Robbert Krebbers committed
98
99
      IntoLaterN' n Q Q'
-------------------------------
100
101
102
IntoLaterN n (P /\ Q) (P /\ Q')
>>
*)
103
104
Class IntoLaterN {M} (n : nat) (P Q : uPred M) := into_laterN : P  ^n Q.
Arguments into_laterN {_} _ _ _ {_}.
105
106
107
108
109
110
111
112
113
Hint Mode IntoLaterN + - - - : typeclass_instances.

Class IntoLaterN' {M} (n : nat) (P Q : uPred M) :=
  into_laterN' :> IntoLaterN n P Q.
Arguments into_laterN' {_} _ _ _ {_}.
Hint Mode IntoLaterN' + - ! - : typeclass_instances.

Instance into_laterN_default {M} n (P : uPred M) : IntoLaterN n P P | 1000.
Proof. apply laterN_intro. Qed.
114
115
116
117
118

Class FromLaterN {M} (n : nat) (P Q : uPred M) := from_laterN : ^n Q  P.
Arguments from_laterN {_} _ _ _ {_}.
Hint Mode FromLaterN + - ! - : typeclass_instances.

119
120
121
122
123
124
125
126
127
128
129
130
Class WandWeaken {M} (p : bool) (P Q P' Q' : uPred M) :=
  wand_weaken : (P - Q)  (?p P' - Q').
Hint Mode WandWeaken + + - - - - : typeclass_instances.

Class WandWeaken' {M} (p : bool) (P Q P' Q' : uPred M) :=
  wand_weaken' :> WandWeaken p P Q P' Q'.
Hint Mode WandWeaken' + + - - ! - : typeclass_instances.
Hint Mode WandWeaken' + + - - - ! : typeclass_instances.

Class IntoWand {M} (p : bool) (R P Q : uPred M) := into_wand : R  ?p P - Q.
Arguments into_wand {_} _ _ _ _ {_}.
Hint Mode IntoWand + + ! - - : typeclass_instances.
131

132
133
134
135
136
Class FromAnd {M} (p : bool) (P Q1 Q2 : uPred M) :=
  from_and : (if p then Q1  Q2 else Q1  Q2)  P.
Arguments from_and {_} _ _ _ _ {_}.
Hint Mode FromAnd + + ! - - : typeclass_instances.
Hint Mode FromAnd + + - ! ! : typeclass_instances. (* For iCombine *)
137

138
139
140
Lemma mk_from_and_and {M} p (P Q1 Q2 : uPred M) :
  (Q1  Q2  P)  FromAnd p P Q1 Q2.
Proof. rewrite /FromAnd=><-. destruct p; auto using sep_and. Qed.
141
Lemma mk_from_and_persistent {M} (P Q1 Q2 : uPred M) :
142
  Or (Persistent Q1) (Persistent Q2)  (Q1  Q2  P)  FromAnd true P Q1 Q2.
143
144
Proof.
  intros [?|?] ?; rewrite /FromAnd.
145
146
  - by rewrite and_sep_l.
  - by rewrite and_sep_r.
147
Qed.
148
149

Class IntoAnd {M} (p : bool) (P Q1 Q2 : uPred M) :=
150
  into_and : P  if p then Q1  Q2 else Q1  Q2.
151
152
Arguments into_and {_} _ _ _ _ {_}.
Hint Mode IntoAnd + + ! - - : typeclass_instances.
153

154
155
Lemma mk_into_and_sep {M} p (P Q1 Q2 : uPred M) :
  (P  Q1  Q2)  IntoAnd p P Q1 Q2.
156
Proof. rewrite /IntoAnd=>->. destruct p; auto using sep_and. Qed.
157

158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
(* There are various versions of [IsOp] with different modes:

- [IsOp a b1 b2]: this one has no mode, it can be used regardless of whether
  any of the arguments is an evar. This class has only one direct instance:
  [IsOp (a ⋅ b) a b].
- [IsOp' a b1 b2]: requires either [a] to start with a constructor, OR [b1] and
  [b2] to start with a constructor. All usual instances should be of this
  class to avoid loops.
- [IsOp'LR a b1 b2]: requires either [a] to start with a constructor. This one
  has just one instance: [IsOp'LR (a ⋅ b) a b] with a very low precendence.
  This is important so that when performing, for example, an [iDestruct] on
  [own γ (q1 + q2)] where [q1] and [q2] are fractions, we actually get
  [own γ q1] and [own γ q2] instead of [own γ ((q1 + q2)/2)] twice.
*)
Class IsOp {A : cmraT} (a b1 b2 : A) := is_op : a  b1  b2.
Arguments is_op {_} _ _ _ {_}.
Hint Mode IsOp + - - - : typeclass_instances.

Instance is_op_op {A : cmraT} (a b : A) : IsOp (a  b) a b | 100.
Proof. by rewrite /IsOp. Qed.

Class IsOp' {A : cmraT} (a b1 b2 : A) := is_op' :> IsOp a b1 b2.
Hint Mode IsOp' + ! - - : typeclass_instances.
Hint Mode IsOp' + - ! ! : typeclass_instances.

Class IsOp'LR {A : cmraT} (a b1 b2 : A) := is_op_lr : IsOp a b1 b2.
Existing Instance is_op_lr | 0.
Hint Mode IsOp'LR + ! - - : typeclass_instances.
Instance is_op_lr_op {A : cmraT} (a b : A) : IsOp'LR (a  b) a b | 0.
Proof. by rewrite /IsOp'LR /IsOp. Qed.
Robbert Krebbers's avatar
Oops!    
Robbert Krebbers committed
188

189
190
191
192
193
194
195
196
197
198
199
200
201
Class Frame {M} (p : bool) (R P Q : uPred M) := frame : ?p R  Q  P.
Arguments frame {_ _} _ _ _ {_}.
Hint Mode Frame + + ! ! - : typeclass_instances.

Class MaybeFrame {M} (p : bool) (R P Q : uPred M) := maybe_frame : ?p R  Q  P.
Arguments maybe_frame {_} _ _ _ {_}.
Hint Mode MaybeFrame + + ! ! - : typeclass_instances.

Instance maybe_frame_frame {M} p (R P Q : uPred M) :
  Frame p R P Q  MaybeFrame p R P Q.
Proof. done. Qed.
Instance maybe_frame_default {M} p (R P : uPred M) : MaybeFrame p R P P | 100.
Proof. apply sep_elim_r. Qed.
Robbert Krebbers's avatar
Oops!    
Robbert Krebbers committed
202

203
204
205
Class FromOr {M} (P Q1 Q2 : uPred M) := from_or : Q1  Q2  P.
Arguments from_or {_} _ _ _ {_}.
Hint Mode FromOr + ! - - : typeclass_instances.
Robbert Krebbers's avatar
Oops!    
Robbert Krebbers committed
206

207
208
209
Class IntoOr {M} (P Q1 Q2 : uPred M) := into_or : P  Q1  Q2.
Arguments into_or {_} _ _ _ {_}.
Hint Mode IntoOr + ! - - : typeclass_instances.
Robbert Krebbers's avatar
Oops!    
Robbert Krebbers committed
210

211
Class FromExist {M A} (P : uPred M) (Φ : A  uPred M) :=
Robbert Krebbers's avatar
Oops!    
Robbert Krebbers committed
212
  from_exist : ( x, Φ x)  P.
213
214
Arguments from_exist {_ _} _ _ {_}.
Hint Mode FromExist + - ! - : typeclass_instances.
Robbert Krebbers's avatar
Oops!    
Robbert Krebbers committed
215

216
Class IntoExist {M A} (P : uPred M) (Φ : A  uPred M) :=
Robbert Krebbers's avatar
Oops!    
Robbert Krebbers committed
217
  into_exist : P   x, Φ x.
218
219
Arguments into_exist {_ _} _ _ {_}.
Hint Mode IntoExist + - ! - : typeclass_instances.
220

221
222
223
224
225
Class IntoForall {M A} (P : uPred M) (Φ : A  uPred M) :=
  into_forall : P   x, Φ x.
Arguments into_forall {_ _} _ _ {_}.
Hint Mode IntoForall + - ! - : typeclass_instances.

226
227
228
229
230
Class FromForall {M A} (P : uPred M) (Φ : A  uPred M) :=
  from_forall : ( x, Φ x)  P.
Arguments from_forall {_ _} _ _ {_}.
Hint Mode FromForall + - ! - : typeclass_instances.

231
232
233
Class FromModal {M} (P Q : uPred M) := from_modal : Q  P.
Arguments from_modal {_} _ _ {_}.
Hint Mode FromModal + ! - : typeclass_instances.
234

235
Class ElimModal {M} (P P' : uPred M) (Q Q' : uPred M) :=
236
  elim_modal : P  (P' - Q')  Q.
237
238
239
Arguments elim_modal {_} _ _ _ _ {_}.
Hint Mode ElimModal + ! - ! - : typeclass_instances.
Hint Mode ElimModal + - ! - ! : typeclass_instances.
240

241
Lemma elim_modal_dummy {M} (P Q : uPred M) : ElimModal P P Q Q.
242
Proof. by rewrite /ElimModal wand_elim_r. Qed.
243

244
245
246
Class IsExcept0 {M} (Q : uPred M) := is_except_0 :  Q  Q.
Arguments is_except_0 {_} _ {_}.
Hint Mode IsExcept0 + ! : typeclass_instances.
247
248
249
250
251
252
253
254
255
256

Class IsCons {A} (l : list A) (x : A) (k : list A) := is_cons : l = x :: k.
Class IsApp {A} (l k1 k2 : list A) := is_app : l = k1 ++ k2.
Global Hint Mode IsCons + ! - - : typeclass_instances.
Global Hint Mode IsApp + ! - - : typeclass_instances.

Instance is_cons_cons {A} (x : A) (l : list A) : IsCons (x :: l) x l.
Proof. done. Qed.
Instance is_app_app {A} (l1 l2 : list A) : IsApp (l1 ++ l2) l1 l2.
Proof. done. Qed.
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271

(* We make sure that tactics that perform actions on *specific* hypotheses or
parts of the goal look through the [tc_opaque] connective, which is used to make
definitions opaque for type class search. For example, when using `iDestruct`,
an explicit hypothesis is affected, and as such, we should look through opaque
definitions. However, when using `iFrame` or `iNext`, arbitrary hypotheses or
parts of the goal are affected, and as such, type class opacity should be
respected.

This means that there are [tc_opaque] instances for all proofmode type classes
with the exception of:

- [FromAssumption] used by [iAssumption]
- [Frame] used by [iFrame]
- [IntoLaterN] and [FromLaterN] used by [iNext]
272
- [IntoPersistent] used by [iPersistent]
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
*)
Instance into_pure_tc_opaque {M} (P : uPred M) φ :
  IntoPure P φ  IntoPure (tc_opaque P) φ := id.
Instance from_pure_tc_opaque {M} (P : uPred M) φ :
  FromPure P φ  FromPure (tc_opaque P) φ := id.
Instance from_laterN_tc_opaque {M} n (P Q : uPred M) :
  FromLaterN n P Q  FromLaterN n (tc_opaque P) Q := id.
Instance into_wand_tc_opaque {M} p (R P Q : uPred M) :
  IntoWand p R P Q  IntoWand p (tc_opaque R) P Q := id.
(* Higher precedence than [from_and_sep] so that [iCombine] does not loop. *)
Instance from_and_tc_opaque {M} p (P Q1 Q2 : uPred M) :
  FromAnd p P Q1 Q2  FromAnd p (tc_opaque P) Q1 Q2 | 102 := id.
Instance into_and_tc_opaque {M} p (P Q1 Q2 : uPred M) :
  IntoAnd p P Q1 Q2  IntoAnd p (tc_opaque P) Q1 Q2 := id.
Instance from_or_tc_opaque {M} (P Q1 Q2 : uPred M) :
  FromOr P Q1 Q2  FromOr (tc_opaque P) Q1 Q2 := id.
Instance into_or_tc_opaque {M} (P Q1 Q2 : uPred M) :
  IntoOr P Q1 Q2  IntoOr (tc_opaque P) Q1 Q2 := id.
Instance from_exist_tc_opaque {M A} (P : uPred M) (Φ : A  uPred M) :
  FromExist P Φ  FromExist (tc_opaque P) Φ := id.
Instance into_exist_tc_opaque {M A} (P : uPred M) (Φ : A  uPred M) :
  IntoExist P Φ  IntoExist (tc_opaque P) Φ := id.
Instance into_forall_tc_opaque {M A} (P : uPred M) (Φ : A  uPred M) :
  IntoForall P Φ  IntoForall (tc_opaque P) Φ := id.
Instance from_modal_tc_opaque {M} (P Q : uPred M) :
  FromModal P Q  FromModal (tc_opaque P) Q := id.
Instance elim_modal_tc_opaque {M} (P P' Q Q' : uPred M) :
  ElimModal P P' Q Q'  ElimModal (tc_opaque P) P' Q Q' := id.