classes.v 2.7 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 5 6 7 8 9 10 11
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 _ _ _ {_}.

Ralf Jung's avatar
Ralf Jung committed
12
Class IntoPure (P : uPred M) (φ : Prop) := into_pure : P  ⌜φ⌝.
13 14
Global Arguments into_pure : clear implicits.

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

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

21 22
Class IntoLaterN (n : nat) (P Q : uPred M) := into_laterN : P  ^n Q.
Global Arguments into_laterN _ _ _ {_}.
23

24 25
Class FromLaterN (n : nat) (P Q : uPred M) := from_laterN : ^n Q  P.
Global Arguments from_laterN _ _ _ {_}.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
26

27
Class IntoWand (R P Q : uPred M) := into_wand : R  P - Q.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
28 29 30 31 32
Global Arguments into_wand : clear implicits.

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

33
Class FromSep (P Q1 Q2 : uPred M) := from_sep : Q1  Q2  P.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
34 35
Global Arguments from_sep : clear implicits.

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

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

43 44 45
Class FromOp {A : cmraT} (a b1 b2 : A) := from_op : b1  b2  a.
Global Arguments from_op {_} _ _ _ {_}.

Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
46 47 48
Class IntoOp {A : cmraT} (a b1 b2 : A) := into_op : a  b1  b2.
Global Arguments into_op {_} _ _ _ {_}.

49
Class Frame (R P Q : uPred M) := frame : R  Q  P.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
50 51 52 53 54 55 56 57 58 59 60 61 62 63 64
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 {_} _ _ {_}.
65

66 67
Class IntoModal (P Q : uPred M) := into_modal : P  Q.
Global Arguments into_modal : clear implicits.
68

69
Class ElimModal (P P' : uPred M) (Q Q' : uPred M) :=
70
  elim_modal : P  (P' - Q')  Q.
71
Global Arguments elim_modal _ _ _ _ {_}.
72

73 74
Lemma elim_modal_dummy P Q : ElimModal P P Q Q.
Proof. by rewrite /ElimModal wand_elim_r. Qed.
75

76 77
Class IsExcept0 (Q : uPred M) := is_except_0 :  Q  Q.
Global Arguments is_except_0 : clear implicits.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
78
End classes.