classes.v 2.53 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
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.

35
36
37
Class IntoAnd (p : bool) (P Q1 Q2 : uPred M) :=
  into_and : P  if p then Q1  Q2 else Q1  Q2.
Global Arguments into_and : clear implicits.
38

39
40
Lemma mk_into_and_sep p P Q1 Q2 : (P  Q1  Q2)  IntoAnd p P Q1 Q2.
Proof. rewrite /IntoAnd=>->. destruct p; auto using sep_and. Qed.
41

Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
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 {_} _ _ {_}.
61

62
63
64
Class IntoNowTrue (P Q : uPred M) := into_now_True : P   Q.
Global Arguments into_now_True : clear implicits.

65
66
67
68
69
70
71
72
73
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
74
End classes.