classes.v 4.11 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 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29
Class FromAssumption {M} (p : bool) (P Q : uPred M) :=
  from_assumption : ?p P  Q.
Arguments from_assumption {_} _ _ _ {_}.
Hint Mode FromAssumption + + ! - : typeclass_instances.

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
30 31 32 33 34 35 36 37
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.

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

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

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

69 70 71
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
72

73 74 75
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
76

77 78 79
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
80

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

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

91 92 93
Class FromModal {M} (P Q : uPred M) := from_modal : Q  P.
Arguments from_modal {_} _ _ {_}.
Hint Mode FromModal + ! - : typeclass_instances.
94

95
Class ElimModal {M} (P P' : uPred M) (Q Q' : uPred M) :=
96
  elim_modal : P  (P' - Q')  Q.
97 98 99
Arguments elim_modal {_} _ _ _ _ {_}.
Hint Mode ElimModal + ! - ! - : typeclass_instances.
Hint Mode ElimModal + - ! - ! : typeclass_instances.
100

101
Lemma elim_modal_dummy {M} (P Q : uPred M) : ElimModal P P Q Q.
102
Proof. by rewrite /ElimModal wand_elim_r. Qed.
103

104 105 106
Class IsExcept0 {M} (Q : uPred M) := is_except_0 :  Q  Q.
Arguments is_except_0 {_} _ {_}.
Hint Mode IsExcept0 + ! : typeclass_instances.