language.v 13.5 KB
 Ralf Jung committed Nov 22, 2016 1 ``````From iris.algebra Require Export ofe. `````` Ralf Jung committed Jan 05, 2017 2 ``````Set Default Proof Using "Type". `````` Ralf Jung committed Jan 04, 2016 3 `````` `````` Robbert Krebbers committed Nov 23, 2017 4 ``````Section language_mixin. `````` 5 `````` Context {expr val state observation : Type}. `````` Robbert Krebbers committed Nov 23, 2017 6 7 `````` Context (of_val : val → expr). Context (to_val : expr → option val). `````` Ralf Jung committed Oct 05, 2018 8 9 10 `````` (** We annotate the reduction relation with observations [κ], which we will use in the definition of weakest preconditions to predict future observations and assert correctness of the predictions. *) `````` Ralf Jung committed Oct 18, 2018 11 `````` Context (prim_step : expr → state → list observation → expr → state → list expr → Prop). `````` Robbert Krebbers committed Nov 23, 2017 12 13 14 15 `````` Record LanguageMixin := { mixin_to_of_val v : to_val (of_val v) = Some v; mixin_of_to_val e v : to_val e = Some v → of_val v = e; `````` 16 `````` mixin_val_stuck e σ κ e' σ' efs : prim_step e σ κ e' σ' efs → to_val e = None `````` Robbert Krebbers committed Nov 23, 2017 17 18 19 `````` }. End language_mixin. `````` Robbert Krebbers committed Feb 01, 2016 20 21 22 23 ``````Structure language := Language { expr : Type; val : Type; state : Type; `````` 24 `````` observation : Type; `````` Robbert Krebbers committed Feb 01, 2016 25 26 `````` of_val : val → expr; to_val : expr → option val; `````` Ralf Jung committed Oct 18, 2018 27 `````` prim_step : expr → state → list observation → expr → state → list expr → Prop; `````` Robbert Krebbers committed Nov 23, 2017 28 `````` language_mixin : LanguageMixin of_val to_val prim_step `````` Ralf Jung committed Jan 04, 2016 29 ``````}. `````` Ralf Jung committed Aug 12, 2020 30 31 `````` Declare Scope expr_scope. `````` Janno committed Aug 25, 2016 32 33 ``````Delimit Scope expr_scope with E. Bind Scope expr_scope with expr. `````` Ralf Jung committed Aug 12, 2020 34 35 36 `````` Declare Scope val_scope. Delimit Scope val_scope with V. `````` Jacques-Henri Jourdan committed Jan 04, 2017 37 ``````Bind Scope val_scope with val. `````` Robbert Krebbers committed Nov 23, 2017 38 `````` `````` 39 ``````Arguments Language {_ _ _ _ _ _ _} _. `````` Robbert Krebbers committed Feb 01, 2016 40 41 ``````Arguments of_val {_} _. Arguments to_val {_} _. `````` 42 ``````Arguments prim_step {_} _ _ _ _ _ _. `````` Robbert Krebbers committed Feb 01, 2016 43 `````` `````` Robbert Krebbers committed Jun 16, 2019 44 45 46 ``````Canonical Structure stateO Λ := leibnizO (state Λ). Canonical Structure valO Λ := leibnizO (val Λ). Canonical Structure exprO Λ := leibnizO (expr Λ). `````` Robbert Krebbers committed Feb 01, 2016 47 48 `````` Definition cfg (Λ : language) := (list (expr Λ) * state Λ)%type. `````` Ralf Jung committed Jan 04, 2016 49 `````` `````` Robbert Krebbers committed Nov 23, 2017 50 ``````Class LanguageCtx {Λ : language} (K : expr Λ → expr Λ) := { `````` Robbert Krebbers committed Mar 15, 2017 51 52 `````` fill_not_val e : to_val e = None → to_val (K e) = None; `````` 53 54 55 56 57 58 `````` fill_step e1 σ1 κ e2 σ2 efs : prim_step e1 σ1 κ e2 σ2 efs → prim_step (K e1) σ1 κ (K e2) σ2 efs; fill_step_inv e1' σ1 κ e2 σ2 efs : to_val e1' = None → prim_step (K e1') σ1 κ e2 σ2 efs → ∃ e2', e2 = K e2' ∧ prim_step e1' σ1 κ e2' σ2 efs `````` Robbert Krebbers committed Mar 15, 2017 59 60 ``````}. `````` Ralf Jung committed Mar 06, 2019 61 ``````Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)). `````` Robbert Krebbers committed Sep 21, 2017 62 63 ``````Proof. constructor; naive_solver. Qed. `````` Ralf Jung committed Dec 07, 2017 64 ``````Inductive atomicity := StronglyAtomic | WeaklyAtomic. `````` David Swasey committed Nov 09, 2017 65 `````` `````` Robbert Krebbers committed Jan 16, 2016 66 ``````Section language. `````` Robbert Krebbers committed Feb 01, 2016 67 68 `````` Context {Λ : language}. Implicit Types v : val Λ. `````` Robbert Krebbers committed Nov 23, 2017 69 70 71 72 73 74 `````` Implicit Types e : expr Λ. Lemma to_of_val v : to_val (of_val v) = Some v. Proof. apply language_mixin. Qed. Lemma of_to_val e v : to_val e = Some v → of_val v = e. Proof. apply language_mixin. Qed. `````` 75 `````` Lemma val_stuck e σ κ e' σ' efs : prim_step e σ κ e' σ' efs → to_val e = None. `````` Robbert Krebbers committed Nov 23, 2017 76 `````` Proof. apply language_mixin. Qed. `````` Ralf Jung committed Jan 04, 2016 77 `````` `````` Robbert Krebbers committed Feb 01, 2016 78 `````` Definition reducible (e : expr Λ) (σ : state Λ) := `````` 79 `````` ∃ κ e' σ' efs, prim_step e σ κ e' σ' efs. `````` Ralf Jung committed Oct 05, 2018 80 81 `````` (* Total WP only permits reductions without observations *) Definition reducible_no_obs (e : expr Λ) (σ : state Λ) := `````` Ralf Jung committed Oct 18, 2018 82 `````` ∃ e' σ' efs, prim_step e σ [] e' σ' efs. `````` 83 `````` Definition irreducible (e : expr Λ) (σ : state Λ) := `````` 84 `````` ∀ κ e' σ' efs, ¬prim_step e σ κ e' σ' efs. `````` David Swasey committed Nov 26, 2017 85 86 `````` Definition stuck (e : expr Λ) (σ : state Λ) := to_val e = None ∧ irreducible e σ. `````` Amin Timany committed Nov 06, 2019 87 88 `````` Definition not_stuck (e : expr Λ) (σ : state Λ) := is_Some (to_val e) ∨ reducible e σ. `````` Robbert Krebbers committed Mar 15, 2017 89 `````` `````` Ralf Jung committed Dec 07, 2017 90 `````` (* [Atomic WeaklyAtomic]: This (weak) form of atomicity is enough to open `````` Ralf Jung committed Dec 05, 2017 91 92 93 94 `````` invariants when WP ensures safety, i.e., programs never can get stuck. We have an example in lambdaRust of an expression that is atomic in this sense, but not in the stronger sense defined below, and we have to be able to open invariants around that expression. See `CasStuckS` in `````` David Swasey committed Nov 09, 2017 95 `````` [lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v). `````` Robbert Krebbers committed Mar 15, 2017 96 `````` `````` Ralf Jung committed Dec 07, 2017 97 `````` [Atomic StronglyAtomic]: To open invariants with a WP that does not ensure `````` Ralf Jung committed Dec 05, 2017 98 99 100 101 `````` safety, we need a stronger form of atomicity. With the above definition, in case `e` reduces to a stuck non-value, there is no proof that the invariants have been established again. *) Class Atomic (a : atomicity) (e : expr Λ) : Prop := `````` 102 103 `````` atomic σ e' κ σ' efs : prim_step e σ κ e' σ' efs → `````` Ralf Jung committed Dec 07, 2017 104 `````` if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e'). `````` Ralf Jung committed Oct 29, 2017 105 `````` `````` Ralf Jung committed Oct 18, 2018 106 `````` Inductive step (ρ1 : cfg Λ) (κ : list (observation Λ)) (ρ2 : cfg Λ) : Prop := `````` Robbert Krebbers committed Aug 08, 2016 107 `````` | step_atomic e1 σ1 e2 σ2 efs t1 t2 : `````` Robbert Krebbers committed Feb 01, 2016 108 `````` ρ1 = (t1 ++ e1 :: t2, σ1) → `````` Robbert Krebbers committed Aug 08, 2016 109 `````` ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2) → `````` 110 111 `````` prim_step e1 σ1 κ e2 σ2 efs → step ρ1 κ ρ2. `````` Tej Chajed committed Nov 29, 2018 112 `````` Hint Constructors step : core. `````` 113 `````` `````` Marianna Rapoport committed Oct 05, 2018 114 `````` Inductive nsteps : nat → cfg Λ → list (observation Λ) → cfg Λ → Prop := `````` Ralf Jung committed Oct 18, 2018 115 116 117 118 119 `````` | nsteps_refl ρ : nsteps 0 ρ [] ρ | nsteps_l n ρ1 ρ2 ρ3 κ κs : step ρ1 κ ρ2 → nsteps n ρ2 κs ρ3 → `````` Ralf Jung committed Oct 18, 2018 120 `````` nsteps (S n) ρ1 (κ ++ κs) ρ3. `````` Tej Chajed committed Nov 29, 2018 121 `````` Hint Constructors nsteps : core. `````` 122 `````` `````` Ralf Jung committed Oct 05, 2018 123 `````` Definition erased_step (ρ1 ρ2 : cfg Λ) := ∃ κ, step ρ1 κ ρ2. `````` 124 `````` `````` Ralf Jung committed Jun 07, 2019 125 126 `````` (** [rtc erased_step] and [nsteps] encode the same thing, just packaged in a different way. *) `````` 127 `````` Lemma erased_steps_nsteps ρ1 ρ2 : `````` Robbert Krebbers committed Jun 07, 2019 128 `````` rtc erased_step ρ1 ρ2 ↔ ∃ n κs, nsteps n ρ1 κs ρ2. `````` 129 `````` Proof. `````` Ralf Jung committed Jun 07, 2019 130 `````` split. `````` Robbert Krebbers committed Jun 07, 2019 131 132 133 `````` - induction 1; firstorder eauto. (* FIXME: [naive_solver eauto] should be able to handle this *) - intros (n & κs & Hsteps). unfold erased_step. induction Hsteps; eauto using rtc_refl, rtc_l. `````` 134 `````` Qed. `````` Robbert Krebbers committed Feb 01, 2016 135 `````` `````` Robbert Krebbers committed Apr 19, 2016 136 137 `````` Lemma of_to_val_flip v e : of_val v = e → to_val e = Some v. Proof. intros <-. by rewrite to_of_val. Qed. `````` Robbert Krebbers committed Mar 15, 2017 138 139 140 `````` Lemma not_reducible e σ : ¬reducible e σ ↔ irreducible e σ. Proof. unfold reducible, irreducible. naive_solver. Qed. `````` Robbert Krebbers committed Jan 19, 2016 141 `````` Lemma reducible_not_val e σ : reducible e σ → to_val e = None. `````` 142 `````` Proof. intros (?&?&?&?&?); eauto using val_stuck. Qed. `````` Ralf Jung committed Oct 05, 2018 143 144 `````` Lemma reducible_no_obs_reducible e σ : reducible_no_obs e σ → reducible e σ. Proof. intros (?&?&?&?); eexists; eauto. Qed. `````` David Swasey committed Nov 08, 2017 145 `````` Lemma val_irreducible e σ : is_Some (to_val e) → irreducible e σ. `````` 146 `````` Proof. intros [??] ???? ?%val_stuck. by destruct (to_val e). Qed. `````` Robbert Krebbers committed Aug 08, 2016 147 `````` Global Instance of_val_inj : Inj (=) (=) (@of_val Λ). `````` Robbert Krebbers committed Feb 11, 2016 148 `````` Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed. `````` Amin Timany committed Nov 06, 2019 149 150 151 152 153 `````` Lemma not_not_stuck e σ : ¬not_stuck e σ ↔ stuck e σ. Proof. rewrite /stuck /not_stuck -not_eq_None_Some -not_reducible. destruct (decide (to_val e = None)); naive_solver. Qed. `````` Ralf Jung committed Jan 05, 2016 154 `````` `````` Ralf Jung committed Dec 07, 2017 155 156 157 `````` Lemma strongly_atomic_atomic e a : Atomic StronglyAtomic e → Atomic a e. Proof. unfold Atomic. destruct a; eauto using val_irreducible. Qed. `````` Ralf Jung committed Oct 29, 2017 158 `````` `````` Ralf Jung committed Mar 06, 2019 159 `````` Lemma reducible_fill `{!@LanguageCtx Λ K} e σ : `````` Robbert Krebbers committed Mar 10, 2020 160 161 162 `````` reducible e σ → reducible (K e) σ. Proof. unfold reducible in *. naive_solver eauto using fill_step. Qed. Lemma reducible_fill_inv `{!@LanguageCtx Λ K} e σ : `````` Robbert Krebbers committed Mar 15, 2017 163 164 `````` to_val e = None → reducible (K e) σ → reducible e σ. Proof. `````` 165 `````` intros ? (e'&σ'&k&efs&Hstep); unfold reducible. `````` Robbert Krebbers committed Mar 15, 2017 166 167 `````` apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto. Qed. `````` Ralf Jung committed Mar 06, 2019 168 `````` Lemma reducible_no_obs_fill `{!@LanguageCtx Λ K} e σ : `````` Robbert Krebbers committed Mar 10, 2020 169 170 171 `````` reducible_no_obs e σ → reducible_no_obs (K e) σ. Proof. unfold reducible_no_obs in *. naive_solver eauto using fill_step. Qed. Lemma reducible_no_obs_fill_inv `{!@LanguageCtx Λ K} e σ : `````` Ralf Jung committed Oct 05, 2018 172 173 174 175 176 `````` to_val e = None → reducible_no_obs (K e) σ → reducible_no_obs e σ. Proof. intros ? (e'&σ'&efs&Hstep); unfold reducible_no_obs. apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto. Qed. `````` Ralf Jung committed Mar 06, 2019 177 `````` Lemma irreducible_fill `{!@LanguageCtx Λ K} e σ : `````` Robbert Krebbers committed Mar 15, 2017 178 `````` to_val e = None → irreducible e σ → irreducible (K e) σ. `````` Robbert Krebbers committed Mar 10, 2020 179 180 181 `````` Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill_inv. Qed. Lemma irreducible_fill_inv `{!@LanguageCtx Λ K} e σ : irreducible (K e) σ → irreducible e σ. `````` Robbert Krebbers committed Mar 15, 2017 182 `````` Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed. `````` Robbert Krebbers committed Sep 24, 2017 183 `````` `````` Robbert Krebbers committed Mar 10, 2020 184 `````` Lemma not_stuck_fill_inv K `{!@LanguageCtx Λ K} e σ : `````` 185 186 187 188 `````` not_stuck (K e) σ → not_stuck e σ. Proof. rewrite /not_stuck -!not_eq_None_Some. intros [?|?]. - auto using fill_not_val. `````` Robbert Krebbers committed Jun 19, 2020 189 `````` - destruct (decide (to_val e = None)); eauto using reducible_fill_inv. `````` 190 191 `````` Qed. `````` Hai Dang committed Jun 20, 2019 192 193 `````` Lemma stuck_fill `{!@LanguageCtx Λ K} e σ : stuck e σ → stuck (K e) σ. `````` Robbert Krebbers committed Mar 10, 2020 194 `````` Proof. rewrite -!not_not_stuck. eauto using not_stuck_fill_inv. Qed. `````` Hai Dang committed Jun 20, 2019 195 `````` `````` 196 197 `````` Lemma step_Permutation (t1 t1' t2 : list (expr Λ)) κ σ1 σ2 : t1 ≡ₚ t1' → step (t1,σ1) κ (t2,σ2) → ∃ t2', t2 ≡ₚ t2' ∧ step (t1',σ1) κ (t2',σ2). `````` Robbert Krebbers committed Sep 24, 2017 198 199 200 201 202 203 204 `````` Proof. intros Ht [e1 σ1' e2 σ2' efs tl tr ?? Hstep]; simplify_eq/=. move: Ht; rewrite -Permutation_middle (symmetry_iff (≡ₚ)). intros (tl'&tr'&->&Ht)%Permutation_cons_inv. exists (tl' ++ e2 :: tr' ++ efs); split; [|by econstructor]. by rewrite -!Permutation_middle !assoc_L Ht. Qed. `````` Dan Frumin committed Sep 25, 2017 205 `````` `````` Amin Timany committed Nov 06, 2019 206 207 208 209 210 211 212 213 214 215 216 217 `````` Lemma step_insert i t2 σ2 e κ e' σ3 efs : t2 !! i = Some e → prim_step e σ2 κ e' σ3 efs → step (t2, σ2) κ (<[i:=e']>t2 ++ efs, σ3). Proof. intros. edestruct (elem_of_list_split_length t2) as (t21&t22&?&?); first (by eauto using elem_of_list_lookup_2); simplify_eq. econstructor; eauto. by rewrite insert_app_r_alt // Nat.sub_diag /= -assoc_L. Qed. `````` 218 219 220 `````` Lemma erased_step_Permutation (t1 t1' t2 : list (expr Λ)) σ1 σ2 : t1 ≡ₚ t1' → erased_step (t1,σ1) (t2,σ2) → ∃ t2', t2 ≡ₚ t2' ∧ erased_step (t1',σ1) (t2',σ2). Proof. `````` Ralf Jung committed Oct 18, 2018 221 `````` intros Heq [? Hs]. pose proof (step_Permutation _ _ _ _ _ _ Heq Hs). firstorder. `````` Ralf Jung committed Oct 18, 2018 222 `````` (* FIXME: [naive_solver] should be able to handle this *) `````` 223 224 `````` Qed. `````` Robbert Krebbers committed Oct 05, 2018 225 `````` Record pure_step (e1 e2 : expr Λ) := { `````` Ralf Jung committed Oct 18, 2018 226 227 `````` pure_step_safe σ1 : reducible_no_obs e1 σ1; pure_step_det σ1 κ e2' σ2 efs : `````` 228 `````` prim_step e1 σ1 κ e2' σ2 efs → κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs = [] `````` Dan Frumin committed Sep 25, 2017 229 230 `````` }. `````` Amin Timany committed Nov 06, 2019 231 232 `````` Notation pure_steps_tp := (Forall2 (rtc pure_step)). `````` Robbert Krebbers committed Oct 05, 2018 233 234 235 `````` (* TODO: Exclude the case of [n=0], either here, or in [wp_pure] to avoid it succeeding when it did not actually do anything. *) Class PureExec (φ : Prop) (n : nat) (e1 e2 : expr Λ) := `````` Ralf Jung committed Oct 18, 2018 236 `````` pure_exec : φ → relations.nsteps pure_step n e1 e2. `````` Dan Frumin committed Sep 25, 2017 237 `````` `````` Ralf Jung committed Mar 06, 2019 238 `````` Lemma pure_step_ctx K `{!@LanguageCtx Λ K} e1 e2 : `````` Robbert Krebbers committed Oct 05, 2018 239 240 `````` pure_step e1 e2 → pure_step (K e1) (K e2). `````` Ralf Jung committed Nov 24, 2017 241 242 `````` Proof. intros [Hred Hstep]. split. `````` Ralf Jung committed Oct 05, 2018 243 `````` - unfold reducible_no_obs in *. naive_solver eauto using fill_step. `````` Ralf Jung committed Oct 18, 2018 244 `````` - intros σ1 κ e2' σ2 efs Hpstep. `````` 245 `````` destruct (fill_step_inv e1 σ1 κ e2' σ2 efs) as (e2'' & -> & ?); [|exact Hpstep|]. `````` Ralf Jung committed Oct 05, 2018 246 `````` + destruct (Hred σ1) as (? & ? & ? & ?); eauto using val_stuck. `````` 247 `````` + edestruct (Hstep σ1 κ e2'' σ2 efs) as (? & -> & -> & ->); auto. `````` Ralf Jung committed Nov 24, 2017 248 249 `````` Qed. `````` Ralf Jung committed Mar 06, 2019 250 `````` Lemma pure_step_nsteps_ctx K `{!@LanguageCtx Λ K} n e1 e2 : `````` Ralf Jung committed Oct 18, 2018 251 252 `````` relations.nsteps pure_step n e1 e2 → relations.nsteps pure_step n (K e1) (K e2). `````` Amin Timany committed Nov 06, 2019 253 254 255 256 257 258 `````` Proof. eauto using nsteps_congruence, pure_step_ctx. Qed. Lemma rtc_pure_step_ctx K `{!@LanguageCtx Λ K} e1 e2 : rtc pure_step e1 e2 → rtc pure_step (K e1) (K e2). Proof. eauto using rtc_congruence, pure_step_ctx. Qed. `````` Robbert Krebbers committed Oct 05, 2018 259 `````` (* We do not make this an instance because it is awfully general. *) `````` Ralf Jung committed Mar 06, 2019 260 `````` Lemma pure_exec_ctx K `{!@LanguageCtx Λ K} φ n e1 e2 : `````` Robbert Krebbers committed Oct 05, 2018 261 262 263 264 `````` PureExec φ n e1 e2 → PureExec φ n (K e1) (K e2). Proof. rewrite /PureExec; eauto using pure_step_nsteps_ctx. Qed. `````` Dan Frumin committed Sep 25, 2017 265 266 `````` (* This is a family of frequent assumptions for PureExec *) Class IntoVal (e : expr Λ) (v : val Λ) := `````` Ralf Jung committed Jun 18, 2018 267 `````` into_val : of_val v = e. `````` Robbert Krebbers committed Nov 02, 2017 268 `````` `````` Ralf Jung committed Jun 18, 2018 269 `````` Class AsVal (e : expr Λ) := as_val : ∃ v, of_val v = e. `````` Robbert Krebbers committed Nov 02, 2017 270 271 272 273 274 `````` (* There is no instance [IntoVal → AsVal] as often one can solve [AsVal] more efficiently since no witness has to be computed. *) Global Instance as_vals_of_val vs : TCForall AsVal (of_val <\$> vs). Proof. apply TCForall_Forall, Forall_fmap, Forall_true=> v. `````` Ralf Jung committed Jun 18, 2018 275 `````` rewrite /AsVal /=; eauto. `````` Robbert Krebbers committed Nov 02, 2017 276 `````` Qed. `````` Amin Timany committed Nov 06, 2019 277 `````` `````` Ralf Jung committed Jun 21, 2018 278 279 280 `````` Lemma as_val_is_Some e : (∃ v, of_val v = e) → is_Some (to_val e). Proof. intros [v <-]. rewrite to_of_val. eauto. Qed. `````` Amin Timany committed Nov 06, 2019 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 `````` Lemma prim_step_not_stuck e σ κ e' σ' efs : prim_step e σ κ e' σ' efs → not_stuck e σ. Proof. rewrite /not_stuck /reducible. eauto 10. Qed. Lemma rtc_pure_step_val `{!Inhabited (state Λ)} v e : rtc pure_step (of_val v) e → to_val e = Some v. Proof. intros ?; rewrite <- to_of_val. f_equal; symmetry; eapply rtc_nf; first done. intros [e' [Hstep _]]. destruct (Hstep inhabitant) as (?&?&?&Hval%val_stuck). by rewrite to_of_val in Hval. Qed. (** Let thread pools [t1] and [t3] be such that each thread in [t1] makes (zero or more) pure steps to the corresponding thread in [t3]. Furthermore, let [t2] be a thread pool such that [t1] under state [σ1] makes a (single) step to thread pool [t2] and state [σ2]. In this situation, either the step from [t1] to [t2] corresponds to one of the pure steps between [t1] and [t3], or, there is an [i] such that [i]th thread does not participate in the pure steps between [t1] and [t3] and [t2] corresponds to taking a step in the [i]th thread starting from [t1]. *) Lemma erased_step_pure_step_tp t1 σ1 t2 σ2 t3 : erased_step (t1, σ1) (t2, σ2) → pure_steps_tp t1 t3 → (σ1 = σ2 ∧ pure_steps_tp t2 t3) ∨ (∃ i e efs e' κ, t1 !! i = Some e ∧ t3 !! i = Some e ∧ t2 = <[i:=e']>t1 ++ efs ∧ prim_step e σ1 κ e' σ2 efs). Proof. intros [κ [e σ e' σ' ? t11 t12 ?? Hstep]] Hps; simplify_eq/=. apply Forall2_app_inv_l in Hps as (t31&?&Hpsteps&(e''&t32&Hps&?&->)%Forall2_cons_inv_l&->). destruct Hps as [e|e1 e2 e3 [_ Hprs]]. - right. exists (length t11), e, efs, e', κ; split_and!; last done. + by rewrite lookup_app_r // Nat.sub_diag. + apply Forall2_length in Hpsteps. by rewrite lookup_app_r Hpsteps // Nat.sub_diag. + by rewrite insert_app_r_alt // Nat.sub_diag /= -assoc_L. - edestruct Hprs as (?&?&?&?); first done; simplify_eq. left; split; first done. rewrite right_id_L. eauto using Forall2_app. Qed. `````` Robbert Krebbers committed Mar 15, 2017 329 ``````End language. `````` Amin Timany committed Nov 06, 2019 330 331 `````` Notation pure_steps_tp := (Forall2 (rtc pure_step)).``````