substitution.v 5.93 KB
 Robbert Krebbers committed Feb 13, 2016 1 ``````From heap_lang Require Export derived. `````` Robbert Krebbers committed Feb 12, 2016 2 3 4 5 6 7 8 9 10 11 12 13 14 `````` (** We define an alternative notion of substitution [gsubst e x ev] that preserves the expression [e] syntactically in case the variable [x] does not occur freely in [e]. By syntactically, we mean that [e] is preserved without unfolding any Coq definitions. For example: << Definition id : val := λ: "x", "x". Eval simpl in subst (id "y") "y" '10. (* (Lam "x" "x") '10 *) Eval simpl in gsubst (id "y") "y" '10. (* id '10 *) >> For [gsubst e x ev] to work, [e] should not contain any opaque parts. `````` Ralf Jung committed Feb 12, 2016 15 16 17 18 ``````Fundamentally, the way this works is that [gsubst] tests whether a subterm needs substitution, before it traverses into the term. This way, unaffected sub-terms are returned directly, rather than their tree structure being deconstructed and composed again. `````` Robbert Krebbers committed Feb 12, 2016 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 `````` The function [gsubst e x ev] differs in yet another way from [subst e x v]. The function [gsubst] substitutes an expression [ev] whereas [subst] substitutes a value [v]. This way we avoid unnecessary conversion back and forth between values and expressions, which could also cause Coq definitions to be unfolded. For example, consider the rule [wp_rec'] from below: << Definition foo : val := rec: "f" "x" := ... . Lemma wp_rec' E e1 f x erec e2 v Q : e1 = Rec f x erec → to_val e2 = Some v → ▷ wp E (gsubst (gsubst erec f e1) x e2) Q ⊑ wp E (App e1 e2) Q. >> We ensure that [e1] is substituted instead of [RecV f x erec]. So, for example when taking [e1 := foo] we ensure that [foo] is substituted without being unfolded. *) (** * Implementation *) (** The core of [gsubst e x ev] is the partial function [gsubst_go e x ev] that returns [None] in case [x] does not occur freely in [e] and [Some e'] in case [x] occurs in [e]. The function [gsubst e x ev] is then simply defined as [from_option e (gsubst_go e x ev)]. *) Definition gsubst_lift {A B C} (f : A → B → C) (x : A) (y : B) (mx : option A) (my : option B) : option C := match mx, my with | Some x, Some y => Some (f x y) | Some x, None => Some (f x y) | None, Some y => Some (f x y) | None, None => None end. Fixpoint gsubst_go (e : expr) (x : string) (ev : expr) : option expr := match e with | Var y => if decide (x = y ∧ x ≠ "") then Some ev else None | Rec f y e => if decide (x ≠ f ∧ x ≠ y) then Rec f y <\$> gsubst_go e x ev else None | App e1 e2 => gsubst_lift App e1 e2 (gsubst_go e1 x ev) (gsubst_go e2 x ev) | Lit l => None | UnOp op e => UnOp op <\$> gsubst_go e x ev | BinOp op e1 e2 => gsubst_lift (BinOp op) e1 e2 (gsubst_go e1 x ev) (gsubst_go e2 x ev) | If e0 e1 e2 => gsubst_lift id (If e0 e1) e2 (gsubst_lift If e0 e1 (gsubst_go e0 x ev) (gsubst_go e1 x ev)) (gsubst_go e2 x ev) | Pair e1 e2 => gsubst_lift Pair e1 e2 (gsubst_go e1 x ev) (gsubst_go e2 x ev) | Fst e => Fst <\$> gsubst_go e x ev | Snd e => Snd <\$> gsubst_go e x ev | InjL e => InjL <\$> gsubst_go e x ev | InjR e => InjR <\$> gsubst_go e x ev | Case e0 x1 e1 x2 e2 => gsubst_lift id (Case e0 x1 e1 x2) e2 (gsubst_lift (λ e0' e1', Case e0' x1 e1' x2) e0 e1 (gsubst_go e0 x ev) (if decide (x ≠ x1) then gsubst_go e1 x ev else None)) (if decide (x ≠ x2) then gsubst_go e2 x ev else None) | Fork e => Fork <\$> gsubst_go e x ev | Loc l => None | Alloc e => Alloc <\$> gsubst_go e x ev | Load e => Load <\$> gsubst_go e x ev | Store e1 e2 => gsubst_lift Store e1 e2 (gsubst_go e1 x ev) (gsubst_go e2 x ev) | Cas e0 e1 e2 => gsubst_lift id (Cas e0 e1) e2 (gsubst_lift Cas e0 e1 (gsubst_go e0 x ev) (gsubst_go e1 x ev)) (gsubst_go e2 x ev) end. Definition gsubst (e : expr) (x : string) (ev : expr) : expr := from_option e (gsubst_go e x ev). (** * Simpl *) (** Ensure that [simpl] unfolds [gsubst e x ev] when applied to a concrete term [e] and use [simpl nomatch] to ensure that it does not reduce in case [e] contains any opaque parts that block reduction. *) Arguments gsubst !_ _ _/ : simpl nomatch. (** We define heap_lang functions as values (see [id] above). In order to ensure too eager conversion to expressions, we block [simpl]. *) Arguments of_val : simpl never. (** * Correctness *) (** We prove that [gsubst] behaves like [subst] when substituting values. *) Lemma gsubst_None e x v : gsubst_go e x (of_val v) = None → e = subst e x v. Proof. induction e; simpl; unfold gsubst_lift; intros; `````` Robbert Krebbers committed Feb 17, 2016 105 `````` repeat (simplify_option_eq || case_match); f_equal; auto. `````` Robbert Krebbers committed Feb 12, 2016 106 107 108 109 110 111 ``````Qed. Lemma gsubst_correct e x v : gsubst e x (of_val v) = subst e x v. Proof. unfold gsubst; destruct (gsubst_go e x (of_val v)) as [e'|] eqn:He; simpl; last by apply gsubst_None. revert e' He; induction e; simpl; unfold gsubst_lift; intros; `````` Robbert Krebbers committed Feb 17, 2016 112 `````` repeat (simplify_option_eq || case_match); `````` Robbert Krebbers committed Feb 12, 2016 113 114 115 116 117 118 119 120 121 122 `````` f_equal; auto using gsubst_None. Qed. (** * Weakest precondition rules *) Section wp. Context {Σ : iFunctor}. Implicit Types P : iProp heap_lang Σ. Implicit Types Q : val → iProp heap_lang Σ. Hint Resolve to_of_val. `````` Ralf Jung committed Feb 12, 2016 123 ``````Lemma wp_rec E e1 f x erec e2 v Q : `````` Robbert Krebbers committed Feb 12, 2016 124 125 126 127 128 129 `````` e1 = Rec f x erec → to_val e2 = Some v → ▷ wp E (gsubst (gsubst erec f e1) x e2) Q ⊑ wp E (App e1 e2) Q. Proof. intros -> <-%of_to_val. rewrite (gsubst_correct _ _ (RecV _ _ _)) gsubst_correct. `````` Ralf Jung committed Feb 12, 2016 130 `````` by apply wp_rec'. `````` Robbert Krebbers committed Feb 12, 2016 131 132 ``````Qed. `````` Ralf Jung committed Feb 12, 2016 133 ``````Lemma wp_lam E x ef e v Q : `````` Robbert Krebbers committed Feb 12, 2016 134 `````` to_val e = Some v → ▷ wp E (gsubst ef x e) Q ⊑ wp E (App (Lam x ef) e) Q. `````` Ralf Jung committed Feb 12, 2016 135 ``````Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_lam'. Qed. `````` Robbert Krebbers committed Feb 12, 2016 136 `````` `````` Ralf Jung committed Feb 12, 2016 137 ``````Lemma wp_let E x e1 e2 v Q : `````` Robbert Krebbers committed Feb 12, 2016 138 `````` to_val e1 = Some v → ▷ wp E (gsubst e2 x e1) Q ⊑ wp E (Let x e1 e2) Q. `````` Ralf Jung committed Feb 12, 2016 139 ``````Proof. apply wp_lam. Qed. `````` Robbert Krebbers committed Feb 12, 2016 140 `````` `````` Ralf Jung committed Feb 12, 2016 141 ``````Lemma wp_case_inl E e0 v0 x1 e1 x2 e2 Q : `````` Robbert Krebbers committed Feb 12, 2016 142 143 `````` to_val e0 = Some v0 → ▷ wp E (gsubst e1 x1 e0) Q ⊑ wp E (Case (InjL e0) x1 e1 x2 e2) Q. `````` Ralf Jung committed Feb 12, 2016 144 ``````Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_case_inl'. Qed. `````` Robbert Krebbers committed Feb 12, 2016 145 `````` `````` Ralf Jung committed Feb 12, 2016 146 ``````Lemma wp_case_inr E e0 v0 x1 e1 x2 e2 Q : `````` Robbert Krebbers committed Feb 12, 2016 147 148 `````` to_val e0 = Some v0 → ▷ wp E (gsubst e2 x2 e0) Q ⊑ wp E (Case (InjR e0) x1 e1 x2 e2) Q. `````` Ralf Jung committed Feb 12, 2016 149 ``````Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_case_inr'. Qed. `````` Robbert Krebbers committed Feb 12, 2016 150 151 ``````End wp. ``````