Mercurial > cpdt > repo

comparison src/Intensional.v @ 257:108ec446fbaf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Easy direction of Intensional
author Adam Chlipala <adamc@hcoop.net>
date Wed, 16 Dec 2009 15:54:50 -0500
parents 2a34c4dc6a10
children 4c9031b62cd0
comparison
equal deleted inserted replaced
256:4293dd6912cd 257:108ec446fbaf
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *) 8 *)
9 9
10 (* begin hide *)
11 Require Import List.
12
13 Require Import Axioms DepList Tactics.
14
15 Set Implicit Arguments.
16 (* end hide *)
17
10 18
11 (** %\chapter{Intensional Transformations}% *) 19 (** %\chapter{Intensional Transformations}% *)
12 20
13 (** TODO: This chapter! (Old version was too complicated) *) 21 (* begin hide *)
22
23 Inductive type : Type :=
24 | Nat : type
25 | Arrow : type -> type -> type.
26
27 Infix "-->" := Arrow (right associativity, at level 60).
28
29 Fixpoint typeDenote (t : type) : Set :=
30 match t with
31 | Nat => nat
32 | t1 --> t2 => typeDenote t1 -> typeDenote t2
33 end.
34
35 Module Phoas.
36 Section vars.
37 Variable var : type -> Type.
38
39 Inductive exp : type -> Type :=
40 | Var : forall t,
41 var t
42 -> exp t
43
44 | Const : nat -> exp Nat
45 | Plus : exp Nat -> exp Nat -> exp Nat
46
47 | App : forall t1 t2,
48 exp (t1 --> t2)
49 -> exp t1
50 -> exp t2
51 | Abs : forall t1 t2,
52 (var t1 -> exp t2)
53 -> exp (t1 --> t2).
54 End vars.
55
56 Definition Exp t := forall var, exp var t.
57
58 Implicit Arguments Var [var t].
59 Implicit Arguments Const [var].
60 Implicit Arguments Plus [var].
61 Implicit Arguments App [var t1 t2].
62 Implicit Arguments Abs [var t1 t2].
63
64 Notation "# v" := (Var v) (at level 70).
65
66 Notation "^ n" := (Const n) (at level 70).
67 Infix "+^" := Plus (left associativity, at level 79).
68
69 Infix "@" := App (left associativity, at level 77).
70 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
71 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
72
73 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
74 match e with
75 | Var _ v => v
76
77 | Const n => n
78 | Plus e1 e2 => expDenote e1 + expDenote e2
79
80 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
81 | Abs _ _ e' => fun x => expDenote (e' x)
82 end.
83
84 Definition ExpDenote t (e : Exp t) := expDenote (e _).
85
86 Section exp_equiv.
87 Variables var1 var2 : type -> Type.
88
89 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type
90 -> forall t, exp var1 t -> exp var2 t -> Prop :=
91 | EqVar : forall G t (v1 : var1 t) v2,
92 In (existT _ t (v1, v2)) G
93 -> exp_equiv G (#v1) (#v2)
94
95 | EqConst : forall G n,
96 exp_equiv G (^n) (^n)
97 | EqPlus : forall G x1 y1 x2 y2,
98 exp_equiv G x1 x2
99 -> exp_equiv G y1 y2
100 -> exp_equiv G (x1 +^ y1) (x2 +^ y2)
101
102 | EqApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2,
103 exp_equiv G f1 f2
104 -> exp_equiv G x1 x2
105 -> exp_equiv G (f1 @ x1) (f2 @ x2)
106 | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2,
107 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2))
108 -> exp_equiv G (Abs f1) (Abs f2).
109 End exp_equiv.
110 End Phoas.
111 (* end hide *)
112
113 Module DeBruijn.
114 Inductive exp : list type -> type -> Type :=
115 | Var : forall G t,
116 member t G
117 -> exp G t
118
119 | Const : forall G, nat -> exp G Nat
120 | Plus : forall G, exp G Nat -> exp G Nat -> exp G Nat
121
122 | App : forall G t1 t2,
123 exp G (t1 --> t2)
124 -> exp G t1
125 -> exp G t2
126 | Abs : forall G t1 t2,
127 exp (t1 :: G) t2
128 -> exp G (t1 --> t2).
129
130 Implicit Arguments Const [G].
131
132 Fixpoint expDenote G t (e : exp G t) : hlist typeDenote G -> typeDenote t :=
133 match e with
134 | Var _ _ v => fun s => hget s v
135
136 | Const _ n => fun _ => n
137 | Plus _ e1 e2 => fun s => expDenote e1 s + expDenote e2 s
138
139 | App _ _ _ e1 e2 => fun s => (expDenote e1 s) (expDenote e2 s)
140 | Abs _ _ _ e' => fun s x => expDenote e' (x ::: s)
141 end.
142 End DeBruijn.
143
144 Import Phoas DeBruijn.
145
146
147 (** * From De Bruijn to PHOAS *)
148
149 Section phoasify.
150 Variable var : type -> Type.
151
152 Fixpoint phoasify G t (e : DeBruijn.exp G t) : hlist var G -> Phoas.exp var t :=
153 match e with
154 | Var _ _ v => fun s => #(hget s v)
155
156 | Const _ n => fun _ => ^n
157 | Plus _ e1 e2 => fun s => phoasify e1 s +^ phoasify e2 s
158
159 | App _ _ _ e1 e2 => fun s => phoasify e1 s @ phoasify e2 s
160 | Abs _ _ _ e' => fun s => \x, phoasify e' (x ::: s)
161 end.
162 End phoasify.
163
164 Definition Phoasify t (e : DeBruijn.exp nil t) : Phoas.Exp t :=
165 fun _ => phoasify e HNil.
166
167 Theorem phoasify_sound : forall G t (e : DeBruijn.exp G t) s,
168 Phoas.expDenote (phoasify e s) = DeBruijn.expDenote e s.
169 induction e; crush; ext_eq; crush.
170 Qed.
171
172 Section vars.
173 Variables var1 var2 : type -> Type.
174
175 Fixpoint zip G (s1 : hlist var1 G) : hlist var2 G -> list {t : type & var1 t * var2 t}%type :=
176 match s1 with
177 | HNil => fun _ => nil
178 | HCons _ _ v1 s1' => fun s2 => existT _ _ (v1, hhd s2) :: zip s1' (htl s2)
179 end.
180
181 Lemma In_zip : forall t G (s1 : hlist _ G) s2 (m : member t G),
182 In (existT _ t (hget s1 m, hget s2 m)) (zip s1 s2).
183 induction s1; intro s2; dep_destruct s2; intro m; dep_destruct m; crush.
184 Qed.
185
186 Lemma unsimpl_zip : forall t (v1 : var1 t) (v2 : var2 t)
187 G (s1 : hlist _ G) s2 t' (e1 : Phoas.exp _ t') e2,
188 exp_equiv (zip (v1 ::: s1) (v2 ::: s2)) e1 e2
189 -> exp_equiv (existT _ _ (v1, v2) :: zip s1 s2) e1 e2.
190 trivial.
191 Qed.
192
193 Hint Resolve In_zip unsimpl_zip.
194
195 Theorem phoasify_wf : forall G t (e : DeBruijn.exp G t) s1 s2,
196 exp_equiv (zip s1 s2) (phoasify e s1) (phoasify e s2).
197 Hint Constructors exp_equiv.
198
199 induction e; crush.
200 Qed.
201 End vars.
202
203
204 (** * From PHOAS to De Bruijn *)