upred.v 52.5 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
50
51
52
53
  Qed.
  Canonical Structure uPredC : cofeT := CofeT uPred_cofe_mixin.
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
279
280
281
Notation "'False'" := (uPred_const False) : uPred_scope.
Notation "'True'" := (uPred_const True) : uPred_scope.
Infix "∧" := uPred_and : uPred_scope.
282
Notation "(∧)" := uPred_and (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
283
Infix "∨" := uPred_or : uPred_scope.
284
Notation "(∨)" := uPred_or (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
285
286
Infix "→" := uPred_impl : uPred_scope.
Infix "★" := uPred_sep (at level 80, right associativity) : uPred_scope.
287
Notation "(★)" := uPred_sep (only parsing) : uPred_scope.
288
Notation "P -★ Q" := (uPred_wand P Q)
289
  (at level 199, Q at level 200, right associativity) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
290
Notation "∀ x .. y , P" :=
291
  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%I) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
292
Notation "∃ x .. y , P" :=
293
  (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%I) : uPred_scope.
294
295
Notation "□ P" := (uPred_always P)
  (at level 20, right associativity) : uPred_scope.
296
297
Notation "▷ P" := (uPred_later P)
  (at level 20, right associativity) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
298
Infix "≡" := uPred_eq : uPred_scope.
299
Notation "✓ x" := (uPred_valid x) (at level 20) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
300

301
302
303
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P  Q)  (Q  P))%I.
Infix "↔" := uPred_iff : uPred_scope.

304
Class TimelessP {M} (P : uPred M) := timelessP :  P  (P   False).
305
Arguments timelessP {_} _ {_}.
306
307
308

Class Persistent {M} (P : uPred M) := persistent : P   P.
Arguments persistent {_} _ {_}.
Robbert Krebbers's avatar
Robbert Krebbers committed
309

310
311
312
313
314
315
316
317
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.
318
Context {M : cmraT}.
319
Implicit Types φ : Prop.
Robbert Krebbers's avatar
Robbert Krebbers committed
320
Implicit Types P Q : uPred M.
321
Implicit Types A : Type.
322
323
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 *)
324
Arguments uPred_holds {_} !_ _ _ /.
325
Hint Immediate uPred_in_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
326

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

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

(** Introduction and elimination rules *)
463
Lemma const_intro φ P : φ  P   φ.
464
Proof. by intros ?; unseal; split. Qed.
465
Lemma const_elim φ Q R : Q   φ  (φ  Q  R)  Q  R.
466
467
468
Proof.
  unseal; intros HQP HQR; split=> n x ??; apply HQR; first eapply HQP; eauto.
Qed.
469
Lemma False_elim P : False  P.
470
Proof. by unseal; split=> n x ?. Qed.
471
Lemma and_elim_l P Q : (P  Q)  P.
472
Proof. by unseal; split=> n x ? [??]. Qed.
473
Lemma and_elim_r P Q : (P  Q)  Q.
474
Proof. by unseal; split=> n x ? [??]. Qed.
475
Lemma and_intro P Q R : P  Q  P  R  P  (Q  R).
476
Proof. intros HQ HR; unseal; split=> n x ??; by split; [apply HQ|apply HR]. Qed.
477
Lemma or_intro_l P Q : P  (P  Q).
478
Proof. unseal; split=> n x ??; left; auto. Qed.
479
Lemma or_intro_r P Q : Q  (P  Q).
480
Proof. unseal; split=> n x ??; right; auto. Qed.
481
Lemma or_elim P Q R : P  R  Q  R  (P  Q)  R.
482
Proof. intros HP HQ; unseal; split=> n x ? [?|?]. by apply HP. by apply HQ. Qed.
483
Lemma impl_intro_r P Q R : (P  Q)  R  P  (Q  R).
Robbert Krebbers's avatar
Robbert Krebbers committed
484
Proof.
485
  unseal; intros HQ; split=> n x ?? n' x' ????.
486
  apply HQ; naive_solver eauto using uPred_weaken.
