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@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@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@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@170: 
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@170: End STLC.
adamc@171: 
adamc@171: 
adamc@171: (** * Adding Products and Sums *)
adamc@171: 
adamc@171: Module PSLC.
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@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@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@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@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@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@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@171: End PSLC.
adamc@173: 
adamc@173: 
adamc@173: (** * Type Variables *)
adamc@173: 
adamc@173: Module SysF.
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@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@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@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@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@173: End SysF.