classes.v 8.02 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 19 20
(* No need to restrict Hint Mode, we have a default instance that will always
be used in case of evars *)
Hint Mode FromAssumption + + - - : typeclass_instances.
21 22 23 24 25 26 27 28 29 30 31 32 33

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

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

Class IntoPersistentP {M} (P Q : uPred M) := into_persistentP : P   Q.
Arguments into_persistentP {_} _ _ {_}.
Hint Mode IntoPersistentP + ! - : typeclass_instances.

34 35 36 37 38 39 40 41 42 43 44 45 46 47
(* 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
48 49 50
IntoLaterN' n P P'       IntoLaterN n Q Q'
------------------------------------------
     IntoLaterN' n (P /\ Q) (P' /\ Q')
51 52


Robbert Krebbers's avatar
Robbert Krebbers committed
53 54
      IntoLaterN' n Q Q'
-------------------------------
55 56 57
IntoLaterN n (P /\ Q) (P /\ Q')
>>
*)
58 59
Class IntoLaterN {M} (n : nat) (P Q : uPred M) := into_laterN : P  ^n Q.
Arguments into_laterN {_} _ _ _ {_}.
60 61 62 63 64 65 66 67 68
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.
69 70 71 72 73

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

74 75 76 77 78 79 80 81 82 83 84 85
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.
86

87 88 89 90 91 92 93 94
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 *)
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.
95 96 97 98 99 100 101
Lemma mk_from_and_persistent {M} (P Q1 Q2 : uPred M) :
  Or (PersistentP Q1) (PersistentP Q2)  (Q1  Q2  P)  FromAnd true P Q1 Q2.
Proof.
  intros [?|?] ?; rewrite /FromAnd.
  - by rewrite always_and_sep_l.
  - by rewrite always_and_sep_r.
Qed.
102 103

Class IntoAnd {M} (p : bool) (P Q1 Q2 : uPred M) :=
104
  into_and : P  if p then Q1  Q2 else Q1  Q2.
105 106 107 108
Arguments into_and {_} _ _ _ _ {_}.
Hint Mode IntoAnd + + ! - - : typeclass_instances.
Lemma mk_into_and_sep {M} p (P Q1 Q2 : uPred M) :
  (P  Q1  Q2)  IntoAnd p P Q1 Q2.
109
Proof. rewrite /IntoAnd=>->. destruct p; auto using sep_and. Qed.
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
(* 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
141

142 143 144 145 146 147 148 149 150 151 152 153 154
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
155

156 157 158
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
159

160 161 162
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
163

164
Class FromExist {M A} (P : uPred M) (Φ : A  uPred M) :=
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
165
  from_exist : ( x, Φ x)  P.
166 167
Arguments from_exist {_ _} _ _ {_}.
Hint Mode FromExist + - ! - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
168

169
Class IntoExist {M A} (P : uPred M) (Φ : A  uPred M) :=
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
170
  into_exist : P   x, Φ x.
171 172
Arguments into_exist {_ _} _ _ {_}.
Hint Mode IntoExist + - ! - : typeclass_instances.
173

174 175 176 177 178
Class IntoForall {M A} (P : uPred M) (Φ : A  uPred M) :=
  into_forall : P   x, Φ x.
Arguments into_forall {_ _} _ _ {_}.
Hint Mode IntoForall + - ! - : typeclass_instances.

179 180 181
Class FromModal {M} (P Q : uPred M) := from_modal : Q  P.
Arguments from_modal {_} _ _ {_}.
Hint Mode FromModal + ! - : typeclass_instances.
182

183
Class ElimModal {M} (P P' : uPred M) (Q Q' : uPred M) :=
184
  elim_modal : P  (P' - Q')  Q.
185 186 187
Arguments elim_modal {_} _ _ _ _ {_}.
Hint Mode ElimModal + ! - ! - : typeclass_instances.
Hint Mode ElimModal + - ! - ! : typeclass_instances.
188

189
Lemma elim_modal_dummy {M} (P Q : uPred M) : ElimModal P P Q Q.
190
Proof. by rewrite /ElimModal wand_elim_r. Qed.
191

192 193 194
Class IsExcept0 {M} (Q : uPred M) := is_except_0 :  Q  Q.
Arguments is_except_0 {_} _ {_}.
Hint Mode IsExcept0 + ! : typeclass_instances.
195 196 197 198 199 200 201 202 203 204

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.