classes.v 5.56 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
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
108

109
110
111
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
112

113
114
115
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
116

117
Class FromExist {M A} (P : uPred M) (Φ : A  uPred M) :=
Robbert Krebbers's avatar
Oops!    
Robbert Krebbers committed
118
  from_exist : ( x, Φ x)  P.
119
120
Arguments from_exist {_ _} _ _ {_}.
Hint Mode FromExist + - ! - : typeclass_instances.
Robbert Krebbers's avatar
Oops!    
Robbert Krebbers committed
121

122
Class IntoExist {M A} (P : uPred M) (Φ : A  uPred M) :=
Robbert Krebbers's avatar
Oops!    
Robbert Krebbers committed
123
  into_exist : P   x, Φ x.
124
125
Arguments into_exist {_ _} _ _ {_}.
Hint Mode IntoExist + - ! - : typeclass_instances.
126

127
128
129
130
131
Class IntoForall {M A} (P : uPred M) (Φ : A  uPred M) :=
  into_forall : P   x, Φ x.
Arguments into_forall {_ _} _ _ {_}.
Hint Mode IntoForall + - ! - : typeclass_instances.

132
133
134
Class FromModal {M} (P Q : uPred M) := from_modal : Q  P.
Arguments from_modal {_} _ _ {_}.
Hint Mode FromModal + ! - : typeclass_instances.
135

136
Class ElimModal {M} (P P' : uPred M) (Q Q' : uPred M) :=
137
  elim_modal : P  (P' - Q')  Q.
138
139
140
Arguments elim_modal {_} _ _ _ _ {_}.
Hint Mode ElimModal + ! - ! - : typeclass_instances.
Hint Mode ElimModal + - ! - ! : typeclass_instances.
141

142
Lemma elim_modal_dummy {M} (P Q : uPred M) : ElimModal P P Q Q.
143
Proof. by rewrite /ElimModal wand_elim_r. Qed.
144

145
146
147
Class IsExcept0 {M} (Q : uPred M) := is_except_0 :  Q  Q.
Arguments is_except_0 {_} _ {_}.
Hint Mode IsExcept0 + ! : typeclass_instances.