classes.v 2.26 KB
Newer Older
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
1
2
3
4
5
6
7
8
9
10
From iris.algebra Require Export upred.
Import uPred.

Section classes.
Context {M : ucmraT}.
Implicit Types P Q : uPred M.

Class FromAssumption (p : bool) (P Q : uPred M) := from_assumption : ?p P  Q.
Global Arguments from_assumption _ _ _ {_}.

11
12
13
14
15
Class IntoPure (P : uPred M) (φ : Prop) := into_pure : P   φ.
Global Arguments into_pure : clear implicits.

Class FromPure (P : uPred M) (φ : Prop) := from_pure : φ  True  P.
Global Arguments from_pure : clear implicits.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
16
17
18
19
20
21

Class IntoPersistentP (P Q : uPred M) := into_persistentP : P   Q.
Global Arguments into_persistentP : clear implicits.

Class IntoLater (P Q : uPred M) := into_later : P   Q.
Global Arguments into_later _ _ {_}.
22

Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
23
24
25
26
27
28
29
30
31
32
33
34
35
36
Class FromLater (P Q : uPred M) := from_later :  Q  P.
Global Arguments from_later _ _ {_}.

Class IntoWand (R P Q : uPred M) := into_wand : R  P - Q.
Global Arguments into_wand : clear implicits.

Class FromAnd (P Q1 Q2 : uPred M) := from_and : Q1  Q2  P.
Global Arguments from_and : clear implicits.

Class FromSep (P Q1 Q2 : uPred M) := from_sep : Q1  Q2  P.
Global Arguments from_sep : clear implicits.

Class IntoSep (p: bool) (P Q1 Q2 : uPred M) := into_sep : ?p P  ?p (Q1  Q2).
Global Arguments into_sep : clear implicits.
37

Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
Class IntoOp {A : cmraT} (a b1 b2 : A) := into_op : a  b1  b2.
Global Arguments into_op {_} _ _ _ {_}.

Class Frame (R P Q : uPred M) := frame : R  Q  P.
Global Arguments frame : clear implicits.

Class FromOr (P Q1 Q2 : uPred M) := from_or : Q1  Q2  P.
Global Arguments from_or : clear implicits.

Class IntoOr P Q1 Q2 := into_or : P  Q1  Q2.
Global Arguments into_or : clear implicits.

Class FromExist {A} (P : uPred M) (Φ : A  uPred M) :=
  from_exist : ( x, Φ x)  P.
Global Arguments from_exist {_} _ _ {_}.

Class IntoExist {A} (P : uPred M) (Φ : A  uPred M) :=
  into_exist : P   x, Φ x.
Global Arguments into_exist {_} _ _ {_}.
57

58
59
60
61
62
63
64
65
66
Class IsNowTrue (Q : uPred M) := is_now_True :  Q  Q.
Global Arguments is_now_True : clear implicits.

Class FromVs (P Q : uPred M) := from_vs : (|=r=> Q)  P.
Global Arguments from_vs : clear implicits.

Class ElimVs (P P' : uPred M) (Q Q' : uPred M) :=
  elim_vs : P  (P' - Q')  Q.
Arguments elim_vs _ _ _ _ {_}.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
67
End classes.