adamc@170: (* Copyright (c) 2008, Adam Chlipala adamc@170: * adamc@170: * This work is licensed under a adamc@170: * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 adamc@170: * Unported License. adamc@170: * The license text is available at: adamc@170: * http://creativecommons.org/licenses/by-nc-nd/3.0/ adamc@170: *) adamc@170: adamc@170: (* begin hide *) adamc@170: Require Import String List. adamc@170: adamc@173: Require Import AxiomsImpred Tactics. adamc@170: adamc@170: Set Implicit Arguments. adamc@170: (* end hide *) adamc@170: adamc@170: adamc@170: (** %\chapter{Type-Theoretic Interpreters}% *) adamc@170: adamc@170: (** TODO: Prose for this chapter *) adamc@170: adamc@170: adamc@170: (** * Simply-Typed Lambda Calculus *) adamc@170: adamc@170: Module STLC. adamc@170: Inductive type : Type := adamc@170: | Nat : type adamc@170: | Arrow : type -> type -> type. adamc@170: adamc@170: Infix "-->" := Arrow (right associativity, at level 60). adamc@170: adamc@170: Section vars. adamc@170: Variable var : type -> Type. adamc@170: adamc@170: Inductive exp : type -> Type := adamc@170: | Var : forall t, adamc@170: var t adamc@170: -> exp t adamc@170: adamc@170: | Const : nat -> exp Nat adamc@170: | Plus : exp Nat -> exp Nat -> exp Nat adamc@170: adamc@170: | App : forall t1 t2, adamc@170: exp (t1 --> t2) adamc@170: -> exp t1 adamc@170: -> exp t2 adamc@170: | Abs : forall t1 t2, adamc@170: (var t1 -> exp t2) adamc@170: -> exp (t1 --> t2). adamc@170: End vars. adamc@170: adamc@170: Definition Exp t := forall var, exp var t. adamc@170: adamc@170: Implicit Arguments Var [var t]. adamc@170: Implicit Arguments Const [var]. adamc@170: Implicit Arguments Plus [var]. adamc@170: Implicit Arguments App [var t1 t2]. adamc@170: Implicit Arguments Abs [var t1 t2]. adamc@170: adamc@170: Notation "# v" := (Var v) (at level 70). adamc@170: adamc@170: Notation "^ n" := (Const n) (at level 70). adamc@171: Infix "+^" := Plus (left associativity, at level 79). adamc@170: adamc@170: Infix "@" := App (left associativity, at level 77). adamc@170: Notation "\ x , e" := (Abs (fun x => e)) (at level 78). adamc@170: Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78). adamc@170: adamc@172: Definition zero : Exp Nat := fun _ => ^0. adamc@172: Definition one : Exp Nat := fun _ => ^1. adamc@172: Definition zpo : Exp Nat := fun _ => zero _ +^ one _. adamc@172: Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x. adamc@172: Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _. adamc@172: Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ => adamc@172: \f, \x, #f @ #x. adamc@172: Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _. adamc@172: adamc@174: (* EX: Define an interpreter for [Exp]s. *) adamc@174: adamc@174: (* begin thide *) adamc@170: Fixpoint typeDenote (t : type) : Set := adamc@170: match t with adamc@170: | Nat => nat adamc@170: | t1 --> t2 => typeDenote t1 -> typeDenote t2 adamc@170: end. adamc@170: adamc@170: Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t := adamc@170: match e in (exp _ t) return (typeDenote t) with adamc@170: | Var _ v => v adamc@170: adamc@170: | Const n => n adamc@170: | Plus e1 e2 => expDenote e1 + expDenote e2 adamc@170: adamc@170: | App _ _ e1 e2 => (expDenote e1) (expDenote e2) adamc@170: | Abs _ _ e' => fun x => expDenote (e' x) adamc@170: end. adamc@170: adamc@170: Definition ExpDenote t (e : Exp t) := expDenote (e _). adamc@174: (* end thide *) adamc@170: adamc@172: Eval compute in ExpDenote zero. adamc@172: Eval compute in ExpDenote one. adamc@172: Eval compute in ExpDenote zpo. adamc@172: Eval compute in ExpDenote ident. adamc@172: Eval compute in ExpDenote app_ident. adamc@172: Eval compute in ExpDenote app. adamc@172: Eval compute in ExpDenote app_ident'. adamc@172: adamc@174: (* EX: Define a constant-folding function for [Exp]s. *) adamc@174: adamc@174: (* begin thide *) adamc@170: Section cfold. adamc@170: Variable var : type -> Type. adamc@170: adamc@170: Fixpoint cfold t (e : exp var t) {struct e} : exp var t := adamc@170: match e in exp _ t return exp _ t with adamc@170: | Var _ v => #v adamc@170: adamc@170: | Const n => ^n adamc@170: | Plus e1 e2 => adamc@170: let e1' := cfold e1 in adamc@170: let e2' := cfold e2 in adamc@170: match e1', e2' with adamc@170: | Const n1, Const n2 => ^(n1 + n2) adamc@171: | _, _ => e1' +^ e2' adamc@170: end adamc@170: adamc@170: | App _ _ e1 e2 => cfold e1 @ cfold e2 adamc@170: | Abs _ _ e' => Abs (fun x => cfold (e' x)) adamc@170: end. adamc@170: End cfold. adamc@170: adamc@170: Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _). adamc@174: (* end thide *) adamc@170: adamc@174: (* EX: Prove the correctness of constant-folding. *) adamc@174: adamc@174: (* begin thide *) adamc@170: Lemma cfold_correct : forall t (e : exp _ t), adamc@170: expDenote (cfold e) = expDenote e. adamc@170: induction e; crush; try (ext_eq; crush); adamc@170: repeat (match goal with adamc@170: | [ |- context[cfold ?E] ] => dep_destruct (cfold E) adamc@170: end; crush). adamc@170: Qed. adamc@170: adamc@170: Theorem Cfold_correct : forall t (E : Exp t), adamc@170: ExpDenote (Cfold E) = ExpDenote E. adamc@170: unfold ExpDenote, Cfold; intros; apply cfold_correct. adamc@170: Qed. adamc@174: (* end thide *) adamc@170: End STLC. adamc@171: adamc@171: adamc@171: (** * Adding Products and Sums *) adamc@171: adamc@171: Module PSLC. adamc@174: (* EX: Extend the development with products and sums. *) adamc@174: adamc@174: (* begin thide *) adamc@171: Inductive type : Type := adamc@171: | Nat : type adamc@171: | Arrow : type -> type -> type adamc@171: | Prod : type -> type -> type adamc@171: | Sum : type -> type -> type. adamc@174: (* end thide *) adamc@171: adamc@171: Infix "-->" := Arrow (right associativity, at level 62). adamc@171: Infix "**" := Prod (right associativity, at level 61). adamc@171: Infix "++" := Sum (right associativity, at level 60). adamc@171: adamc@174: (* begin thide *) adamc@171: Section vars. adamc@171: Variable var : type -> Type. adamc@171: adamc@171: Inductive exp : type -> Type := adamc@171: | Var : forall t, adamc@171: var t adamc@171: -> exp t adamc@171: adamc@171: | Const : nat -> exp Nat adamc@171: | Plus : exp Nat -> exp Nat -> exp Nat adamc@171: adamc@171: | App : forall t1 t2, adamc@171: exp (t1 --> t2) adamc@171: -> exp t1 adamc@171: -> exp t2 adamc@171: | Abs : forall t1 t2, adamc@171: (var t1 -> exp t2) adamc@171: -> exp (t1 --> t2) adamc@171: adamc@171: | Pair : forall t1 t2, adamc@171: exp t1 adamc@171: -> exp t2 adamc@171: -> exp (t1 ** t2) adamc@171: | Fst : forall t1 t2, adamc@171: exp (t1 ** t2) adamc@171: -> exp t1 adamc@171: | Snd : forall t1 t2, adamc@171: exp (t1 ** t2) adamc@171: -> exp t2 adamc@171: adamc@171: | Inl : forall t1 t2, adamc@171: exp t1 adamc@171: -> exp (t1 ++ t2) adamc@171: | Inr : forall t1 t2, adamc@171: exp t2 adamc@171: -> exp (t1 ++ t2) adamc@171: | SumCase : forall t1 t2 t, adamc@171: exp (t1 ++ t2) adamc@171: -> (var t1 -> exp t) adamc@171: -> (var t2 -> exp t) adamc@171: -> exp t. adamc@171: End vars. adamc@171: adamc@171: Definition Exp t := forall var, exp var t. adamc@174: (* end thide *) adamc@171: adamc@171: Implicit Arguments Var [var t]. adamc@171: Implicit Arguments Const [var]. adamc@171: Implicit Arguments Abs [var t1 t2]. adamc@171: Implicit Arguments Inl [var t1 t2]. adamc@171: Implicit Arguments Inr [var t1 t2]. adamc@171: adamc@171: Notation "# v" := (Var v) (at level 70). adamc@171: adamc@171: Notation "^ n" := (Const n) (at level 70). adamc@172: Infix "+^" := Plus (left associativity, at level 78). adamc@171: adamc@171: Infix "@" := App (left associativity, at level 77). adamc@171: Notation "\ x , e" := (Abs (fun x => e)) (at level 78). adamc@171: Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78). adamc@171: adamc@171: Notation "[ e1 , e2 ]" := (Pair e1 e2). adamc@171: Notation "#1 e" := (Fst e) (at level 75). adamc@171: Notation "#2 e" := (Snd e) (at level 75). adamc@171: adamc@171: Notation "'case' e 'of' x => e1 | y => e2" := (SumCase e (fun x => e1) (fun y => e2)) adamc@171: (at level 79). adamc@171: adamc@172: Definition swap : Exp (Nat ** Nat --> Nat ** Nat) := fun _ => adamc@172: \p, [#2 #p, #1 #p]. adamc@172: Definition zo : Exp (Nat ** Nat) := fun _ => [^0, ^1]. adamc@172: Definition swap_zo : Exp (Nat ** Nat) := fun _ => swap _ @ zo _. adamc@172: adamc@172: Definition natOut : Exp (Nat ++ Nat --> Nat) := fun _ => adamc@172: \s, case #s of x => #x | y => #y +^ #y. adamc@172: Definition ns1 : Exp (Nat ++ Nat) := fun _ => Inl (^3). adamc@172: Definition ns2 : Exp (Nat ++ Nat) := fun _ => Inr (^5). adamc@172: Definition natOut_ns1 : Exp Nat := fun _ => natOut _ @ ns1 _. adamc@172: Definition natOut_ns2 : Exp Nat := fun _ => natOut _ @ ns2 _. adamc@172: adamc@174: (* begin thide *) adamc@171: Fixpoint typeDenote (t : type) : Set := adamc@171: match t with adamc@171: | Nat => nat adamc@171: | t1 --> t2 => typeDenote t1 -> typeDenote t2 adamc@171: | t1 ** t2 => typeDenote t1 * typeDenote t2 adamc@171: | t1 ++ t2 => typeDenote t1 + typeDenote t2 adamc@171: end%type. adamc@171: adamc@171: Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t := adamc@171: match e in (exp _ t) return (typeDenote t) with adamc@171: | Var _ v => v adamc@171: adamc@171: | Const n => n adamc@171: | Plus e1 e2 => expDenote e1 + expDenote e2 adamc@171: adamc@171: | App _ _ e1 e2 => (expDenote e1) (expDenote e2) adamc@171: | Abs _ _ e' => fun x => expDenote (e' x) adamc@171: adamc@171: | Pair _ _ e1 e2 => (expDenote e1, expDenote e2) adamc@171: | Fst _ _ e' => fst (expDenote e') adamc@171: | Snd _ _ e' => snd (expDenote e') adamc@171: adamc@171: | Inl _ _ e' => inl _ (expDenote e') adamc@171: | Inr _ _ e' => inr _ (expDenote e') adamc@171: | SumCase _ _ _ e' e1 e2 => adamc@171: match expDenote e' with adamc@171: | inl v => expDenote (e1 v) adamc@171: | inr v => expDenote (e2 v) adamc@171: end adamc@171: end. adamc@171: adamc@171: Definition ExpDenote t (e : Exp t) := expDenote (e _). adamc@174: (* end thide *) adamc@171: adamc@172: Eval compute in ExpDenote swap. adamc@172: Eval compute in ExpDenote zo. adamc@172: Eval compute in ExpDenote swap_zo. adamc@172: adamc@172: Eval compute in ExpDenote natOut. adamc@172: Eval compute in ExpDenote ns1. adamc@172: Eval compute in ExpDenote ns2. adamc@172: Eval compute in ExpDenote natOut_ns1. adamc@172: Eval compute in ExpDenote natOut_ns2. adamc@172: adamc@174: (* begin thide *) adamc@171: Section cfold. adamc@171: Variable var : type -> Type. adamc@171: adamc@172: Definition pairOutType t := adamc@172: match t with adamc@172: | t1 ** t2 => option (exp var t1 * exp var t2) adamc@172: | _ => unit adamc@172: end. adamc@172: adamc@172: Definition pairOutDefault (t : type) : pairOutType t := adamc@172: match t return pairOutType t with adamc@172: | _ ** _ => None adamc@172: | _ => tt adamc@172: end. adamc@172: adamc@172: Definition pairOut t1 t2 (e : exp var (t1 ** t2)) : option (exp var t1 * exp var t2) := adamc@172: match e in exp _ t return pairOutType t with adamc@172: | Pair _ _ e1 e2 => Some (e1, e2) adamc@172: | _ => pairOutDefault _ adamc@172: end. adamc@172: adamc@171: Fixpoint cfold t (e : exp var t) {struct e} : exp var t := adamc@171: match e in exp _ t return exp _ t with adamc@171: | Var _ v => #v adamc@171: adamc@171: | Const n => ^n adamc@171: | Plus e1 e2 => adamc@171: let e1' := cfold e1 in adamc@171: let e2' := cfold e2 in adamc@171: match e1', e2' with adamc@171: | Const n1, Const n2 => ^(n1 + n2) adamc@171: | _, _ => e1' +^ e2' adamc@171: end adamc@171: adamc@171: | App _ _ e1 e2 => cfold e1 @ cfold e2 adamc@171: | Abs _ _ e' => Abs (fun x => cfold (e' x)) adamc@171: adamc@171: | Pair _ _ e1 e2 => [cfold e1, cfold e2] adamc@172: | Fst t1 _ e' => adamc@172: let e'' := cfold e' in adamc@172: match pairOut e'' with adamc@172: | None => #1 e'' adamc@172: | Some (e1, _) => e1 adamc@172: end adamc@172: | Snd _ _ e' => adamc@172: let e'' := cfold e' in adamc@172: match pairOut e'' with adamc@172: | None => #2 e'' adamc@172: | Some (_, e2) => e2 adamc@172: end adamc@171: adamc@171: | Inl _ _ e' => Inl (cfold e') adamc@171: | Inr _ _ e' => Inr (cfold e') adamc@171: | SumCase _ _ _ e' e1 e2 => adamc@171: case cfold e' of adamc@171: x => cfold (e1 x) adamc@171: | y => cfold (e2 y) adamc@171: end. adamc@171: End cfold. adamc@171: adamc@171: Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _). adamc@171: adamc@172: Section pairs. adamc@172: Variables A B : Type. adamc@172: adamc@172: Variable v1 : A. adamc@172: Variable v2 : B. adamc@172: Variable v : A * B. adamc@172: adamc@172: Theorem pair_eta1 : (v1, v2) = v -> v1 = fst v. adamc@172: destruct v; crush. adamc@172: Qed. adamc@172: adamc@172: Theorem pair_eta2 : (v1, v2) = v -> v2 = snd v. adamc@172: destruct v; crush. adamc@172: Qed. adamc@172: End pairs. adamc@172: adamc@172: Hint Resolve pair_eta1 pair_eta2. adamc@172: adamc@171: Lemma cfold_correct : forall t (e : exp _ t), adamc@171: expDenote (cfold e) = expDenote e. adamc@171: induction e; crush; try (ext_eq; crush); adamc@171: repeat (match goal with adamc@171: | [ |- context[cfold ?E] ] => dep_destruct (cfold E) adamc@171: | [ |- match ?E with inl _ => _ | inr _ => _ end = _ ] => destruct E adamc@172: end; crush); eauto. adamc@171: Qed. adamc@171: adamc@171: Theorem Cfold_correct : forall t (E : Exp t), adamc@171: ExpDenote (Cfold E) = ExpDenote E. adamc@171: unfold ExpDenote, Cfold; intros; apply cfold_correct. adamc@171: Qed. adamc@174: (* end thide *) adamc@171: End PSLC. adamc@173: adamc@173: adamc@173: (** * Type Variables *) adamc@173: adamc@173: Module SysF. adamc@174: (* EX: Follow a similar progression for System F. *) adamc@174: adamc@174: (* begin thide *) adamc@173: Section vars. adamc@173: Variable tvar : Type. adamc@173: adamc@173: Inductive type : Type := adamc@173: | Nat : type adamc@173: | Arrow : type -> type -> type adamc@173: | TVar : tvar -> type adamc@173: | All : (tvar -> type) -> type. adamc@173: adamc@173: Notation "## v" := (TVar v) (at level 40). adamc@173: Infix "-->" := Arrow (right associativity, at level 60). adamc@173: adamc@173: Section Subst. adamc@173: Variable t : type. adamc@173: adamc@173: Inductive Subst : (tvar -> type) -> type -> Prop := adamc@173: | SNat : Subst (fun _ => Nat) Nat adamc@173: | SArrow : forall dom ran dom' ran', adamc@173: Subst dom dom' adamc@173: -> Subst ran ran' adamc@173: -> Subst (fun v => dom v --> ran v) (dom' --> ran') adamc@173: | SVarEq : Subst TVar t adamc@173: | SVarNe : forall v, Subst (fun _ => ##v) (##v) adamc@173: | SAll : forall ran ran', adamc@173: (forall v', Subst (fun v => ran v v') (ran' v')) adamc@173: -> Subst (fun v => All (ran v)) (All ran'). adamc@173: End Subst. adamc@173: adamc@173: Variable var : type -> Type. adamc@173: adamc@173: Inductive exp : type -> Type := adamc@173: | Var : forall t, adamc@173: var t adamc@173: -> exp t adamc@173: adamc@173: | Const : nat -> exp Nat adamc@173: | Plus : exp Nat -> exp Nat -> exp Nat adamc@173: adamc@173: | App : forall t1 t2, adamc@173: exp (t1 --> t2) adamc@173: -> exp t1 adamc@173: -> exp t2 adamc@173: | Abs : forall t1 t2, adamc@173: (var t1 -> exp t2) adamc@173: -> exp (t1 --> t2) adamc@173: adamc@173: | TApp : forall tf, adamc@173: exp (All tf) adamc@173: -> forall t tf', Subst t tf tf' adamc@173: -> exp tf' adamc@173: | TAbs : forall tf, adamc@173: (forall v, exp (tf v)) adamc@173: -> exp (All tf). adamc@173: End vars. adamc@173: adamc@173: Definition Typ := forall tvar, type tvar. adamc@173: Definition Exp (T : Typ) := forall tvar (var : type tvar -> Type), exp var (T _). adamc@174: (* end thide *) adamc@173: adamc@173: Implicit Arguments Nat [tvar]. adamc@173: adamc@173: Notation "## v" := (TVar v) (at level 40). adamc@173: Infix "-->" := Arrow (right associativity, at level 60). adamc@173: Notation "\\\ x , t" := (All (fun x => t)) (at level 65). adamc@173: adamc@173: Implicit Arguments Var [tvar var t]. adamc@173: Implicit Arguments Const [tvar var]. adamc@173: Implicit Arguments Plus [tvar var]. adamc@173: Implicit Arguments App [tvar var t1 t2]. adamc@173: Implicit Arguments Abs [tvar var t1 t2]. adamc@173: adamc@173: Implicit Arguments TAbs [tvar var tf]. adamc@173: adamc@173: Notation "# v" := (Var v) (at level 70). adamc@173: adamc@173: Notation "^ n" := (Const n) (at level 70). adamc@173: Infix "+^" := Plus (left associativity, at level 79). adamc@173: adamc@173: Infix "@" := App (left associativity, at level 77). adamc@173: Notation "\ x , e" := (Abs (fun x => e)) (at level 78). adamc@173: Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78). adamc@173: adamc@173: Notation "e @@ t" := (TApp e (t := t) _) (left associativity, at level 77). adamc@173: Notation "\\ x , e" := (TAbs (fun x => e)) (at level 78). adamc@173: Notation "\\ ! , e" := (TAbs (fun _ => e)) (at level 78). adamc@173: adamc@173: Definition zero : Exp (fun _ => Nat) := fun _ _ => adamc@173: ^0. adamc@173: Definition ident : Exp (fun _ => \\\T, ##T --> ##T) := fun _ _ => adamc@173: \\T, \x, #x. adamc@173: Definition ident_zero : Exp (fun _ => Nat). adamc@173: do 2 intro; refine (ident _ @@ _ @ zero _); adamc@173: repeat constructor. adamc@173: Defined. adamc@173: Definition ident_ident : Exp (fun _ => \\\T, ##T --> ##T). adamc@173: do 2 intro; refine (ident _ @@ _ @ ident _); adamc@173: repeat constructor. adamc@173: Defined. adamc@173: Definition ident5 : Exp (fun _ => \\\T, ##T --> ##T). adamc@173: do 2 intro; refine (ident_ident _ @@ _ @ ident_ident _ @@ _ @ ident _); adamc@173: repeat constructor. adamc@173: Defined. adamc@173: adamc@174: (* begin thide *) adamc@173: Fixpoint typeDenote (t : type Set) : Set := adamc@173: match t with adamc@173: | Nat => nat adamc@173: | t1 --> t2 => typeDenote t1 -> typeDenote t2 adamc@173: | ##v => v adamc@173: | All tf => forall T, typeDenote (tf T) adamc@173: end. adamc@173: adamc@173: Lemma Subst_typeDenote : forall t tf tf', adamc@173: Subst t tf tf' adamc@173: -> typeDenote (tf (typeDenote t)) = typeDenote tf'. adamc@173: induction 1; crush; ext_eq; crush. adamc@173: Defined. adamc@173: adamc@173: Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t := adamc@173: match e in (exp _ t) return (typeDenote t) with adamc@173: | Var _ v => v adamc@173: adamc@173: | Const n => n adamc@173: | Plus e1 e2 => expDenote e1 + expDenote e2 adamc@173: adamc@173: | App _ _ e1 e2 => (expDenote e1) (expDenote e2) adamc@173: | Abs _ _ e' => fun x => expDenote (e' x) adamc@173: adamc@173: | TApp _ e' t' _ pf => match Subst_typeDenote pf in _ = T return T with adamc@173: | refl_equal => (expDenote e') (typeDenote t') adamc@173: end adamc@173: | TAbs _ e' => fun T => expDenote (e' T) adamc@173: end. adamc@173: adamc@173: Definition ExpDenote T (E : Exp T) := expDenote (E _ _). adamc@174: (* end thide *) adamc@173: adamc@173: Eval compute in ExpDenote zero. adamc@173: Eval compute in ExpDenote ident. adamc@173: Eval compute in ExpDenote ident_zero. adamc@173: Eval compute in ExpDenote ident_ident. adamc@173: Eval compute in ExpDenote ident5. adamc@173: adamc@174: (* begin thide *) adamc@173: Section cfold. adamc@173: Variable tvar : Type. adamc@173: Variable var : type tvar -> Type. adamc@173: adamc@173: Fixpoint cfold t (e : exp var t) {struct e} : exp var t := adamc@173: match e in exp _ t return exp _ t with adamc@173: | Var _ v => #v adamc@173: adamc@173: | Const n => ^n adamc@173: | Plus e1 e2 => adamc@173: let e1' := cfold e1 in adamc@173: let e2' := cfold e2 in adamc@173: match e1', e2' with adamc@173: | Const n1, Const n2 => ^(n1 + n2) adamc@173: | _, _ => e1' +^ e2' adamc@173: end adamc@173: adamc@173: | App _ _ e1 e2 => cfold e1 @ cfold e2 adamc@173: | Abs _ _ e' => Abs (fun x => cfold (e' x)) adamc@173: adamc@173: | TApp _ e' _ _ pf => TApp (cfold e') pf adamc@173: | TAbs _ e' => \\T, cfold (e' T) adamc@173: end. adamc@173: End cfold. adamc@173: adamc@173: Definition Cfold T (E : Exp T) : Exp T := fun _ _ => cfold (E _ _). adamc@173: adamc@173: Lemma cfold_correct : forall t (e : exp _ t), adamc@173: expDenote (cfold e) = expDenote e. adamc@173: induction e; crush; try (ext_eq; crush); adamc@173: repeat (match goal with adamc@173: | [ |- context[cfold ?E] ] => dep_destruct (cfold E) adamc@173: end; crush). adamc@173: Qed. adamc@173: adamc@173: Theorem Cfold_correct : forall t (E : Exp t), adamc@173: ExpDenote (Cfold E) = ExpDenote E. adamc@173: unfold ExpDenote, Cfold; intros; apply cfold_correct. adamc@173: Qed. adamc@174: (* end thide *) adamc@173: End SysF.