heap_lang.v 12.9 KB
Newer Older
 Ralf Jung committed Jan 04, 2016 1 ``````Require Import mathcomp.ssreflect.ssreflect. `````` Ralf Jung committed Jan 04, 2016 2 ``````Require Import Autosubst.Autosubst. `````` Ralf Jung committed Jan 06, 2016 3 ``````Require Import prelude.option prelude.gmap iris.language. `````` Ralf Jung committed Jan 04, 2016 4 `````` `````` Ralf Jung committed Jan 04, 2016 5 6 ``````Set Bullet Behavior "Strict Subproofs". `````` Ralf Jung committed Jan 05, 2016 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 ``````(** Some tactics useful when dealing with equality of sigma-like types: existT T0 t0 = existT T1 t1. They all assume such an equality is the first thing on the "stack" (goal). *) Ltac case_depeq1 := let Heq := fresh "Heq" in case=>_ /EqdepFacts.eq_sigT_sig_eq=>Heq; destruct Heq as (->,<-). Ltac case_depeq2 := let Heq := fresh "Heq" in case=>_ _ /EqdepFacts.eq_sigT_sig_eq=>Heq; destruct Heq as (->,Heq); case:Heq=>_ /EqdepFacts.eq_sigT_sig_eq=>Heq; destruct Heq as (->,<-). Ltac case_depeq3 := let Heq := fresh "Heq" in case=>_ _ _ /EqdepFacts.eq_sigT_sig_eq=>Heq; destruct Heq as (->,Heq); case:Heq=>_ _ /EqdepFacts.eq_sigT_sig_eq=>Heq; destruct Heq as (->,Heq); case:Heq=>_ /EqdepFacts.eq_sigT_sig_eq=>Heq; destruct Heq as (->,<-). (** Expressions and values. *) `````` Ralf Jung committed Jan 06, 2016 26 27 ``````Definition loc := nat. (* Any countable type. *) `````` Ralf Jung committed Jan 04, 2016 28 ``````Inductive expr := `````` Ralf Jung committed Jan 06, 2016 29 ``````(* Base lambda calculus *) `````` Ralf Jung committed Jan 04, 2016 30 ``````| Var (x : var) `````` Ralf Jung committed Jan 06, 2016 31 ``````| Rec (e : {bind 2 of expr}) (* These are recursive lambdas. *) `````` Ralf Jung committed Jan 05, 2016 32 ``````| App (e1 e2 : expr) `````` Ralf Jung committed Jan 06, 2016 33 ``````(* Embedding of Coq values and operations *) `````` Ralf Jung committed Jan 05, 2016 34 35 36 ``````| Lit {T : Type} (t: T) (* arbitrary Coq values become literals *) | Op1 {T1 To : Type} (f : T1 -> To) (e1 : expr) | Op2 {T1 T2 To : Type} (f : T1 -> T2 -> To) (e1 : expr) (e2 : expr) `````` Ralf Jung committed Jan 06, 2016 37 ``````(* Products *) `````` Ralf Jung committed Jan 04, 2016 38 39 40 ``````| Pair (e1 e2 : expr) | Fst (e : expr) | Snd (e : expr) `````` Ralf Jung committed Jan 06, 2016 41 ``````(* Sums *) `````` Ralf Jung committed Jan 04, 2016 42 43 ``````| InjL (e : expr) | InjR (e : expr) `````` Ralf Jung committed Jan 05, 2016 44 ``````| Case (e0 : expr) (e1 : {bind expr}) (e2 : {bind expr}) `````` Ralf Jung committed Jan 06, 2016 45 46 47 48 49 50 ``````(* Concurrency *) | Fork (e : expr) (* Heap *) | Loc (l : loc) | Ref (e : expr) | Load ( e : expr). `````` Ralf Jung committed Jan 04, 2016 51 52 53 54 55 56 `````` Instance Ids_expr : Ids expr. derive. Defined. Instance Rename_expr : Rename expr. derive. Defined. Instance Subst_expr : Subst expr. derive. Defined. Instance SubstLemmas_expr : SubstLemmas expr. derive. Qed. `````` Ralf Jung committed Jan 06, 2016 57 58 59 ``````Definition Lam (e: expr) := Rec (e.[up ids]). Definition LitUnit := Lit tt. `````` Ralf Jung committed Jan 04, 2016 60 ``````Inductive value := `````` Ralf Jung committed Jan 06, 2016 61 ``````| RecV (e : {bind 2 of expr}) `````` Ralf Jung committed Jan 05, 2016 62 ``````| LitV (T : Type) (t : T) (* arbitrary Coq values become literal values *) `````` Ralf Jung committed Jan 04, 2016 63 64 ``````| PairV (v1 v2 : value) | InjLV (v : value) `````` Ralf Jung committed Jan 06, 2016 65 66 ``````| InjRV (v : value) | LocV (l : loc). `````` Ralf Jung committed Jan 04, 2016 67 `````` `````` 68 ``````Fixpoint v2e (v : value) : expr := `````` Ralf Jung committed Jan 04, 2016 69 `````` match v with `````` Ralf Jung committed Jan 05, 2016 70 `````` | LitV _ t => Lit t `````` Ralf Jung committed Jan 06, 2016 71 `````` | RecV e => Rec e `````` Ralf Jung committed Jan 04, 2016 72 73 74 `````` | PairV v1 v2 => Pair (v2e v1) (v2e v2) | InjLV v => InjL (v2e v) | InjRV v => InjR (v2e v) `````` Ralf Jung committed Jan 06, 2016 75 `````` | LocV l => Loc l `````` Ralf Jung committed Jan 04, 2016 76 77 `````` end. `````` 78 79 ``````Fixpoint e2v (e : expr) : option value := match e with `````` Ralf Jung committed Jan 06, 2016 80 `````` | Rec e => Some (RecV e) `````` Ralf Jung committed Jan 05, 2016 81 `````` | Lit T t => Some (LitV T t) `````` 82 83 84 85 86 `````` | Pair e1 e2 => v1 ← e2v e1; v2 ← e2v e2; Some (PairV v1 v2) | InjL e => InjLV <\$> e2v e | InjR e => InjRV <\$> e2v e `````` Ralf Jung committed Jan 06, 2016 87 `````` | Loc l => Some (LocV l) `````` Ralf Jung committed Jan 05, 2016 88 `````` | _ => None `````` 89 90 91 92 93 `````` end. Lemma v2v v: e2v (v2e v) = Some v. Proof. `````` Ralf Jung committed Jan 04, 2016 94 `````` induction v; simpl; rewrite ?IHv ?IHv1 /= ?IHv2; reflexivity. `````` 95 96 ``````Qed. `````` Ralf Jung committed Jan 05, 2016 97 ``````Section e2e. (* To get local tactics. *) `````` 98 ``````Lemma e2e e v: `````` 99 `````` e2v e = Some v -> v2e v = e. `````` 100 ``````Proof. `````` Ralf Jung committed Jan 05, 2016 101 102 103 104 105 106 107 108 109 110 111 112 113 114 `````` Ltac case0 := case =><-; simpl; eauto using f_equal, f_equal2. Ltac case1 e1 := destruct (e2v e1); simpl; [|discriminate]; case0. Ltac case2 e1 e2 := destruct (e2v e1); simpl; [|discriminate]; destruct (e2v e2); simpl; [|discriminate]; case0. revert v; induction e; intros v; simpl; try discriminate; by (case2 e1 e2 || case1 e || case0). Qed. End e2e. Lemma v2e_inj v1 v2: v2e v1 = v2e v2 -> v1 = v2. Proof. `````` Ralf Jung committed Jan 05, 2016 115 116 `````` revert v2; induction v1=>v2; destruct v2; simpl; try discriminate; first [case_depeq3 | case_depeq2 | case_depeq1 | case]; eauto using f_equal, f_equal2. `````` Ralf Jung committed Jan 04, 2016 117 ``````Qed. `````` 118 `````` `````` Ralf Jung committed Jan 06, 2016 119 120 ``````(** The state: heaps of values. *) Definition state := gmap loc value. `````` Ralf Jung committed Jan 06, 2016 121 `````` `````` Ralf Jung committed Jan 05, 2016 122 ``````(** Evaluation contexts *) `````` Ralf Jung committed Jan 04, 2016 123 124 125 126 ``````Inductive ectx := | EmptyCtx | AppLCtx (K1 : ectx) (e2 : expr) | AppRCtx (v1 : value) (K2 : ectx) `````` Ralf Jung committed Jan 05, 2016 127 128 129 ``````| Op1Ctx {T1 To : Type} (f : T1 -> To) (K : ectx) | Op2LCtx {T1 T2 To : Type} (f : T1 -> T2 -> To) (K1 : ectx) (e2 : expr) | Op2RCtx {T1 T2 To : Type} (f : T1 -> T2 -> To) (v1 : value) (K2 : ectx) `````` Ralf Jung committed Jan 04, 2016 130 131 132 133 134 135 ``````| PairLCtx (K1 : ectx) (e2 : expr) | PairRCtx (v1 : value) (K2 : ectx) | FstCtx (K : ectx) | SndCtx (K : ectx) | InjLCtx (K : ectx) | InjRCtx (K : ectx) `````` Ralf Jung committed Jan 06, 2016 136 137 138 ``````| CaseCtx (K : ectx) (e1 : {bind expr}) (e2 : {bind expr}) | RefCtx (K : ectx) | LoadCtx (K : ectx). `````` Ralf Jung committed Jan 04, 2016 139 140 141 142 143 144 `````` Fixpoint fill (K : ectx) (e : expr) := match K with | EmptyCtx => e | AppLCtx K1 e2 => App (fill K1 e) e2 | AppRCtx v1 K2 => App (v2e v1) (fill K2 e) `````` Ralf Jung committed Jan 05, 2016 145 146 147 `````` | Op1Ctx _ _ f K => Op1 f (fill K e) | Op2LCtx _ _ _ f K1 e2 => Op2 f (fill K1 e) e2 | Op2RCtx _ _ _ f v1 K2 => Op2 f (v2e v1) (fill K2 e) `````` Ralf Jung committed Jan 04, 2016 148 149 150 151 152 153 154 `````` | PairLCtx K1 e2 => Pair (fill K1 e) e2 | PairRCtx v1 K2 => Pair (v2e v1) (fill K2 e) | FstCtx K => Fst (fill K e) | SndCtx K => Snd (fill K e) | InjLCtx K => InjL (fill K e) | InjRCtx K => InjR (fill K e) | CaseCtx K e1 e2 => Case (fill K e) e1 e2 `````` Ralf Jung committed Jan 06, 2016 155 156 `````` | RefCtx K => Ref (fill K e) | LoadCtx K => Load (fill K e) `````` Ralf Jung committed Jan 04, 2016 157 158 159 160 161 162 163 `````` end. Fixpoint comp_ctx (Ko : ectx) (Ki : ectx) := match Ko with | EmptyCtx => Ki | AppLCtx K1 e2 => AppLCtx (comp_ctx K1 Ki) e2 | AppRCtx v1 K2 => AppRCtx v1 (comp_ctx K2 Ki) `````` Ralf Jung committed Jan 05, 2016 164 165 166 `````` | Op1Ctx _ _ f K => Op1Ctx f (comp_ctx K Ki) | Op2LCtx _ _ _ f K1 e2 => Op2LCtx f (comp_ctx K1 Ki) e2 | Op2RCtx _ _ _ f v1 K2 => Op2RCtx f v1 (comp_ctx K2 Ki) `````` Ralf Jung committed Jan 04, 2016 167 168 169 170 171 172 173 `````` | PairLCtx K1 e2 => PairLCtx (comp_ctx K1 Ki) e2 | PairRCtx v1 K2 => PairRCtx v1 (comp_ctx K2 Ki) | FstCtx K => FstCtx (comp_ctx K Ki) | SndCtx K => SndCtx (comp_ctx K Ki) | InjLCtx K => InjLCtx (comp_ctx K Ki) | InjRCtx K => InjRCtx (comp_ctx K Ki) | CaseCtx K e1 e2 => CaseCtx (comp_ctx K Ki) e1 e2 `````` Ralf Jung committed Jan 06, 2016 174 175 `````` | RefCtx K => RefCtx (comp_ctx K Ki) | LoadCtx K => LoadCtx (comp_ctx K Ki) `````` Ralf Jung committed Jan 04, 2016 176 177 178 179 180 181 182 183 184 185 186 `````` end. Lemma fill_empty e : fill EmptyCtx e = e. Proof. reflexivity. Qed. Lemma fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ctx K1 K2) e. Proof. `````` Ralf Jung committed Jan 04, 2016 187 `````` revert K2 e; induction K1 => K2 e /=; rewrite ?IHK1 ?IHK2; reflexivity. `````` Ralf Jung committed Jan 04, 2016 188 189 190 191 192 ``````Qed. Lemma fill_inj_r K e1 e2 : fill K e1 = fill K e2 -> e1 = e2. Proof. `````` Ralf Jung committed Jan 04, 2016 193 194 `````` revert e1 e2; induction K => el er /=; (move=><-; reflexivity) || (case => /IHK <-; reflexivity). `````` Ralf Jung committed Jan 04, 2016 195 196 ``````Qed. `````` Ralf Jung committed Jan 04, 2016 197 ``````Lemma fill_value K e v': `````` Ralf Jung committed Jan 05, 2016 198 `````` e2v (fill K e) = Some v' -> is_Some (e2v e). `````` Ralf Jung committed Jan 04, 2016 199 ``````Proof. `````` Ralf Jung committed Jan 04, 2016 200 `````` revert v'; induction K => v' /=; try discriminate; `````` Ralf Jung committed Jan 04, 2016 201 202 203 `````` try destruct (e2v (fill K e)); rewrite ?v2v; eauto. Qed. `````` Ralf Jung committed Jan 05, 2016 204 205 206 ``````Lemma fill_not_value e K : e2v e = None -> e2v (fill K e) = None. Proof. `````` Ralf Jung committed Jan 05, 2016 207 `````` intros Hnval. induction K =>/=; by rewrite ?v2v /= ?IHK /=. `````` Ralf Jung committed Jan 05, 2016 208 ``````Qed. `````` 209 `````` `````` Ralf Jung committed Jan 05, 2016 210 211 212 213 214 215 216 217 ``````Lemma fill_not_value2 e K v : e2v e = None -> e2v (fill K e) = Some v -> False. Proof. intros Hnval Hval. erewrite fill_not_value in Hval by assumption. discriminate. Qed. (** The stepping relation *) `````` Ralf Jung committed Jan 04, 2016 218 ``````Inductive prim_step : expr -> state -> expr -> state -> option expr -> Prop := `````` Ralf Jung committed Jan 05, 2016 219 ``````| BetaS e1 e2 v2 σ (Hv2 : e2v e2 = Some v2): `````` Ralf Jung committed Jan 06, 2016 220 `````` prim_step (App (Rec e1) e2) σ (e1.[e2.:(Rec e1).:ids]) σ None `````` Ralf Jung committed Jan 05, 2016 221 222 223 224 ``````| Op1S T1 To (f : T1 -> To) t σ: prim_step (Op1 f (Lit t)) σ (Lit (f t)) σ None | Op2S T1 T2 To (f : T1 -> T2 -> To) t1 t2 σ: prim_step (Op2 f (Lit t1) (Lit t2)) σ (Lit (f t1 t2)) σ None `````` Ralf Jung committed Jan 04, 2016 225 226 227 228 ``````| FstS e1 v1 e2 v2 σ (Hv1 : e2v e1 = Some v1) (Hv2 : e2v e2 = Some v2): prim_step (Fst (Pair e1 e2)) σ e1 σ None | SndS e1 v1 e2 v2 σ (Hv1 : e2v e1 = Some v1) (Hv2 : e2v e2 = Some v2): prim_step (Snd (Pair e1 e2)) σ e2 σ None `````` Ralf Jung committed Jan 05, 2016 229 ``````| CaseLS e0 v0 e1 e2 σ (Hv0 : e2v e0 = Some v0): `````` Ralf Jung committed Jan 04, 2016 230 `````` prim_step (Case (InjL e0) e1 e2) σ (e1.[e0/]) σ None `````` Ralf Jung committed Jan 05, 2016 231 232 233 ``````| CaseRS e0 v0 e1 e2 σ (Hv0 : e2v e0 = Some v0): prim_step (Case (InjR e0) e1 e2) σ (e2.[e0/]) σ None | ForkS e σ: `````` Ralf Jung committed Jan 06, 2016 234 235 236 237 238 `````` prim_step (Fork e) σ LitUnit σ (Some e) | RefS e v σ l (Hv : e2v e = Some v) (Hfresh : σ !! l = None): prim_step (Ref e) σ (Loc l) (<[l:=v]>σ) None | LoadS l σ v (Hlookup : σ !! l = Some v): prim_step (Load (Loc l)) σ (v2e v) σ None. `````` 239 240 `````` Definition reducible e: Prop := `````` Ralf Jung committed Jan 04, 2016 241 `````` exists σ e' σ' ef, prim_step e σ e' σ' ef. `````` 242 `````` `````` Ralf Jung committed Jan 06, 2016 243 244 245 246 247 248 ``````Lemma reducible_not_value e: reducible e -> e2v e = None. Proof. intros (σ' & e'' & σ'' & ef & Hstep). destruct Hstep; simpl in *; reflexivity. Qed. `````` 249 250 251 252 253 254 255 256 ``````Definition stuck (e : expr) : Prop := forall K e', e = fill K e' -> ~reducible e'. Lemma values_stuck v : stuck (v2e v). Proof. `````` Ralf Jung committed Jan 04, 2016 257 258 259 `````` intros ?? Heq. edestruct (fill_value K) as [v' Hv']. { by rewrite <-Heq, v2v. } `````` Ralf Jung committed Jan 06, 2016 260 261 `````` clear -Hv' => Hred. apply reducible_not_value in Hred. destruct (e2v e'); discriminate. `````` Ralf Jung committed Jan 04, 2016 262 ``````Qed. `````` Ralf Jung committed Jan 04, 2016 263 `````` `````` Ralf Jung committed Jan 05, 2016 264 ``````Section step_by_value. `````` Ralf Jung committed Jan 04, 2016 265 266 267 268 ``````(* When something does a step, and another decomposition of the same expression has a non-value e in the hole, then K is a left sub-context of K' - in other words, e also contains the reducible expression *) `````` Ralf Jung committed Jan 05, 2016 269 ``````Lemma step_by_value {K K' e e'} : `````` Ralf Jung committed Jan 04, 2016 270 271 272 273 274 `````` fill K e = fill K' e' -> reducible e' -> e2v e = None -> exists K'', K' = comp_ctx K K''. Proof. `````` Ralf Jung committed Jan 05, 2016 275 276 277 278 `````` Ltac bad_fill Hfill := exfalso; move: Hfill; first [case_depeq3 | case_depeq2 | case_depeq1 | case] =>Hfill; intros; subst; (eapply values_stuck; eassumption) || (eapply fill_not_value2; first eassumption; by erewrite ?Hfill, ?v2v). `````` Ralf Jung committed Jan 06, 2016 279 `````` Ltac bad_red Hfill e' Hred := exfalso; destruct e'; try discriminate Hfill; []; `````` Ralf Jung committed Jan 05, 2016 280 281 282 283 284 285 `````` case: Hfill; intros; subst; destruct Hred as (σ' & e'' & σ'' & ef & Hstep); inversion Hstep; done || (clear Hstep; subst; eapply fill_not_value2; last ( try match goal with [ H : _ = fill _ _ |- _ ] => erewrite <-H end; simpl; repeat match goal with [ H : e2v _ = _ |- _ ] => erewrite H; simpl end ); eassumption || done). `````` Ralf Jung committed Jan 05, 2016 286 `````` Ltac good Hfill IH := move: Hfill; first [case_depeq3 | case_depeq2 | case_depeq1 | case]; intros; subst; `````` Ralf Jung committed Jan 05, 2016 287 288 289 290 `````` let K'' := fresh "K''" in edestruct IH as [K'' Hcomp]; first eassumption; exists K''; by eauto using f_equal, f_equal2, f_equal3, v2e_inj. intros Hfill Hred Hnval. `````` Ralf Jung committed Jan 06, 2016 291 292 293 `````` revert K' Hfill; induction K=>K' /= Hfill; first (now eexists; reflexivity); destruct K'; simpl; try discriminate Hfill; try first [ `````` Ralf Jung committed Jan 05, 2016 294 `````` bad_red Hfill e' Hred `````` Ralf Jung committed Jan 05, 2016 295 `````` | bad_fill Hfill `````` Ralf Jung committed Jan 05, 2016 296 `````` | good Hfill IHK `````` Ralf Jung committed Jan 06, 2016 297 `````` ]. `````` Ralf Jung committed Jan 05, 2016 298 299 ``````Qed. End step_by_value. `````` Ralf Jung committed Jan 05, 2016 300 `````` `````` 301 302 303 ``````(** Atomic expressions *) Definition atomic (e: expr) := match e with `````` Ralf Jung committed Jan 06, 2016 304 305 `````` | Ref e => is_Some (e2v e) | Load e => is_Some (e2v e) `````` 306 307 308 `````` | _ => False end. `````` Ralf Jung committed Jan 06, 2016 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 ``````Lemma atomic_not_value e : atomic e -> e2v e = None. Proof. destruct e; simpl; contradiction || reflexivity. Qed. Lemma atomic_step e1 σ1 e2 σ2 ef : atomic e1 -> prim_step e1 σ1 e2 σ2 ef -> is_Some (e2v e2). Proof. destruct e1; simpl; intros Hatomic Hstep; inversion Hstep; try contradiction Hatomic; rewrite ?v2v /=; eexists; reflexivity. Qed. (* Atomics must not contain evaluation positions. *) Lemma atomic_fill e K : atomic (fill K e) -> e2v e = None -> K = EmptyCtx. Proof. destruct K; simpl; first reflexivity; intros Hatomic Hnval; exfalso; try assumption; destruct Hatomic; eapply fill_not_value2; eassumption. Qed. `````` 333 ``````(** Tests, making sure that stuff works. *) `````` Ralf Jung committed Jan 05, 2016 334 ``````Module Tests. `````` Ralf Jung committed Jan 06, 2016 335 `````` Definition add := Op2 plus (Lit 21) (Lit 21). `````` Ralf Jung committed Jan 05, 2016 336 `````` `````` Ralf Jung committed Jan 06, 2016 337 `````` Goal forall σ, prim_step add σ (Lit 42) σ None. `````` Ralf Jung committed Jan 05, 2016 338 339 340 `````` Proof. apply Op2S. Qed. `````` Ralf Jung committed Jan 06, 2016 341 342 343 344 345 346 347 348 349 350 351 352 353 354 `````` Definition rec := Rec (App (Var 1) (Var 0)). (* fix f x => f x *) Definition rec_app := App rec (Lit 0). Goal forall σ, prim_step rec_app σ rec_app σ None. Proof. move=>?. eapply BetaS. (* Honestly, I have no idea why this works. *) reflexivity. Qed. Definition lam := Lam (Op2 plus (Var 0) (Lit 21)). Goal forall σ, prim_step (App lam (Lit 21)) σ add σ None. Proof. move=>?. eapply BetaS. reflexivity. Qed. `````` Ralf Jung committed Jan 05, 2016 355 ``````End Tests. `````` 356 357 358 359 360 361 `````` (** Instantiate the Iris language interface. This closes reduction under evaluation contexts. We could potentially make this a generic construction. *) Section Language. Local Obligation Tactic := idtac. `````` Ralf Jung committed Jan 05, 2016 362 `````` Definition ectx_step e1 σ1 e2 σ2 (ef: option expr) := `````` 363 364 `````` exists K e1' e2', e1 = fill K e1' /\ e2 = fill K e2' /\ prim_step e1' σ1 e2' σ2 ef. `````` Ralf Jung committed Jan 05, 2016 365 `````` Instance heap_lang : Language expr value state := Build_Language v2e e2v atomic ectx_step. `````` 366 367 368 369 `````` Proof. - exact v2v. - exact e2e. - intros e1 σ1 e2 σ2 ef (K & e1' & e2' & He1 & He2 & Hstep). subst e1 e2. `````` Ralf Jung committed Jan 06, 2016 370 371 372 373 374 375 376 `````` eapply fill_not_value. eapply reducible_not_value. do 4 eexists; eassumption. - exact atomic_not_value. - intros ? ? ? ? ? Hatomic (K & e1' & e2' & Heq1 & Heq2 & Hstep). subst. move: (Hatomic). rewrite (atomic_fill e1' K). (* RJ: this is kind of annoying. *) + rewrite !fill_empty. eauto using atomic_step. + assumption. + clear Hatomic. eapply reducible_not_value. do 4 eexists; eassumption. `````` Ralf Jung committed Jan 05, 2016 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 `````` Defined. (** We can have bind with arbitrary evaluation contexts **) Lemma fill_is_ctx K: is_ctx (fill K). Proof. split; last split. - intros ? [v Hval]. eapply fill_value. eassumption. - intros ? ? ? ? ? (K' & e1' & e2' & Heq1 & Heq2 & Hstep). exists (comp_ctx K K'), e1', e2'. rewrite -!fill_comp Heq1 Heq2. split; last split; reflexivity || assumption. - intros ? ? ? ? ? Hnval (K'' & e1'' & e2'' & Heq1 & Heq2 & Hstep). destruct (step_by_value Heq1) as [K' HeqK]. + do 4 eexists. eassumption. + assumption. + subst e2 K''. rewrite -fill_comp in Heq1. apply fill_inj_r in Heq1. subst e1'. exists (fill K' e2''). split; first by rewrite -fill_comp. do 3 eexists. split; last split; eassumption || reflexivity. `````` 394 `````` Qed. `````` Ralf Jung committed Jan 05, 2016 395 `````` `````` 396 ``End Language.``