upred.v 9.03 KB
 Robbert Krebbers committed Oct 25, 2016 1 ``````From iris.algebra Require Export cmra. `````` Ralf Jung committed Jan 05, 2017 2 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Oct 25, 2016 3 `````` `````` Ralf Jung committed Jan 05, 2017 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. *) `````` Robbert Krebbers committed Oct 25, 2016 9 10 ``````Record uPred (M : ucmraT) : Type := IProp { uPred_holds :> nat → M → Prop; `````` Jacques-Henri Jourdan committed Apr 04, 2017 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. *) `````` Robbert Krebbers committed Oct 25, 2016 15 `````` uPred_mono n x1 x2 : uPred_holds n x1 → x1 ≼{n} x2 → uPred_holds n x2; `````` Jacques-Henri Jourdan committed Apr 04, 2017 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 committed Apr 05, 2017 21 `````` truth value on invalid elements. This, in turn, is required by `````` Jacques-Henri Jourdan committed Apr 04, 2017 22 23 24 `````` the fact that entailment has to ignore invalid elements, which is itself essential for proving [ownM_valid]. `````` Jacques-Henri Jourdan committed Apr 05, 2017 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). *) `````` Robbert Krebbers committed Oct 25, 2016 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'. `````` Ralf Jung committed Nov 22, 2016 64 `````` Definition uPred_ofe_mixin : OfeMixin (uPred M). `````` Robbert Krebbers committed Oct 25, 2016 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. `````` Ralf Jung committed Nov 22, 2016 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. `````` Robbert Krebbers committed Oct 25, 2016 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) `````` Robbert Krebbers committed Oct 25, 2017 109 `````` `{!CmraMorphism f} (P : uPred M1) : `````` Robbert Krebbers committed Oct 25, 2016 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. `````` Robbert Krebbers committed Oct 25, 2016 113 114 `````` Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1) `````` Robbert Krebbers committed Oct 25, 2017 115 `````` `{!CmraMorphism f} n : Proper (dist n ==> dist n) (uPred_map f). `````` Robbert Krebbers committed Oct 25, 2016 116 117 ``````Proof. intros x1 x2 Hx; split=> n' y ??. `````` 118 `````` split; apply Hx; auto using cmra_morphism_validN. `````` Robbert Krebbers committed Oct 25, 2016 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) `````` Robbert Krebbers committed Oct 25, 2017 123 `````` `{!CmraMorphism f, !CmraMorphism g} (P : uPred M3): `````` Robbert Krebbers committed Oct 25, 2016 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) `````` Robbert Krebbers committed Oct 25, 2017 127 `````` `{!CmraMorphism f} `{!CmraMorphism g}: `````` Robbert Krebbers committed Oct 25, 2016 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. `````` Robbert Krebbers committed Oct 25, 2017 130 ``````Definition uPredC_map {M1 M2 : ucmraT} (f : M2 -n> M1) `{!CmraMorphism f} : `````` Robbert Krebbers committed Oct 25, 2016 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) `````` Robbert Krebbers committed Oct 25, 2017 133 `````` `{!CmraMorphism f, !CmraMorphism g} n : `````` Robbert Krebbers committed Oct 25, 2016 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. `````` Robbert Krebbers committed Dec 05, 2016 160 161 `````` intros ? A1 A2 B1 B2 n P Q HPQ. apply uPredC_map_ne, urFunctor_contractive. destruct n; split; by apply HPQ. `````` Robbert Krebbers committed Oct 25, 2016 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 committed Nov 11, 2017 174 175 `````` (at level 99, Q at level 200, right associativity) : stdpp_scope. Notation "(⊢)" := uPred_entails (only parsing) : stdpp_scope. `````` Robbert Krebbers committed Oct 25, 2016 176 ``````Notation "P ⊣⊢ Q" := (equiv (A:=uPred _) P%I Q%I) `````` Robbert Krebbers committed Nov 11, 2017 177 178 `````` (at level 95, no associativity) : stdpp_scope. Notation "(⊣⊢)" := (equiv (A:=uPred _)) (only parsing) : stdpp_scope. `````` Robbert Krebbers committed Oct 25, 2016 179 `````` `````` Robbert Krebbers committed Dec 13, 2016 180 ``````Module uPred. `````` Robbert Krebbers committed Oct 25, 2016 181 182 183 184 ``````Section entails. Context {M : ucmraT}. Implicit Types P Q : uPred M. `````` Robbert Krebbers committed Mar 09, 2017 185 ``````Global Instance entails_po : PreOrder (@uPred_entails M). `````` Robbert Krebbers committed Oct 25, 2016 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 committed Mar 09, 2017 191 ``````Global Instance entails_anti_sym : AntiSymm (⊣⊢) (@uPred_entails M). `````` Robbert Krebbers committed Oct 25, 2016 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. `````` Ralf Jung committed Dec 21, 2016 214 `````` `````` Robbert Krebbers committed Mar 09, 2017 215 216 ``````Lemma entails_lim (cP cQ : chain (uPredC M)) : (∀ n, cP n ⊢ cQ n) → compl cP ⊢ compl cQ. `````` Ralf Jung committed Dec 21, 2016 217 ``````Proof. `````` Robbert Krebbers committed Mar 09, 2017 218 `````` intros Hlim; split=> n m ? HP. `````` Ralf Jung committed Dec 21, 2016 219 220 221 `````` eapply uPred_holds_ne, Hlim, HP; eauto using conv_compl. Qed. `````` Robbert Krebbers committed Mar 09, 2017 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. `````` Robbert Krebbers committed Oct 25, 2016 225 ``````End entails. `````` Robbert Krebbers committed Dec 13, 2016 226 ``End uPred.``