adamc@152: (* Copyright (c) 2008, Adam Chlipala
adamc@152:  * 
adamc@152:  * This work is licensed under a
adamc@152:  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@152:  * Unported License.
adamc@152:  * The license text is available at:
adamc@152:  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@152:  *)
adamc@152: 
adamc@152: (* begin hide *)
adamc@152: Require Import List String.
adamc@152: 
adamc@152: Require Import Tactics.
adamc@152: 
adamc@152: Set Implicit Arguments.
adamc@152: (* end hide *)
adamc@152: 
adamc@152: 
adamc@152: (** %\section{Formalizing Programming Languages and Compilers}
adamc@152: 
adamc@152:    \chapter{First-Order Variable Representations}% *)
adamc@152: 
adamc@152: (** TODO: Prose for this chapter *)
adamc@152: 
adamc@152: 
adamc@152: (** * Concrete Binding *)
adamc@152: 
adamc@152: Module Concrete.
adamc@152: 
adamc@152:   Definition var := string.
adamc@152:   Definition var_eq := string_dec.
adamc@152: 
adamc@152:   Inductive exp : Set :=
adamc@152:   | Const : bool -> exp
adamc@152:   | Var : var -> exp
adamc@152:   | App : exp -> exp -> exp
adamc@152:   | Abs : var -> exp -> exp.
adamc@152: 
adamc@152:   Inductive type : Set :=
adamc@152:   | Bool : type
adamc@152:   | Arrow : type -> type -> type.
adamc@152: 
adamc@152:   Infix "-->" := Arrow (right associativity, at level 60).
adamc@152: 
adamc@152:   Definition ctx := list (var * type).
adamc@152: 
adamc@152:   Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
adamc@152: 
adamc@152:   Inductive lookup : ctx -> var -> type -> Prop :=
adamc@152:   | First : forall x t G,
adamc@152:     (x, t) :: G |-v x : t
adamc@152:   | Next : forall x t x' t' G,
adamc@152:     x <> x'
adamc@152:     -> G |-v x : t
adamc@152:     -> (x', t') :: G |-v x : t
adamc@152: 
adamc@152:     where "G |-v x : t" := (lookup G x t).
adamc@152: 
adamc@152:   Hint Constructors lookup.
adamc@152: 
adamc@152:   Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
adamc@152: 
adamc@152:   Inductive hasType : ctx -> exp -> type -> Prop :=
adamc@152:   | TConst : forall G b,
adamc@152:     G |-e Const b : Bool
adamc@152:   | TVar : forall G v t,
adamc@152:     G |-v v : t
adamc@152:     -> G |-e Var v : t
adamc@152:   | TApp : forall G e1 e2 dom ran,
adamc@152:     G |-e e1 : dom --> ran
adamc@152:     -> G |-e e2 : dom
adamc@152:     -> G |-e App e1 e2 : ran
adamc@152:   | TAbs : forall G x e' dom ran,
adamc@152:     (x, dom) :: G |-e e' : ran
adamc@152:     -> G |-e Abs x e' : dom --> ran
adamc@152: 
adamc@152:     where "G |-e e : t" := (hasType G e t).
adamc@152: 
adamc@152:   Hint Constructors hasType.
adamc@152: 
adamc@152:   Notation "x ## G" := (forall t' : type, In (x, t') G -> False) (no associativity, at level 90).
adamc@152: 
adamc@152:   Notation "G' # G" := (forall (x : var) (t : type), In (x, t) G -> x ## G') (no associativity, at level 90).
adamc@152: 
adamc@152:   Lemma lookup_In : forall G x t,
adamc@152:     G |-v x : t
adamc@152:     -> In (x, t) G.
adamc@152:     induction 1; crush.
adamc@152:   Qed.
adamc@152: 
adamc@152:   Hint Resolve lookup_In.
adamc@152: 
adamc@152:   Lemma disjoint_invert1 : forall G x t G' x' t',
adamc@152:     G |-v x : t
adamc@152:     -> (x', t') :: G' # G
adamc@152:     -> x <> x'.
adamc@152:     crush; eauto.
adamc@152:   Qed.
adamc@152: 
adamc@152:   Lemma disjoint_invert2 : forall G' G p,
adamc@152:     p :: G' # G
adamc@152:     -> G' # G.
adamc@152:     firstorder.
adamc@152:   Qed.
adamc@152: 
adamc@152:   Hint Resolve disjoint_invert1 disjoint_invert2.
adamc@152:   Hint Extern 1 (_ <> _) => (intro; subst).
adamc@152: 
adamc@152:   Lemma weaken_lookup' : forall G x t,
adamc@152:     G |-v x : t
adamc@152:     -> forall G', G' # G
adamc@152:       -> G' ++ G |-v x : t.
adamc@152:     induction G' as [ | [x' t'] tl ]; crush; eauto 9.
adamc@152:   Qed.
adamc@152: 
adamc@152:   Lemma weaken_lookup : forall G2 x t G',
adamc@152:     G' # G2
adamc@152:     -> forall G1, G1 ++ G2 |-v x : t
adamc@152:       -> G1 ++ G' ++ G2 |-v x : t.
adamc@152:     Hint Resolve weaken_lookup'.
adamc@152: 
adamc@152:     induction G1 as [ | [x' t'] tl ]; crush;
adamc@152:       match goal with
adamc@152:         | [ H : _ |-v _ : _ |- _ ] => inversion H; crush
adamc@152:       end.
adamc@152:   Qed.
adamc@152: 
adamc@152:   Hint Resolve weaken_lookup.
adamc@152: 
adamc@152:   Lemma hasType_push : forall x t G1 G2 e t',
adamc@152:     ((x, t) :: G1) ++ G2 |-e e : t'
adamc@152:     -> (x, t) :: G1 ++ G2 |-e e : t'.
adamc@152:     trivial.
adamc@152:   Qed.
adamc@152: 
adamc@152:   Hint Resolve hasType_push.
adamc@152: 
adamc@152:   Theorem weaken_hasType' : forall G' G e t,
adamc@152:     G |-e e : t
adamc@152:       -> forall G1 G2, G = G1 ++ G2
adamc@152:         -> G' # G2
adamc@152:         -> G1 ++ G' ++ G2 |-e e : t.
adamc@152:     induction 1; crush; eauto.
adamc@152:   Qed.
adamc@152: 
adamc@152:   Theorem weaken_hasType : forall G e t,
adamc@152:     G |-e e : t
adamc@152:     -> forall G', G' # G
adamc@152:       -> G' ++ G |-e e : t.
adamc@152:     intros; change (G' ++ G) with (nil ++ G' ++ G);
adamc@152:       eapply weaken_hasType'; eauto.
adamc@152:   Qed.
adamc@152: 
adamc@152:   Theorem weaken_hasType_closed : forall e t,
adamc@152:     nil |-e e : t
adamc@152:     -> forall G, G |-e e : t.
adamc@152:     intros; rewrite (app_nil_end G); apply weaken_hasType; auto.
adamc@152:   Qed.
adamc@152: 
adamc@152:   Theorem weaken_hasType1 : forall G e t,
adamc@152:     G |-e e : t
adamc@152:     -> forall x t', x ## G
adamc@152:       -> (x, t') :: G |-e e : t.
adamc@152:     intros; change ((x, t') :: G) with (((x, t') :: nil) ++ G);
adamc@152:       apply weaken_hasType; crush;
adamc@152:         match goal with
adamc@152:           | [ H : (_, _) = (_, _) |- _ ] => injection H
adamc@152:         end; crush; eauto.
adamc@152:   Qed.
adamc@152: 
adamc@152:   Hint Resolve weaken_hasType_closed weaken_hasType1.
adamc@152: 
adamc@152:   Section subst.
adamc@152:     Variable x : var.
adamc@152:     Variable e1 : exp.
adamc@152: 
adamc@152:     Fixpoint subst (e2 : exp) : exp :=
adamc@152:       match e2 with
adamc@152:         | Const b => Const b
adamc@152:         | Var x' =>
adamc@152:           if var_eq x' x
adamc@152:             then e1
adamc@152:             else Var x'
adamc@152:         | App e1 e2 => App (subst e1) (subst e2)
adamc@152:         | Abs x' e' =>
adamc@152:           Abs x' (if var_eq x' x
adamc@152:             then e'
adamc@152:             else subst e')
adamc@152:       end.
adamc@152: 
adamc@152:     Variable xt : type.
adamc@152:     Hypothesis Ht' : nil |-e e1 : xt.
adamc@152: 
adamc@152:     Lemma subst_lookup' : forall G2 x' t,
adamc@152:       x' ## G2
adamc@152:       -> (x, xt) :: G2 |-v x' : t
adamc@152:       -> t = xt.
adamc@152:       inversion 2; crush; elimtype False; eauto.
adamc@152:     Qed.
adamc@152: 
adamc@152:     Lemma subst_lookup : forall x' t G2,
adamc@152:       x <> x'
adamc@152:       -> forall G1, G1 ++ (x, xt) :: G2 |-v x' : t
adamc@152:         -> G1 ++ G2 |-v x' : t.
adamc@152:       induction G1 as [ | [x'' t'] tl ]; crush;
adamc@152:         match goal with
adamc@152:           | [ H : _ |-v _ : _ |- _ ] => inversion H
adamc@152:         end; crush.
adamc@152:     Qed.
adamc@152: 
adamc@152:     Hint Resolve subst_lookup.
adamc@152: 
adamc@152:     Lemma subst_lookup'' : forall G2 x' t,
adamc@152:       x' ## G2
adamc@152:       -> forall G1, x' ## G1
adamc@152:         -> G1 ++ (x, xt) :: G2 |-v x' : t
adamc@152:         -> t = xt.
adamc@152:       Hint Resolve subst_lookup'.
adamc@152: 
adamc@152:       induction G1 as [ | [x'' t'] tl ]; crush; eauto;
adamc@152:         match goal with
adamc@152:           | [ H : _ |-v _ : _ |- _ ] => inversion H
adamc@152:         end; crush; elimtype False; eauto.
adamc@152:     Qed.
adamc@152: 
adamc@152:     Implicit Arguments subst_lookup'' [G2 x' t G1].
adamc@152: 
adamc@152:     Lemma disjoint_cons : forall x x' t (G : ctx),
adamc@152:       x ## G
adamc@152:       -> x' <> x
adamc@152:       -> x ## (x', t) :: G.
adamc@152:       firstorder;
adamc@152:         match goal with
adamc@152:           | [ H : (_, _) = (_, _) |- _ ] => injection H
adamc@152:         end; crush.
adamc@152:     Qed.
adamc@152: 
adamc@152:     Hint Resolve disjoint_cons.
adamc@152: 
adamc@152:     Lemma shadow_lookup : forall G2 v t t' G1,
adamc@152:       G1 |-v x : t'
adamc@152:       -> G1 ++ (x, xt) :: G2 |-v v : t
adamc@152:       -> G1 ++ G2 |-v v : t.
adamc@152:       induction G1 as [ | [x'' t''] tl ]; crush;
adamc@152:         match goal with
adamc@152:           | [ H : nil |-v _ : _ |- _ ] => inversion H
adamc@152:           | [ H1 : _ |-v _ : _, H2 : _ |-v _ : _ |- _ ] =>
adamc@152:             inversion H1; crush; inversion H2; crush
adamc@152:         end.
adamc@152:     Qed.
adamc@152: 
adamc@152:     Lemma shadow_hasType' : forall G2 G e t,
adamc@152:       G |-e e : t
adamc@152:       -> forall G1, G = G1 ++ (x, xt) :: G2
adamc@152:         -> forall t'', G1 |-v x : t''
adamc@152:           -> G1 ++ G2 |-e e : t.
adamc@152:       Hint Resolve shadow_lookup.
adamc@152: 
adamc@152:       induction 1; crush; eauto;
adamc@152:         match goal with
adamc@152:           | [ H : (?x0, _) :: _ ++ (x, _) :: _ |-e _ : _ |- _ ] =>
adamc@152:             destruct (var_eq x0 x); subst; eauto
adamc@152:         end.
adamc@152:     Qed.      
adamc@152: 
adamc@152:     Lemma shadow_hasType : forall G1 G2 e t t'',
adamc@152:       G1 ++ (x, xt) :: G2 |-e e : t
adamc@152:       -> G1 |-v x : t''
adamc@152:       -> G1 ++ G2 |-e e : t.
adamc@152:       intros; eapply shadow_hasType'; eauto.
adamc@152:     Qed.
adamc@152: 
adamc@152:     Hint Resolve shadow_hasType.
adamc@152: 
adamc@152:     Theorem subst_hasType : forall G e2 t,
adamc@152:       G |-e e2 : t
adamc@152:         -> forall G1 G2, G = G1 ++ (x, xt) :: G2
adamc@152:           -> x ## G1
adamc@152:           -> x ## G2
adamc@152:           -> G1 ++ G2 |-e subst e2 : t.
adamc@152:       induction 1; crush;
adamc@152:         try match goal with
adamc@152:               | [ |- context[if ?E then _ else _] ] => destruct E
adamc@152:             end; crush; eauto 6;
adamc@152:         match goal with
adamc@152:           | [ H1 : x ## _, H2 : x ## _, H3 : _ |-v x : _ |- _ ] =>
adamc@152:             rewrite (subst_lookup'' H2 H1 H3)
adamc@152:         end; crush.
adamc@152:     Qed.
adamc@152: 
adamc@152:     Theorem subst_hasType_closed : forall e2 t,
adamc@152:       (x, xt) :: nil |-e e2 : t
adamc@152:       -> nil |-e subst e2 : t.
adamc@152:       intros; change (nil ++ nil |-e subst e2 : t);
adamc@152:         eapply subst_hasType; eauto.
adamc@152:     Qed.
adamc@152:   End subst.
adamc@152: 
adamc@152: End Concrete.