Robbert Krebbers's avatar
Robbert Krebbers committed
487
Qed.
488
Lemma impl_elim P Q R : P  (Q  R)  P  Q  P  R.
489
Proof. by unseal; intros HP HP'; split=> n x ??; apply HP with n x, HP'. Qed.
490
Lemma forall_intro {A} P (Ψ : A  uPred M): ( a, P  Ψ a)  P  ( a, Ψ a).
491
Proof. unseal; intros HPΨ; split=> n x ?? a; by apply HPΨ. Qed.
492
Lemma forall_elim {A} {Ψ : A  uPred M} a : ( a, Ψ a)  Ψ a.
493
Proof. unseal; split=> n x ? HP; apply HP. Qed.
494
Lemma exist_intro {A} {Ψ : A  uPred M} a : Ψ a  ( a, Ψ a).
495
Proof. unseal; split=> n x ??; by exists a. Qed.
496
Lemma exist_elim {A} (Φ : A  uPred M) Q : ( a, Φ a  Q)  ( a, Φ a)  Q.
497
Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed.
498
Lemma eq_refl {A : cofeT} (a : A) P : P  (a  a).
499
Proof. unseal; by split=> n x ??; simpl. Qed.
500
Lemma eq_rewrite {A : cofeT} a b (Ψ : A  uPred M) P
501
  `{HΨ :  n, Proper (dist n ==> dist n) Ψ} : P  (a  b)  P  Ψ a  P  Ψ b.
502
Proof.
503
  unseal; intros Hab Ha; split=> n x ??.
504
  apply HΨ with n a; auto. by symmetry; apply Hab with x. by apply Ha.
505
Qed.
Ralf Jung's avatar
Ralf Jung committed
506
Lemma eq_equiv `{Empty M, !CMRAUnit M} {A : cofeT} (a b : A) :
507
  True  (a  b)  a  b.
508
Proof.
509
  unseal=> Hab; apply equiv_dist; intros n; apply Hab with ; last done.
Ralf Jung's avatar
Ralf Jung committed
510
  apply cmra_valid_validN, cmra_unit_valid.
511
Qed.
512
Lemma iff_equiv P Q : True  (P  Q)  P ⊣⊢ Q.
513
514
515
516
Proof.
  rewrite /uPred_iff; unseal=> HPQ.
  split=> n x ?; split; intros; by apply HPQ with n x.
Qed.
517
518

(* Derived logical stuff *)
519
Lemma True_intro P : P  True.
Robbert Krebbers's avatar
Robbert Krebbers committed
520
Proof. by apply const_intro. Qed.
521
Lemma and_elim_l' P Q R : P  R  (P  Q)  R.
522
Proof. by rewrite and_elim_l. Qed.
523
Lemma and_elim_r' P Q R : Q  R  (P  Q)  R.
524
Proof. by rewrite and_elim_r. Qed.
525
Lemma or_intro_l' P Q R : P  Q  P  (Q  R).
526
Proof. intros ->; apply or_intro_l. Qed.
527
Lemma or_intro_r' P Q R : P  R  P  (Q  R).
528
Proof. intros ->; apply or_intro_r. Qed.
529
Lemma exist_intro' {A} P (Ψ : A  uPred M) a : P  Ψ a  P  ( a, Ψ a).
530
Proof. intros ->; apply exist_intro. Qed.
531
Lemma forall_elim' {A} P (Ψ : A  uPred M) : P  ( a, Ψ a)  ( a, P  Ψ a).
532
Proof. move=> HP a. by rewrite HP forall_elim. Qed.
533

534
Hint Resolve or_elim or_intro_l' or_intro_r'.
Robbert Krebbers's avatar
Robbert Krebbers committed
535
536
Hint Resolve and_intro and_elim_l' and_elim_r'.
Hint Immediate True_intro False_elim.
537

538
Lemma impl_intro_l P Q R : (Q  P)  R  P  (Q  R).
539
Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
540
Lemma impl_elim_l P Q : ((P  Q)  P)  Q.
541
Proof. apply impl_elim with P; auto. Qed.
542
Lemma impl_elim_r P Q : (P  (P  Q))  Q.
543
Proof. apply impl_elim with P; auto. Qed.
544
Lemma impl_elim_l' P Q R : P  (Q  R)  (P  Q)  R.
545
Proof. intros; apply impl_elim with Q; auto. Qed.
546
Lemma impl_elim_r' P Q R : Q  (P  R)  (P  Q)  R.
547
Proof. intros; apply impl_elim with P; auto. Qed.
548
Lemma impl_entails P Q : True  (P  Q)  P  Q.
549
Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
550
Lemma entails_impl P Q : (P  Q)  True  (P  Q).
551
Proof. auto using impl_intro_l. Qed.
552

