upred.v 52.9 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.
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
303
304
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P  Q)  (Q  P))%I.
Infix "↔" := uPred_iff : uPred_scope.

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

308
309
Class PersistentP {M} (P : uPred M) := persistentP : P   P.
Arguments persistentP {_} _ {_}.
Robbert Krebbers's avatar
Robbert Krebbers committed
310

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

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

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

(** Introduction and elimination rules *)
464
Lemma const_intro φ P : φ  P   φ.
465
Proof. by intros ?; unseal; split. Qed.
466
Lemma const_elim φ Q R : Q   φ  (φ  Q  R)  Q  R.
467
468
469
Proof.
  unseal; intros HQP HQR; split=> n x ??; apply HQR; first eapply HQP; eauto.
Qed.
470
Lemma and_elim_l P Q : (P  Q)  P.
471
Proof. by unseal; split=> n x ? [??]. Qed.
472
Lemma and_elim_r P Q : (P  Q)  Q.
473
Proof. by unseal; split=> n x ? [??]. Qed.
474
Lemma and_intro P Q R : P  Q  P  R  P  (Q  R).
475
Proof. intros HQ HR; unseal; split=> n x ??; by split; [apply HQ|apply HR]. Qed.
476
Lemma or_intro_l P Q : P  (P  Q).
477
Proof. unseal; split=> n x ??; left; auto. Qed.
478
Lemma or_intro_r P Q : Q  (P  Q).
479
Proof. unseal; split=> n x ??; right; auto. Qed.
480
Lemma or_elim P Q R : P  R  Q  R  (P  Q)  R.
481
Proof. intros HP HQ; unseal; split=> n x ? [?|?]. by apply HP. by apply HQ. Qed.
482
Lemma impl_intro_r P Q R : (P  Q)  R  P  (Q  R).
Robbert Krebbers's avatar
Robbert Krebbers committed
483
Proof.
484
  unseal; intros HQ; split=> n x ?? n' x' ????.
485
  apply HQ; naive_solver eauto using uPred_weaken.
Robbert Krebbers's avatar
Robbert Krebbers committed
486
Qed.
487
Lemma impl_elim P Q R : P  (Q  R)  P  Q  P  R.
488
Proof. by unseal; intros HP HP'; split=> n x ??; apply HP with n x, HP'. Qed.
489
Lemma forall_intro {A} P (Ψ : A  uPred M): ( a, P  Ψ a)  P  ( a, Ψ a).
490
Proof. unseal; intros HPΨ; split=> n x ?? a; by apply HPΨ. Qed.
491
Lemma forall_elim {A} {Ψ : A  uPred M} a : ( a, Ψ a)  Ψ a.
492
Proof. unseal; split=> n x ? HP; apply HP. Qed.
493
Lemma exist_intro {A} {Ψ : A  uPred M} a : Ψ a  ( a, Ψ a).
494
Proof. unseal; split=> n x ??; by exists a. Qed.
495
Lemma exist_elim {A} (Φ : A  uPred M) Q : ( a, Φ a  Q)  ( a, Φ a)  Q.
496
Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed.
497
Lemma eq_refl {A : cofeT} (a : A) : True  (a  a).
498
Proof. unseal; by split=> n x ??; simpl. Qed.
499
Lemma eq_rewrite {A : cofeT} a b (Ψ : A  uPred M) P
500
  {HΨ :  n, Proper (dist n ==> dist n) Ψ} : P  (a  b)  P  Ψ a  P  Ψ b.
501
Proof.
502
503
504
  unseal; intros Hab Ha; split=> n x ??. 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
513
514
515
516
517
518
519
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.
520
521

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

539
Hint Resolve or_elim or_intro_l' or_intro_r'.
Robbert Krebbers's avatar
Robbert Krebbers committed
540
541
Hint Resolve and_intro and_elim_l' and_elim_r'.
Hint Immediate True_intro False_elim.
542

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

558
559
560
561
562
563
564
565
566
567
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.

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

617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
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 ()).
648
649
  - 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
650
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
651

652
Lemma or_and_l P Q R : (P  Q  R) ⊣⊢ ((P  Q)  (P  R)).
653
Proof.
654
  apply (anti_symm ()); first auto.
655
  do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
656
Qed.
657
Lemma or_and_r P Q R : (P  Q  R) ⊣⊢ ((P  R)  (Q  R)).
658
Proof. by rewrite -!(comm _ R) or_and_l. Qed.
659
Lemma and_or_l P Q R : (P  (Q  R)) ⊣⊢ (P  Q  P  R).