classes.v 5.97 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
Class FromAssumption {M} (p : bool) (P Q : uPred M) :=
  from_assumption : ?p P  Q.
Arguments from_assumption {_} _ _ _ {_}.
8 9 10
(* 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.
11 12 13 14 15 16 17 18 19 20 21 22 23

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.

24 25 26 27 28 29 30 31 32 33 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:

<<
ProgIntoLaterN n P P'       IntoLaterN n Q Q'
---------------------------------------------
ProgIntoLaterN n (P /\ Q) (P' /\ Q')


   ProgIntoLaterN n Q Q'
--------------------------------
IntoLaterN n (P /\ Q) (P /\ Q')
>>
*)
48 49
Class IntoLaterN {M} (n : nat) (P Q : uPred M) := into_laterN : P  ^n Q.
Arguments into_laterN {_} _ _ _ {_}.
50 51 52 53 54 55 56 57 58
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.
59 60 61 62 63

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

Robbert Krebbers's avatar
Robbert Krebbers committed
64 65 66 67 68 69 70
Class WandWeaken {M} (P Q P' Q' : uPred M) := wand_weaken : (P - Q)  (P' - Q').
Hint Mode WandWeaken + - - - - : typeclass_instances.

Class WandWeaken' {M} (P Q P' Q' : uPred M) :=
  wand_weaken' :> WandWeaken P Q P' Q'.
Hint Mode WandWeaken' + - - ! - : typeclass_instances.
Hint Mode WandWeaken' + - - - ! : typeclass_instances.
71 72
Instance wand_weaken_exact {M} (P Q : uPred M) : WandWeaken P Q P Q | 1000.
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
73

74 75 76 77 78 79 80 81 82 83 84 85 86 87
Class IntoWand {M} (R P Q : uPred M) := into_wand : R  P - Q.
Arguments into_wand {_} _ _ _ {_}.
Hint Mode IntoWand + ! - - : typeclass_instances.

Class FromAnd {M} (P Q1 Q2 : uPred M) := from_and : Q1  Q2  P.
Arguments from_and {_} _ _ _ {_}.
Hint Mode FromAnd + ! - - : typeclass_instances.

Class FromSep {M} (P Q1 Q2 : uPred M) := from_sep : Q1  Q2  P.
Arguments from_sep {_} _ _ _ {_}.
Hint Mode FromSep + ! - - : typeclass_instances.
Hint Mode FromSep + - ! ! : typeclass_instances. (* For iCombine *)

Class IntoAnd {M} (p : bool) (P Q1 Q2 : uPred M) :=
88
  into_and : P  if p then Q1  Q2 else Q1  Q2.
89 90 91 92
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.
93
Proof. rewrite /IntoAnd=>->. destruct p; auto using sep_and. Qed.
94

95
Class FromOp {A : cmraT} (a b1 b2 : A) := from_op : b1  b2  a.
96 97 98
Arguments from_op {_} _ _ _ {_}.
Hint Mode FromOp + ! - - : typeclass_instances.
Hint Mode FromOp + - ! ! : typeclass_instances. (* For iCombine *)
99

Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
100
Class IntoOp {A : cmraT} (a b1 b2 : A) := into_op : a  b1  b2.
101 102 103
Arguments into_op {_} _ _ _ {_}.
(* No [Hint Mode] since we want to turn [?x] into [?x1 ⋅ ?x2], for example
when having [H : own ?x]. *)
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
104

105 106 107 108 109 110 111 112 113 114 115 116 117
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
118

119 120 121
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
122

123 124 125
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
126

127
Class FromExist {M A} (P : uPred M) (Φ : A  uPred M) :=
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
128
  from_exist : ( x, Φ x)  P.
129 130
Arguments from_exist {_ _} _ _ {_}.
Hint Mode FromExist + - ! - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
131

132
Class IntoExist {M A} (P : uPred M) (Φ : A  uPred M) :=
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
133
  into_exist : P   x, Φ x.
134 135
Arguments into_exist {_ _} _ _ {_}.
Hint Mode IntoExist + - ! - : typeclass_instances.
136

137 138 139 140 141
Class IntoForall {M A} (P : uPred M) (Φ : A  uPred M) :=
  into_forall : P   x, Φ x.
Arguments into_forall {_ _} _ _ {_}.
Hint Mode IntoForall + - ! - : typeclass_instances.

142 143 144
Class FromModal {M} (P Q : uPred M) := from_modal : Q  P.
Arguments from_modal {_} _ _ {_}.
Hint Mode FromModal + ! - : typeclass_instances.
145

146
Class ElimModal {M} (P P' : uPred M) (Q Q' : uPred M) :=
147
  elim_modal : P  (P' - Q')  Q.
148 149 150
Arguments elim_modal {_} _ _ _ _ {_}.
Hint Mode ElimModal + ! - ! - : typeclass_instances.
Hint Mode ElimModal + - ! - ! : typeclass_instances.
151

152
Lemma elim_modal_dummy {M} (P Q : uPred M) : ElimModal P P Q Q.
153
Proof. by rewrite /ElimModal wand_elim_r. Qed.
154

155 156 157
Class IsExcept0 {M} (Q : uPred M) := is_except_0 :  Q  Q.
Arguments is_except_0 {_} _ {_}.
Hint Mode IsExcept0 + ! : typeclass_instances.