Mercurial > cpdt > repo

comparison src/Impure.v @ 192:32ce9b28d7e7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Templatize Impure
author Adam Chlipala <adamc@hcoop.net>
date Tue, 18 Nov 2008 13:09:09 -0500
parents cf5ddf078858
children cbf2f74a5130
comparison
equal deleted inserted replaced
191:cf5ddf078858 192:32ce9b28d7e7
65 | EvalBind : forall T1 T2 (c1 : computation T1) (c2 : T1 -> computation T2) v1 v2, 65 | EvalBind : forall T1 T2 (c1 : computation T1) (c2 : T1 -> computation T2) v1 v2,
66 eval c1 v1 66 eval c1 v1
67 -> eval (c2 v1) v2 67 -> eval (c2 v1) v2
68 -> eval (Bind c1 c2) v2. 68 -> eval (Bind c1 c2) v2.
69 69
70 (* begin thide *)
70 Fixpoint termDenote (e : term dynamic) : computation dynamic := 71 Fixpoint termDenote (e : term dynamic) : computation dynamic :=
71 match e with 72 match e with
72 | Var v => Return v 73 | Var v => Return v
73 | App e1 e2 => Bind (termDenote e1) (fun f => 74 | App e1 e2 => Bind (termDenote e1) (fun f =>
74 Bind (termDenote e2) (fun x => 75 Bind (termDenote e2) (fun x =>
76 f' x))) 77 f' x)))
77 | Abs e' => Return (Dyn (fun x => termDenote (e' x))) 78 | Abs e' => Return (Dyn (fun x => termDenote (e' x)))
78 79
79 | Unit => Return (Dyn tt) 80 | Unit => Return (Dyn tt)
80 end. 81 end.
82 (* end thide *)
81 83
82 Definition TermDenote (E : Term) := termDenote (E _). 84 Definition TermDenote (E : Term) := termDenote (E _).
83 85
84 Eval compute in TermDenote ident. 86 Eval compute in TermDenote ident.
85 Eval compute in TermDenote unite. 87 Eval compute in TermDenote unite.
86 Eval compute in TermDenote ident_self. 88 Eval compute in TermDenote ident_self.
87 Eval compute in TermDenote ident_unit. 89 Eval compute in TermDenote ident_unit.
88 90
89 Theorem eval_ident_unit : eval (TermDenote ident_unit) (Dyn tt). 91 Theorem eval_ident_unit : eval (TermDenote ident_unit) (Dyn tt).
92 (* begin thide *)
90 compute. 93 compute.
91 repeat econstructor. 94 repeat econstructor.
92 simpl. 95 simpl.
93 constructor. 96 constructor.
94 Qed. 97 Qed.
98 (* end thide *)
95 99
96 Theorem invert_ident : forall (E : Term) d, 100 Theorem invert_ident : forall (E : Term) d,
97 eval (TermDenote (fun _ => ident _ @ E _)) d 101 eval (TermDenote (fun _ => ident _ @ E _)) d
98 -> eval (TermDenote E) d. 102 -> eval (TermDenote E) d.
103 (* begin thide *)
99 inversion 1. 104 inversion 1.
100 105
101 crush. 106 crush.
102 107
103 Focus 3. 108 Focus 3.
104 crush. 109 crush.
105 unfold TermDenote in H0. 110 unfold TermDenote in H0.
106 simpl in H0. 111 simpl in H0.
107 (** [injection H0.] *) 112 (** [injection H0.] *)
108 Abort. 113 Abort.
114 (* end thide *)
109 115
110 End impredicative. 116 End impredicative.
111 117
112 118
113 Module predicative. 119 Module predicative.
145 | EvalCApp : forall ds i d2 f ds' d3, 151 | EvalCApp : forall ds i d2 f ds' d3,
146 get i ds = Some f 152 get i ds = Some f
147 -> eval ds (f d2) ds' d3 153 -> eval ds (f d2) ds' d3
148 -> eval ds (CApp (Func i) d2) ds' d3. 154 -> eval ds (CApp (Func i) d2) ds' d3.
149 155
156 (* begin thide *)
150 Fixpoint termDenote (e : term val) : computation := 157 Fixpoint termDenote (e : term val) : computation :=
151 match e with 158 match e with
152 | Var v => Return v 159 | Var v => Return v
153 | App e1 e2 => Bind (termDenote e1) (fun f => 160 | App e1 e2 => Bind (termDenote e1) (fun f =>
154 Bind (termDenote e2) (fun x => 161 Bind (termDenote e2) (fun x =>
155 CApp f x)) 162 CApp f x))
156 | Abs e' => CAbs (fun x => termDenote (e' x)) 163 | Abs e' => CAbs (fun x => termDenote (e' x))
157 164
158 | Unit => Return VUnit 165 | Unit => Return VUnit
159 end. 166 end.
167 (* end thide *)
160 168
161 Definition TermDenote (E : Term) := termDenote (E _). 169 Definition TermDenote (E : Term) := termDenote (E _).
162 170
163 Eval compute in TermDenote ident. 171 Eval compute in TermDenote ident.
164 Eval compute in TermDenote unite. 172 Eval compute in TermDenote unite.
165 Eval compute in TermDenote ident_self. 173 Eval compute in TermDenote ident_self.
166 Eval compute in TermDenote ident_unit. 174 Eval compute in TermDenote ident_unit.
167 175
168 Theorem eval_ident_unit : exists ds, eval nil (TermDenote ident_unit) ds VUnit. 176 Theorem eval_ident_unit : exists ds, eval nil (TermDenote ident_unit) ds VUnit.
177 (* begin thide *)
169 compute. 178 compute.
170 repeat econstructor. 179 repeat econstructor.
171 simpl. 180 simpl.
172 rewrite (eta Return). 181 rewrite (eta Return).
173 reflexivity. 182 reflexivity.
205 induction ds1; crush; 214 induction ds1; crush;
206 match goal with 215 match goal with
207 | [ |- context[if ?E then _ else _] ] => destruct E 216 | [ |- context[if ?E then _ else _] ] => destruct E
208 end; crush. 217 end; crush.
209 Qed. 218 Qed.
219 (* end thide *)
210 220
211 Theorem invert_ident : forall (E : Term) ds ds' d, 221 Theorem invert_ident : forall (E : Term) ds ds' d,
212 eval ds (TermDenote (fun _ => ident _ @ E _)) ds' d 222 eval ds (TermDenote (fun _ => ident _ @ E _)) ds' d
213 -> eval ((fun x => Return x) :: ds) (TermDenote E) ds' d. 223 -> eval ((fun x => Return x) :: ds) (TermDenote E) ds' d.
224 (* begin thide *)
214 inversion 1; subst. 225 inversion 1; subst.
215 clear H. 226 clear H.
216 inversion H3; clear H3; subst. 227 inversion H3; clear H3; subst.
217 inversion H6; clear H6; subst. 228 inversion H6; clear H6; subst.
218 generalize (eval_monotone H2); crush. 229 generalize (eval_monotone H2); crush.
220 rewrite get_app in H3. 231 rewrite get_app in H3.
221 inversion H3; clear H3; subst. 232 inversion H3; clear H3; subst.
222 inversion H7; clear H7; subst. 233 inversion H7; clear H7; subst.
223 assumption. 234 assumption.
224 Qed. 235 Qed.
236 (* end thide *)
225 237
226 End predicative. 238 End predicative.