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

comparison src/ProgLang.v @ 497:6252dd4540a9

Small fixes in ProgLang

author	Adam Chlipala <adam@chlipala.net>
date	Thu, 31 Jan 2013 11:22:53 -0500
parents	4320c1a967c2
children	fd6ec9b2dccb

comparison

equal deleted inserted replaced

-:07f2fb4d9b36
+:6252dd4540a9
 I apologize in advance to those readers not familiar with the theory of programming language semantics.  I will make a few remarks intended to relate the material here with common ideas in semantics, but these remarks should be safe for others to skip.
 We will define a small programming language and reason about its semantics, expressed as an interpreter into Coq terms, much as we have done in examples throughout the book.  It will be helpful to build a slight extension of [crush] that tries to apply %\index{functional extensionality}%functional extensionality, an axiom we met in Chapter 12, which says that two functions are equal if they map equal inputs to equal outputs. *)
 Ltac ext := let x := fresh "x" in extensionality x.
-Ltac t := crush; repeat (ext || f_equal; crush).
+Ltac pl := crush; repeat (ext || f_equal; crush).
 (** At this point in the book source, some auxiliary proofs also appear. *)
 (* begin hide *)
 Section hmap.
 | Let _ _ _ e1 e2 => Let (ident e1) (ident e2)
 end.
 Theorem identSound : forall G t (e : term G t) s,
 termDenote (ident e) s = termDenote e s.
-induction e; t.
+induction e; pl.
 Qed.
 (** A slightly more ambitious transformation belongs to the family of _constant folding_ optimizations we have used as examples in other chapters. *)
 Fixpoint cfold G t (e : term G t) : term G t :=
 (** The correctness proof is more complex, but only slightly so. *)
 Theorem cfoldSound : forall G t (e : term G t) s,
 termDenote (cfold e) s = termDenote e s.
