compatibility.v 9.91 KB
 Robbert Krebbers committed Jan 20, 2020 1 ``````From solutions Require Export sem_typed sem_operators. `````` Robbert Krebbers committed Jan 16, 2020 2 `````` `````` Robbert Krebbers committed Jan 20, 2020 3 ``````(** * Compatibility lemmas *) `````` Robbert Krebbers committed Jan 20, 2020 4 5 6 ``````(** We prove that the logical relations, i.e., the semantic typing judgment, that we have defined is compatible with typing rules. That is, the logical relations is a congruence with respect to the typing rules. `````` Amin Timany committed Jan 17, 2020 7 `````` `````` Robbert Krebbers committed Jan 20, 2020 8 9 10 ``````These compatibility lemmas are what one gets when the syntactic typing judgment is replaced semantic typing judgment in syntactic typing rules. For instance ([sem_typed_pair]): `````` Amin Timany committed Jan 17, 2020 11 12 `````` << `````` Robbert Krebbers committed Jan 20, 2020 13 14 15 `````` Γ ⊢ e1 : τ1 Γ ⊢ e2 : τ2 -------------------------------- Γ ⊢ (e1, e2) : τ1 × τ2 `````` Amin Timany committed Jan 17, 2020 16 ``````>> `````` Robbert Krebbers committed Jan 20, 2020 17 18 `````` becomes: `````` Amin Timany committed Jan 17, 2020 19 20 `````` << `````` Robbert Krebbers committed Jan 20, 2020 21 `````` (Γ ⊨ e1 : A1) -∗ (Γ ⊨ e2 : A2) -∗ Γ ⊢ (e1, e2) : A1 * A2 `````` Amin Timany committed Jan 17, 2020 22 ``````>> `````` Robbert Krebbers committed Jan 20, 2020 23 ``````*) `````` Amin Timany committed Jan 17, 2020 24 `````` `````` Robbert Krebbers committed Jan 16, 2020 25 ``````Section compatibility. `````` Robbert Krebbers committed Jan 19, 2020 26 `````` Context `{!heapG Σ}. `````` Robbert Krebbers committed Jan 16, 2020 27 28 29 `````` Implicit Types A B : sem_ty Σ. Implicit Types C : sem_ty Σ → sem_ty Σ. `````` Robbert Krebbers committed Jan 20, 2020 30 31 `````` (** * Compatibility rules for expression typing *) (** * Variables *) `````` Robbert Krebbers committed Jan 19, 2020 32 `````` Lemma Var_sem_typed Γ (x : string) A : Γ !! x = Some A → (Γ ⊨ x : A)%I. `````` Robbert Krebbers committed Jan 16, 2020 33 34 35 36 37 38 `````` Proof. iIntros (HΓx vs) "!# #HΓ /=". iDestruct (env_sem_typed_lookup with "HΓ") as (v ->) "HA"; first done. by iApply wp_value. Qed. `````` Robbert Krebbers committed Jan 18, 2020 39 `````` Lemma Val_sem_typed Γ v A : ⊨ᵥ v : A -∗ Γ ⊨ v : A. `````` Robbert Krebbers committed Jan 18, 2020 40 41 42 43 `````` Proof. iIntros "#Hv" (vs) "!# #HΓ /=". iApply wp_value. iApply "Hv". Qed. `````` Robbert Krebbers committed Jan 16, 2020 44 `````` `````` Robbert Krebbers committed Jan 20, 2020 45 `````` (** * Products and sums *) `````` Robbert Krebbers committed Jan 18, 2020 46 `````` Lemma Pair_sem_typed Γ e1 e2 A1 A2 : `````` Robbert Krebbers committed Jan 18, 2020 47 `````` Γ ⊨ e1 : A1 -∗ Γ ⊨ e2 : A2 -∗ Γ ⊨ (e1,e2) : A1 * A2. `````` Robbert Krebbers committed Jan 16, 2020 48 49 50 51 52 53 `````` Proof. iIntros "#H1 #H2" (vs) "!# #HΓ /=". wp_apply (wp_wand with "(H2 [//])"); iIntros (w2) "#HA2". wp_apply (wp_wand with "(H1 [//])"); iIntros (w1) "#HA1". wp_pures. iExists w1, w2. auto. Qed. `````` Robbert Krebbers committed Jan 18, 2020 54 `````` Lemma Fst_sem_typed Γ e A1 A2 : Γ ⊨ e : A1 * A2 -∗ Γ ⊨ Fst e : A1. `````` Robbert Krebbers committed Jan 16, 2020 55 56 57 58 59 `````` Proof. iIntros "#H" (vs) "!# #HΓ /=". wp_apply (wp_wand with "(H [//])"); iIntros (w). iDestruct 1 as (w1 w2 ->) "[??]". by wp_pures. Qed. `````` Robbert Krebbers committed Jan 20, 2020 60 `````` (* REMOVE *) Lemma Snd_sem_typed Γ e A1 A2 : Γ ⊨ e : A1 * A2 -∗ Γ ⊨ Snd e : A2. `````` Robbert Krebbers committed Jan 16, 2020 61 62 63 64 65 66 `````` Proof. iIntros "#H" (vs) "!# #HΓ /=". wp_apply (wp_wand with "(H [//])"); iIntros (w). iDestruct 1 as (w1 w2 ->) "[??]". by wp_pures. Qed. `````` Robbert Krebbers committed Jan 18, 2020 67 `````` Lemma InjL_sem_typed Γ e A1 A2 : Γ ⊨ e : A1 -∗ Γ ⊨ InjL e : A1 + A2. `````` Robbert Krebbers committed Jan 20, 2020 68 `````` (* REMOVE *) Proof. `````` Robbert Krebbers committed Jan 16, 2020 69 70 71 72 `````` iIntros "#H" (vs) "!# #HΓ /=". wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HA". wp_pures. iLeft. iExists w. auto. Qed. `````` Robbert Krebbers committed Jan 20, 2020 73 `````` (* REMOVE *) Lemma InjR_sem_typed Γ e A1 A2 : Γ ⊨ e : A2 -∗ Γ ⊨ InjR e : A1 + A2. `````` Robbert Krebbers committed Jan 16, 2020 74 75 76 77 78 `````` Proof. iIntros "#H" (vs) "!# #HΓ /=". wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HA". wp_pures. iRight. iExists w. auto. Qed. `````` Robbert Krebbers committed Jan 18, 2020 79 `````` Lemma Case_sem_typed Γ e e1 e2 A1 A2 B : `````` Robbert Krebbers committed Jan 18, 2020 80 `````` Γ ⊨ e : A1 + A2 -∗ Γ ⊨ e1 : (A1 → B) -∗ Γ ⊨ e2 : (A2 → B) -∗ `````` Robbert Krebbers committed Jan 16, 2020 81 `````` Γ ⊨ Case e e1 e2 : B. `````` Robbert Krebbers committed Jan 20, 2020 82 `````` (* REMOVE *) Proof. `````` Robbert Krebbers committed Jan 16, 2020 83 84 85 86 87 88 89 90 `````` iIntros "#H #H1 #H2" (vs) "!# #HΓ /=". wp_apply (wp_wand with "(H [//])"); iIntros (w) "#[HA|HA]". - iDestruct "HA" as (w1 ->) "HA". wp_pures. wp_apply (wp_wand with "(H1 [//])"); iIntros (v) "#HAB". by iApply "HAB". - iDestruct "HA" as (w2 ->) "HA". wp_pures. wp_apply (wp_wand with "(H2 [//])"); iIntros (v) "#HAB". by iApply "HAB". Qed. `````` Robbert Krebbers committed Jan 20, 2020 91 `````` (** * Functions *) `````` Robbert Krebbers committed Jan 18, 2020 92 `````` Lemma Rec_sem_typed Γ f x e A1 A2 : `````` Robbert Krebbers committed Jan 18, 2020 93 94 `````` binder_insert f (A1 → A2)%sem_ty (binder_insert x A1 Γ) ⊨ e : A2 -∗ Γ ⊨ (rec: f x := e) : (A1 → A2). `````` Robbert Krebbers committed Jan 16, 2020 95 96 97 `````` Proof. iIntros "#H" (vs) "!# #HΓ /=". wp_pures. iLöb as "IH". iIntros "!#" (v) "#HA1". wp_pures. set (r := RecV f x _). `````` Robbert Krebbers committed Jan 18, 2020 98 99 `````` rewrite -subst_map_binder_insert_2. iApply "H". iApply (env_sem_typed_insert with "IH"). by iApply env_sem_typed_insert. `````` Robbert Krebbers committed Jan 16, 2020 100 101 `````` Qed. `````` Robbert Krebbers committed Jan 18, 2020 102 `````` Lemma App_sem_typed Γ e1 e2 A1 A2 : `````` Robbert Krebbers committed Jan 18, 2020 103 `````` Γ ⊨ e1 : (A1 → A2) -∗ Γ ⊨ e2 : A1 -∗ Γ ⊨ e1 e2 : A2. `````` Robbert Krebbers committed Jan 16, 2020 104 105 106 107 108 109 `````` Proof. iIntros "#H1 #H2" (vs) "!# #HΓ /=". wp_apply (wp_wand with "(H2 [//])"); iIntros (w) "#HA1". wp_apply (wp_wand with "(H1 [//])"); iIntros (v) "#HA". by iApply "HA". Qed. `````` Robbert Krebbers committed Jan 20, 2020 110 `````` (** * Polymorphic functions and existentials *) `````` Robbert Krebbers committed Jan 18, 2020 111 `````` Lemma TLam_sem_typed Γ e C : (∀ A, Γ ⊨ e : C A) -∗ Γ ⊨ (Λ: e) : ∀ A, C A. `````` Robbert Krebbers committed Jan 16, 2020 112 113 114 115 `````` Proof. iIntros "#H" (vs) "!# #HΓ /=". wp_pures. iIntros "!#" (A) "/=". wp_pures. by iApply ("H" \$! A). Qed. `````` Robbert Krebbers committed Jan 18, 2020 116 `````` Lemma TApp_sem_typed Γ e C A : (Γ ⊨ e : ∀ A, C A) -∗ Γ ⊨ e <_> : C A. `````` Robbert Krebbers committed Jan 16, 2020 117 118 119 120 121 `````` Proof. iIntros "#H" (vs) "!# #HΓ /=". wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HB". by iApply ("HB" \$! A). Qed. `````` Robbert Krebbers committed Jan 18, 2020 122 `````` Lemma Pack_sem_typed Γ e C A : Γ ⊨ e : C A -∗ Γ ⊨ (pack: e) : ∃ A, C A. `````` Robbert Krebbers committed Jan 20, 2020 123 `````` (* REMOVE *) Proof. `````` Robbert Krebbers committed Jan 16, 2020 124 `````` iIntros "#H" (vs) "!# #HΓ /=". `````` Robbert Krebbers committed Jan 18, 2020 125 126 `````` wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HB". wp_lam. by iExists A. `````` Robbert Krebbers committed Jan 16, 2020 127 `````` Qed. `````` Robbert Krebbers committed Jan 18, 2020 128 `````` Lemma Unpack_sem_typed Γ x e1 e2 C B : `````` Robbert Krebbers committed Jan 16, 2020 129 130 `````` (Γ ⊨ e1 : ∃ A, C A) -∗ (∀ A, binder_insert x (C A) Γ ⊨ e2 : B) -∗ Γ ⊨ (unpack: x := e1 in e2) : B. `````` Robbert Krebbers committed Jan 20, 2020 131 `````` (* REMOVE *) Proof. `````` Robbert Krebbers committed Jan 16, 2020 132 133 134 135 136 137 138 139 `````` iIntros "#H1 #H2" (vs) "!# #HΓ /=". wp_apply (wp_wand with "(H1 [//])"); iIntros (v); iDestruct 1 as (A) "#HC". rewrite /exist_unpack; wp_pures. rewrite -subst_map_binder_insert. wp_apply (wp_wand with "(H2 [])"). { by iApply env_sem_typed_insert. } auto. Qed. `````` Robbert Krebbers committed Jan 20, 2020 140 `````` (** ** Heap operations *) `````` Robbert Krebbers committed Jan 18, 2020 141 `````` Lemma Alloc_sem_typed Γ e A : Γ ⊨ e : A -∗ Γ ⊨ ref e : ref A. `````` Robbert Krebbers committed Jan 16, 2020 142 143 144 145 146 147 148 149 `````` Proof. iIntros "#H" (vs) "!# #HΓ /=". wp_bind (subst_map _ e). iApply (wp_wand with "(H [//])"); iIntros (w) "HA". iApply wp_fupd. wp_alloc l as "Hl". iMod (inv_alloc (tyN .@ l) _ (∃ v, l ↦ v ∗ A v)%I with "[Hl HA]") as "#?". { iExists w. iFrame. } iModIntro. iExists l; auto. Qed. `````` Robbert Krebbers committed Jan 18, 2020 150 `````` Lemma Load_sem_typed Γ e A : Γ ⊨ e : ref A -∗ Γ ⊨ ! e : A. `````` Robbert Krebbers committed Jan 16, 2020 151 152 153 154 155 156 `````` Proof. iIntros "#H" (vs) "!# #HΓ /=". wp_bind (subst_map _ e). iApply (wp_wand with "(H [//])"); iIntros (w). iDestruct 1 as (l ->) "#?". iInv (tyN.@l) as (v) "[>Hl HA]". wp_load. eauto 10. Qed. `````` Robbert Krebbers committed Jan 18, 2020 157 `````` Lemma Store_sem_typed Γ e1 e2 A : `````` Robbert Krebbers committed Jan 18, 2020 158 `````` Γ ⊨ e1 : ref A -∗ Γ ⊨ e2 : A -∗ Γ ⊨ (e1 <- e2) : (). `````` Robbert Krebbers committed Jan 20, 2020 159 `````` (* REMOVE *) Proof. `````` Robbert Krebbers committed Jan 16, 2020 160 161 162 163 164 `````` iIntros "#H1 #H2" (vs) "!# #HΓ /=". wp_apply (wp_wand with "(H2 [//])"); iIntros (w2) "#HA". wp_apply (wp_wand with "(H1 [//])"); iIntros (w1); iDestruct 1 as (l ->) "#?". iInv (tyN.@l) as (v) "[>Hl _]". wp_store. eauto 10. Qed. `````` Robbert Krebbers committed Jan 18, 2020 165 `````` Lemma FAA_sem_typed Γ e1 e2 : `````` Robbert Krebbers committed Jan 18, 2020 166 `````` Γ ⊨ e1 : ref sem_ty_int -∗ Γ ⊨ e2 : sem_ty_int -∗ Γ ⊨ FAA e1 e2 : sem_ty_int. `````` Robbert Krebbers committed Jan 20, 2020 167 `````` (* REMOVE *) Proof. `````` Robbert Krebbers committed Jan 16, 2020 168 169 170 171 172 173 `````` iIntros "#H1 #H2" (vs) "!# #HΓ /=". wp_apply (wp_wand with "(H2 [//])"); iIntros (w2); iDestruct 1 as (n) "->". wp_apply (wp_wand with "(H1 [//])"); iIntros (w1); iDestruct 1 as (l ->) "#?". iInv (tyN.@l) as (v) "[>Hl Hv]"; iDestruct "Hv" as (n') "> ->". wp_faa. iModIntro. eauto 10. Qed. `````` Robbert Krebbers committed Jan 18, 2020 174 `````` Lemma CmpXchg_sem_typed Γ A e1 e2 e3 : `````` Robbert Krebbers committed Jan 16, 2020 175 `````` SemTyUnboxed A → `````` Robbert Krebbers committed Jan 18, 2020 176 177 `````` Γ ⊨ e1 : ref A -∗ Γ ⊨ e2 : A -∗ Γ ⊨ e3 : A -∗ Γ ⊨ CmpXchg e1 e2 e3 : A * sem_ty_bool. `````` Robbert Krebbers committed Jan 20, 2020 178 `````` (* REMOVE *) Proof. `````` Robbert Krebbers committed Jan 16, 2020 179 180 181 182 183 184 185 186 187 `````` intros. iIntros "#H1 #H2 #H3" (vs) "!# #HΓ /=". wp_apply (wp_wand with "(H3 [//])"); iIntros (w3) "HA3". wp_apply (wp_wand with "(H2 [//])"); iIntros (w2) "HA2". iDestruct (sem_ty_unboxed with "HA2") as %?. wp_apply (wp_wand with "(H1 [//])"); iIntros (w1); iDestruct 1 as (l ->) "#?". iInv (tyN.@l) as (v) "[>Hl #Hv]". wp_cmpxchg as ?|?; iModIntro; (iSplitL; [by eauto 12 with iFrame | iExists _, _; eauto]). Qed. `````` Robbert Krebbers committed Jan 20, 2020 188 `````` (** ** Operators *) `````` Robbert Krebbers committed Jan 18, 2020 189 `````` Lemma UnOp_sem_typed Γ e op A B : `````` Robbert Krebbers committed Jan 18, 2020 190 `````` SemTyUnOp op A B → Γ ⊨ e : A -∗ Γ ⊨ UnOp op e : B. `````` Robbert Krebbers committed Jan 16, 2020 191 192 193 194 195 `````` Proof. intros ?. iIntros "#H" (vs) "!# #HΓ /=". wp_apply (wp_wand with "(H [//])"); iIntros (v) "#HA". iDestruct (sem_ty_un_op with "HA") as (w ?) "#HB". by wp_unop. Qed. `````` Robbert Krebbers committed Jan 18, 2020 196 `````` Lemma BinOp_sem_typed Γ e1 e2 op A1 A2 B : `````` Robbert Krebbers committed Jan 18, 2020 197 `````` SemTyBinOp op A1 A2 B → Γ ⊨ e1 : A1 -∗ Γ ⊨ e2 : A2 -∗ Γ ⊨ BinOp op e1 e2 : B. `````` Robbert Krebbers committed Jan 20, 2020 198 `````` (* REMOVE *) Proof. `````` Robbert Krebbers committed Jan 16, 2020 199 200 201 202 203 204 `````` intros. iIntros "#H1 #H2" (vs) "!# #HΓ /=". wp_apply (wp_wand with "(H2 [//])"); iIntros (v2) "#HA2". wp_apply (wp_wand with "(H1 [//])"); iIntros (v1) "#HA1". iDestruct (sem_ty_bin_op with "HA1 HA2") as (w ?) "#HB". by wp_binop. Qed. `````` Robbert Krebbers committed Jan 18, 2020 205 `````` Lemma If_sem_typed Γ e e1 e2 B : `````` Robbert Krebbers committed Jan 18, 2020 206 `````` Γ ⊨ e : sem_ty_bool -∗ Γ ⊨ e1 : B -∗ Γ ⊨ e2 : B -∗ `````` Robbert Krebbers committed Jan 16, 2020 207 `````` Γ ⊨ (if: e then e1 else e2) : B. `````` Robbert Krebbers committed Jan 20, 2020 208 `````` (* REMOVE *) Proof. `````` Robbert Krebbers committed Jan 16, 2020 209 210 211 212 213 `````` iIntros "#H #H1 #H2" (vs) "!# #HΓ /=". iSpecialize ("H1" with "HΓ"). iSpecialize ("H2" with "HΓ"). wp_apply (wp_wand with "(H [//])"); iIntros (w). iDestruct 1 as ([]) "->"; by wp_if. Qed. `````` Robbert Krebbers committed Jan 20, 2020 214 `````` (** ** Fork *) `````` Robbert Krebbers committed Jan 18, 2020 215 `````` Lemma Fork_sem_typed Γ e : Γ ⊨ e : () -∗ Γ ⊨ Fork e : (). `````` Robbert Krebbers committed Jan 20, 2020 216 `````` (* REMOVE *) Proof. `````` Robbert Krebbers committed Jan 16, 2020 217 218 219 `````` iIntros "#H" (vs) "!# #HΓ /=". wp_apply wp_fork; last done. by iApply (wp_wand with "(H [//])"). Qed. `````` Robbert Krebbers committed Jan 18, 2020 220 `````` `````` Robbert Krebbers committed Jan 20, 2020 221 222 `````` (** * Compatibility rules for value typing *) (** ** Base types *) `````` Robbert Krebbers committed Jan 19, 2020 223 `````` Lemma UnitV_sem_typed : (⊨ᵥ #() : ())%I. `````` Robbert Krebbers committed Jan 18, 2020 224 `````` Proof. by iPureIntro. Qed. `````` Robbert Krebbers committed Jan 19, 2020 225 `````` Lemma BoolV_sem_typed (b : bool) : (⊨ᵥ #b : sem_ty_bool)%I. `````` Robbert Krebbers committed Jan 18, 2020 226 `````` Proof. by iExists b. Qed. `````` Robbert Krebbers committed Jan 19, 2020 227 `````` Lemma IntV_sem_typed (n : Z) : (⊨ᵥ #n : sem_ty_int)%I. `````` Robbert Krebbers committed Jan 20, 2020 228 `````` (* REMOVE *) Proof. by iExists n. Qed. `````` Robbert Krebbers committed Jan 18, 2020 229 `````` `````` Robbert Krebbers committed Jan 20, 2020 230 `````` (** ** Products and sums *) `````` Robbert Krebbers committed Jan 18, 2020 231 `````` Lemma PairV_sem_typed v1 v2 τ1 τ2 : `````` Robbert Krebbers committed Jan 18, 2020 232 `````` ⊨ᵥ v1 : τ1 -∗ ⊨ᵥ v2 : τ2 -∗ `````` Robbert Krebbers committed Jan 18, 2020 233 234 235 `````` ⊨ᵥ PairV v1 v2 : (τ1 * τ2). Proof. iIntros "#H1 #H2". iExists v1, v2. auto. Qed. Lemma InjLV_sem_typed v τ1 τ2 : `````` Robbert Krebbers committed Jan 18, 2020 236 `````` ⊨ᵥ v : τ1 -∗ `````` Robbert Krebbers committed Jan 18, 2020 237 238 239 `````` ⊨ᵥ InjLV v : (τ1 + τ2). Proof. iIntros "H". iLeft. auto. Qed. Lemma InjRV_sem_typed v τ1 τ2 : `````` Robbert Krebbers committed Jan 18, 2020 240 `````` ⊨ᵥ v : τ2 -∗ `````` Robbert Krebbers committed Jan 18, 2020 241 242 243 `````` ⊨ᵥ InjRV v : (τ1 + τ2). Proof. iIntros "H". iRight. auto. Qed. `````` Robbert Krebbers committed Jan 20, 2020 244 `````` (** ** Functions *) `````` Robbert Krebbers committed Jan 18, 2020 245 `````` Lemma RecV_sem_typed f x e A B : `````` Robbert Krebbers committed Jan 18, 2020 246 `````` binder_insert f (A → B)%sem_ty (binder_insert x A ∅) ⊨ e : B -∗ `````` Robbert Krebbers committed Jan 18, 2020 247 248 249 250 251 252 253 254 `````` ⊨ᵥ RecV f x e : (A → B). Proof. iIntros "#H". iLöb as "IH". iIntros "!#" (v) "#HA1". wp_pures. set (r := RecV f x _). rewrite -subst_map_binder_insert_2_empty. iApply "H". iApply (env_sem_typed_insert with "IH"). iApply (env_sem_typed_insert with "[\$]"). iApply env_sem_typed_empty. Qed. `````` Robbert Krebbers committed Jan 19, 2020 255 256 257 258 259 260 261 `````` Lemma TLamV_sem_typed e C : (∀ A, ∅ ⊨ e : C A) -∗ ⊨ᵥ (Λ: e) : ∀ A, C A. Proof. iIntros "#H !#" (A) "/=". wp_pures. rewrite -{2}(subst_map_empty e). iApply ("H" \$! A). by iApply env_sem_typed_empty. Qed. `````` Robbert Krebbers committed Jan 16, 2020 262 ``End compatibility.``