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 _ _ _ {_}.

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.

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 _ _ {_}.

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.

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 {_} _ _ {_}.

Class TimelessElim (Q : uPred M) :=
  timeless_elim `{!TimelessP P} : ▷ P ★ (P -★ Q) ⊢ Q.
Global Arguments timeless_elim _ {_} _ {_}.
End classes.