# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1225651911 18000
# Node ID be15ed0a8baea141e0dcf30bf4bcc9017f74025d
# Parent  b31ca896f211422cb47d59059c2bf0e8f5fa5998
De Bruijn

diff -r b31ca896f211 -r be15ed0a8bae src/Firstorder.v
--- a/src/Firstorder.v	Sun Nov 02 13:25:42 2008 -0500
+++ b/src/Firstorder.v	Sun Nov 02 13:51:51 2008 -0500
@@ -8,7 +8,7 @@
  *)
 
 (* begin hide *)
-Require Import List String.
+Require Import Arith String List.
 
 Require Import Tactics.
 
@@ -341,3 +341,232 @@
   Qed.
 
 End Concrete.
+
+
+(** * De Bruijn Indices *)
+
+Module DeBruijn.
+
+  Definition var := nat.
+  Definition var_eq := eq_nat_dec.
+
+  Inductive exp : Set :=
+  | Const : bool -> exp
+  | Var : var -> exp
+  | App : exp -> exp -> exp
+  | Abs : exp -> exp.
+
+  Inductive type : Set :=
+  | Bool : type
+  | Arrow : type -> type -> type.
+
+  Infix "-->" := Arrow (right associativity, at level 60).
+
+  Definition ctx := list type.
+
+  Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
+
+  Inductive lookup : ctx -> var -> type -> Prop :=
+  | First : forall t G,
+    t :: G |-v O : t
+  | Next : forall x t t' G,
+    G |-v x : t
+    -> t' :: G |-v S x : t
+
+    where "G |-v x : t" := (lookup G x t).
+
+  Hint Constructors lookup.
+
+  Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
+
+  Inductive hasType : ctx -> exp -> type -> Prop :=
+  | TConst : forall G b,
+    G |-e Const b : Bool
+  | TVar : forall G v t,
+    G |-v v : t
+    -> G |-e Var v : t
+  | TApp : forall G e1 e2 dom ran,
+    G |-e e1 : dom --> ran
+    -> G |-e e2 : dom
+    -> G |-e App e1 e2 : ran
+  | TAbs : forall G e' dom ran,
+    dom :: G |-e e' : ran
+    -> G |-e Abs e' : dom --> ran
+
+    where "G |-e e : t" := (hasType G e t).
+
+  Hint Constructors hasType.
+
+  Lemma weaken_lookup : forall G' v t G,
+    G |-v v : t
+    -> G ++ G' |-v v : t.
+    induction 1; crush.
+  Qed.
+
+  Hint Resolve weaken_lookup.
+
+  Theorem weaken_hasType' : forall G' G e t,
+    G |-e e : t
+    -> G ++ G' |-e e : t.
+    induction 1; crush; eauto.
+  Qed.
+
+  Theorem weaken_hasType : forall e t,
+    nil |-e e : t
+    -> forall G', G' |-e e : t.
+    intros; change G' with (nil ++ G');
+      eapply weaken_hasType'; eauto.
+  Qed.
+
+  Theorem weaken_hasType_closed : forall e t,
+    nil |-e e : t
+    -> forall G, G |-e e : t.
+    intros; rewrite (app_nil_end G); apply weaken_hasType; auto.
+  Qed.
+
+  Theorem weaken_hasType1 : forall e t,
+    nil |-e e : t
+    -> forall t', t' :: nil |-e e : t.
+    intros; change (t' :: nil) with ((t' :: nil) ++ nil);
+      apply weaken_hasType; crush.
+  Qed.
+
+  Hint Resolve weaken_hasType_closed weaken_hasType1.
+
+  Section subst.
+    Variable e1 : exp.
+
+    Fixpoint subst (x : var) (e2 : exp) : exp :=
+      match e2 with
+        | Const b => Const b
+        | Var x' =>
+          if var_eq x' x
+            then e1
+            else Var x'
+        | App e1 e2 => App (subst x e1) (subst x e2)
+        | Abs e' => Abs (subst (S x) e')
+      end.
+
+    Variable xt : type.
+
+    Lemma subst_eq : forall t G1,
+      G1 ++ xt :: nil |-v length G1 : t
+      -> t = xt.
+      induction G1; inversion 1; crush.
+    Qed.
+
+    Implicit Arguments subst_eq [t G1].
+
+    Lemma subst_eq' : forall t G1 x,
+      G1 ++ xt :: nil |-v x : t
+      -> x <> length G1
+      -> G1 |-v x : t.
+      induction G1; inversion 1; crush;
+        match goal with
+          | [ H : nil |-v _ : _ |- _ ] => inversion H
+        end.
+    Qed.
+
+    Hint Resolve subst_eq'.
+
+    Lemma subst_neq : forall v t G1,
+      G1 ++ xt :: nil |-v v : t
+      -> v <> length G1
+      -> G1 |-e Var v : t.
+      induction G1; inversion 1; crush.
+    Qed.
+
+    Hint Resolve subst_neq.
+
+    Hypothesis Ht' : nil |-e e1 : xt.
+
+    Lemma hasType_push : forall dom G1 e' ran,
+      dom :: G1 |-e subst (length (dom :: G1)) e' : ran
+      -> dom :: G1 |-e subst (S (length G1)) e' : ran.
+      trivial.
+    Qed.
+
+    Hint Resolve hasType_push.
+
+    Theorem subst_hasType : forall G e2 t,
+      G |-e e2 : t
+        -> forall G1, G = G1 ++ xt :: nil
+          -> G1 |-e subst (length G1) e2 : t.
+      induction 1; crush;
+        try match goal with
+              | [ |- context[if ?E then _ else _] ] => destruct E
+            end; crush; eauto 6;
+        try match goal with
+              | [ H : _ |-v _ : _ |- _ ] =>
+                rewrite (subst_eq H)
+            end; crush.
+    Qed.
+
+    Theorem subst_hasType_closed : forall e2 t,
+      xt :: nil |-e e2 : t
+      -> nil |-e subst O e2 : t.
+      intros; change O with (length (@nil type)); eapply subst_hasType; eauto.
+    Qed.
+  End subst.
+
+  Hint Resolve subst_hasType_closed.
+
+  Notation "[ x ~> e1 ] e2" := (subst e1 x e2) (no associativity, at level 80).
+
+  Inductive val : exp -> Prop :=
+  | VConst : forall b, val (Const b)
+  | VAbs : forall e, val (Abs e).
+
+  Hint Constructors val.
+
+  Reserved Notation "e1 ==> e2" (no associativity, at level 90).
+
+  Inductive step : exp -> exp -> Prop :=
+  | Beta : forall e1 e2,
+    App (Abs e1) e2 ==> [O ~> e2] e1
+  | Cong1 : forall e1 e2 e1',
+    e1 ==> e1'
+    -> App e1 e2 ==> App e1' e2
+  | Cong2 : forall e1 e2 e2',
+    val e1
+    -> e2 ==> e2'
+    -> App e1 e2 ==> App e1 e2'
+
+    where "e1 ==> e2" := (step e1 e2).
+
+  Hint Constructors step.
+
+  Lemma progress' : forall G e t, G |-e e : t
+    -> G = nil
+    -> val e \/ exists e', e ==> e'.
+    induction 1; crush; eauto;
+      try match goal with
+            | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
+          end;
+      repeat match goal with
+               | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
+             end.
+  Qed.
+
+  Theorem progress : forall e t, nil |-e e : t
+    -> val e \/ exists e', e ==> e'.
+    intros; eapply progress'; eauto.
+  Qed.
+
+  Lemma preservation' : forall G e t, G |-e e : t
+    -> G = nil
+    -> forall e', e ==> e'
+      -> nil |-e e' : t.
+    induction 1; inversion 2; crush; eauto;
+      match goal with
+        | [ H : _ |-e Abs _ : _ |- _ ] => inversion H
+      end; eauto.
+  Qed.
+
+  Theorem preservation : forall e t, nil |-e e : t
+    -> forall e', e ==> e'
+      -> nil |-e e' : t.
+    intros; eapply preservation'; eauto.
+  Qed.
+
+End DeBruijn.