upred.v 9.03 KB
Newer Older
1
From iris.algebra Require Export cmra.
2
Set Default Proof Using "Type".
3

Ralf Jung's avatar
Ralf Jung committed
4
5
6
7
8
(** The basic definition of the uPred type, its metric and functor laws.
    You probably do not want to import this file. Instead, import
    base_logic.base_logic; that will also give you all the primitive
    and many derived laws for the logic. *)

9
10
Record uPred (M : ucmraT) : Type := IProp {
  uPred_holds :> nat  M  Prop;
11
12
13
14

  (* [uPred_mono] is used to prove non-expansiveness (guaranteed by
     [uPred_ne]). Therefore, it is important that we do not restrict
     it to only valid elements. *)
15
  uPred_mono n x1 x2 : uPred_holds n x1  x1 {n} x2  uPred_holds n x2;
16
17
18
19
20

  (* We have to restrict this to hold only for valid elements,
     otherwise this condition is no longer limit preserving, and uPred
     does no longer form a COFE (i.e., [uPred_compl] breaks). This is
     because the distance and equivalence on this cofe ignores the
Jacques-Henri Jourdan's avatar
Typos.    
Jacques-Henri Jourdan committed
21
     truth value on invalid elements. This, in turn, is required by
22
23
24
     the fact that entailment has to ignore invalid elements, which is
     itself essential for proving [ownM_valid].

Jacques-Henri Jourdan's avatar
Typos.    
Jacques-Henri Jourdan committed
25
26
27
28
29
30
     We could, actually, remove this restriction and make this
     condition apply even to invalid elements: we have proved that
     uPred is isomorphic to a sub-COFE of the COFE of predicates that
     are monotonous both with respect to the step index and with
     respect to x. However, that would essentially require changing
     (by making it more complicated) the model of many connectives of
31
32
33
34
35
36
37
38
39
40
41
42
43
44
     the logic, which we don't want.
     This sub-COFE is the sub-COFE of monotonous sProp predicates P
     such that the following sProp assertion is valid:
          ∀ x, (V(x) → P(x)) → P(x)
     Where V is the validity predicate.

     Another way of saying that this is equivalent to this definition of
     uPred is to notice that our definition of uPred is equivalent to
     quotienting the COFE of monotonous sProp predicates with the
     following (sProp) equivalence relation:
       P1 ≡ P2  :=  ∀ x, V(x) → (P1(x) ↔ P2(x))
     whose equivalence classes appear to all have one only canonical
     representative such that ∀ x, (V(x) → P(x)) → P(x).
 *)
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
  uPred_closed n1 n2 x : uPred_holds n1 x  n2  n1  {n2} x  uPred_holds n2 x
}.
Arguments uPred_holds {_} _ _ _ : simpl never.
Add Printing Constructor uPred.
Instance: Params (@uPred_holds) 3.

Delimit Scope uPred_scope with I.
Bind Scope uPred_scope with uPred.
Arguments uPred_holds {_} _%I _ _.

Section cofe.
  Context {M : ucmraT}.

  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'.
64
  Definition uPred_ofe_mixin : OfeMixin (uPred M).
65
66
67
68
69
70
71
72
73
74
75
76
  Proof.
    split.
    - intros P Q; split.
      + by intros HPQ n; split=> i x ??; apply HPQ.
      + intros HPQ; split=> n x ?; apply HPQ with n; auto.
    - intros n; split.
      + 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.
  Qed.
77
78
79
80
81
82
83
84
85
86
87
88
89
  Canonical Structure uPredC : ofeT := OfeT (uPred M) uPred_ofe_mixin.

  Program Definition uPred_compl : Compl uPredC := λ c,
    {| uPred_holds n x := c n n x |}.
  Next Obligation. naive_solver eauto using uPred_mono. Qed.
  Next Obligation.
    intros c n1 n2 x ???; simpl in *.
    apply (chain_cauchy c n2 n1); eauto using uPred_closed.
  Qed.
  Global Program Instance uPred_cofe : Cofe uPredC := {| compl := uPred_compl |}.
  Next Obligation.
    intros n c; split=>i x ??; symmetry; apply (chain_cauchy c i n); auto.
  Qed.
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
End cofe.
Arguments uPredC : clear implicits.

Instance uPred_ne {M} (P : uPred M) n : Proper (dist n ==> iff) (P n).
Proof.
  intros x1 x2 Hx; split=> ?; eapply uPred_mono; eauto; by rewrite Hx.
Qed.
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} (P Q : uPred M) n1 n2 x :
  P {n2} Q  n2  n1  {n2} x  Q n1 x  P n2 x.
Proof.
  intros [Hne] ???. eapply Hne; try done.
  eapply uPred_closed; eauto using cmra_validN_le.
Qed.

(** functor *)
Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
109
  `{!CmraMorphism f} (P : uPred M1) :
110
  uPred M2 := {| uPred_holds n x := P n (f x) |}.
111
112
Next Obligation. naive_solver eauto using uPred_mono, cmra_morphism_monotoneN. Qed.
Next Obligation. naive_solver eauto using uPred_closed, cmra_morphism_validN. Qed.
113
114

Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
115
  `{!CmraMorphism f} n : Proper (dist n ==> dist n) (uPred_map f).
116
117
Proof.
  intros x1 x2 Hx; split=> n' y ??.
118
  split; apply Hx; auto using cmra_morphism_validN.
