Mercurial > cpdt > repo

comparison src/Extensional.v @ 181:ec44782bffdd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Extensional exercise
author Adam Chlipala <adamc@hcoop.net>
date Mon, 10 Nov 2008 17:27:55 -0500
parents de33d1ed7c63
children 24b99e025fe8
comparison
equal deleted inserted replaced
180:de33d1ed7c63 181:ec44782bffdd
14 14
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16 (* end hide *) 16 (* end hide *)
17 17
18 18
19 (** %\chapter{Certifying Extensional Transformations}% *) 19 (** %\chapter{Extensional Transformations}% *)
20 20
21 (** TODO: Prose for this chapter *) 21 (** TODO: Prose for this chapter *)
22 22
23 23
24 (** * Simply-Typed Lambda Calculus *) 24 (** * Simply-Typed Lambda Calculus *)
106 (* begin thide *) 106 (* begin thide *)
107 Section exp_equiv. 107 Section exp_equiv.
108 Variables var1 var2 : type -> Type. 108 Variables var1 var2 : type -> Type.
109 109
110 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type -> forall t, exp var1 t -> exp var2 t -> Prop := 110 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type -> forall t, exp var1 t -> exp var2 t -> Prop :=
111 | EqEVar : forall G t (v1 : var1 t) v2, 111 | EqVar : forall G t (v1 : var1 t) v2,
112 In (existT _ t (v1, v2)) G 112 In (existT _ t (v1, v2)) G
113 -> exp_equiv G (#v1) (#v2) 113 -> exp_equiv G (#v1) (#v2)
114 114
115 | EqEConst : forall G n, 115 | EqConst : forall G n,
116 exp_equiv G (^n) (^n) 116 exp_equiv G (^n) (^n)
117 | EqEPlus : forall G x1 y1 x2 y2, 117 | EqPlus : forall G x1 y1 x2 y2,
118 exp_equiv G x1 x2 118 exp_equiv G x1 x2
119 -> exp_equiv G y1 y2 119 -> exp_equiv G y1 y2
120 -> exp_equiv G (x1 +^ y1) (x2 +^ y2) 120 -> exp_equiv G (x1 +^ y1) (x2 +^ y2)
121 121
122 | EqEApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2, 122 | EqApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2,
123 exp_equiv G f1 f2 123 exp_equiv G f1 f2
124 -> exp_equiv G x1 x2 124 -> exp_equiv G x1 x2
125 -> exp_equiv G (f1 @ x1) (f2 @ x2) 125 -> exp_equiv G (f1 @ x1) (f2 @ x2)
126 | EqEAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2, 126 | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2,
127 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2)) 127 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2))
128 -> exp_equiv G (Abs f1) (Abs f2). 128 -> exp_equiv G (Abs f1) (Abs f2).
129 End exp_equiv. 129 End exp_equiv.
130 130
131 Axiom Exp_equiv : forall t (E : Exp t) var1 var2, 131 Axiom Exp_equiv : forall t (E : Exp t) var1 var2,
1001 unfold Elab.ExpDenote, Elaborate, Source.ExpDenote; 1001 unfold Elab.ExpDenote, Elaborate, Source.ExpDenote;
1002 intros; apply elaborate_correct. 1002 intros; apply elaborate_correct.
1003 Qed. 1003 Qed.
1004 1004
1005 End PatMatch. 1005 End PatMatch.
1006
1007
1008 (** * Exercises *)
1009
1010 (** %\begin{enumerate}%#<ol>#
1011
1012 %\item%#<li># When in the last chapter we implemented constant folding for simply-typed lambda calculus, it may have seemed natural to try applying beta reductions. This would have been a lot more trouble than is apparent at first, because we would have needed to convince Coq that our normalizing function always terminated.
1013
1014 It might also seem that beta reduction is a lost cause because we have no effective way of substituting in the [exp] type; we only managed to write a substitution function for the parametric [Exp] type. This is not as big of a problem as it seems. For instance, for the language we built by extending simply-typed lambda calculus with products and sums, it also appears that we need substitution for simplifying [case] expressions whose discriminees are known to be [inl] or [inr], but the function is still implementable.
1015
1016 For this exercise, extend the products and sums constant folder from the last chapter so that it simplifies [case] expressions as well, by checking if the discriminee is a known [inl] or known [inr]. Also extend the correctness theorem to apply to your new definition. You will probably want to assert an axiom relating to an expression equivalence relation like the one defined in this chapter.
1017 #</li>#
1018
1019 #</ol>#%\end{enumerate}% *)