# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1260561642 18000
# Node ID 8bd90fe41acd2ca6a483b91483ed0e254f15708b
# Parent  ecfa8eec3852aa538ceb1500ad8bfdf67ab693a1
Automated LocallyNameless

diff -r ecfa8eec3852 -r 8bd90fe41acd src/Firstorder.v
--- a/src/Firstorder.v	Fri Dec 11 14:05:56 2009 -0500
+++ b/src/Firstorder.v	Fri Dec 11 15:00:42 2009 -0500
@@ -682,13 +682,16 @@
 
   Hint Constructors lclosed.
 
+  Ltac ln := crush;
+    repeat (match goal with
+              | [ |- context[if ?E then _ else _] ] => destruct E
+              | [ _ : context[if ?E then _ else _] |- _ ] => destruct E
+            end; crush); eauto.
+  
   Lemma lclosed_S : forall x e n,
     lclosed n (open x n e)
     -> lclosed (S n) e.
-    induction e; inversion 1; crush;
-      repeat (match goal with
-                | [ _ : context[if ?E then _ else _] |- _ ] => destruct E
-              end; crush).
+    induction e; inversion 1; ln.
   Qed.
 
   Hint Resolve lclosed_S.
@@ -711,13 +714,12 @@
       | S n' => primes n' ++ "'"
     end.
 
-  Check fold_left.
-
   Fixpoint sumLengths (L : list free_var) : nat :=
     match L with
       | nil => O
       | x :: L' => String.length x + sumLengths L'
     end.
+
   Definition fresh (L : list free_var) := primes (sumLengths L).
 
   Theorem freshOk' : forall x L, String.length x > sumLengths L
@@ -751,16 +753,25 @@
 
   Lemma lclosed_open : forall n e, lclosed n e
     -> forall x, open x n e = e.
-    induction 1; crush;
-      repeat (match goal with
-                | [ |- context[if ?E then _ else _] ] => destruct E
-              end; crush).
+    induction 1; ln.
   Qed.
 
   Hint Resolve lclosed_open hasType_lclosed.
 
   Open Scope list_scope.
 
