Commit 8968f2c1 by Ralf Jung

### show that evaluation contexts are 'contexts' in the sense required by bind

parent 65e7a75e
 ... @@ -176,7 +176,7 @@ Proof. ... @@ -176,7 +176,7 @@ Proof. Qed. Qed. Lemma fill_value K e v': Lemma fill_value K e v': e2v (fill K e) = Some v' -> exists v, e2v e = Some v. e2v (fill K e) = Some v' -> is_Some (e2v e). Proof. Proof. revert v'; induction K => v' /=; try discriminate; revert v'; induction K => v' /=; try discriminate; try destruct (e2v (fill K e)); rewrite ?v2v; eauto. try destruct (e2v (fill K e)); rewrite ?v2v; eauto. ... @@ -240,7 +240,7 @@ Section step_by_value. ... @@ -240,7 +240,7 @@ Section step_by_value. expression has a non-value e in the hole, then K is a left 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 sub-context of K' - in other words, e also contains the reducible expression *) expression *) Lemma step_by_value K K' e e' : Lemma step_by_value {K K' e e'} : fill K e = fill K' e' -> fill K e = fill K' e' -> reducible e' -> reducible e' -> e2v e = None -> e2v e = None -> ... @@ -295,10 +295,10 @@ End Tests. ... @@ -295,10 +295,10 @@ End Tests. Section Language. Section Language. Local Obligation Tactic := idtac. Local Obligation Tactic := idtac. Definition ctx_step e1 σ1 e2 σ2 (ef: option expr) := Definition ectx_step e1 σ1 e2 σ2 (ef: option expr) := exists K e1' e2', e1 = fill K e1' /\ e2 = fill K e2' /\ prim_step e1' σ1 e2' σ2 ef. exists K e1' e2', e1 = fill K e1' /\ e2 = fill K e2' /\ prim_step e1' σ1 e2' σ2 ef. Instance heap_lang : Language expr value state := Build_Language v2e e2v atomic ctx_step. Instance heap_lang : Language expr value state := Build_Language v2e e2v atomic ectx_step. Proof. Proof. - exact v2v. - exact v2v. - exact e2e. - exact e2e. ... @@ -308,5 +308,23 @@ Section Language. ... @@ -308,5 +308,23 @@ Section Language. eapply e2e. eassumption. eapply e2e. eassumption. - intros. contradiction. - intros. contradiction. - intros. contradiction. - intros. contradiction. 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. Qed. Qed. End Language. End Language.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!