adamc@190
|
1 (* Copyright (c) 2008, Adam Chlipala
|
adamc@190
|
2 *
|
adamc@190
|
3 * This work is licensed under a
|
adamc@190
|
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
|
adamc@190
|
5 * Unported License.
|
adamc@190
|
6 * The license text is available at:
|
adamc@190
|
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
|
adamc@190
|
8 *)
|
adamc@190
|
9
|
adamc@190
|
10 (* begin hide *)
|
adamc@190
|
11 Require Import Arith List Omega.
|
adamc@190
|
12
|
adamc@190
|
13 Require Import Axioms Tactics.
|
adamc@190
|
14
|
adamc@190
|
15 Set Implicit Arguments.
|
adamc@190
|
16 (* end hide *)
|
adamc@190
|
17
|
adamc@190
|
18
|
adamc@190
|
19 (** %\chapter{Modeling Impure Languages}% *)
|
adamc@190
|
20
|
adamc@190
|
21 (** TODO: Prose for this chapter *)
|
adamc@190
|
22
|
adamc@190
|
23 Section var.
|
adamc@190
|
24 Variable var : Type.
|
adamc@190
|
25
|
adamc@190
|
26 Inductive term : Type :=
|
adamc@190
|
27 | Var : var -> term
|
adamc@190
|
28 | App : term -> term -> term
|
adamc@190
|
29 | Abs : (var -> term) -> term
|
adamc@190
|
30 | Unit : term.
|
adamc@190
|
31 End var.
|
adamc@190
|
32
|
adamc@190
|
33 Implicit Arguments Unit [var].
|
adamc@190
|
34
|
adamc@190
|
35 Notation "# v" := (Var v) (at level 70).
|
adamc@190
|
36 Notation "()" := Unit.
|
adamc@190
|
37
|
adamc@190
|
38 Infix "@" := App (left associativity, at level 72).
|
adamc@190
|
39 Notation "\ x , e" := (Abs (fun x => e)) (at level 73).
|
adamc@190
|
40 Notation "\ ? , e" := (Abs (fun _ => e)) (at level 73).
|
adamc@190
|
41
|
adamc@191
|
42 Definition Term := forall var, term var.
|
adamc@191
|
43
|
adamc@191
|
44 Definition ident : Term := fun _ => \x, #x.
|
adamc@191
|
45 Definition unite : Term := fun _ => ().
|
adamc@191
|
46 Definition ident_self : Term := fun _ => ident _ @ ident _.
|
adamc@191
|
47 Definition ident_unit : Term := fun _ => ident _ @ unite _.
|
adamc@191
|
48
|
adamc@191
|
49
|
adamc@191
|
50 Module impredicative.
|
adamc@191
|
51 Inductive dynamic : Set :=
|
adamc@191
|
52 | Dyn : forall (dynTy : Type), dynTy -> dynamic.
|
adamc@191
|
53
|
adamc@191
|
54 Inductive computation (T : Type) : Set :=
|
adamc@191
|
55 | Return : T -> computation T
|
adamc@191
|
56 | Bind : forall (T' : Type),
|
adamc@191
|
57 computation T' -> (T' -> computation T) -> computation T
|
adamc@191
|
58 | Unpack : dynamic -> computation T.
|
adamc@191
|
59
|
adamc@191
|
60 Inductive eval : forall T, computation T -> T -> Prop :=
|
adamc@191
|
61 | EvalReturn : forall T (v : T),
|
adamc@191
|
62 eval (Return v) v
|
adamc@191
|
63 | EvalUnpack : forall T (v : T),
|
adamc@191
|
64 eval (Unpack T (Dyn v)) v
|
adamc@191
|
65 | EvalBind : forall T1 T2 (c1 : computation T1) (c2 : T1 -> computation T2) v1 v2,
|
adamc@191
|
66 eval c1 v1
|
adamc@191
|
67 -> eval (c2 v1) v2
|
adamc@191
|
68 -> eval (Bind c1 c2) v2.
|
adamc@191
|
69
|
adamc@192
|
70 (* begin thide *)
|
adamc@191
|
71 Fixpoint termDenote (e : term dynamic) : computation dynamic :=
|
adamc@191
|
72 match e with
|
adamc@191
|
73 | Var v => Return v
|
adamc@191
|
74 | App e1 e2 => Bind (termDenote e1) (fun f =>
|
adamc@191
|
75 Bind (termDenote e2) (fun x =>
|
adamc@191
|
76 Bind (Unpack (dynamic -> computation dynamic) f) (fun f' =>
|
adamc@191
|
77 f' x)))
|
adamc@191
|
78 | Abs e' => Return (Dyn (fun x => termDenote (e' x)))
|
adamc@191
|
79
|
adamc@191
|
80 | Unit => Return (Dyn tt)
|
adamc@191
|
81 end.
|
adamc@192
|
82 (* end thide *)
|
adamc@191
|
83
|
adamc@191
|
84 Definition TermDenote (E : Term) := termDenote (E _).
|
adamc@191
|
85
|
adamc@191
|
86 Eval compute in TermDenote ident.
|
adamc@191
|
87 Eval compute in TermDenote unite.
|
adamc@191
|
88 Eval compute in TermDenote ident_self.
|
adamc@191
|
89 Eval compute in TermDenote ident_unit.
|
adamc@191
|
90
|
adamc@191
|
91 Theorem eval_ident_unit : eval (TermDenote ident_unit) (Dyn tt).
|
adamc@192
|
92 (* begin thide *)
|
adamc@191
|
93 compute.
|
adamc@191
|
94 repeat econstructor.
|
adamc@191
|
95 simpl.
|
adamc@191
|
96 constructor.
|
adamc@191
|
97 Qed.
|
adamc@192
|
98 (* end thide *)
|
adamc@191
|
99
|
adamc@191
|
100 Theorem invert_ident : forall (E : Term) d,
|
adamc@191
|
101 eval (TermDenote (fun _ => ident _ @ E _)) d
|
adamc@191
|
102 -> eval (TermDenote E) d.
|
adamc@192
|
103 (* begin thide *)
|
adamc@191
|
104 inversion 1.
|
adamc@191
|
105
|
adamc@191
|
106 crush.
|
adamc@191
|
107
|
adamc@191
|
108 Focus 3.
|
adamc@191
|
109 crush.
|
adamc@191
|
110 unfold TermDenote in H0.
|
adamc@191
|
111 simpl in H0.
|
adamc@191
|
112 (** [injection H0.] *)
|
adamc@191
|
113 Abort.
|
adamc@192
|
114 (* end thide *)
|
adamc@191
|
115
|
adamc@191
|
116 End impredicative.
|
adamc@191
|
117
|
adamc@190
|
118
|
adamc@190
|
119 Module predicative.
|
adamc@190
|
120
|
adamc@190
|
121 Inductive val : Type :=
|
adamc@190
|
122 | Func : nat -> val
|
adamc@190
|
123 | VUnit.
|
adamc@190
|
124
|
adamc@190
|
125 Inductive computation : Type :=
|
adamc@190
|
126 | Return : val -> computation
|
adamc@190
|
127 | Bind : computation -> (val -> computation) -> computation
|
adamc@190
|
128 | CAbs : (val -> computation) -> computation
|
adamc@190
|
129 | CApp : val -> val -> computation.
|
adamc@190
|
130
|
adamc@190
|
131 Definition func := val -> computation.
|
adamc@190
|
132
|
adamc@190
|
133 Fixpoint get (n : nat) (ls : list func) {struct ls} : option func :=
|
adamc@190
|
134 match ls with
|
adamc@190
|
135 | nil => None
|
adamc@190
|
136 | x :: ls' =>
|
adamc@190
|
137 if eq_nat_dec n (length ls')
|
adamc@190
|
138 then Some x
|
adamc@190
|
139 else get n ls'
|
adamc@190
|
140 end.
|
adamc@190
|
141
|
adamc@190
|
142 Inductive eval : list func -> computation -> list func -> val -> Prop :=
|
adamc@190
|
143 | EvalReturn : forall ds d,
|
adamc@190
|
144 eval ds (Return d) ds d
|
adamc@190
|
145 | EvalBind : forall ds c1 c2 ds' d1 ds'' d2,
|
adamc@190
|
146 eval ds c1 ds' d1
|
adamc@190
|
147 -> eval ds' (c2 d1) ds'' d2
|
adamc@190
|
148 -> eval ds (Bind c1 c2) ds'' d2
|
adamc@190
|
149 | EvalCAbs : forall ds f,
|
adamc@190
|
150 eval ds (CAbs f) (f :: ds) (Func (length ds))
|
adamc@190
|
151 | EvalCApp : forall ds i d2 f ds' d3,
|
adamc@190
|
152 get i ds = Some f
|
adamc@190
|
153 -> eval ds (f d2) ds' d3
|
adamc@190
|
154 -> eval ds (CApp (Func i) d2) ds' d3.
|
adamc@190
|
155
|
adamc@192
|
156 (* begin thide *)
|
adamc@190
|
157 Fixpoint termDenote (e : term val) : computation :=
|
adamc@190
|
158 match e with
|
adamc@190
|
159 | Var v => Return v
|
adamc@190
|
160 | App e1 e2 => Bind (termDenote e1) (fun f =>
|
adamc@190
|
161 Bind (termDenote e2) (fun x =>
|
adamc@190
|
162 CApp f x))
|
adamc@190
|
163 | Abs e' => CAbs (fun x => termDenote (e' x))
|
adamc@190
|
164
|
adamc@190
|
165 | Unit => Return VUnit
|
adamc@190
|
166 end.
|
adamc@192
|
167 (* end thide *)
|
adamc@190
|
168
|
adamc@190
|
169 Definition TermDenote (E : Term) := termDenote (E _).
|
adamc@190
|
170
|
adamc@190
|
171 Eval compute in TermDenote ident.
|
adamc@190
|
172 Eval compute in TermDenote unite.
|
adamc@190
|
173 Eval compute in TermDenote ident_self.
|
adamc@190
|
174 Eval compute in TermDenote ident_unit.
|
adamc@190
|
175
|
adamc@190
|
176 Theorem eval_ident_unit : exists ds, eval nil (TermDenote ident_unit) ds VUnit.
|
adamc@192
|
177 (* begin thide *)
|
adamc@190
|
178 compute.
|
adamc@190
|
179 repeat econstructor.
|
adamc@190
|
180 simpl.
|
adamc@190
|
181 rewrite (eta Return).
|
adamc@190
|
182 reflexivity.
|
adamc@190
|
183 Qed.
|
adamc@190
|
184
|
adamc@190
|
185 Hint Constructors eval.
|
adamc@190
|
186
|
adamc@190
|
187 Lemma app_nil_start : forall A (ls : list A),
|
adamc@190
|
188 ls = nil ++ ls.
|
adamc@190
|
189 reflexivity.
|
adamc@190
|
190 Qed.
|
adamc@190
|
191
|
adamc@190
|
192 Lemma app_cons : forall A (x : A) (ls : list A),
|
adamc@190
|
193 x :: ls = (x :: nil) ++ ls.
|
adamc@190
|
194 reflexivity.
|
adamc@190
|
195 Qed.
|
adamc@190
|
196
|
adamc@190
|
197 Theorem eval_monotone : forall ds c ds' d,
|
adamc@190
|
198 eval ds c ds' d
|
adamc@190
|
199 -> exists ds'', ds' = ds'' ++ ds.
|
adamc@190
|
200 Hint Resolve app_nil_start app_ass app_cons.
|
adamc@190
|
201
|
adamc@190
|
202 induction 1; firstorder; subst; eauto.
|
adamc@190
|
203 Qed.
|
adamc@190
|
204
|
adamc@190
|
205 Lemma length_app : forall A (ds2 ds1 : list A),
|
adamc@190
|
206 length (ds1 ++ ds2) = length ds1 + length ds2.
|
adamc@190
|
207 induction ds1; simpl; intuition.
|
adamc@190
|
208 Qed.
|
adamc@190
|
209
|
adamc@190
|
210 Lemma get_app : forall ds2 d ds1,
|
adamc@190
|
211 get (length ds2) (ds1 ++ d :: ds2) = Some d.
|
adamc@190
|
212 Hint Rewrite length_app : cpdt.
|
adamc@190
|
213
|
adamc@190
|
214 induction ds1; crush;
|
adamc@190
|
215 match goal with
|
adamc@190
|
216 | [ |- context[if ?E then _ else _] ] => destruct E
|
adamc@190
|
217 end; crush.
|
adamc@190
|
218 Qed.
|
adamc@192
|
219 (* end thide *)
|
adamc@190
|
220
|
adamc@190
|
221 Theorem invert_ident : forall (E : Term) ds ds' d,
|
adamc@190
|
222 eval ds (TermDenote (fun _ => ident _ @ E _)) ds' d
|
adamc@190
|
223 -> eval ((fun x => Return x) :: ds) (TermDenote E) ds' d.
|
adamc@192
|
224 (* begin thide *)
|
adamc@190
|
225 inversion 1; subst.
|
adamc@190
|
226 clear H.
|
adamc@190
|
227 inversion H3; clear H3; subst.
|
adamc@190
|
228 inversion H6; clear H6; subst.
|
adamc@190
|
229 generalize (eval_monotone H2); crush.
|
adamc@190
|
230 inversion H5; clear H5; subst.
|
adamc@190
|
231 rewrite get_app in H3.
|
adamc@190
|
232 inversion H3; clear H3; subst.
|
adamc@190
|
233 inversion H7; clear H7; subst.
|
adamc@190
|
234 assumption.
|
adamc@190
|
235 Qed.
|
adamc@192
|
236 (* end thide *)
|
adamc@190
|
237
|
adamc@190
|
238 End predicative.
|