(* iris/bi/derived_connectives.v *)
From iris.algebra Require Import monoid
From iris.bi Require Export interface
From iris.prelude Require Import options

Definition bi_iff{PROP : bi} (P Q : PROP) : PROP := (P → Q) ∧ (Q → P).

Global Argumentsbi_iff {_} _%_I _%_I : simpl never.

Global Instance: Params (@bi_iff) 1 := {}.
Infix "↔" := bi_iff : bi_scope.

Definition bi_wand_iff{PROP : bi} (P Q : PROP) : PROP :=
  (P -∗ Q) ∧ (Q -∗ P).

Global Argumentsbi_wand_iff {_} _%_I _%_I : simpl never.

Global Instance: Params (@bi_wand_iff) 1 := {}.
Infix "∗-∗" := bi_wand_iff : bi_scope.

Class Persistent{PROP : bi} (P : PROP) := persistent : P ⊢ <pers> P.

Global ArgumentsPersistent {_} _%_I : simpl never.

Global Argumentspersistent {_} _%_I {_}.

Global HintMode Persistent + ! : typeclass_instances.

Global Instance: Params (@Persistent) 1 := {}.

Global HintExtern 100 (Persistent (match ?x with _ => _ end)) =>
  destruct x : typeclass_instances.

Definition bi_affinely{PROP : bi} (P : PROP) : PROP := emp ∧ P.

Global Argumentsbi_affinely {_} _%_I : simpl never.

Global Instance: Params (@bi_affinely) 1 := {}.

Global TypeclassesOpaque bi_affinely.

Class Affine{PROP : bi} (Q : PROP) := affine : Q ⊢ emp.

Global ArgumentsAffine {_} _%_I : simpl never.

Global Argumentsaffine {_} _%_I {_}.

Global HintMode Affine + ! : typeclass_instances.

Global HintExtern 100 (Affine (match ?x with _ => _ end)) =>
  destruct x : typeclass_instances.

Definition bi_absorbingly{PROP : bi} (P : PROP) : PROP := True ∗ P.

Global Argumentsbi_absorbingly {_} _%_I : simpl never.

Global Instance: Params (@bi_absorbingly) 1 := {}.

Global TypeclassesOpaque bi_absorbingly.

Class Absorbing{PROP : bi} (P : PROP) := absorbing : <absorb> P ⊢ P.

Global ArgumentsAbsorbing {_} _%_I : simpl never.

Global Argumentsabsorbing {_} _%_I.

Global HintMode Absorbing + ! : typeclass_instances.

Global HintExtern 100 (Absorbing (match ?x with _ => _ end)) =>
  destruct x : typeclass_instances.

Definition bi_persistently_if{PROP : bi} (p : bool) (P : PROP) : PROP :=
  (if p then <pers> P else P)%I.

Global Argumentsbi_persistently_if {_} !_ _%_I /.

Global Instance: Params (@bi_persistently_if) 2 := {}.

Global TypeclassesOpaque bi_persistently_if.

Definition bi_affinely_if{PROP : bi} (p : bool) (P : PROP) : PROP :=
  (if p then <affine> P else P)%I.

Global Argumentsbi_affinely_if {_} !_ _%_I /.

Global Instance: Params (@bi_affinely_if) 2 := {}.

Global TypeclassesOpaque bi_affinely_if.

Definition bi_absorbingly_if{PROP : bi} (p : bool) (P : PROP) : PROP :=
  (if p then <absorb> P else P)%I.

Global Argumentsbi_absorbingly_if {_} !_ _%_I /.

Global Instance: Params (@bi_absorbingly_if) 2 := {}.

Global TypeclassesOpaque bi_absorbingly_if.

Definition bi_intuitionistically{PROP : bi} (P : PROP) : PROP :=
  (<affine> <pers> P)%I.

Global Argumentsbi_intuitionistically {_} _%_I : simpl never.

Global Instance: Params (@bi_intuitionistically) 1 := {}.

Global TypeclassesOpaque bi_intuitionistically.

Definition bi_intuitionistically_if{PROP : bi} (p : bool) (P : PROP) : PROP :=
  (if p then □ P else P)%I.

Global Argumentsbi_intuitionistically_if {_} !_ _%_I /.

Global Instance: Params (@bi_intuitionistically_if) 2 := {}.

Global TypeclassesOpaque bi_intuitionistically_if.

Fixpoint bi_laterN{PROP : bi} (n : nat) (P : PROP) : PROP :=
  match n with
  | O => P
  | S n' => ▷ ▷^n' P
  end
where "▷^ n P" := (bi_laterN n P) : bi_scope.

Global Argumentsbi_laterN {_} !_%_nat_scope _%_I.

Global Instance: Params (@bi_laterN) 2 := {}.

Definition bi_except_0{PROP : bi} (P : PROP) : PROP := ▷ False ∨ P.

Global Argumentsbi_except_0 {_} _%_I : simpl never.

Global Instance: Params (@bi_except_0) 1 := {}.

Global TypeclassesOpaque bi_except_0.

Class Timeless{PROP : bi} (P : PROP) := timeless : ▷ P ⊢ ◇ P.

Global ArgumentsTimeless {_} _%_I : simpl never.

Global Argumentstimeless {_} _%_I {_}.

Global HintMode Timeless + ! : typeclass_instances.

Global Instance: Params (@Timeless) 1 := {}.

Global HintExtern 100 (Timeless (match ?x with _ => _ end)) =>
  destruct x : typeclass_instances.

Definition bi_wandM{PROP : bi} (mP : option PROP) (Q : PROP) : PROP :=
  match mP with
  | None => Q
  | Some P => P -∗ Q
  end.

Global Argumentsbi_wandM {_} !_%_I _%_I /.