Certified Programming with Dependent Types: src/ProgLang.v comparison

comparison src/ProgLang.v @ 414:73f8165a3c1d

Typesetting pass over ProgLang

author	Adam Chlipala <adam@chlipala.net>
date	Fri, 08 Jun 2012 15:54:36 -0400
parents	05efde66559d
children	92f386c33e94

comparison

equal deleted inserted replaced

-:6f0f80ffd5b6
+:73f8165a3c1d
 termDenote (ident e) s = termDenote e s.
 induction e; t.
 Qed.
 (** A slightly more ambitious transformation belongs to the family of _constant folding_ optimizations we have used as examples in other chapters. *)
-Axiom admit : forall T, T.
 Fixpoint cfold G t (e : term G t) : term G t :=
 match e with
 | Plus G e1 e2 =>
 let e1' := cfold e1 in
 Theorem cfoldSound : forall G t (e : term G t) s,
 termDenote (cfold e) s = termDenote e s.
 induction e; t;
 repeat (match goal with
-| [ |- context[match ?E with
+| [ |- context[match ?E with Var _ _ _ => _ | _ => _ end] ] =>
-| Var _ _ _ => _ | Const _ _ => _ | Plus _ _ _ => _
+dep_destruct E
-| Abs _ _ _ _ => _ | App _ _ _ _ _ => _
-| Let _ _ _ _ _ => _
-end] ] => dep_destruct E
 end; t).
 Qed.
-(** The transformations we have tried so far have been straightforward because they do not have interesting effects on the variable binding structure of terms.  The dependent de Bruijn representation is called %\index{first-order syntax}%_first-order_ because it encodes variable identity explicitly; all such representations incur bookkeeping overheads in transformations that rearrange binding structure.
+(** The transformations we have tried so far have been straightforward because they do not have interesting effects on the variable binding structure of terms.  The dependent de Bruijn representation is called%\index{first-order syntax}% _first-order_ because it encodes variable identity explicitly; all such representations incur bookkeeping overheads in transformations that rearrange binding structure.
 As an example of a tricky transformation, consider one that removes all uses of %``%#"#[let x = e1 in e2]#"#%''% by substituting [e1] for [x] in [e2].  We will implement the translation by pairing the %``%#"#compile-time#"#%''% typing environment with a %``%#"#run-time#"#%''% value environment or _substitution_, mapping each variable to a value to be substituted for it.  Such a substitute term may be placed within a program in a position with a larger typing environment than applied at the point where the substitute term was chosen.  To support such context transplantation, we need _lifting_, a standard de Bruijn indices operation.  With dependent typing, lifting corresponds to weakening for typing judgments.
 The fundamental goal of lifting is to add a new variable to a typing context, maintaining the validity of a term in the expanded context.  To express the operation of adding a type to a context, we use a helper function [insertAt]. *)
 (** The [Let] removal optimization is a good case study of a simple transformation that may turn out to be much more work than expected, based on representation choices.  In the second part of this chapter, we consider an alternate choice that produces a more pleasant experience. *)
 (** * Parametric Higher-Order Abstract Syntax *)
-(** In contrast to first-order encodings, %\index{higher-order syntax}%_higher-order_ encodings avoid explicit modeling of variable identity.  Instead, the binding constructs of an %\index{object language}%_object language_ (the language being formalized) can be represented using the binding constructs of the %\index{meta language}%_meta language_ (the language in which the formalization is done).  The best known higher-order encoding is called %\index{higher-order abstract syntax}\index{HOAS}%_higher-order abstract syntax (HOAS)_ %\cite{HOAS}%, and we can start by attempting to apply it directly in Coq. *)
+(** In contrast to first-order encodings,%\index{higher-order syntax}% _higher-order_ encodings avoid explicit modeling of variable identity.  Instead, the binding constructs of an%\index{object language}% _object language_ (the language being formalized) can be represented using the binding constructs of the%\index{meta language}% _meta language_ (the language in which the formalization is done).  The best known higher-order encoding is called%\index{higher-order abstract syntax}\index{HOAS}% _higher-order abstract syntax_ (HOAS) %\cite{HOAS}%, and we can start by attempting to apply it directly in Coq. *)
 Module HigherOrder.
 (** With HOAS, each object language binding construct is represented with a _function_ of the meta language.  Here is what we get if we apply that idea within an inductive definition of term syntax. *)
 | Let : forall t1 t2, term t1 -> (term t1 -> term t2) -> term t2.
 ]]
 However, Coq rejects this definition for failing to meet the %\index{strict positivity restriction}%strict positivity restriction.  For instance, the constructor [Abs] takes an argument that is a function over the same type family [term] that we are defining.  Inductive definitions of this kind can be used to write non-terminating Gallina programs, which breaks the consistency of Coq's logic.
