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.