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.