upred.v 55.1 KB
Newer Older
1
From iris.algebra Require Export cmra.
2
3
Local Hint Extern 1 (_  _) => etrans; [eassumption|].
Local Hint Extern 1 (_  _) => etrans; [|eassumption].
Robbert Krebbers's avatar
Robbert Krebbers committed
4
5
Local Hint Extern 10 (_  _) => omega.

Robbert Krebbers's avatar
Robbert Krebbers committed
6
Record uPred (M : cmraT) : Type := IProp {
Robbert Krebbers's avatar
Robbert Krebbers committed
7
  uPred_holds :> nat  M  Prop;
Robbert Krebbers's avatar
Robbert Krebbers committed
8
9
  uPred_ne n x1 x2 : uPred_holds n x1  x1 {n} x2  uPred_holds n x2;
  uPred_weaken  n1 n2 x1 x2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
10
    uPred_holds n1 x1  x1  x2  n2  n1  {n2} x2  uPred_holds n2 x2
Robbert Krebbers's avatar
Robbert Krebbers committed
11
}.
12
Arguments uPred_holds {_} _ _ _ : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
13
14
Add Printing Constructor uPred.
Instance: Params (@uPred_holds) 3.
Robbert Krebbers's avatar
Robbert Krebbers committed
15

16
17
18
19
Delimit Scope uPred_scope with I.
Bind Scope uPred_scope with uPred.
Arguments uPred_holds {_} _%I _ _.

20
21
Section cofe.
  Context {M : cmraT}.
