classes.v 4.39 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 24 25 26 27 28 29 30 31

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.

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

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
32 33 34 35 36 37 38 39
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.

40 41 42 43 44 45 46 47 48 49 50 51 52 53
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) :=
54
  into_and : P  if p then Q1  Q2 else Q1  Q2.
55 56 57 58
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.
59
Proof. rewrite /IntoAnd=>->. destruct p; auto using sep_and. Qed.
60

61
Class FromOp {A : cmraT} (a b1 b2 : A) := from_op : b1  b2  a.
62 63 64
Arguments from_op {_} _ _ _ {_}.
Hint Mode FromOp + ! - - : typeclass_instances.
Hint Mode FromOp + - ! ! : typeclass_instances. (* For iCombine *)
65

Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
66
Class IntoOp {A : cmraT} (a b1 b2 : A) := into_op : a  b1  b2.
67 68 69
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
70

71 72 73
Class Frame {M} (R P Q : uPred M) := frame : R  Q  P.
Arguments frame {_} _ _ _ {_}.
Hint Mode Frame + ! ! - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
74

75 76 77
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
78

79 80 81
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
82

83
Class FromExist {M A} (P : uPred M) (Φ : A  uPred M) :=
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
84
  from_exist : ( x, Φ x)  P.
85 86
Arguments from_exist {_ _} _ _ {_}.
Hint Mode FromExist + - ! - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
87

88
Class IntoExist {M A} (P : uPred M) (Φ : A  uPred M) :=
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
89
  into_exist : P   x, Φ x.
90 91
Arguments into_exist {_ _} _ _ {_}.
Hint Mode IntoExist + - ! - : typeclass_instances.
92

93 94 95 96 97
Class IntoForall {M A} (P : uPred M) (Φ : A  uPred M) :=
  into_forall : P   x, Φ x.
Arguments into_forall {_ _} _ _ {_}.
Hint Mode IntoForall + - ! - : typeclass_instances.

98 99 100
Class FromModal {M} (P Q : uPred M) := from_modal : Q  P.
Arguments from_modal {_} _ _ {_}.
Hint Mode FromModal + ! - : typeclass_instances.
101

102
Class ElimModal {M} (P P' : uPred M) (Q Q' : uPred M) :=
103
  elim_modal : P  (P' - Q')  Q.
104 105 106
Arguments elim_modal {_} _ _ _ _ {_}.
Hint Mode ElimModal + ! - ! - : typeclass_instances.
Hint Mode ElimModal + - ! - ! : typeclass_instances.
107

108
Lemma elim_modal_dummy {M} (P Q : uPred M) : ElimModal P P Q Q.
109
Proof. by rewrite /ElimModal wand_elim_r. Qed.
110

111 112 113
Class IsExcept0 {M} (Q : uPred M) := is_except_0 :  Q  Q.
Arguments is_except_0 {_} _ {_}.
Hint Mode IsExcept0 + ! : typeclass_instances.