119
120
121
122
Qed.
Lemma uPred_map_id {M : ucmraT} (P : uPred M): uPred_map cid P  P.
Proof. by split=> n x ?. Qed.
Lemma uPred_map_compose {M1 M2 M3 : ucmraT} (f : M1 -n> M2) (g : M2 -n> M3)
123
    `{!CmraMorphism f, !CmraMorphism g} (P : uPred M3):
124
125
126
  uPred_map (g  f) P  uPred_map f (uPred_map g P).
Proof. by split=> n x Hx. Qed.
Lemma uPred_map_ext {M1 M2 : ucmraT} (f g : M1 -n> M2)
127
      `{!CmraMorphism f} `{!CmraMorphism g}:
128
129
  ( x, f x  g x)   x, uPred_map f x  uPred_map g x.
Proof. intros Hf P; split=> n x Hx /=; by rewrite /uPred_holds /= Hf. Qed.
130
Definition uPredC_map {M1 M2 : ucmraT} (f : M2 -n> M1) `{!CmraMorphism f} :
131
132
  uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1  uPredC M2).
Lemma uPredC_map_ne {M1 M2 : ucmraT} (f g : M2 -n> M1)
133
    `{!CmraMorphism f, !CmraMorphism g} n :
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
  f {n} g  uPredC_map f {n} uPredC_map g.
Proof.
  by intros Hfg P; split=> n' y ??;
    rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia.
Qed.

Program Definition uPredCF (F : urFunctor) : cFunctor := {|
  cFunctor_car A B := uPredC (urFunctor_car F B A);
  cFunctor_map A1 A2 B1 B2 fg := uPredC_map (urFunctor_map F (fg.2, fg.1))
|}.
Next Obligation.
  intros F A1 A2 B1 B2 n P Q HPQ.
  apply uPredC_map_ne, urFunctor_ne; split; by apply HPQ.
Qed.
Next Obligation.
  intros F A B P; simpl. rewrite -{2}(uPred_map_id P).
  apply uPred_map_ext=>y. by rewrite urFunctor_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 urFunctor_compose.
Qed.

Instance uPredCF_contractive F :
  urFunctorContractive F  cFunctorContractive (uPredCF F).
Proof.
160
161
  intros ? A1 A2 B1 B2 n P Q HPQ. apply uPredC_map_ne, urFunctor_contractive.
  destruct n; split; by apply HPQ.
162
163
164
165
166
167
168
169
170
171
172
173
Qed.

(** logical entailement *)
Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
  { uPred_in_entails :  n x, {n} x  P n x  Q n x }.
Hint Extern 0 (uPred_entails _ _) => reflexivity.
Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).

Hint Resolve uPred_mono uPred_closed : uPred_def.

(** Notations *)
Notation "P ⊢ Q" := (uPred_entails P%I Q%I)
Robbert Krebbers's avatar
Robbert Krebbers committed
174
175
  (at level 99, Q at level 200, right associativity) : stdpp_scope.
Notation "(⊢)" := uPred_entails (only parsing) : stdpp_scope.
176
Notation "P ⊣⊢ Q" := (equiv (A:=uPred _) P%I Q%I)
Robbert Krebbers's avatar
Robbert Krebbers committed
177
178
  (at level 95, no associativity) : stdpp_scope.
Notation "(⊣⊢)" := (equiv (A:=uPred _)) (only parsing) : stdpp_scope.
179

180
Module uPred.
181
182
183
184
Section entails.
Context {M : ucmraT}.
Implicit Types P Q : uPred M.

Robbert Krebbers's avatar
Robbert Krebbers committed
185
Global Instance entails_po : PreOrder (@uPred_entails M).
186
187
188
189
190
Proof.
  split.
  - by intros P; split=> x i.
  - by intros P Q Q' HP HQ; split=> x i ??; apply HQ, HP.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
Global Instance entails_anti_sym : AntiSymm () (@uPred_entails M).
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed.

Lemma equiv_spec P Q : (P  Q)  (P  Q)  (Q  P).
Proof.
  split; [|by intros [??]; apply (anti_symm ())].
  intros HPQ; split; split=> x i; apply HPQ.
Qed.
Lemma equiv_entails P Q : (P  Q)  (P  Q).
Proof. apply equiv_spec. Qed.
Lemma equiv_entails_sym P Q : (Q  P)  (P  Q).
Proof. apply equiv_spec. Qed.
Global Instance entails_proper :
  Proper (() ==> () ==> iff) (() : relation (uPred M)).
Proof.
  move => P1 P2 /equiv_spec [HP1 HP2] Q1 Q2 /equiv_spec [HQ1 HQ2]; split; intros.
  - by trans P1; [|trans Q1].
  - by trans P2; [|trans Q2].
Qed.
Lemma entails_equiv_l (P Q R : uPred M) : (P  Q)  (Q  R)  (P  R).
Proof. by intros ->. Qed.
Lemma entails_equiv_r (P Q R : uPred M) : (P  Q)  (Q  R)  (P  R).
Proof. by intros ? <-. Qed.
214

Robbert Krebbers's avatar
Robbert Krebbers committed
215
216
Lemma entails_lim (cP cQ : chain (uPredC M)) :
  ( n, cP n  cQ n)  compl cP  compl cQ.
217
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
218
  intros Hlim; split=> n m ? HP.
219
220
221
  eapply uPred_holds_ne, Hlim, HP; eauto using conv_compl.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
222
223
224
Lemma limit_preserving_entails `{Cofe A} (Φ Ψ : A  uPred M) :
  NonExpansive Φ  NonExpansive Ψ  LimitPreserving (λ x, Φ x  Ψ x).
Proof. intros HΦ HΨ c Hc. rewrite -!compl_chain_map /=. by apply entails_lim. Qed.
225
End entails.
226
End uPred.