22
23
24
25
26
27
28

  Inductive uPred_equiv' (P Q : uPred M) : Prop :=
    { uPred_in_equiv :  n x, {n} x  P n x  Q n x }.
  Instance uPred_equiv : Equiv (uPred M) := uPred_equiv'.
  Inductive uPred_dist' (n : nat) (P Q : uPred M) : Prop :=
    { uPred_in_dist :  n' x, n'  n  {n'} x  P n' x  Q n' x }.
  Instance uPred_dist : Dist (uPred M) := uPred_dist'.
29
  Program Instance uPred_compl : Compl (uPred M) := λ c,
30
    {| uPred_holds n x := c n n x |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
31
  Next Obligation. by intros c n x y ??; simpl in *; apply uPred_ne with x. Qed.
32
  Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
33
    intros c n1 n2 x1 x2 ????; simpl in *.
34
    apply (chain_cauchy c n2 n1); eauto using uPred_weaken.
35
36
37
38
  Qed.
  Definition uPred_cofe_mixin : CofeMixin (uPred M).
  Proof.
    split.
39
40
41
    - intros P Q; split.
      + by intros HPQ n; split=> i x ??; apply HPQ.
      + intros HPQ; split=> n x ?; apply HPQ with n; auto.
42
    - intros n; split.
43
44
45
46
47
      + by intros P; split=> x i.
      + by intros P Q HPQ; split=> x i ??; symmetry; apply HPQ.
      + intros P Q Q' HP HQ; split=> i x ??.
        by trans (Q i x);[apply HP|apply HQ].
    - intros n P Q HPQ; split=> i x ??; apply HPQ; auto.
48
    - intros n c; split=>i x ??; symmetry; apply (chain_cauchy c i n); auto.
49
  Qed.
50
  Canonical Structure uPredC : cofeT := CofeT (uPred M) uPred_cofe_mixin.
51
52
53
End cofe.
Arguments uPredC : clear implicits.

54
Instance uPred_ne' {M} (P : uPred M) n : Proper (dist n ==> iff) (P n).
Robbert Krebbers's avatar
Robbert Krebbers committed
55
Proof. intros x1 x2 Hx; split; eauto using uPred_ne. Qed.
56
57
58
59
Instance uPred_proper {M} (P : uPred M) n : Proper (() ==> iff) (P n).
Proof. by intros x1 x2 Hx; apply uPred_ne', equiv_dist. Qed.

Lemma uPred_holds_ne {M} (P1 P2 : uPred M) n x :
60
  P1 {n} P2  {n} x  P1 n x  P2 n x.
61
Proof. intros HP ?; apply HP; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
Lemma uPred_weaken' {M} (P : uPred M) n1 n2 x1 x2 :
63
  x1  x2  n2  n1  {n2} x2  P n1 x1  P n2 x2.
64
Proof. eauto using uPred_weaken. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
66

(** functor *)
67
68
69
70
Program Definition uPred_map {M1 M2 : cmraT} (f : M2 -n> M1)
  `{!CMRAMonotone f} (P : uPred M1) :
  uPred M2 := {| uPred_holds n x := P n (f x) |}.
Next Obligation. by intros M1 M2 f ? P y1 y2 n ? Hy; rewrite /= -Hy. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
  naive_solver eauto using uPred_weaken, included_preserving, validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
Qed.
74
Instance uPred_map_ne {M1 M2 : cmraT} (f : M2 -n> M1)
Robbert Krebbers's avatar
Robbert Krebbers committed
75
  `{!CMRAMonotone f} n : Proper (dist n ==> dist n) (uPred_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Proof.
77
78
  intros x1 x2 Hx; split=> n' y ??.
  split; apply Hx; auto using validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Qed.
80
Lemma uPred_map_id {M : cmraT} (P : uPred M): uPred_map cid P  P.
81
Proof. by split=> n x ?. Qed.
82
Lemma uPred_map_compose {M1 M2 M3 : cmraT} (f : M1 -n> M2) (g : M2 -n> M3)
Robbert Krebbers's avatar
Robbert Krebbers committed
83
    `{!CMRAMonotone f, !CMRAMonotone g} (P : uPred M3):
84
  uPred_map (g  f) P  uPred_map f (uPred_map g P).
85
Proof. by split=> n x Hx. Qed.
86
Lemma uPred_map_ext {M1 M2 : cmraT} (f g : M1 -n> M2)
87
      `{!CMRAMonotone f} `{!CMRAMonotone g}:
88
  ( x, f x  g x)   x, uPred_map f x  uPred_map g x.
89
Proof. intros Hf P; split=> n x Hx /=; by rewrite /uPred_holds /= Hf. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
Robbert Krebbers's avatar
Robbert Krebbers committed
91
  uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1  uPredC M2).
92
Lemma uPredC_map_ne {M1 M2 : cmraT} (f g : M2 -n> M1)
Robbert Krebbers's avatar
Robbert Krebbers committed
93
    `{!CMRAMonotone f, !CMRAMonotone g} n :
94
  f {n} g  uPredC_map f {n} uPredC_map g.
Robbert Krebbers's avatar
Robbert Krebbers committed
95
Proof.
96
  by intros Hfg P; split=> n' y ??;
97
    rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
99

100
101
102
103
Program Definition uPredCF (F : rFunctor) : cFunctor := {|
  cFunctor_car A B := uPredC (rFunctor_car F B A);
  cFunctor_map A1 A2 B1 B2 fg := uPredC_map (rFunctor_map F (fg.2, fg.1))
|}.
104
105
106
107
Next Obligation.
  intros F A1 A2 B1 B2 n P Q HPQ.
  apply uPredC_map_ne, rFunctor_ne; split; by apply HPQ.
Qed.
108
109
110
111
112
113
114
115
116
Next Obligation.
  intros F A B P; simpl. rewrite -{2}(uPred_map_id P).
  apply uPred_map_ext=>y. by rewrite rFunctor_id.
Qed.
Next Obligation.
  intros F A1 A2 A3 B1 B2 B3 f g f' g' P; simpl. rewrite -uPred_map_compose.
  apply uPred_map_ext=>y; apply rFunctor_compose.
Qed.

117
118
119
120
121
122
123
Instance uPredCF_contractive F :
  rFunctorContractive F  cFunctorContractive (uPredCF F).
Proof.
  intros ? A1 A2 B1 B2 n P Q HPQ.
  apply uPredC_map_ne, rFunctor_contractive=> i ?; split; by apply HPQ.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
124
(** logical entailement *)
125
126
Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
  { uPred_in_entails :  n x, {n} x  P n x  Q n x }.
127
Hint Extern 0 (uPred_entails _ _) => reflexivity.
128
Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
Robbert Krebbers's avatar
Robbert Krebbers committed
129
130

(** logical connectives *)
131
Program Definition uPred_const_def {M} (φ : Prop) : uPred M :=
132
  {| uPred_holds n x := φ |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
133
Solve Obligations with done.
134
135
136
137
138
Definition uPred_const_aux : { x | x = @uPred_const_def }. by eexists. Qed.
Definition uPred_const {M} := proj1_sig uPred_const_aux M.
Definition uPred_const_eq :
  @uPred_const = @uPred_const_def := proj2_sig uPred_const_aux.

139
Instance uPred_inhabited M : Inhabited (uPred M) := populate (uPred_const True).
Robbert Krebbers's avatar
Robbert Krebbers committed
140

141
Program Definition uPred_and_def {M} (P Q : uPred M) : uPred M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
142
143
  {| uPred_holds n x := P n x  Q n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
144
145
146
147
148
Definition uPred_and_aux : { x | x = @uPred_and_def }. by eexists. Qed.
Definition uPred_and {M} := proj1_sig uPred_and_aux M.
Definition uPred_and_eq: @uPred_and = @uPred_and_def := proj2_sig uPred_and_aux.

Program Definition uPred_or_def {M} (P Q : uPred M) : uPred M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
149
150
  {| uPred_holds n x := P n x  Q n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
151
152
153
154
155
Definition uPred_or_aux : { x | x = @uPred_or_def }. by eexists. Qed.
Definition uPred_or {M} := proj1_sig uPred_or_aux M.
Definition uPred_or_eq: @uPred_or = @uPred_or_def := proj2_sig uPred_or_aux.

Program Definition uPred_impl_def {M} (P Q : uPred M) : uPred M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
156
  {| uPred_holds n x :=  n' x',
Robbert Krebbers's avatar
Robbert Krebbers committed
157
       x  x'  n'  n  {n'} x'  P n' x'  Q n' x' |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
159
160
  intros M P Q n1 x1' x1 HPQ Hx1 n2 x2 ????.
  destruct (cmra_included_dist_l n1 x1 x2 x1') as (x2'&?&Hx2); auto.
161
  assert (x2' {n2} x2) as Hx2' by (by apply dist_le with n1).
162
  assert ({n2} x2') by (by rewrite Hx2'); rewrite -Hx2'.
Robbert Krebbers's avatar
Robbert Krebbers committed
163
  eauto using uPred_weaken, uPred_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
164
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
Next Obligation. intros M P Q [|n] x1 x2; auto with lia. Qed.
166
167
168
169
Definition uPred_impl_aux : { x | x = @uPred_impl_def }. by eexists. Qed.
Definition uPred_impl {M} := proj1_sig uPred_impl_aux M.
Definition uPred_impl_eq :
  @uPred_impl = @uPred_impl_def := proj2_sig uPred_impl_aux.
Robbert Krebbers's avatar
Robbert Krebbers committed
170

171
Program Definition uPred_forall_def {M A} (Ψ : A  uPred M) : uPred M :=
172
  {| uPred_holds n x :=  a, Ψ a n x |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
174
175
176
177
178
179
Definition uPred_forall_aux : { x | x = @uPred_forall_def }. by eexists. Qed.
Definition uPred_forall {M A} := proj1_sig uPred_forall_aux M A.
Definition uPred_forall_eq :
  @uPred_forall = @uPred_forall_def := proj2_sig uPred_forall_aux.

Program Definition uPred_exist_def {M A} (Ψ : A  uPred M) : uPred M :=
180
  {| uPred_holds n x :=  a, Ψ a n x |}.
181
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
182
183
184
Definition uPred_exist_aux : { x | x = @uPred_exist_def }. by eexists. Qed.
Definition uPred_exist {M A} := proj1_sig uPred_exist_aux M A.
Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := proj2_sig uPred_exist_aux.
Robbert Krebbers's avatar
Robbert Krebbers committed
185

186
Program Definition uPred_eq_def {M} {A : cofeT} (a1 a2 : A) : uPred M :=
187
  {| uPred_holds n x := a1 {n} a2 |}.
188
Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
189
190
191
Definition uPred_eq_aux : { x | x = @uPred_eq_def }. by eexists. Qed.
Definition uPred_eq {M A} := proj1_sig uPred_eq_aux M A.
Definition uPred_eq_eq: @uPred_eq = @uPred_eq_def := proj2_sig uPred_eq_aux.
Robbert Krebbers's avatar
Robbert Krebbers committed
192

193
Program Definition uPred_sep_def {M} (P Q : uPred M) : uPred M :=
194
  {| uPred_holds n x :=  x1 x2, x {n} x1  x2  P n x1  Q n x2 |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
195
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
196
  by intros M P Q n x y (x1&x2&?&?&?) Hxy; exists x1, x2; rewrite -Hxy.
Robbert Krebbers's avatar
Robbert Krebbers committed
197
198
Qed.
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
199
  intros M P Q n1 n2 x y (x1&x2&Hx&?&?) Hxy ??.
200
  assert ( x2', y {n2} x1  x2'  x2  x2') as (x2'&Hy&?).
201
  { destruct Hxy as [z Hy]; exists (x2  z); split; eauto using cmra_included_l.
202
    apply dist_le with n1; auto. by rewrite (assoc op) -Hx Hy. }
203
  clear Hxy; cofe_subst y; exists x1, x2'; split_and?; [done| |].
Robbert Krebbers's avatar
Robbert Krebbers committed
204
205
  - apply uPred_weaken with n1 x1; eauto using cmra_validN_op_l.
  - apply uPred_weaken with n1 x2; eauto using cmra_validN_op_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
206
Qed.
207
208
209
Definition uPred_sep_aux : { x | x = @uPred_sep_def }. by eexists. Qed.
Definition uPred_sep {M} := proj1_sig uPred_sep_aux M.
Definition uPred_sep_eq: @uPred_sep = @uPred_sep_def := proj2_sig uPred_sep_aux.
Robbert Krebbers's avatar
Robbert Krebbers committed
210

211
Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
212
  {| uPred_holds n x :=  n' x',
Robbert Krebbers's avatar
Robbert Krebbers committed
213
       n'  n  {n'} (x  x')  P n' x'  Q n' (x  x') |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
214
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
215
  intros M P Q n1 x1 x2 HPQ Hx n2 x3 ???; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
216
  rewrite -(dist_le _ _ _ _ Hx) //; apply HPQ; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
217
  by rewrite (dist_le _ _ _ _ Hx).
Robbert Krebbers's avatar
Robbert Krebbers committed
218
219
Qed.
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
220
221
  intros M P Q n1 n2 x1 x2 HPQ ??? n3 x3 ???; simpl in *.
  apply uPred_weaken with n3 (x1  x3);
222
    eauto using cmra_validN_included, cmra_preserving_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
223
Qed.
224
225
226
227
Definition uPred_wand_aux : { x | x = @uPred_wand_def }. by eexists. Qed.
Definition uPred_wand {M} := proj1_sig uPred_wand_aux M.
Definition uPred_wand_eq :
  @uPred_wand = @uPred_wand_def := proj2_sig uPred_wand_aux.
Robbert Krebbers's avatar
Robbert Krebbers committed
228

229
Program Definition uPred_always_def {M} (P : uPred M) : uPred M :=
Ralf Jung's avatar
Ralf Jung committed
230
  {| uPred_holds n x := P n (core x) |}.
231
Next Obligation. by intros M P x1 x2 n ? Hx; rewrite /= -Hx. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
232
Next Obligation.
Ralf Jung's avatar
Ralf Jung committed
233
234
  intros M P n1 n2 x1 x2 ????; eapply uPred_weaken with n1 (core x1);
    eauto using cmra_core_preserving, cmra_core_validN.
Robbert Krebbers's avatar
Robbert Krebbers committed
235
Qed.
236
237
238
239
240
241
Definition uPred_always_aux : { x | x = @uPred_always_def }. by eexists. Qed.
Definition uPred_always {M} := proj1_sig uPred_always_aux M.
Definition uPred_always_eq :
  @uPred_always = @uPred_always_def := proj2_sig uPred_always_aux.

Program Definition uPred_later_def {M} (P : uPred M) : uPred M :=
242
243
244
245
246
  {| uPred_holds n x := match n return _ with 0 => True | S n' => P n' x end |}.
Next Obligation. intros M P [|n] ??; eauto using uPred_ne,(dist_le (A:=M)). Qed.
Next Obligation.
  intros M P [|n1] [|n2] x1 x2; eauto using uPred_weaken,cmra_validN_S; try lia.
Qed.
247
248
249
250
Definition uPred_later_aux : { x | x = @uPred_later_def }. by eexists. Qed.
Definition uPred_later {M} := proj1_sig uPred_later_aux M.
Definition uPred_later_eq :
  @uPred_later = @uPred_later_def := proj2_sig uPred_later_aux.
Robbert Krebbers's avatar
Robbert Krebbers committed
251

252
Program Definition uPred_ownM_def {M : cmraT} (a : M) : uPred M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
253
  {| uPred_holds n x := a {n} x |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
254
Next Obligation. by intros M a n x1 x2 [a' ?] Hx; exists a'; rewrite -Hx. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
255
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
256
  intros M a n1 n2 x1 x [a' Hx1] [x2 Hx] ??.
257
  exists (a'  x2). by rewrite (assoc op) -(dist_le _ _ _ _ Hx1) // Hx.
Robbert Krebbers's avatar
Robbert Krebbers committed
258
Qed.
259
260
261
262
263
264
Definition uPred_ownM_aux : { x | x = @uPred_ownM_def }. by eexists. Qed.
Definition uPred_ownM {M} := proj1_sig uPred_ownM_aux M.
Definition uPred_ownM_eq :
  @uPred_ownM = @uPred_ownM_def := proj2_sig uPred_ownM_aux.

Program Definition uPred_valid_def {M A : cmraT} (a : A) : uPred M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
265
  {| uPred_holds n x := {n} a |}.
266
Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
267
268
269
270
Definition uPred_valid_aux : { x | x = @uPred_valid_def }. by eexists. Qed.
Definition uPred_valid {M A} := proj1_sig uPred_valid_aux M A.
Definition uPred_valid_eq :
  @uPred_valid = @uPred_valid_def := proj2_sig uPred_valid_aux.
Robbert Krebbers's avatar
Robbert Krebbers committed
271

272
273
274
275
Notation "P ⊢ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope.
Notation "(⊢)" := uPred_entails (only parsing) : C_scope.
Notation "P ⊣⊢ Q" := (equiv (A:=uPred _) P%I Q%I) (at level 70) : C_scope.
Notation "(⊣⊢)" := (equiv (A:=uPred _)) (only parsing) : C_scope.
276
277
Notation "■ φ" := (uPred_const φ%C%type)
  (at level 20, right associativity) : uPred_scope.
Ralf Jung's avatar
Ralf Jung committed
278
Notation "x = y" := (uPred_const (x%C%type = y%C%type)) : uPred_scope.
279
Notation "x ⊥ y" := (uPred_const (x%C%type  y%C%type)) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
280
281
282
Notation "'False'" := (uPred_const False) : uPred_scope.
Notation "'True'" := (uPred_const True) : uPred_scope.
Infix "∧" := uPred_and : uPred_scope.
283
Notation "(∧)" := uPred_and (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
284
Infix "∨" := uPred_or : uPred_scope.
285
Notation "(∨)" := uPred_or (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
286
287
Infix "→" := uPred_impl : uPred_scope.
Infix "★" := uPred_sep (at level 80, right associativity) : uPred_scope.
288
Notation "(★)" := uPred_sep (only parsing) : uPred_scope.
289
Notation "P -★ Q" := (uPred_wand P Q)
Robbert Krebbers's avatar
Robbert Krebbers committed
290
  (at level 99, Q at level 200, right associativity) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
291
Notation "∀ x .. y , P" :=
292
  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%I) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
293
Notation "∃ x .. y , P" :=
294
  (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%I) : uPred_scope.
295
296
Notation "□ P" := (uPred_always P)
  (at level 20, right associativity) : uPred_scope.
297
298
Notation "▷ P" := (uPred_later P)
  (at level 20, right associativity) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
299
Infix "≡" := uPred_eq : uPred_scope.
300
Notation "✓ x" := (uPred_valid x) (at level 20) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
301

302
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P  Q)  (Q  P))%I.
303
Instance: Params (@uPred_iff) 1.
304
305
Infix "↔" := uPred_iff : uPred_scope.

306
307
308
309
310
311
312
Definition uPred_always_if {M} (p : bool) (P : uPred M) : uPred M :=
  (if p then  P else P)%I.
Instance: Params (@uPred_always_if) 2.
Arguments uPred_always_if _ !_ _/.
Notation "□? p P" := (uPred_always_if p P)
  (at level 20, p at level 0, P at level 20, format "□? p  P").

313
Class TimelessP {M} (P : uPred M) := timelessP :  P  (P   False).
314
Arguments timelessP {_} _ {_}.
315

316
317
Class PersistentP {M} (P : uPred M) := persistentP : P   P.
Arguments persistentP {_} _ {_}.
Robbert Krebbers's avatar
Robbert Krebbers committed
318

319
320
321
322
323
324
325
326
Module uPred.
Definition unseal :=
  (uPred_const_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
  uPred_exist_eq, uPred_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_always_eq,
  uPred_later_eq, uPred_ownM_eq, uPred_valid_eq).
Ltac unseal := rewrite !unseal.

Section uPred_logic.
327
Context {M : cmraT}.
328
Implicit Types φ : Prop.
Robbert Krebbers's avatar
Robbert Krebbers committed
329
Implicit Types P Q : uPred M.
330
Implicit Types A : Type.
331
332
Notation "P ⊢ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
Notation "P ⊣⊢ Q" := (equiv (A:=uPred M) P%I Q%I). (* Force implicit argument M *)
333
Arguments uPred_holds {_} !_ _ _ /.
334
Hint Immediate uPred_in_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
335

336
Global Instance: PreOrder (@uPred_entails M).
337
338
339
340
341
Proof.
  split.
  * by intros P; split=> x i.
  * by intros P Q Q' HP HQ; split=> x i ??; apply HQ, HP.
Qed.
342
Global Instance: AntiSymm (⊣⊢) (@uPred_entails M).
343
Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed.
344
Lemma equiv_spec P Q : P ⊣⊢ Q  P  Q  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
345
Proof.
346
  split; [|by intros [??]; apply (anti_symm ())].
347
  intros HPQ; split; split=> x i; apply HPQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
348
Qed.
349
Lemma equiv_entails P Q : P ⊣⊢ Q  P  Q.
350
Proof. apply equiv_spec. Qed.
351
Lemma equiv_entails_sym P Q : Q ⊣⊢ P  P  Q.
352
Proof. apply equiv_spec. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
353
Global Instance entails_proper :
354
  Proper ((⊣⊢) ==> (⊣⊢) ==> iff) (() : relation (uPred M)).
Robbert Krebbers's avatar
Robbert Krebbers committed
355
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
356
  move => P1 P2 /equiv_spec [HP1 HP2] Q1 Q2 /equiv_spec [HQ1 HQ2]; split; intros.
357
358
  - by trans P1; [|trans Q1].
  - by trans P2; [|trans Q2].
Robbert Krebbers's avatar
Robbert Krebbers committed
359
Qed.
360
Lemma entails_equiv_l (P Q R : uPred M) : P ⊣⊢ Q  Q  R  P  R.
361
Proof. by intros ->. Qed.
362
Lemma entails_equiv_r (P Q R : uPred M) : P  Q  Q ⊣⊢ R  P  R.
363
Proof. by intros ? <-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
364

365
(** Non-expansiveness and setoid morphisms *)
366
Global Instance const_proper : Proper (iff ==> (⊣⊢)) (@uPred_const M).
367
Proof. intros φ1 φ2 Hφ. by unseal; split=> -[|n] ?; try apply Hφ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
368
Global Instance and_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_and M).
Robbert Krebbers's avatar
Robbert Krebbers committed
369
Proof.
370
  intros P P' HP Q Q' HQ; unseal; split=> x n' ??.
371
  split; (intros [??]; split; [by apply HP|by apply HQ]).
Robbert Krebbers's avatar
Robbert Krebbers committed
372
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
373
Global Instance and_proper :
374
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_and M) := ne_proper_2 _.
Robbert Krebbers's avatar
Robbert Krebbers committed
375
Global Instance or_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_or M).
Robbert Krebbers's avatar
Robbert Krebbers committed
376
Proof.
377
  intros P P' HP Q Q' HQ; split=> x n' ??.
378
  unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
Robbert Krebbers's avatar
Robbert Krebbers committed
379
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
380
Global Instance or_proper :
381
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_or M) := ne_proper_2 _.
Robbert Krebbers's avatar
Robbert Krebbers committed
382
Global Instance impl_ne n :
Robbert Krebbers's avatar
Robbert Krebbers committed
383
  Proper (dist n ==> dist n ==> dist n) (@uPred_impl M).
Robbert Krebbers's avatar
Robbert Krebbers committed
384
Proof.
385
  intros P P' HP Q Q' HQ; split=> x n' ??.
386
  unseal; split; intros HPQ x' n'' ????; apply HQ, HPQ, HP; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
387
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
388
Global Instance impl_proper :
389
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_impl M) := ne_proper_2 _.
Robbert Krebbers's avatar
Robbert Krebbers committed
390
Global Instance sep_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
391
Proof.
392
  intros P P' HP Q Q' HQ; split=> n' x ??.
393
  unseal; split; intros (x1&x2&?&?&?); cofe_subst x;
394
    exists x1, x2; split_and!; try (apply HP || apply HQ);
395
    eauto using cmra_validN_op_l, cmra_validN_op_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
396
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
397
Global Instance sep_proper :
398
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_sep M) := ne_proper_2 _.
Robbert Krebbers's avatar
Robbert Krebbers committed
399
Global Instance wand_ne n :
Robbert Krebbers's avatar
Robbert Krebbers committed
400
  Proper (dist n ==> dist n ==> dist n) (@uPred_wand M).
Robbert Krebbers's avatar
Robbert Krebbers committed
401
Proof.
402
  intros P P' HP Q Q' HQ; split=> n' x ??; unseal; split; intros HPQ x' n'' ???;
403
    apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
404
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
405
Global Instance wand_proper :
406
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_wand M) := ne_proper_2 _.
Robbert Krebbers's avatar
Robbert Krebbers committed
407
Global Instance eq_ne (A : cofeT) n :
Robbert Krebbers's avatar
Robbert Krebbers committed
408
  Proper (dist n ==> dist n ==> dist n) (@uPred_eq M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
409
Proof.
410
  intros x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
411
412
  * by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
  * by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
413
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
414
Global Instance eq_proper (A : cofeT) :
415
  Proper (() ==> () ==> (⊣⊢)) (@uPred_eq M A) := ne_proper_2 _.
416
Global Instance forall_ne A n :
Robbert Krebbers's avatar
Robbert Krebbers committed
417
  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A).
418
419
420
Proof.
  by intros Ψ1 Ψ2 HΨ; unseal; split=> n' x; split; intros HP a; apply HΨ.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
421
Global Instance forall_proper A :
422
  Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (@uPred_forall M A).
423
424
425
Proof.
  by intros Ψ1 Ψ2 HΨ; unseal; split=> n' x; split; intros HP a; apply HΨ.
Qed.
426
Global Instance exist_ne A n :
Robbert Krebbers's avatar
Robbert Krebbers committed
427
  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A).
428
Proof.
429
430
  intros Ψ1 Ψ2 HΨ.
  unseal; split=> n' x ??; split; intros [a ?]; exists a; by apply HΨ.
431
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
432
Global Instance exist_proper A :
433
  Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (@uPred_exist M A).
434
Proof.
435
436
  intros Ψ1 Ψ2 HΨ.
  unseal; split=> n' x ?; split; intros [a ?]; exists a; by apply HΨ.
437
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
438
Global Instance later_contractive : Contractive (@uPred_later M).
Robbert Krebbers's avatar
Robbert Krebbers committed
439
Proof.
440
  intros n P Q HPQ; unseal; split=> -[|n'] x ??; simpl; [done|].
441
  apply (HPQ n'); eauto using cmra_validN_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
442
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
443
Global Instance later_proper :
444
  Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_later M) := ne_proper _.
445
446
Global Instance always_ne n : Proper (dist n ==> dist n) (@uPred_always M).
Proof.
447
  intros P1 P2 HP.
Ralf Jung's avatar
Ralf Jung committed
448
  unseal; split=> n' x; split; apply HP; eauto using cmra_core_validN.
449
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
450
Global Instance always_proper :
451
  Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always M) := ne_proper _.
452
Global Instance ownM_ne n : Proper (dist n ==> dist n) (@uPred_ownM M).
453
Proof.
454
455
  intros a b Ha.
  unseal; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
456
Qed.
457
Global Instance ownM_proper: Proper (() ==> (⊣⊢)) (@uPred_ownM M) := ne_proper _.
458
Global Instance valid_ne {A : cmraT} n :
459
460
Proper (dist n ==> dist n) (@uPred_valid M A).
Proof.
461
462
  intros a b Ha; unseal; split=> n' x ? /=.
  by rewrite (dist_le _ _ _ _ Ha); last lia.
463
Qed.
464
Global Instance valid_proper {A : cmraT} :
465
  Proper (() ==> (⊣⊢)) (@uPred_valid M A) := ne_proper _.
Robbert Krebbers's avatar
Robbert Krebbers committed
466
Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
467
Proof. unfold uPred_iff; solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
468
Global Instance iff_proper :
469
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_iff M) := ne_proper_2 _.
Robbert Krebbers's avatar
Robbert Krebbers committed
470
471

(** Introduction and elimination rules *)
472
Lemma const_intro φ P : φ  P   φ.
473
Proof. by intros ?; unseal; split. Qed.
474
Lemma const_elim φ Q R : Q   φ  (φ  Q  R)  Q  R.
475
476
477
Proof.
  unseal; intros HQP HQR; split=> n x ??; apply HQR; first eapply HQP; eauto.
Qed.
478
Lemma and_elim_l P Q : (P  Q)  P.
479
Proof. by unseal; split=> n x ? [??]. Qed.
480
Lemma and_elim_r P Q : (P  Q)  Q.
481
Proof. by unseal; split=> n x ? [??]. Qed.
482
Lemma and_intro P Q R : P  Q  P  R  P  (Q  R).
483
Proof. intros HQ HR; unseal; split=> n x ??; by split; [apply HQ|apply HR]. Qed.
484
Lemma or_intro_l P Q : P  (P  Q).
485
Proof. unseal; split=> n x ??; left; auto. Qed.
486
Lemma or_intro_r P Q : Q  (P  Q).
487
Proof. unseal; split=> n x ??; right; auto. Qed.
488
Lemma or_elim P Q R : P  R  Q  R  (P  Q)  R.
489
Proof. intros HP HQ; unseal; split=> n x ? [?|?]. by apply HP. by apply HQ. Qed.
490
Lemma impl_intro_r P Q R : (P  Q)  R  P  (Q  R).
Robbert Krebbers's avatar
Robbert Krebbers committed
491
Proof.
492
  unseal; intros HQ; split=> n x ?? n' x' ????.
493
  apply HQ; naive_solver eauto using uPred_weaken.
Robbert Krebbers's avatar
Robbert Krebbers committed
494
Qed.
495
Lemma impl_elim P Q R : P  (Q  R)  P  Q  P  R.
496
Proof. by unseal; intros HP HP'; split=> n x ??; apply HP with n x, HP'. Qed.
497
Lemma forall_intro {A} P (Ψ : A  uPred M): ( a, P  Ψ a)  P  ( a, Ψ a).
498
Proof. unseal; intros HPΨ; split=> n x ?? a; by apply HPΨ. Qed.
499
Lemma forall_elim {A} {Ψ : A  uPred M} a : ( a, Ψ a)  Ψ a.
500
Proof. unseal; split=> n x ? HP; apply HP. Qed.
501
Lemma exist_intro {A} {Ψ : A  uPred M} a : Ψ a  ( a, Ψ a).
502
Proof. unseal; split=> n x ??; by exists a. Qed.
503
Lemma exist_elim {A} (Φ : A  uPred M) Q : ( a, Φ a  Q)  ( a, Φ a)  Q.
504
Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed.
505
Lemma eq_refl {A : cofeT} (a : A) : True  (a  a).
506
Proof. unseal; by split=> n x ??; simpl. Qed.
507
Lemma eq_rewrite {A : cofeT} a b (Ψ : A  uPred M) P
508
  {HΨ :  n, Proper (dist n ==> dist n) Ψ} : P  (a  b)  P  Ψ a  P  Ψ b.
509
Proof.
510
511
512
  unseal; intros Hab Ha; split=> n x ??. apply HΨ with n a; auto.
  - by symmetry; apply Hab with x.
  - by apply Ha.
513
Qed.
Ralf Jung's avatar
Ralf Jung committed
514
Lemma eq_equiv `{Empty M, !CMRAUnit M} {A : cofeT} (a b : A) :
515
  True  (a  b)  a  b.
516
Proof.
517
  unseal=> Hab; apply equiv_dist; intros n; apply Hab with ; last done.
Ralf Jung's avatar
Ralf Jung committed
518
  apply cmra_valid_validN, cmra_unit_valid.
519
Qed.
520
521
522
523
524
525
526
527
Lemma eq_rewrite_contractive {A : cofeT} a b (Ψ : A  uPred M) P
  {HΨ : Contractive Ψ} : P   (a  b)  P  Ψ a  P  Ψ b.
Proof.
  unseal; intros Hab Ha; split=> n x ??. apply HΨ with n a; auto.
  - destruct n; intros m ?; first omega. apply (dist_le n); last omega.
    symmetry. by destruct Hab as [Hab]; eapply (Hab (S n)).
  - by apply Ha.
Qed.
528
529

(* Derived logical stuff *)
530
531
Lemma False_elim P : False  P.
Proof. by apply (const_elim False). Qed.
532
Lemma True_intro P : P  True.
Robbert Krebbers's avatar
Robbert Krebbers committed
533
Proof. by apply const_intro. Qed.
534
Lemma and_elim_l' P Q R : P  R  (P  Q)  R.
535
Proof. by rewrite and_elim_l. Qed.
536
Lemma and_elim_r' P Q R : Q  R  (P  Q)  R.
537
Proof. by rewrite and_elim_r. Qed.
538
Lemma or_intro_l' P Q R : P  Q  P  (Q  R).
539
Proof. intros ->; apply or_intro_l. Qed.
540
Lemma or_intro_r' P Q R : P  R  P  (Q  R).
541
Proof. intros ->; apply or_intro_r. Qed.
542
Lemma exist_intro' {A} P (Ψ : A  uPred M) a : P  Ψ a  P  ( a, Ψ a).
543
Proof. intros ->; apply exist_intro. Qed.
544
Lemma forall_elim' {A} P (Ψ : A  uPred M) : P  ( a, Ψ a)  ( a, P  Ψ a).
545
Proof. move=> HP a. by rewrite HP forall_elim. Qed.
546

547
Hint Resolve or_elim or_intro_l' or_intro_r'.
Robbert Krebbers's avatar
Robbert Krebbers committed
548
549
Hint Resolve and_intro and_elim_l' and_elim_r'.
Hint Immediate True_intro False_elim.
550

551
Lemma impl_intro_l P Q R : (Q  P)  R  P  (Q  R).
552
Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
553
Lemma impl_elim_l P Q : ((P  Q)  P)  Q.
554
Proof. apply impl_elim with P; auto. Qed.
555
Lemma impl_elim_r P Q : (P  (P  Q))  Q.
556
Proof. apply impl_elim with P; auto. Qed.
557
Lemma impl_elim_l' P Q R : P  (Q  R)  (P  Q)  R.
558
Proof. intros; apply impl_elim with Q; auto. Qed.
559
Lemma impl_elim_r' P Q R : Q  (P  R)  (P  Q)  R.
560
Proof. intros; apply impl_elim with P; auto. Qed.
561
Lemma impl_entails P Q : True  (P  Q)  P  Q.
562
Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
563
Lemma entails_impl P Q : (P  Q)  True  (P  Q).
564
Proof. auto using impl_intro_l. Qed.
565

566
567
568
569
570
571
572
573
574
575
Lemma iff_refl Q P : Q  (P  P).
Proof. rewrite /uPred_iff; apply and_intro; apply impl_intro_l; auto. Qed.
Lemma iff_equiv P Q : True  (P  Q)  P ⊣⊢ Q.
Proof.
  intros HPQ; apply (anti_symm ());
    apply impl_entails; rewrite HPQ /uPred_iff; auto.
Qed.
Lemma equiv_iff P Q : P ⊣⊢ Q  True  (P  Q).
Proof. intros ->; apply iff_refl. Qed.

576
Lemma const_mono φ1 φ2 : (φ1  φ2)   φ1   φ2.
577
Proof. intros; apply const_elim with φ1; eauto using const_intro. Qed.
578
Lemma and_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
579
Proof. auto. Qed.
580
Lemma and_mono_l P P' Q : P  Q  (P  P')  (Q  P').
581
Proof. by intros; apply and_mono. Qed.
582
Lemma and_mono_r P P' Q' : P'  Q'  (P  P')  (P  Q').
583
Proof. by apply and_mono. Qed.
584
Lemma or_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
585
Proof. auto. Qed.
586
Lemma or_mono_l P P' Q : P  Q  (P  P')  (Q  P').
587
Proof. by intros; apply or_mono. Qed.
588
Lemma or_mono_r P P' Q' : P'  Q'  (P  P')  (P  Q').
589
Proof. by apply or_mono. Qed.
590
Lemma impl_mono P P' Q Q' : Q  P  P'  Q'  (P  P')  (Q  Q').
591
Proof.
592
  intros HP HQ'; apply impl_intro_l; rewrite -HQ'.
593
  apply impl_elim with P; eauto.
594
Qed.
595
Lemma forall_mono {A} (Φ Ψ : A  uPred M) :
596
  ( a, Φ a  Ψ a)  ( a, Φ a)  ( a, Ψ a).
597
Proof.
598
  intros HP. apply forall_intro=> a; rewrite -(HP a); apply forall_elim.
599
Qed.
600
Lemma exist_mono {A} (Φ Ψ : A  uPred M) :
601
  ( a, Φ a  Ψ a)  ( a, Φ a)  ( a, Ψ a).
602
Proof. intros HΦ. apply exist_elim=> a; rewrite (HΦ a); apply exist_intro. Qed.
603
Global Instance const_mono' : Proper (impl ==> ()) (@uPred_const M).
604
Proof. intros φ1 φ2; apply const_mono. Qed.
605
Global Instance and_mono' : Proper (() ==> () ==> ()) (@uPred_and M).
Robbert Krebbers's avatar
Robbert Krebbers committed
606
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
607
Global Instance and_flip_mono' :
608
  Proper (flip () ==> flip () ==> flip ()) (@uPred_and M).
609
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
610
Global Instance or_mono' : Proper (() ==> () ==> ()) (@uPred_or M).
Robbert Krebbers's avatar
Robbert Krebbers committed
611
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
612
Global Instance or_flip_mono' :
613
  Proper (flip () ==> flip () ==> flip ()) (@uPred_or M).
614
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
615
Global Instance impl_mono' :
616
  Proper (flip () ==> () ==> ()) (@uPred_impl M).
Robbert Krebbers's avatar
Robbert Krebbers committed
617
618
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
Global Instance forall_mono' A :
619
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
620
621
Proof. intros P1 P2; apply forall_mono. Qed.
Global Instance exist_mono' A :
622
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
623
Proof. intros P1 P2; apply exist_mono. Qed.
624

625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
Global Instance and_idem : IdemP (⊣⊢) (@uPred_and M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance or_idem : IdemP (⊣⊢) (@uPred_or M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance and_comm : Comm (⊣⊢) (@uPred_and M).
Proof. intros P Q; apply (anti_symm ()); auto. Qed.
Global Instance True_and : LeftId (⊣⊢) True%I (@uPred_and M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance and_True : RightId (⊣⊢) True%I (@uPred_and M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance False_and : LeftAbsorb (⊣⊢) False%I (@uPred_and M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance and_False : RightAbsorb (⊣⊢) False%I (@uPred_and M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance True_or : LeftAbsorb (⊣⊢) True%I (@uPred_or M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance or_True : RightAbsorb (⊣⊢) True%I (@uPred_or M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance False_or : LeftId (⊣⊢) False%I (@uPred_or M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance or_False : RightId (⊣⊢) False%I (@uPred_or M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance and_assoc : Assoc (⊣⊢) (@uPred_and M).
Proof. intros P Q R; apply (anti_symm ()); auto. Qed.
Global Instance or_comm : Comm (⊣⊢) (@uPred_or M).
Proof. intros P Q; apply (anti_symm ()); auto. Qed.
Global Instance or_assoc : Assoc (⊣⊢) (@uPred_or M).
Proof. intros P Q R; apply (anti_symm ()); auto. Qed.
Global Instance True_impl : LeftId (⊣⊢) True%I (@uPred_impl M).
Proof.
  intros P; apply (anti_symm ()).
656
657
  - by rewrite -(left_id True%I uPred_and (_  _)%I) impl_elim_r.
  - by apply impl_intro_l; rewrite left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
658
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
659

660
Lemma or_and_l P Q R : (P  Q  R) ⊣⊢ ((P  Q)  (P  R)).
661
Proof.
662
  apply (anti_symm ()); first auto.
663
  do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.