553
Lemma const_mono φ1 φ2 : (φ1  φ2)   φ1   φ2.
554
Proof. intros; apply const_elim with φ1; eauto using const_intro. Qed.
555
Lemma and_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
556
Proof. auto. Qed.
557
Lemma and_mono_l P P' Q : P  Q  (P  P')  (Q  P').
558
Proof. by intros; apply and_mono. Qed.
559
Lemma and_mono_r P P' Q' : P'  Q'  (P  P')  (P  Q').
560
Proof. by apply and_mono. Qed.
561
Lemma or_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
562
Proof. auto. Qed.
563
Lemma or_mono_l P P' Q : P  Q  (P  P')  (Q  P').
564
Proof. by intros; apply or_mono. Qed.
565
Lemma or_mono_r P P' Q' : P'  Q'  (P  P')  (P  Q').
566
Proof. by apply or_mono. Qed.
567
Lemma impl_mono P P' Q Q' : Q  P  P'  Q'  (P  P')  (Q  Q').
568
Proof.
569
  intros HP HQ'; apply impl_intro_l; rewrite -HQ'.
570
  apply impl_elim with P; eauto.
571
Qed.
572
Lemma forall_mono {A} (Φ Ψ : A  uPred M) :
573
  ( a, Φ a  Ψ a)  ( a, Φ a)  ( a, Ψ a).
574
Proof.
575
  intros HP. apply forall_intro=> a; rewrite -(HP a); apply forall_elim.
576
Qed.
577
Lemma exist_mono {A} (Φ Ψ : A  uPred M) :
578
  ( a, Φ a  Ψ a)  ( a, Φ a)  ( a, Ψ a).
579
Proof. intros HΦ. apply exist_elim=> a; rewrite (HΦ a); apply exist_intro. Qed.
580
Global Instance const_mono' : Proper (impl ==> ()) (@uPred_const M).
581
Proof. intros φ1 φ2; apply const_mono. Qed.
582
Global Instance and_mono' : Proper (() ==> () ==> ()) (@uPred_and M).
Robbert Krebbers's avatar
Robbert Krebbers committed
583
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
584
Global Instance and_flip_mono' :
585
  Proper (flip () ==> flip () ==> flip ()) (@uPred_and M).
586
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
587
Global Instance or_mono' : Proper (() ==> () ==> ()) (@uPred_or M).
Robbert Krebbers's avatar
Robbert Krebbers committed
588
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
589
Global Instance or_flip_mono' :
590
  Proper (flip () ==> flip () ==> flip ()) (@uPred_or M).
591
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
592
Global Instance impl_mono' :
593
  Proper (flip () ==> () ==> ()) (@uPred_impl M).
Robbert Krebbers's avatar
Robbert Krebbers committed
594
595
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
Global Instance forall_mono' A :
596
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
597
598
Proof. intros P1 P2; apply forall_mono. Qed.
Global Instance exist_mono' A :
599
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
600
Proof. intros P1 P2; apply exist_mono. Qed.
601

602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
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 ()).
633
634
  - 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
635
Qed.
636
Lemma iff_refl Q P : Q  (P  P).
Robbert Krebbers's avatar
Robbert Krebbers committed
637
638
Proof. rewrite /uPred_iff; apply and_intro; apply impl_intro_l; auto. Qed.

639
Lemma or_and_l P Q R : (P  Q  R) ⊣⊢ ((P  Q)  (P  R)).
640
Proof.
641
  apply (anti_symm ()); first auto.
642
  do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
643
Qed.
644
Lemma or_and_r P Q R : (P  Q  R) ⊣⊢ ((P  R)  (Q  R)).
645
Proof. by rewrite -!(comm _ R) or_and_l. Qed.
646
Lemma and_or_l P Q R : (P  (Q  R)) ⊣⊢ (P  Q  P  R).
647
Proof.
648
  apply (anti_symm ()); last auto.
649
  apply impl_elim_r', or_elim; apply impl_intro_l; auto.