substitution.v 5.93 KB
Newer Older
1
From heap_lang Require Export derived.
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's avatar
Ralf Jung committed
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.
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;
105
    repeat (simplify_option_eq || case_match); f_equal; auto.
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;
112
    repeat (simplify_option_eq || case_match);
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.

123
Lemma wp_rec E e1 f x erec e2 v Q :
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.
130
  by apply wp_rec'.
131
132
Qed.

133
Lemma wp_lam E x ef e v Q :
134
  to_val e = Some v   wp E (gsubst ef x e) Q  wp E (App (Lam x ef) e) Q.
135
Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_lam'. Qed.
136

137
Lemma wp_let E x e1 e2 v Q :
138
  to_val e1 = Some v   wp E (gsubst e2 x e1) Q  wp E (Let x e1 e2) Q.
139
Proof. apply wp_lam. Qed.
140

141
Lemma wp_case_inl E e0 v0 x1 e1 x2 e2 Q :
142
143
  to_val e0 = Some v0 
   wp E (gsubst e1 x1 e0) Q  wp E (Case (InjL e0) x1 e1 x2 e2) Q.
144
Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_case_inl'. Qed.
145

146
Lemma wp_case_inr E e0 v0 x1 e1 x2 e2 Q :
147
148
  to_val e0 = Some v0 
   wp E (gsubst e2 x2 e0) Q  wp E (Case (InjR e0) x1 e1 x2 e2) Q.
149
Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_case_inr'. Qed.
150
151
End wp.