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@156: Require Import Arith String List.
adamc@152: 
adamc@152: Require Import Tactics.
adamc@152: 
adamc@152: Set Implicit Arguments.
adamc@152: (* end hide *)
adamc@152: 
adamc@152: 
adamc@153: (** %\part{Formalizing Programming Languages and Compilers}
adamc@152: 
adamc@153:    \chapter{First-Order Abstract Syntax}% *)
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@155:   Lemma weaken_lookup : forall x t G' G1,
adamc@155:     G1 |-v x : t
adamc@155:     -> G1 ++ G' |-v x : t.
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:   Theorem weaken_hasType' : forall G' G e t,
adamc@152:     G |-e e : t
adamc@155:     -> G ++ G' |-e e : t.
adamc@152:     induction 1; crush; eauto.
adamc@152:   Qed.
adamc@152: 
adamc@155:   Theorem weaken_hasType : forall e t,
adamc@155:     nil |-e e : t
adamc@155:     -> forall G', G' |-e e : t.
adamc@155:     intros; change G' with (nil ++ G');
adamc@152:       eapply weaken_hasType'; eauto.
adamc@152:   Qed.
adamc@152: 
adamc@161:   Hint Resolve weaken_hasType.
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@157:     Notation "x # G" := (forall t' : type, In (x, t') G -> False) (no associativity, at level 90).
adamc@152: 
adamc@157:     Lemma subst_lookup' : forall x' t,
adamc@152:       x <> x'
adamc@155:       -> forall G1, G1 ++ (x, xt) :: nil |-v x' : t
adamc@155:         -> G1 |-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@157:     Hint Resolve subst_lookup'.
adamc@152: 
adamc@157:     Lemma subst_lookup : forall x' t G1,
adamc@157:       x' # G1
adamc@155:       -> G1 ++ (x, xt) :: nil |-v x' : t
adamc@155:       -> t = xt.
adamc@152:       induction G1 as [ | [x'' t'] tl ]; crush; eauto;
adamc@152:         match goal with
adamc@152:           | [ H : _ |-v _ : _ |- _ ] => inversion H
adamc@155:         end; crush; elimtype False; eauto;
adamc@155:         match goal with
adamc@155:           | [ H : nil |-v _ : _ |- _ ] => inversion H
adamc@155:         end.
adamc@152:     Qed.
adamc@152: 
adamc@157:     Implicit Arguments subst_lookup [x' t G1].
adamc@152: 
adamc@155:     Lemma shadow_lookup : forall v t t' G1,
adamc@152:       G1 |-v x : t'
adamc@155:       -> G1 ++ (x, xt) :: nil |-v v : t
adamc@155:       -> G1 |-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@155:     Lemma shadow_hasType' : forall G e t,
adamc@152:       G |-e e : t
adamc@155:       -> forall G1, G = G1 ++ (x, xt) :: nil
adamc@152:         -> forall t'', G1 |-v x : t''
adamc@155:           -> G1 |-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@155:     Qed.
adamc@152: 
adamc@155:     Lemma shadow_hasType : forall G1 e t t'',
adamc@155:       G1 ++ (x, xt) :: nil |-e e : t
adamc@152:       -> G1 |-v x : t''
adamc@155:       -> G1 |-e e : t.
adamc@152:       intros; eapply shadow_hasType'; eauto.
adamc@152:     Qed.
adamc@152: 
adamc@152:     Hint Resolve shadow_hasType.
adamc@152: 
adamc@157:     Lemma disjoint_cons : forall x x' t (G : ctx),
adamc@157:       x # G
adamc@157:       -> x' <> x
adamc@157:       -> x # (x', t) :: G.
adamc@157:       firstorder;
adamc@157:         match goal with
adamc@157:           | [ H : (_, _) = (_, _) |- _ ] => injection H
adamc@157:         end; crush.
adamc@157:     Qed.
adamc@157: 
adamc@157:     Hint Resolve disjoint_cons.
adamc@157: 
adamc@152:     Theorem subst_hasType : forall G e2 t,
adamc@152:       G |-e e2 : t
adamc@155:         -> forall G1, G = G1 ++ (x, xt) :: nil
adamc@157:           -> x # G1
adamc@155:           -> G1 |-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@157:           | [ H1 : x # _, H2 : _ |-v x : _ |- _ ] =>
adamc@157:             rewrite (subst_lookup H1 H2)
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@155:       intros; eapply subst_hasType; eauto.
adamc@152:     Qed.
adamc@152:   End subst.
adamc@152: 
adamc@154:   Hint Resolve subst_hasType_closed.
adamc@154: 
adamc@154:   Notation "[ x ~> e1 ] e2" := (subst x e1 e2) (no associativity, at level 80).
adamc@154: 
adamc@154:   Inductive val : exp -> Prop :=
adamc@154:   | VConst : forall b, val (Const b)
adamc@154:   | VAbs : forall x e, val (Abs x e).
adamc@154: 
adamc@154:   Hint Constructors val.
adamc@154: 
adamc@154:   Reserved Notation "e1 ==> e2" (no associativity, at level 90).
adamc@154: 
adamc@154:   Inductive step : exp -> exp -> Prop :=
adamc@154:   | Beta : forall x e1 e2,
adamc@161:     val e2
adamc@161:     -> App (Abs x e1) e2 ==> [x ~> e2] e1
adamc@154:   | Cong1 : forall e1 e2 e1',
adamc@154:     e1 ==> e1'
adamc@154:     -> App e1 e2 ==> App e1' e2
adamc@154:   | Cong2 : forall e1 e2 e2',
adamc@154:     val e1
adamc@154:     -> e2 ==> e2'
adamc@154:     -> App e1 e2 ==> App e1 e2'
adamc@154: 
adamc@154:     where "e1 ==> e2" := (step e1 e2).
adamc@154: 
adamc@154:   Hint Constructors step.
adamc@154: 
adamc@155:   Lemma progress' : forall G e t, G |-e e : t
adamc@154:     -> G = nil
adamc@154:     -> val e \/ exists e', e ==> e'.
adamc@154:     induction 1; crush; eauto;
adamc@154:       try match goal with
adamc@154:             | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
adamc@154:           end;
adamc@154:       repeat match goal with
adamc@154:                | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
adamc@154:              end.
adamc@154:   Qed.
adamc@154: 
adamc@155:   Theorem progress : forall e t, nil |-e e : t
adamc@155:     -> val e \/ exists e', e ==> e'.
adamc@155:     intros; eapply progress'; eauto.
adamc@155:   Qed.
adamc@155: 
adamc@155:   Lemma preservation' : forall G e t, G |-e e : t
adamc@154:     -> G = nil
adamc@154:     -> forall e', e ==> e'
adamc@155:       -> nil |-e e' : t.
adamc@154:     induction 1; inversion 2; crush; eauto;
adamc@154:       match goal with
adamc@154:         | [ H : _ |-e Abs _ _ : _ |- _ ] => inversion H
adamc@154:       end; eauto.
adamc@154:   Qed.
adamc@154: 
adamc@155:   Theorem preservation : forall e t, nil |-e e : t
adamc@155:     -> forall e', e ==> e'
adamc@155:       -> nil |-e e' : t.
adamc@155:     intros; eapply preservation'; eauto.
adamc@155:   Qed.
adamc@155: 
adamc@152: End Concrete.
adamc@156: 
adamc@156: 
adamc@156: (** * De Bruijn Indices *)
adamc@156: 
adamc@156: Module DeBruijn.
adamc@156: 
adamc@156:   Definition var := nat.
adamc@156:   Definition var_eq := eq_nat_dec.
adamc@156: 
adamc@156:   Inductive exp : Set :=
adamc@156:   | Const : bool -> exp
adamc@156:   | Var : var -> exp
adamc@156:   | App : exp -> exp -> exp
adamc@156:   | Abs : exp -> exp.
adamc@156: 
adamc@156:   Inductive type : Set :=
adamc@156:   | Bool : type
adamc@156:   | Arrow : type -> type -> type.
adamc@156: 
adamc@156:   Infix "-->" := Arrow (right associativity, at level 60).
adamc@156: 
adamc@156:   Definition ctx := list type.
adamc@156: 
adamc@156:   Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
adamc@156: 
adamc@156:   Inductive lookup : ctx -> var -> type -> Prop :=
adamc@156:   | First : forall t G,
adamc@156:     t :: G |-v O : t
adamc@156:   | Next : forall x t t' G,
adamc@156:     G |-v x : t
adamc@156:     -> t' :: G |-v S x : t
adamc@156: 
adamc@156:     where "G |-v x : t" := (lookup G x t).
adamc@156: 
adamc@156:   Hint Constructors lookup.
adamc@156: 
adamc@156:   Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
adamc@156: 
adamc@156:   Inductive hasType : ctx -> exp -> type -> Prop :=
adamc@156:   | TConst : forall G b,
adamc@156:     G |-e Const b : Bool
adamc@156:   | TVar : forall G v t,
adamc@156:     G |-v v : t
adamc@156:     -> G |-e Var v : t
adamc@156:   | TApp : forall G e1 e2 dom ran,
adamc@156:     G |-e e1 : dom --> ran
adamc@156:     -> G |-e e2 : dom
adamc@156:     -> G |-e App e1 e2 : ran
adamc@156:   | TAbs : forall G e' dom ran,
adamc@156:     dom :: G |-e e' : ran
adamc@156:     -> G |-e Abs e' : dom --> ran
adamc@156: 
adamc@156:     where "G |-e e : t" := (hasType G e t).
adamc@156: 
adamc@156:   Hint Constructors hasType.
adamc@156: 
adamc@156:   Lemma weaken_lookup : forall G' v t G,
adamc@156:     G |-v v : t
adamc@156:     -> G ++ G' |-v v : t.
adamc@156:     induction 1; crush.
adamc@156:   Qed.
adamc@156: 
adamc@156:   Hint Resolve weaken_lookup.
adamc@156: 
adamc@156:   Theorem weaken_hasType' : forall G' G e t,
adamc@156:     G |-e e : t
adamc@156:     -> G ++ G' |-e e : t.
adamc@156:     induction 1; crush; eauto.
adamc@156:   Qed.
adamc@156: 
adamc@156:   Theorem weaken_hasType : forall e t,
adamc@156:     nil |-e e : t
adamc@156:     -> forall G', G' |-e e : t.
adamc@156:     intros; change G' with (nil ++ G');
adamc@156:       eapply weaken_hasType'; eauto.
adamc@156:   Qed.
adamc@156: 
adamc@161:   Hint Resolve weaken_hasType.
adamc@156: 
adamc@156:   Section subst.
adamc@156:     Variable e1 : exp.
adamc@156: 
adamc@156:     Fixpoint subst (x : var) (e2 : exp) : exp :=
adamc@156:       match e2 with
adamc@156:         | Const b => Const b
adamc@156:         | Var x' =>
adamc@156:           if var_eq x' x
adamc@156:             then e1
adamc@156:             else Var x'
adamc@156:         | App e1 e2 => App (subst x e1) (subst x e2)
adamc@156:         | Abs e' => Abs (subst (S x) e')
adamc@156:       end.
adamc@156: 
adamc@156:     Variable xt : type.
adamc@156: 
adamc@156:     Lemma subst_eq : forall t G1,
adamc@156:       G1 ++ xt :: nil |-v length G1 : t
adamc@156:       -> t = xt.
adamc@156:       induction G1; inversion 1; crush.
adamc@156:     Qed.
adamc@156: 
adamc@156:     Implicit Arguments subst_eq [t G1].
adamc@156: 
adamc@156:     Lemma subst_eq' : forall t G1 x,
adamc@156:       G1 ++ xt :: nil |-v x : t
adamc@156:       -> x <> length G1
adamc@156:       -> G1 |-v x : t.
adamc@156:       induction G1; inversion 1; crush;
adamc@156:         match goal with
adamc@156:           | [ H : nil |-v _ : _ |- _ ] => inversion H
adamc@156:         end.
adamc@156:     Qed.
adamc@156: 
adamc@156:     Hint Resolve subst_eq'.
adamc@156: 
adamc@156:     Lemma subst_neq : forall v t G1,
adamc@156:       G1 ++ xt :: nil |-v v : t
adamc@156:       -> v <> length G1
adamc@156:       -> G1 |-e Var v : t.
adamc@156:       induction G1; inversion 1; crush.
adamc@156:     Qed.
adamc@156: 
adamc@156:     Hint Resolve subst_neq.
adamc@156: 
adamc@156:     Hypothesis Ht' : nil |-e e1 : xt.
adamc@156: 
adamc@156:     Lemma hasType_push : forall dom G1 e' ran,
adamc@156:       dom :: G1 |-e subst (length (dom :: G1)) e' : ran
adamc@156:       -> dom :: G1 |-e subst (S (length G1)) e' : ran.
adamc@156:       trivial.
adamc@156:     Qed.
adamc@156: 
adamc@156:     Hint Resolve hasType_push.
adamc@156: 
adamc@156:     Theorem subst_hasType : forall G e2 t,
adamc@156:       G |-e e2 : t
adamc@156:         -> forall G1, G = G1 ++ xt :: nil
adamc@156:           -> G1 |-e subst (length G1) e2 : t.
adamc@156:       induction 1; crush;
adamc@156:         try match goal with
adamc@156:               | [ |- context[if ?E then _ else _] ] => destruct E
adamc@156:             end; crush; eauto 6;
adamc@156:         try match goal with
adamc@156:               | [ H : _ |-v _ : _ |- _ ] =>
adamc@156:                 rewrite (subst_eq H)
adamc@156:             end; crush.
adamc@156:     Qed.
adamc@156: 
adamc@156:     Theorem subst_hasType_closed : forall e2 t,
adamc@156:       xt :: nil |-e e2 : t
adamc@156:       -> nil |-e subst O e2 : t.
adamc@156:       intros; change O with (length (@nil type)); eapply subst_hasType; eauto.
adamc@156:     Qed.
adamc@156:   End subst.
adamc@156: 
adamc@156:   Hint Resolve subst_hasType_closed.
adamc@156: 
adamc@156:   Notation "[ x ~> e1 ] e2" := (subst e1 x e2) (no associativity, at level 80).
adamc@156: 
adamc@156:   Inductive val : exp -> Prop :=
adamc@156:   | VConst : forall b, val (Const b)
adamc@156:   | VAbs : forall e, val (Abs e).
adamc@156: 
adamc@156:   Hint Constructors val.
adamc@156: 
adamc@156:   Reserved Notation "e1 ==> e2" (no associativity, at level 90).
adamc@156: 
adamc@156:   Inductive step : exp -> exp -> Prop :=
adamc@156:   | Beta : forall e1 e2,
adamc@161:     val e2
adamc@161:     -> App (Abs e1) e2 ==> [O ~> e2] e1
adamc@156:   | Cong1 : forall e1 e2 e1',
adamc@156:     e1 ==> e1'
adamc@156:     -> App e1 e2 ==> App e1' e2
adamc@156:   | Cong2 : forall e1 e2 e2',
adamc@156:     val e1
adamc@156:     -> e2 ==> e2'
adamc@156:     -> App e1 e2 ==> App e1 e2'
adamc@156: 
adamc@156:     where "e1 ==> e2" := (step e1 e2).
adamc@156: 
adamc@156:   Hint Constructors step.
adamc@156: 
adamc@156:   Lemma progress' : forall G e t, G |-e e : t
adamc@156:     -> G = nil
adamc@156:     -> val e \/ exists e', e ==> e'.
adamc@156:     induction 1; crush; eauto;
adamc@156:       try match goal with
adamc@156:             | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
adamc@156:           end;
adamc@156:       repeat match goal with
adamc@156:                | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
adamc@156:              end.
adamc@156:   Qed.
adamc@156: 
adamc@156:   Theorem progress : forall e t, nil |-e e : t
adamc@156:     -> val e \/ exists e', e ==> e'.
adamc@156:     intros; eapply progress'; eauto.
adamc@156:   Qed.
adamc@156: 
adamc@156:   Lemma preservation' : forall G e t, G |-e e : t
adamc@156:     -> G = nil
adamc@156:     -> forall e', e ==> e'
adamc@156:       -> nil |-e e' : t.
adamc@156:     induction 1; inversion 2; crush; eauto;
adamc@156:       match goal with
adamc@156:         | [ H : _ |-e Abs _ : _ |- _ ] => inversion H
adamc@156:       end; eauto.
adamc@156:   Qed.
adamc@156: 
adamc@156:   Theorem preservation : forall e t, nil |-e e : t
adamc@156:     -> forall e', e ==> e'
adamc@156:       -> nil |-e e' : t.
adamc@156:     intros; eapply preservation'; eauto.
adamc@156:   Qed.
adamc@156: 
adamc@156: End DeBruijn.