Formalization of Girard\'s SN proof is completed

Author: pi8027

README.mkd

@@ -1,6 +1,6 @@
 # A Formalization of Typed and Untyped λ-Calculus in SSReflect-Coq and Agda2
 
-By Kazuhiko Sakaguchi, Nov. 2011 - July 2014.
+By Kazuhiko Sakaguchi, Nov. 2011 - Aug. 2014.
 
 This is a formalization of the λ-calculus written in SSReflect-Coq and Agda2, and it contains the following definitions and theorems:
 
@@ -12,11 +12,12 @@ This is a formalization of the λ-calculus written in SSReflect-Coq and Agda2, a
     * Subject reduction (type preservation) theorem
     * Strong normalization theorem
         * Using a type-free version of the reducibility predicate
-        * Using a typed version of the reducibility predicate (depends on a part of the subject reduction proof)
+        * Using a typed version of the reducibility predicate
 * System F (second order typed lambda calculus): coq/LC/Debruijn/F.v
     * Subject reduction (type preservation) theorem
     * Strong normalization theorem
         * Using a type-free version of the reducibility candidates
+        * Using a typed version of the reducibility candidates (Girard's original proof)
 
 ## References
 

coq/LC/Debruijn/F.v

@@ -1351,6 +1351,31 @@ Proof.
         by rewrite /insert take0 drop0 sub0n => _ /=; apply.
 Qed.
 
-
+Theorem typed_term_is_snorm ctx t ty : typing ctx t ty -> SN t.
+Proof.
+  move => H.
+  have {H}: typing (map some (map (odflt (tyvar 0)) ctx)) t ty
+    by move: H; apply ctxleq_preserves_typing;
+      elim: ctx {t ty} => // [[]] // ty ctx H; rewrite ctxleqE eqxx.
+  move: {ctx} (map _ ctx) => ctx.
+  have ->: (map some ctx) =
+           [seq Some x.2 | x <- zip (map var (iota 0 (size ctx))) ctx]
+    by elim: ctx 0 => //= {t ty} ty ctx IH n; rewrite -IH.
+  move => /reduce_lemma; move => /(_ (map some ctx) [::]) /= /(_ I).
+  rewrite unzip1_zip ?size_map ?size_iota ?leqnn; last by [].
+  have H: Forall
+      (fun c => reducible c.2 [::] (map some ctx) c.1)
+      (zip (map var (iota 0 (size ctx))) ctx)
+    by apply Forall_nth; case => {t ty} t ty n; rewrite
+      size_zip size_map size_iota minnn nth_map' (nth_map' (@fst _ _)) /=
+      -/unzip1 -/unzip2 unzip1_zip ?unzip2_zip ?size_map ?size_iota // => H;
+      rewrite (nth_map 0 t var) ?size_iota // nth_iota // add0n;
+      apply (CR4' (@reducibility_isrc (nth ty ctx n) [::] I)) => //=;
+      rewrite subst_nil_ty (nth_map ty).
+  move/(_ H) => {H} /(rc_cr1 (reducibility_isrc _ _)) /= /(_ I).
+  set f := subst_term _ _ _; set g := typemap _ _.
+  rewrite -/((fun t => f (g t)) t); apply acc_preservation => x y H.
+  by rewrite {}/f {}/g; apply subst_reduction1, substtyp_reduction1.
+Qed.
 
 End strong_normalization_proof_typed.