ectx_language.v 6.44 KB
 Ralf Jung committed Mar 30, 2016 1 2 ``````(** An axiomatization of evaluation-context based languages, including a proof that this gives rise to a "language" in the Iris sense. *) `````` 3 ``````From iris.algebra Require Export base. `````` Ralf Jung committed Mar 30, 2016 4 ``````From iris.program_logic Require Import language. `````` Ralf Jung committed Jan 05, 2017 5 ``````Set Default Proof Using "Type". `````` 6 7 8 `````` (* We need to make thos arguments indices that we want canonical structure inference to use a keys. *) `````` Robbert Krebbers committed Mar 29, 2016 9 ``````Class EctxLanguage (expr val ectx state : Type) := { `````` 10 11 12 13 14 `````` of_val : val → expr; to_val : expr → option val; empty_ectx : ectx; comp_ectx : ectx → ectx → ectx; fill : ectx → expr → expr; `````` Robbert Krebbers committed Aug 08, 2016 15 `````` head_step : expr → state → expr → state → list expr → Prop; `````` 16 17 18 `````` to_of_val v : to_val (of_val v) = Some v; of_to_val e v : to_val e = Some v → of_val v = e; `````` Robbert Krebbers committed Aug 08, 2016 19 `````` val_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → to_val e1 = None; `````` 20 21 22 `````` fill_empty e : fill empty_ectx e = e; fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e; `````` Robbert Krebbers committed Mar 29, 2016 23 `````` fill_inj K :> Inj (=) (=) (fill K); `````` 24 25 `````` fill_not_val K e : to_val e = None → to_val (fill K e) = None; `````` Robbert Krebbers committed Mar 29, 2016 26 27 28 `````` (* There are a whole lot of sensible axioms (like associativity, and left and right identity, we could demand for [comp_ectx] and [empty_ectx]. However, positivity suffices. *) `````` Ralf Jung committed Mar 29, 2016 29 `````` ectx_positive K1 K2 : `````` Robbert Krebbers committed Mar 29, 2016 30 `````` comp_ectx K1 K2 = empty_ectx → K1 = empty_ectx ∧ K2 = empty_ectx; `````` Ralf Jung committed Mar 29, 2016 31 `````` `````` Robbert Krebbers committed Aug 08, 2016 32 `````` step_by_val K K' e1 e1' σ1 e2 σ2 efs : `````` 33 34 `````` fill K e1 = fill K' e1' → to_val e1 = None → `````` Robbert Krebbers committed Aug 08, 2016 35 `````` head_step e1' σ1 e2 σ2 efs → `````` 36 37 `````` exists K'', K' = comp_ectx K K''; }. `````` Robbert Krebbers committed Mar 29, 2016 38 `````` `````` Robbert Krebbers committed Sep 09, 2017 39 40 ``````Arguments of_val {_ _ _ _ _} _%V. Arguments to_val {_ _ _ _ _} _%E. `````` 41 42 ``````Arguments empty_ectx {_ _ _ _ _}. Arguments comp_ectx {_ _ _ _ _} _ _. `````` Robbert Krebbers committed Sep 09, 2017 43 44 ``````Arguments fill {_ _ _ _ _} _ _%E. Arguments head_step {_ _ _ _ _} _%E _ _%E _ _. `````` 45 46 47 48 49 50 51 `````` Arguments to_of_val {_ _ _ _ _} _. Arguments of_to_val {_ _ _ _ _} _ _ _. Arguments val_stuck {_ _ _ _ _} _ _ _ _ _ _. Arguments fill_empty {_ _ _ _ _} _. Arguments fill_comp {_ _ _ _ _} _ _ _. Arguments fill_not_val {_ _ _ _ _} _ _ _. `````` Ralf Jung committed Mar 29, 2016 52 ``````Arguments ectx_positive {_ _ _ _ _} _ _ _. `````` 53 54 55 ``````Arguments step_by_val {_ _ _ _ _} _ _ _ _ _ _ _ _ _ _ _. (* From an ectx_language, we can construct a language. *) `````` Robbert Krebbers committed Mar 29, 2016 56 57 ``````Section ectx_language. Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}. `````` 58 59 `````` Implicit Types (e : expr) (K : ectx). `````` Ralf Jung committed Mar 29, 2016 60 `````` Definition head_reducible (e : expr) (σ : state) := `````` Robbert Krebbers committed Aug 08, 2016 61 `````` ∃ e' σ' efs, head_step e σ e' σ' efs. `````` Robbert Krebbers committed Mar 15, 2017 62 63 64 65 66 `````` Definition head_irreducible (e : expr) (σ : state) := ∀ e' σ' efs, ¬head_step e σ e' σ' efs. Definition sub_values (e : expr) := ∀ K e', e = fill K e' → to_val e' = None → K = empty_ectx. `````` Ralf Jung committed Mar 29, 2016 67 `````` `````` 68 `````` Inductive prim_step (e1 : expr) (σ1 : state) `````` Robbert Krebbers committed Aug 08, 2016 69 `````` (e2 : expr) (σ2 : state) (efs : list expr) : Prop := `````` Robbert Krebbers committed Mar 29, 2016 70 71 `````` Ectx_step K e1' e2' : e1 = fill K e1' → e2 = fill K e2' → `````` Robbert Krebbers committed Aug 08, 2016 72 `````` head_step e1' σ1 e2' σ2 efs → prim_step e1 σ1 e2 σ2 efs. `````` 73 `````` `````` Robbert Krebbers committed Aug 29, 2016 74 75 76 77 `````` Lemma Ectx_step' K e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → prim_step (fill K e1) σ1 (fill K e2) σ2 efs. Proof. econstructor; eauto. Qed. `````` Robbert Krebbers committed Aug 08, 2016 78 79 `````` Lemma val_prim_stuck e1 σ1 e2 σ2 efs : prim_step e1 σ1 e2 σ2 efs → to_val e1 = None. `````` 80 81 82 83 84 `````` Proof. intros [??? -> -> ?]; eauto using fill_not_val, val_stuck. Qed. Canonical Structure ectx_lang : language := {| language.expr := expr; language.val := val; language.state := state; language.of_val := of_val; language.to_val := to_val; `````` Robbert Krebbers committed Mar 29, 2016 85 `````` language.prim_step := prim_step; `````` 86 `````` language.to_of_val := to_of_val; language.of_to_val := of_to_val; `````` Robbert Krebbers committed Mar 29, 2016 87 `````` language.val_stuck := val_prim_stuck; `````` 88 89 `````` |}. `````` Ralf Jung committed Mar 29, 2016 90 `````` (* Some lemmas about this language *) `````` Robbert Krebbers committed Aug 08, 2016 91 92 `````` Lemma head_prim_step e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → prim_step e1 σ1 e2 σ2 efs. `````` Robbert Krebbers committed Mar 29, 2016 93 94 `````` Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed. `````` Robbert Krebbers committed Mar 15, 2017 95 96 97 `````` Lemma not_head_reducible e σ : ¬head_reducible e σ ↔ head_irreducible e σ. Proof. unfold head_reducible, head_irreducible. naive_solver. Qed. `````` Robbert Krebbers committed Mar 29, 2016 98 `````` Lemma head_prim_reducible e σ : head_reducible e σ → reducible e σ. `````` Robbert Krebbers committed Aug 08, 2016 99 `````` Proof. intros (e'&σ'&efs&?). eexists e', σ', efs. by apply head_prim_step. Qed. `````` Robbert Krebbers committed Mar 15, 2017 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 `````` Lemma head_prim_irreducible e σ : irreducible e σ → head_irreducible e σ. Proof. rewrite -not_reducible -not_head_reducible. eauto using head_prim_reducible. Qed. Lemma prim_head_reducible e σ : reducible e σ → sub_values e → head_reducible e σ. Proof. intros (e'&σ'&efs&[K e1' e2' -> -> Hstep]) ?. assert (K = empty_ectx) as -> by eauto 10 using val_stuck. rewrite fill_empty /head_reducible; eauto. Qed. Lemma prim_head_irreducible e σ : head_irreducible e σ → sub_values e → irreducible e σ. Proof. rewrite -not_reducible -not_head_reducible. eauto using prim_head_reducible. Qed. `````` Ralf Jung committed Mar 29, 2016 117 `````` `````` Robbert Krebbers committed Jul 21, 2016 118 `````` Lemma ectx_language_atomic e : `````` 119 `````` (∀ σ e' σ' efs, head_step e σ e' σ' efs → irreducible e' σ') → `````` Robbert Krebbers committed Mar 15, 2017 120 `````` sub_values e → `````` Robbert Krebbers committed Nov 04, 2017 121 `````` Atomic e. `````` Jacques-Henri Jourdan committed Jul 20, 2016 122 `````` Proof. `````` Robbert Krebbers committed Aug 08, 2016 123 `````` intros Hatomic_step Hatomic_fill σ e' σ' efs [K e1' e2' -> -> Hstep]. `````` Robbert Krebbers committed Jul 21, 2016 124 125 `````` assert (K = empty_ectx) as -> by eauto 10 using val_stuck. rewrite fill_empty. eapply Hatomic_step. by rewrite fill_empty. `````` Jacques-Henri Jourdan committed Jul 20, 2016 126 127 `````` Qed. `````` Robbert Krebbers committed Aug 08, 2016 128 `````` Lemma head_reducible_prim_step e1 σ1 e2 σ2 efs : `````` Robbert Krebbers committed Mar 15, 2017 129 130 `````` head_reducible e1 σ1 → prim_step e1 σ1 e2 σ2 efs → `````` Robbert Krebbers committed Aug 08, 2016 131 `````` head_step e1 σ1 e2 σ2 efs. `````` Ralf Jung committed Mar 29, 2016 132 `````` Proof. `````` Robbert Krebbers committed Aug 08, 2016 133 134 `````` intros (e2''&σ2''&efs''&?) [K e1' e2' -> -> Hstep]. destruct (step_by_val K empty_ectx e1' (fill K e1') σ1 e2'' σ2'' efs'') `````` Robbert Krebbers committed Mar 29, 2016 135 `````` as [K' [-> _]%symmetry%ectx_positive]; `````` Ralf Jung committed Mar 29, 2016 136 137 138 139 `````` eauto using fill_empty, fill_not_val, val_stuck. by rewrite !fill_empty. Qed. `````` 140 141 142 143 144 145 146 147 `````` (* Every evaluation context is a context. *) Global Instance ectx_lang_ctx K : LanguageCtx ectx_lang (fill K). Proof. split. - eauto using fill_not_val. - intros ????? [K' e1' e2' Heq1 Heq2 Hstep]. by exists (comp_ectx K K') e1' e2'; rewrite ?Heq1 ?Heq2 ?fill_comp. - intros e1 σ1 e2 σ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep]. `````` Robbert Krebbers committed Aug 08, 2016 148 `````` destruct (step_by_val K K'' e1 e1'' σ1 e2'' σ2 efs) as [K' ->]; eauto. `````` Robbert Krebbers committed Mar 29, 2016 149 `````` rewrite -fill_comp in Heq1; apply (inj (fill _)) in Heq1. `````` 150 151 152 `````` exists (fill K' e2''); rewrite -fill_comp; split; auto. econstructor; eauto. Qed. `````` Dan Frumin committed Sep 25, 2017 153 `````` `````` Robbert Krebbers committed Oct 05, 2017 154 `````` Lemma det_head_step_pure_exec (P : Prop) e1 e2 : `````` Robbert Krebbers committed Oct 05, 2017 155 156 157 158 `````` (∀ σ, P → head_reducible e1 σ) → (∀ σ1 e2' σ2 efs, P → head_step e1 σ1 e2' σ2 efs → σ1 = σ2 ∧ e2=e2' ∧ efs = []) → PureExec P e1 e2. `````` Dan Frumin committed Sep 25, 2017 159 160 `````` Proof. intros Hp1 Hp2. split. `````` Robbert Krebbers committed Oct 05, 2017 161 162 163 `````` - intros σ ?. destruct (Hp1 σ) as (e2' & σ2 & efs & ?); first done. eexists e2', σ2, efs. by apply head_prim_step. - intros σ1 e2' σ2 efs ? ?%head_reducible_prim_step; eauto. `````` Dan Frumin committed Sep 25, 2017 164 `````` Qed. `````` Robbert Krebbers committed Mar 29, 2016 165 ``````End ectx_language. `````` 166 `````` `````` Ralf Jung committed Mar 30, 2016 167 ``Arguments ectx_lang _ {_ _ _ _}.``