-induction e; t;
+induction e; pl;
 repeat (match goal with
 | [ |- context[match ?E with Var _ _ _ => _ | _ => _ end] ] =>
 dep_destruct E
-end; t).
+end; pl).
 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.
 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.
 (** Next we prove that [liftVar] is correct.  That is, a lifted variable retains its value with respect to a substitution when we perform an analogue to lifting by inserting a new mapping into the substitution. *)
 Lemma liftVarSound : forall t' (x : typeDenote t') t G (m : member t G) s n,
 hget s m = hget (insertAtS x n s) (liftVar m t' n).
-induction m; destruct n; dep_destruct s; t.
+induction m; destruct n; dep_destruct s; pl.
 Qed.
 Hint Resolve liftVarSound.
 (** An analogous lemma establishes correctness of [lift']. *)
 Lemma lift'Sound : forall G t' (x : typeDenote t') t (e : term G t) n s,
 termDenote e s = termDenote (lift' t' n e) (insertAtS x n s).
-induction e; t;
+induction e; pl;
 repeat match goal with
 | [ IH : forall n s, _ = termDenote (lift' _ n ?E) _
 |- context[lift' _ (S ?N) ?E] ] => specialize (IH (S N))
-end; t.
+end; pl.
 Qed.
 (** Correctness of [lift] itself is an easy corollary. *)
 Lemma liftSound : forall G t' (x : typeDenote t') t (e : term G t) s,
 (** Finally, we can prove correctness of [unletSound] for terms in arbitrary typing environments. *)
 Lemma unletSound' : forall G t (e : term G t) G' (s : hlist (term G') G) s1,
 termDenote (unlet e s) s1
 = termDenote e (hmap (fun t' (e' : term G' t') => termDenote e' s1) s).
-induction e; t.
+induction e; pl.
 Qed.
 (** The lemma statement is a mouthful, with all its details of typing contexts and substitutions.  It is usually prudent to state a final theorem in as simple a way as possible, to help your readers believe that you have proved what they expect.  We do that here for the simple case of terms with empty typing contexts. *)
 Theorem unletSound : forall t (e : term nil t),
 (** %\vspace{-.15in}%[[
 = "(((fun x => (fun x' => (x + x'))) N) N)"
 ]]
 *)
-(** However, it is not necessary to convert to first-order form to support many common operations on terms.  For instance, we can implement substitution of one term in another.  The key insight here is to _tag variables with terms_, so that, on encountering a variable, we can simply replace it by the term in its tag.  We will call this function initially on a term with exactly one free variable, tagged with the appropriate substitute.  During recursion, new variables are added, but they are only tagged with their own term equivalents.  Note that this function [squash] is parameterized over a specific [var] choice. *)
+(** However, it is not necessary to convert to first-order form to support many common operations on terms.  For instance, we can implement substitution of terms for variables.  The key insight here is to _tag variables with terms_, so that, on encountering a variable, we can simply replace it by the term in its tag.  We will call this function initially on a term with exactly one free variable, tagged with the appropriate substitute.  During recursion, new variables are added, but they are only tagged with their own term equivalents.  Note that this function [squash] is parameterized over a specific [var] choice. *)
 Fixpoint squash var t (e : term (term var) t) : term var t :=
 match e with
 | Var _ e1 => e1
 (** Proving correctness is both easier and harder than in the last section, easier because we do not need to manipulate substitutions, and harder because we do the induction in an extra lemma about [ident], to establish the correctness theorem for [Ident]. *)
 Lemma identSound : forall t (e : term typeDenote t),
 termDenote (ident e) = termDenote e.
-induction e; t.
+induction e; pl.
 Qed.
 Theorem IdentSound : forall t (E : Term t),
 TermDenote (Ident E) = TermDenote E.
 intros; apply identSound.
 Definition Cfold t (E : Term t) : Term t := fun var =>
 cfold (E var).
 Lemma cfoldSound : forall t (e : term typeDenote t),
 termDenote (cfold e) = termDenote e.
-induction e; t;
+induction e; pl;
 repeat (match goal with
 | [ |- context[match ?E with Var _ _ => _ | _ => _ end] ] =>
 dep_destruct E
-end; t).
+end; pl).
 Qed.
 Theorem CfoldSound : forall t (E : Term t),
 TermDenote (Cfold E) = TermDenote E.
 intros; apply cfoldSound.
 red; intros; repeat match goal with
 | [ |- wf _ _ _ ] => constructor; intros
 end; intuition.
 Qed.
-(** Now we are ready to give a nice simple proof of correctness for [unlet].  First, we add one hint to apply a standard library theorem connecting [Forall], a higher-order predicate asserting that every element of a list satisfies some property; and [In], the list membership predicate. *)
+(** Now we are ready to give a nice simple proof of correctness for [unlet].  First, we add one hint to apply a small variant of a standard library theorem connecting [Forall], a higher-order predicate asserting that every element of a list satisfies some property; and [In], the list membership predicate. *)
 Hint Extern 1 => match goal with
 | [ H1 : Forall _ _, H2 : In _ _ |- _ ] => apply (Forall_In H1 _ H2)
 end.
 Lemma unletSound : forall G t (e1 : term _ t) e2,
 wf G e1 e2
 -> Forall (fun ve => termDenote (First ve) = Second ve) G
 -> termDenote (unlet e1) = termDenote e2.
-induction 1; t.
+induction 1; pl.
 Qed.
 Theorem UnletSound : forall t (E : Term t), Wf E
 -> TermDenote (Unlet E) = TermDenote E.
 intros; eapply unletSound; eauto.
 Lemma wf_monotone : forall var1 var2 G t (e1 : term var1 t) (e2 : term var2 t),
 wf G e1 e2
 -> forall G', Forall (fun x => In x G') G
 -> wf G' e1 e2.
-induction 1; t; auto 6.
+induction 1; pl; auto 6.
 Qed.
 Hint Resolve wf_monotone Forall_In'.
 (** Now we are ready to prove that [unlet] preserves any [wf] instance.  The key invariant has to do with the parallel execution of [unlet] on two different [var] instantiations of a particular term.  Since [unlet] uses [term] as the type of variable data, our variable isomorphism context [G] contains pairs of terms, which, conveniently enough, allows us to state the invariant that any pair of terms in the context is also related by [wf]. *)
 Lemma unletWf : forall var1 var2 G t (e1 : term (term var1) t) (e2 : term (term var2) t),
 wf G e1 e2
 -> forall G', Forall (fun ve => wf G' (First ve) (Second ve)) G
 -> wf G' (unlet e1) (unlet e2).
-induction 1; t; eauto 9.
+induction 1; pl; eauto 9.
 Qed.
 (** Repackaging [unletWf] into a theorem about [Wf] and [Unlet] is straightforward. *)
 Theorem UnletWf : forall t (E : Term t), Wf E

Mercurial > cpdt > repo

comparison src/ProgLang.v @ 497:6252dd4540a9