-An alternate higher-order encoding is %\index{parametric higher-order abstract syntax}\index{PHOAS}%_parametric HOAS_, as introduced by Washburn and Weirich%~\cite{BGB}% for Haskell and tweaked by me%~\cite{PhoasICFP08}% for use in Coq.  Here the idea is to parametrize the syntax type by a type family standing for a _representation of variables_. *)
+An alternate higher-order encoding is%\index{parametric higher-order abstract syntax}\index{PHOAS}% _parametric HOAS_, as introduced by Washburn and Weirich%~\cite{BGB}% for Haskell and tweaked by me%~\cite{PhoasICFP08}% for use in Coq.  Here the idea is to parametrize the syntax type by a type family standing for a _representation of variables_. *)
 Section var.
 Variable var : type -> Type.
 Inductive term : type -> Type :=
 Lemma cfoldSound : forall t (e : term typeDenote t),
 termDenote (cfold e) = termDenote e.
 induction e; t;
 repeat (match goal with
-| [ |- context[match ?E with
+| [ |- context[match ?E with Var _ _ => _ | _ => _ end] ] =>
-| Var _ _ => _ | Const _ => _ | Plus _ _ => _
+dep_destruct E
-| Abs _ _ _ => _ | App _ _ _ _ => _
-| Let _ _ _ _ => _
-end] ] => dep_destruct E
 end; t).
 Qed.
 Theorem CfoldSound : forall t (E : Term t),
 TermDenote (Cfold E) = TermDenote E.
 Have we really avoided first-order reasoning about the output terms of translations?  The answer depends on some subtle issues, which deserve a subsection of their own. *)
 (** ** Establishing Term Well-Formedness *)
-(** Can there be values of type [Term t] that are not well-formed according to [Wf]?  We expect that Gallina satisfies key %\index{parametricity}%_parametricity_ %\cite{parametricity}% properties, which indicate how polymorphic types may only be inhabited by specific values.  We omit details of parametricity theorems here, but [forall t (E : Term t), Wf E] follows the flavor of such theorems.  One option would be to assert that fact as an axiom, %``%#"#proving#"#%''% that any output of any of our translations is well-formed.  We could even prove the soundness of the theorem on paper meta-theoretically, say by considering some particular model of CIC.
+(** Can there be values of type [Term t] that are not well-formed according to [Wf]?  We expect that Gallina satisfies key%\index{parametricity}% _parametricity_ %\cite{parametricity}% properties, which indicate how polymorphic types may only be inhabited by specific values.  We omit details of parametricity theorems here, but [forall t (E : Term t), Wf E] follows the flavor of such theorems.  One option would be to assert that fact as an axiom, %``%#"#proving#"#%''% that any output of any of our translations is well-formed.  We could even prove the soundness of the theorem on paper meta-theoretically, say by considering some particular model of CIC.
 To be more cautious, we could prove [Wf] for every term that interests us, threading such proofs through all transformations.  Here is an example exercise of that kind, for [Unlet].
 First, we prove that [wf] is _monotone_, in that a given instance continues to hold as we add new variable pairs to the variable isomorphism. *)

Mercurial > cpdt > repo

comparison src/ProgLang.v @ 414:73f8165a3c1d