derived_connectives.v 4.49 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
From iris.bi Require Export interface.
From iris.algebra Require Import monoid.
From stdpp Require Import hlist.

Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P  Q)  (Q  P))%I.
Arguments bi_iff {_} _%I _%I : simpl never.
Instance: Params (@bi_iff) 1.
Infix "↔" := bi_iff : bi_scope.

Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP :=
  ((P - Q)  (Q - P))%I.
Arguments bi_wand_iff {_} _%I _%I : simpl never.
Instance: Params (@bi_wand_iff) 1.
Infix "∗-∗" := bi_wand_iff (at level 95, no associativity) : bi_scope.

Class Plain {PROP : bi} (P : PROP) := plain : P  bi_plainly P.
Arguments Plain {_} _%I : simpl never.
Arguments plain {_} _%I {_}.
Hint Mode Plain + ! : typeclass_instances.
Instance: Params (@Plain) 1.

Class Persistent {PROP : bi} (P : PROP) := persistent : P  bi_persistently P.
Arguments Persistent {_} _%I : simpl never.
Arguments persistent {_} _%I {_}.
Hint Mode Persistent + ! : typeclass_instances.
Instance: Params (@Persistent) 1.

Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp  P)%I.
Arguments bi_affinely {_} _%I : simpl never.
Instance: Params (@bi_affinely) 1.
Typeclasses Opaque bi_affinely.
Notation "□ P" := (bi_affinely (bi_persistently P))%I
  (at level 20, right associativity) : bi_scope.
Notation "■ P" := (bi_affinely (bi_plainly P))%I
  (at level 20, right associativity) : bi_scope.

Class Affine {PROP : bi} (Q : PROP) := affine : Q  emp.
Arguments Affine {_} _%I : simpl never.
Arguments affine {_} _%I {_}.
Hint Mode Affine + ! : typeclass_instances.

Class BiAffine (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
Existing Instance absorbing_bi | 0.

Class BiPositive (PROP : bi) :=
  bi_positive (P Q : PROP) : bi_affinely (P  Q)  bi_affinely P  Q.

48 49 50 51 52
Class BiPlainlyExist (PROP : bi) :=
  plainly_exist_1 A (Ψ : A  PROP) :
    bi_plainly ( a, Ψ a)   a, bi_plainly (Ψ a).
Arguments plainly_exist_1 _ {_ _} _.

53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96
Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True  P)%I.
Arguments bi_absorbingly {_} _%I : simpl never.
Instance: Params (@bi_absorbingly) 1.
Typeclasses Opaque bi_absorbingly.

Class Absorbing {PROP : bi} (P : PROP) := absorbing : bi_absorbingly P  P.
Arguments Absorbing {_} _%I : simpl never.
Arguments absorbing {_} _%I.

Definition bi_plainly_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
  (if p then bi_plainly P else P)%I.
Arguments bi_plainly_if {_} !_ _%I /.
Instance: Params (@bi_plainly_if) 2.
Typeclasses Opaque bi_plainly_if.

Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
  (if p then bi_persistently P else P)%I.
Arguments bi_persistently_if {_} !_ _%I /.
Instance: Params (@bi_persistently_if) 2.
Typeclasses Opaque bi_persistently_if.

Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
  (if p then bi_affinely P else P)%I.
Arguments bi_affinely_if {_} !_ _%I /.
Instance: Params (@bi_affinely_if) 2.
Typeclasses Opaque bi_affinely_if.
Notation "□? p P" := (bi_affinely_if p (bi_persistently_if p P))%I
  (at level 20, p at level 9, P at level 20,
   right associativity, format "□? p  P") : bi_scope.
Notation "■? p P" := (bi_affinely_if p (bi_plainly_if p P))%I
  (at level 20, p at level 9, P at level 20,
   right associativity, format "■? p  P") : bi_scope.

Fixpoint bi_hexist {PROP : bi} {As} : himpl As PROP  PROP :=
  match As return himpl As PROP  PROP with
  | tnil => id
  | tcons A As => λ Φ,  x, bi_hexist (Φ x)
  end%I.
Fixpoint bi_hforall {PROP : bi} {As} : himpl As PROP  PROP :=
  match As return himpl As PROP  PROP with
  | tnil => id
  | tcons A As => λ Φ,  x, bi_hforall (Φ x)
  end%I.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
97 98 99 100 101
Definition sbi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP :=
  Nat.iter n sbi_later P.
Arguments sbi_laterN {_} !_%nat_scope _%I.
Instance: Params (@sbi_laterN) 2.
Notation "▷^ n P" := (sbi_laterN n P)
102
  (at level 20, n at level 9, P at level 20, format "▷^ n  P") : bi_scope.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
103
Notation "▷? p P" := (sbi_laterN (Nat.b2n p) P)
104 105
  (at level 20, p at level 9, P at level 20, format "▷? p  P") : bi_scope.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
106 107 108 109 110
Definition sbi_except_0 {PROP : sbi} (P : PROP) : PROP := ( False  P)%I.
Arguments sbi_except_0 {_} _%I : simpl never.
Notation "◇ P" := (sbi_except_0 P) (at level 20, right associativity) : bi_scope.
Instance: Params (@sbi_except_0) 1.
Typeclasses Opaque sbi_except_0.
111 112 113 114 115 116

Class Timeless {PROP : sbi} (P : PROP) := timeless :  P   P.
Arguments Timeless {_} _%I : simpl never.
Arguments timeless {_} _%I {_}.
Hint Mode Timeless + ! : typeclass_instances.
Instance: Params (@Timeless) 1.