### changeset 155:b31ca896f211

Removed G2 everywhere
author Adam Chlipala Sun, 02 Nov 2008 13:25:42 -0500 358dcb6e08f2 be15ed0a8bae src/Firstorder.v 1 files changed, 54 insertions(+), 59 deletions(-) [+]
line wrap: on
line diff
```--- a/src/Firstorder.v	Sun Nov 02 13:14:08 2008 -0500
+++ b/src/Firstorder.v	Sun Nov 02 13:25:42 2008 -0500
@@ -113,10 +113,9 @@
induction G' as [ | [x' t'] tl ]; crush; eauto 9.
Qed.

-  Lemma weaken_lookup : forall G2 x t G',
-    G' # G2
-    -> forall G1, G1 ++ G2 |-v x : t
-      -> G1 ++ G' ++ G2 |-v x : t.
+  Lemma weaken_lookup : forall x t G' G1,
+    G1 |-v x : t
+    -> G1 ++ G' |-v x : t.
Hint Resolve weaken_lookup'.

induction G1 as [ | [x' t'] tl ]; crush;
@@ -127,27 +126,16 @@

Hint Resolve weaken_lookup.

-  Lemma hasType_push : forall x t G1 G2 e t',
-    ((x, t) :: G1) ++ G2 |-e e : t'
-    -> (x, t) :: G1 ++ G2 |-e e : t'.
-    trivial.
-  Qed.
-
-  Hint Resolve hasType_push.
-
Theorem weaken_hasType' : forall G' G e t,
G |-e e : t
-      -> forall G1 G2, G = G1 ++ G2
-        -> G' # G2
-        -> G1 ++ G' ++ G2 |-e e : t.
+    -> G ++ G' |-e e : t.
induction 1; crush; eauto.
Qed.

-  Theorem weaken_hasType : forall G e t,
-    G |-e e : t
-    -> forall G', G' # G
-      -> G' ++ G |-e e : t.
-    intros; change (G' ++ G) with (nil ++ G' ++ G);
+  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.

@@ -157,15 +145,11 @@
intros; rewrite (app_nil_end G); apply weaken_hasType; auto.
Qed.

-  Theorem weaken_hasType1 : forall G e t,
-    G |-e e : t
-    -> forall x t', x ## G
-      -> (x, t') :: G |-e e : t.
-    intros; change ((x, t') :: G) with (((x, t') :: nil) ++ G);
-      apply weaken_hasType; crush;
-        match goal with
-          | [ H : (_, _) = (_, _) |- _ ] => injection H
-        end; crush; eauto.
+  Theorem weaken_hasType1 : forall e t,
+    nil |-e e : t
+    -> forall x t', (x, t') :: nil |-e e : t.
+    intros; change ((x, t') :: nil) with (((x, t') :: nil) ++ nil);
+      apply weaken_hasType; crush.
Qed.

Hint Resolve weaken_hasType_closed weaken_hasType1.
@@ -198,10 +182,10 @@
inversion 2; crush; elimtype False; eauto.
Qed.

-    Lemma subst_lookup : forall x' t G2,
+    Lemma subst_lookup : forall x' t,
x <> x'
-      -> forall G1, G1 ++ (x, xt) :: G2 |-v x' : t
-        -> G1 ++ G2 |-v x' : t.
+      -> forall G1, G1 ++ (x, xt) :: nil |-v x' : t
+        -> G1 |-v x' : t.
induction G1 as [ | [x'' t'] tl ]; crush;
match goal with
| [ H : _ |-v _ : _ |- _ ] => inversion H
@@ -210,20 +194,22 @@

Hint Resolve subst_lookup.

-    Lemma subst_lookup'' : forall G2 x' t,
-      x' ## G2
-      -> forall G1, x' ## G1
-        -> G1 ++ (x, xt) :: G2 |-v x' : t
-        -> t = xt.
+    Lemma subst_lookup'' : forall x' t G1,
+      x' ## G1
+      -> G1 ++ (x, xt) :: nil |-v x' : t
+      -> t = xt.
Hint Resolve subst_lookup'.

induction G1 as [ | [x'' t'] tl ]; crush; eauto;
match goal with
| [ H : _ |-v _ : _ |- _ ] => inversion H
-        end; crush; elimtype False; eauto.
+        end; crush; elimtype False; eauto;
+        match goal with
+          | [ H : nil |-v _ : _ |- _ ] => inversion H
+        end.
Qed.

-    Implicit Arguments subst_lookup'' [G2 x' t G1].
+    Implicit Arguments subst_lookup'' [x' t G1].

Lemma disjoint_cons : forall x x' t (G : ctx),
x ## G
@@ -237,10 +223,10 @@

Hint Resolve disjoint_cons.

-    Lemma shadow_lookup : forall G2 v t t' G1,
+    Lemma shadow_lookup : forall v t t' G1,
G1 |-v x : t'
-      -> G1 ++ (x, xt) :: G2 |-v v : t
-      -> G1 ++ G2 |-v v : t.
+      -> G1 ++ (x, xt) :: nil |-v v : t
+      -> G1 |-v v : t.
induction G1 as [ | [x'' t''] tl ]; crush;
match goal with
| [ H : nil |-v _ : _ |- _ ] => inversion H
@@ -249,11 +235,11 @@
end.
Qed.

-    Lemma shadow_hasType' : forall G2 G e t,
+    Lemma shadow_hasType' : forall G e t,
G |-e e : t
-      -> forall G1, G = G1 ++ (x, xt) :: G2
+      -> forall G1, G = G1 ++ (x, xt) :: nil
-> forall t'', G1 |-v x : t''
-          -> G1 ++ G2 |-e e : t.
+          -> G1 |-e e : t.

induction 1; crush; eauto;
@@ -261,12 +247,12 @@
| [ H : (?x0, _) :: _ ++ (x, _) :: _ |-e _ : _ |- _ ] =>
destruct (var_eq x0 x); subst; eauto
end.
-    Qed.
+    Qed.

-    Lemma shadow_hasType : forall G1 G2 e t t'',
-      G1 ++ (x, xt) :: G2 |-e e : t
+    Lemma shadow_hasType : forall G1 e t t'',
+      G1 ++ (x, xt) :: nil |-e e : t
-> G1 |-v x : t''
-      -> G1 ++ G2 |-e e : t.
+      -> G1 |-e e : t.
Qed.

@@ -274,25 +260,23 @@

Theorem subst_hasType : forall G e2 t,
G |-e e2 : t
-        -> forall G1 G2, G = G1 ++ (x, xt) :: G2
+        -> forall G1, G = G1 ++ (x, xt) :: nil
-> x ## G1
-          -> x ## G2
-          -> G1 ++ G2 |-e subst e2 : t.
+          -> G1 |-e subst e2 : t.
induction 1; crush;
try match goal with
| [ |- context[if ?E then _ else _] ] => destruct E
end; crush; eauto 6;
match goal with
-          | [ H1 : x ## _, H2 : x ## _, H3 : _ |-v x : _ |- _ ] =>
-            rewrite (subst_lookup'' H2 H1 H3)
+          | [ H1 : x ## _, H2 : _ |-v x : _ |- _ ] =>
+            rewrite (subst_lookup'' H1 H2)
end; crush.
Qed.

Theorem subst_hasType_closed : forall e2 t,
(x, xt) :: nil |-e e2 : t
-> nil |-e subst e2 : t.
-      intros; change (nil ++ nil |-e subst e2 : t);
-        eapply subst_hasType; eauto.
+      intros; eapply subst_hasType; eauto.
Qed.
End subst.

@@ -323,7 +307,7 @@

Hint Constructors step.

-  Theorem progress : forall G e t, G |-e e : t
+  Lemma progress' : forall G e t, G |-e e : t
-> G = nil
-> val e \/ exists e', e ==> e'.
induction 1; crush; eauto;
@@ -335,14 +319,25 @@
end.
Qed.

-  Theorem preservation : forall G e t, G |-e e : t
+  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'
-      -> G |-e e' : t.
+      -> 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 Concrete.```