+  Lemma In_cons1 : forall T (x x' : T) ls,
+    x = x'
+    -> In x (x' :: ls).
+    crush.
+  Qed.
+
+  Lemma In_cons2 : forall T (x x' : T) ls,
+    In x ls
+    -> In x (x' :: ls).
+    crush.
+  Qed.
+
   Lemma In_app1 : forall T (x : T) ls2 ls1,
     In x ls1
     -> In x (ls1 ++ ls2).
@@ -773,9 +784,21 @@
     induction ls1; crush.
   Qed.
 
-  Hint Resolve In_app1 In_app2.
+  Lemma freshOk_app1 : forall L1 L2,
+    ~ In (fresh (L1 ++ L2)) L1.
+    intros; generalize (freshOk (L1 ++ L2)); crush.
+  Qed.
+
+  Lemma freshOk_app2 : forall L1 L2,
+    ~ In (fresh (L1 ++ L2)) L2.
+    intros; generalize (freshOk (L1 ++ L2)); crush.
+  Qed.
+
+  Hint Resolve In_cons1 In_cons2 In_app1 In_app2.
 
   Section subst.
+    Hint Resolve freshOk_app1 freshOk_app2.
+
     Variable x : free_var.
     Variable e1 : exp.
 
@@ -793,15 +816,17 @@
     Definition disj x (G : ctx) := In x (map (@fst _ _) G) -> False.
     Infix "#" := disj (no associativity, at level 90).
 
+    Ltac disj := crush;
+      match goal with
+        | [ _ : _ :: _ = ?G0 ++ _ |- _ ] => destruct G0
+      end; crush; eauto.
+
     Lemma lookup_disj' : forall t G1,
       G1 |-v x : t
       -> forall G, x # G
         -> G1 = G ++ (x, xt) :: nil
         -> t = xt.
-      unfold disj; induction 1; crush;
-        match goal with
-          | [ _ : _ :: _ = ?G0 ++ _ |- _ ] => destruct G0
-        end; crush; eauto.
+      unfold disj; induction 1; disj.
     Qed.
 
     Lemma lookup_disj : forall t G,
@@ -816,10 +841,7 @@
         -> forall G, G1 = G ++ (x, xt) :: nil
           -> v <> x
           -> G |-v v : t.
-      induction 1; crush;
-        match goal with
-          | [ _ : _ :: _ = ?G0 ++ _ |- _ ] => destruct G0
-        end; crush.
+      induction 1; disj.
     Qed.
 
     Lemma lookup_ne : forall G v t,
@@ -841,13 +863,18 @@
       lclosed n e1
       -> x <> x0
       -> open x0 n (subst e') = subst (open x0 n e').
-      induction e'; crush;
-        repeat (match goal with
-                  | [ |- context[if ?E then _ else _] ] => destruct E
-                end; crush); eauto 6.
+      induction e'; ln.
     Qed.
 
-    Hint Rewrite open_subst : cpdt.
+    Lemma hasType_open_subst : forall G x0 e t,
+      G |-e subst (open x0 0 e) : t
+      -> x <> x0
+      -> lclosed 0 e1
+      -> G |-e open x0 0 (subst e) : t.
+      intros; rewrite open_subst; eauto.
+    Qed.
+
+    Hint Resolve hasType_open_subst.
 
     Lemma disj_push : forall x0 (t : type) G,
       x # G
@@ -856,13 +883,13 @@
       unfold disj; crush.
     Qed.
 
-    Hint Immediate disj_push.
+    Hint Resolve disj_push.
 
     Lemma lookup_cons : forall x0 dom G x1 t,
       G |-v x1 : t
-      -> x0 # G
+      -> ~In x0 (map (@fst _ _) G)
       -> (x0, dom) :: G |-v x1 : t.
-      unfold disj; induction 1; crush;
+      induction 1; crush;
         match goal with
           | [ H : _ |-v _ : _ |- _ ] => inversion H
         end; crush.
@@ -871,18 +898,23 @@
     Hint Resolve lookup_cons.
     Hint Unfold disj.
 
+    Lemma TAbs_specialized : forall G e' dom ran L x1,
+      (forall x, ~In x (x1 :: L ++ map (@fst _ _) G) -> (x, dom) :: G |-e open x O e' : ran)
+      -> G |-e Abs e' : dom --> ran.
+      eauto.
+    Qed.
+
     Lemma hasType_subst' : forall G1 e t,
       G1 |-e e : t
       -> forall G, G1 = G ++ (x, xt) :: nil
         -> x # G
         -> G |-e e1 : xt
         -> G |-e subst e : t.
-      induction 1; crush; eauto.
-
-      destruct (string_dec v x); crush.
-
-      apply TAbs with (x :: L ++ map (@fst _ _) G0); crush; eauto 7.
-      apply H0; eauto 6.
+      induction 1; ln;
+        match goal with
+          | [ L : list free_var, _ : ?x # _ |- _ ] =>
+            apply TAbs_specialized with L x; eauto 20
+        end.
     Qed.
       
     Theorem hasType_subst : forall e t,
@@ -897,6 +929,16 @@
 
   Notation "[ x ~> e1 ] e2" := (subst x e1 e2) (no associativity, at level 60).
 
+  Lemma alpha_open : forall x1 x2 e1 e2 n,
+    ~In x1 (freeVars e2)
+    -> ~In x2 (freeVars e2)
+    -> [x1 ~> e1](open x1 n e2) = [x2 ~> e1](open x2 n e2).
+    induction e2; crush;
+      repeat (match goal with
+                | [ |- context[if ?E then _ else _] ] => destruct E
+              end; crush).
+  Qed.
+
   Inductive val : exp -> Prop :=
   | VConst : forall b, val (Const b)
   | VAbs : forall e, val (Abs e).
@@ -939,27 +981,16 @@
     intros; eapply progress'; eauto.
   Qed.
 
-  Lemma alpha_open : forall x1 x2 e1 e2 n,
-    ~In x1 (freeVars e2)
-    -> ~In x2 (freeVars e2)
-    -> [x1 ~> e1](open x1 n e2) = [x2 ~> e1](open x2 n e2).
-    induction e2; crush;
-      repeat (match goal with
-                | [ |- context[if ?E then _ else _] ] => destruct E
-              end; crush).
+  Hint Resolve freshOk_app1 freshOk_app2.
+
+  Lemma hasType_alpha_open : forall G L e0 e2 x t,
+    ~ In x (freeVars e0)
+    -> G |-e [fresh (L ++ freeVars e0) ~> e2](open (fresh (L ++ freeVars e0)) 0 e0) : t
+    -> G |-e [x ~> e2](open x 0 e0) : t.
+    intros; rewrite (alpha_open x (fresh (L ++ freeVars e0))); auto.
   Qed.
 
-  Lemma freshOk_app1 : forall L1 L2,
-    ~ In (fresh (L1 ++ L2)) L1.
-    intros; generalize (freshOk (L1 ++ L2)); crush.
-  Qed.
-
-  Lemma freshOk_app2 : forall L1 L2,
-    ~ In (fresh (L1 ++ L2)) L2.
-    intros; generalize (freshOk (L1 ++ L2)); crush.
-  Qed.
-
-  Hint Resolve freshOk_app1 freshOk_app2.
+  Hint Resolve hasType_alpha_open.
 
   Lemma preservation' : forall G e t, G |-e e : t
     -> G = nil
@@ -969,8 +1000,6 @@
       match goal with
         | [ H : _ |-e Abs _ : _ |- _ ] => inversion H
       end; eauto.
-
-    rewrite (alpha_open x (fresh (L ++ freeVars e0))); eauto.
   Qed.
 
   Theorem preservation : forall e t, nil |-e e : t