derived_connectives.v 4.6 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
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.
14
Infix "∗-∗" := bi_wand_iff : bi_scope.
15

16
Class Persistent {PROP : bi} (P : PROP) := persistent : P  <pers> P.
17
18
19
20
21
22
23
24
25
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.
26
Notation "'<affine>' P" := (bi_affinely P) : bi_scope.
27

28
29
30
31
32
33
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.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
34
Hint Mode BiAffine ! : typeclass_instances.
35
36
37
Existing Instance absorbing_bi | 0.

Class BiPositive (PROP : bi) :=
38
  bi_positive (P Q : PROP) : <affine> (P  Q)  <affine> P  Q.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
39
Hint Mode BiPositive ! : typeclass_instances.
40
41
42
43
44

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.
45
Notation "'<absorb>' P" := (bi_absorbingly P) : bi_scope.
46

47
Class Absorbing {PROP : bi} (P : PROP) := absorbing : <absorb> P  P.
48
49
Arguments Absorbing {_} _%I : simpl never.
Arguments absorbing {_} _%I.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
50
Hint Mode Absorbing + ! : typeclass_instances.
51
52

Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
53
  (if p then <pers> P else P)%I.
54
55
56
Arguments bi_persistently_if {_} !_ _%I /.
Instance: Params (@bi_persistently_if) 2.
Typeclasses Opaque bi_persistently_if.
57
Notation "'<pers>?' p P" := (bi_persistently_if p P) : bi_scope.
58
59

Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
60
  (if p then <affine> P else P)%I.
61
62
63
Arguments bi_affinely_if {_} !_ _%I /.
Instance: Params (@bi_affinely_if) 2.
Typeclasses Opaque bi_affinely_if.
64
Notation "'<affine>?' p P" := (bi_affinely_if p P) : bi_scope.
65

66
67
68
69
70
Definition bi_intuitionistically {PROP : bi} (P : PROP) : PROP :=
  (<affine> <pers> P)%I.
Arguments bi_intuitionistically {_} _%I : simpl never.
Instance: Params (@bi_intuitionistically) 1.
Typeclasses Opaque bi_intuitionistically.
71
Notation "□ P" := (bi_intuitionistically P) : bi_scope.
72
73
74
75
76
77

Definition bi_intuitionistically_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
  (if p then  P else P)%I.
Arguments bi_intuitionistically_if {_} !_ _%I /.
Instance: Params (@bi_intuitionistically_if) 2.
Typeclasses Opaque bi_intuitionistically_if.
78
Notation "'□?' p P" := (bi_intuitionistically_if p P) : bi_scope.
79
80
81
82
83
84
85
86
87
88
89
90

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.

91
92
93
94
95
Fixpoint sbi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP :=
  match n with
  | O => P
  | S n' =>  sbi_laterN n' P
  end%I.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
96
97
Arguments sbi_laterN {_} !_%nat_scope _%I.
Instance: Params (@sbi_laterN) 2.
98
99
Notation "▷^ n P" := (sbi_laterN n P) : bi_scope.
Notation "▷? p P" := (sbi_laterN (Nat.b2n p) P) : bi_scope.
100

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
101
102
Definition sbi_except_0 {PROP : sbi} (P : PROP) : PROP := ( False  P)%I.
Arguments sbi_except_0 {_} _%I : simpl never.
103
Notation "◇ P" := (sbi_except_0 P) : bi_scope.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
104
105
Instance: Params (@sbi_except_0) 1.
Typeclasses Opaque sbi_except_0.
106
107
108
109
110
111

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.
112
113
114
115
116
117
118
119
120
121
122
123

(** An optional precondition [mP] to [Q].
    TODO: We may actually consider generalizing this to a list of preconditions,
    and e.g. also using it for texan triples. *)
Definition bi_wandM {PROP : bi} (mP : option PROP) (Q : PROP) : PROP :=
  match mP with
  | None => Q
  | Some P => (P - Q)%I
  end.
Arguments bi_wandM {_} !_%I _%I /.
Notation "mP -∗? Q" := (bi_wandM mP Q)
  (at level 99, Q at level 200, right associativity) : bi_scope.