ectx_language.v 4.82 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. `````` 5 6 7 `````` (* We need to make thos arguments indices that we want canonical structure inference to use a keys. *) `````` Robbert Krebbers committed Mar 29, 2016 8 ``````Class EctxLanguage (expr val ectx state : Type) := { `````` 9 10 11 12 13 14 15 16 17 18 19 20 21 `````` of_val : val → expr; to_val : expr → option val; empty_ectx : ectx; comp_ectx : ectx → ectx → ectx; fill : ectx → expr → expr; head_step : expr → state → expr → state → option expr → Prop; 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; val_stuck e1 σ1 e2 σ2 ef : head_step e1 σ1 e2 σ2 ef → to_val e1 = None; 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 22 `````` fill_inj K :> Inj (=) (=) (fill K); `````` 23 24 `````` fill_not_val K e : to_val e = None → to_val (fill K e) = None; `````` Robbert Krebbers committed Mar 29, 2016 25 26 27 `````` (* 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 28 `````` ectx_positive K1 K2 : `````` Robbert Krebbers committed Mar 29, 2016 29 `````` comp_ectx K1 K2 = empty_ectx → K1 = empty_ectx ∧ K2 = empty_ectx; `````` Ralf Jung committed Mar 29, 2016 30 `````` `````` 31 32 33 34 35 36 `````` step_by_val K K' e1 e1' σ1 e2 σ2 ef : fill K e1 = fill K' e1' → to_val e1 = None → head_step e1' σ1 e2 σ2 ef → exists K'', K' = comp_ectx K K''; }. `````` Robbert Krebbers committed Mar 29, 2016 37 `````` `````` 38 39 40 41 42 43 44 45 46 47 48 49 50 ``````Arguments of_val {_ _ _ _ _} _. Arguments to_val {_ _ _ _ _} _. Arguments empty_ectx {_ _ _ _ _}. Arguments comp_ectx {_ _ _ _ _} _ _. Arguments fill {_ _ _ _ _} _ _. Arguments head_step {_ _ _ _ _} _ _ _ _ _. 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 51 ``````Arguments ectx_positive {_ _ _ _ _} _ _ _. `````` 52 53 54 ``````Arguments step_by_val {_ _ _ _ _} _ _ _ _ _ _ _ _ _ _ _. (* From an ectx_language, we can construct a language. *) `````` Robbert Krebbers committed Mar 29, 2016 55 56 ``````Section ectx_language. Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}. `````` 57 58 `````` Implicit Types (e : expr) (K : ectx). `````` Ralf Jung committed Mar 29, 2016 59 60 61 `````` Definition head_reducible (e : expr) (σ : state) := ∃ e' σ' ef, head_step e σ e' σ' ef. `````` 62 `````` Inductive prim_step (e1 : expr) (σ1 : state) `````` Robbert Krebbers committed Mar 29, 2016 63 64 65 66 `````` (e2 : expr) (σ2 : state) (ef : option expr) : Prop := Ectx_step K e1' e2' : e1 = fill K e1' → e2 = fill K e2' → head_step e1' σ1 e2' σ2 ef → prim_step e1 σ1 e2 σ2 ef. `````` 67 68 69 70 71 72 73 74 `````` Lemma val_prim_stuck e1 σ1 e2 σ2 ef : prim_step e1 σ1 e2 σ2 ef → to_val e1 = None. 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 75 `````` language.prim_step := prim_step; `````` 76 `````` language.to_of_val := to_of_val; language.of_to_val := of_to_val; `````` Robbert Krebbers committed Mar 29, 2016 77 `````` language.val_stuck := val_prim_stuck; `````` 78 79 `````` |}. `````` Ralf Jung committed Mar 29, 2016 80 `````` (* Some lemmas about this language *) `````` Robbert Krebbers committed Mar 29, 2016 81 82 83 84 85 86 `````` Lemma head_prim_step e1 σ1 e2 σ2 ef : head_step e1 σ1 e2 σ2 ef → prim_step e1 σ1 e2 σ2 ef. Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed. Lemma head_prim_reducible e σ : head_reducible e σ → reducible e σ. Proof. intros (e'&σ'&ef&?). eexists e', σ', ef. by apply head_prim_step. Qed. `````` Ralf Jung committed Mar 29, 2016 87 `````` `````` Robbert Krebbers committed Jul 21, 2016 88 89 90 91 `````` Lemma ectx_language_atomic e : (∀ σ e' σ' ef, head_step e σ e' σ' ef → is_Some (to_val e')) → (∀ K e', e = fill K e' → to_val e' = None → K = empty_ectx) → atomic e. `````` Jacques-Henri Jourdan committed Jul 20, 2016 92 `````` Proof. `````` Robbert Krebbers committed Jul 21, 2016 93 94 95 `````` intros Hatomic_step Hatomic_fill σ e' σ' ef [K e1' e2' -> -> Hstep]. 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 96 97 `````` Qed. `````` Ralf Jung committed Mar 29, 2016 98 99 100 101 `````` Lemma head_reducible_prim_step e1 σ1 e2 σ2 ef : head_reducible e1 σ1 → prim_step e1 σ1 e2 σ2 ef → head_step e1 σ1 e2 σ2 ef. Proof. `````` Robbert Krebbers committed Mar 29, 2016 102 103 104 `````` intros (e2''&σ2''&ef''&?) [K e1' e2' -> -> Hstep]. destruct (step_by_val K empty_ectx e1' (fill K e1') σ1 e2'' σ2'' ef'') as [K' [-> _]%symmetry%ectx_positive]; `````` Ralf Jung committed Mar 29, 2016 105 106 107 108 `````` eauto using fill_empty, fill_not_val, val_stuck. by rewrite !fill_empty. Qed. `````` 109 110 111 112 113 114 115 116 117 `````` (* 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]. destruct (step_by_val K K'' e1 e1'' σ1 e2'' σ2 ef) as [K' ->]; eauto. `````` Robbert Krebbers committed Mar 29, 2016 118 `````` rewrite -fill_comp in Heq1; apply (inj (fill _)) in Heq1. `````` 119 120 121 `````` exists (fill K' e2''); rewrite -fill_comp; split; auto. econstructor; eauto. Qed. `````` Robbert Krebbers committed Mar 29, 2016 122 ``````End ectx_language. `````` 123 `````` `````` Ralf Jung committed Mar 30, 2016 124 ``Arguments ectx_lang _ {_ _ _ _}.``