matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/fwd.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/fwd".
  18
  19 include "nf2/defs.ma".
  20
  21 include "pr2/clen.ma".
  22
  23 theorem nf2_gen_base__aux:
  24  \forall (k: K).(\forall (t: T).(\forall (u: T).((eq T (THead k u t) t) \to
  25 (\forall (P: Prop).P))))
  26 \def
  27  \lambda (k: K).(\lambda (t: T).(T_ind (\lambda (t0: T).(\forall (u: T).((eq
  28 T (THead k u t0) t0) \to (\forall (P: Prop).P)))) (\lambda (n: nat).(\lambda
  29 (u: T).(\lambda (H: (eq T (THead k u (TSort n)) (TSort n))).(\lambda (P:
  30 Prop).(let H0 \def (eq_ind T (THead k u (TSort n)) (\lambda (ee: T).(match ee
  31 in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef
  32 _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H) in
  33 (False_ind P H0)))))) (\lambda (n: nat).(\lambda (u: T).(\lambda (H: (eq T
  34 (THead k u (TLRef n)) (TLRef n))).(\lambda (P: Prop).(let H0 \def (eq_ind T
  35 (THead k u (TLRef n)) (\lambda (ee: T).(match ee in T return (\lambda (_:
  36 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
  37 (THead _ _ _) \Rightarrow True])) I (TLRef n) H) in (False_ind P H0))))))
  38 (\lambda (k0: K).(\lambda (t0: T).(\lambda (_: ((\forall (u: T).((eq T (THead
  39 k u t0) t0) \to (\forall (P: Prop).P))))).(\lambda (t1: T).(\lambda (H0:
  40 ((\forall (u: T).((eq T (THead k u t1) t1) \to (\forall (P:
  41 Prop).P))))).(\lambda (u: T).(\lambda (H1: (eq T (THead k u (THead k0 t0 t1))
  42 (THead k0 t0 t1))).(\lambda (P: Prop).(let H2 \def (f_equal T K (\lambda (e:
  43 T).(match e in T return (\lambda (_: T).K) with [(TSort _) \Rightarrow k |
  44 (TLRef _) \Rightarrow k | (THead k1 _ _) \Rightarrow k1])) (THead k u (THead
  45 k0 t0 t1)) (THead k0 t0 t1) H1) in ((let H3 \def (f_equal T T (\lambda (e:
  46 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u |
  47 (TLRef _) \Rightarrow u | (THead _ t2 _) \Rightarrow t2])) (THead k u (THead
  48 k0 t0 t1)) (THead k0 t0 t1) H1) in ((let H4 \def (f_equal T T (\lambda (e:
  49 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow (THead
  50 k0 t0 t1) | (TLRef _) \Rightarrow (THead k0 t0 t1) | (THead _ _ t2)
  51 \Rightarrow t2])) (THead k u (THead k0 t0 t1)) (THead k0 t0 t1) H1) in
  52 (\lambda (_: (eq T u t0)).(\lambda (H6: (eq K k k0)).(let H7 \def (eq_ind K k
  53 (\lambda (k1: K).(\forall (u0: T).((eq T (THead k1 u0 t1) t1) \to (\forall
  54 (P0: Prop).P0)))) H0 k0 H6) in (H7 t0 H4 P))))) H3)) H2)))))))))) t)).
  55
  56 theorem nf2_gen_lref:
  57  \forall (c: C).(\forall (d: C).(\forall (u: T).(\forall (i: nat).((getl i c
  58 (CHead d (Bind Abbr) u)) \to ((nf2 c (TLRef i)) \to (\forall (P: Prop).P))))))
  59 \def
  60  \lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda
  61 (H: (getl i c (CHead d (Bind Abbr) u))).(\lambda (H0: ((\forall (t2: T).((pr2
  62 c (TLRef i) t2) \to (eq T (TLRef i) t2))))).(\lambda (P:
  63 Prop).(lift_gen_lref_false (S i) O i (le_O_n i) (le_n (plus O (S i))) u (H0
  64 (lift (S i) O u) (pr2_delta c d u i H (TLRef i) (TLRef i) (pr0_refl (TLRef
  65 i)) (lift (S i) O u) (subst0_lref u i))) P))))))).
  66
  67 theorem nf2_gen_abst:
  68  \forall (c: C).(\forall (u: T).(\forall (t: T).((nf2 c (THead (Bind Abst) u
  69 t)) \to (land (nf2 c u) (nf2 (CHead c (Bind Abst) u) t)))))
  70 \def
  71  \lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (H: ((\forall (t2:
  72 T).((pr2 c (THead (Bind Abst) u t) t2) \to (eq T (THead (Bind Abst) u t)
  73 t2))))).(conj (\forall (t2: T).((pr2 c u t2) \to (eq T u t2))) (\forall (t2:
  74 T).((pr2 (CHead c (Bind Abst) u) t t2) \to (eq T t t2))) (\lambda (t2:
  75 T).(\lambda (H0: (pr2 c u t2)).(let H1 \def (f_equal T T (\lambda (e:
  76 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u |
  77 (TLRef _) \Rightarrow u | (THead _ t0 _) \Rightarrow t0])) (THead (Bind Abst)
  78 u t) (THead (Bind Abst) t2 t) (H (THead (Bind Abst) t2 t) (pr2_head_1 c u t2
  79 H0 (Bind Abst) t))) in (let H2 \def (eq_ind_r T t2 (\lambda (t0: T).(pr2 c u
  80 t0)) H0 u H1) in (eq_ind T u (\lambda (t0: T).(eq T u t0)) (refl_equal T u)
  81 t2 H1))))) (\lambda (t2: T).(\lambda (H0: (pr2 (CHead c (Bind Abst) u) t
  82 t2)).(let H1 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda
  83 (_: T).T) with [(TSort _) \Rightarrow t | (TLRef _) \Rightarrow t | (THead _
  84 _ t0) \Rightarrow t0])) (THead (Bind Abst) u t) (THead (Bind Abst) u t2) (H
  85 (THead (Bind Abst) u t2) (let H_y \def (pr2_gen_cbind Abst c u t t2 H0) in
  86 H_y))) in (let H2 \def (eq_ind_r T t2 (\lambda (t0: T).(pr2 (CHead c (Bind
  87 Abst) u) t t0)) H0 t H1) in (eq_ind T t (\lambda (t0: T).(eq T t t0))
  88 (refl_equal T t) t2 H1))))))))).
  89
  90 theorem nf2_gen_cast:
  91  \forall (c: C).(\forall (u: T).(\forall (t: T).((nf2 c (THead (Flat Cast) u
  92 t)) \to (\forall (P: Prop).P))))
  93 \def
  94  \lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (H: (nf2 c (THead
  95 (Flat Cast) u t))).(\lambda (P: Prop).(nf2_gen_base__aux (Flat Cast) t u (H t
  96 (pr2_free c (THead (Flat Cast) u t) t (pr0_epsilon t t (pr0_refl t) u)))
  97 P))))).
  98
  99 theorem nf2_gen_flat:
 100  \forall (f: F).(\forall (c: C).(\forall (u: T).(\forall (t: T).((nf2 c
 101 (THead (Flat f) u t)) \to (land (nf2 c u) (nf2 c t))))))
 102 \def
 103  \lambda (f: F).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (H:
 104 ((\forall (t2: T).((pr2 c (THead (Flat f) u t) t2) \to (eq T (THead (Flat f)
 105 u t) t2))))).(conj (\forall (t2: T).((pr2 c u t2) \to (eq T u t2))) (\forall
 106 (t2: T).((pr2 c t t2) \to (eq T t t2))) (\lambda (t2: T).(\lambda (H0: (pr2 c
 107 u t2)).(let H1 \def (f_equal T T (\lambda (e: T).(match e in T return
 108 (\lambda (_: T).T) with [(TSort _) \Rightarrow u | (TLRef _) \Rightarrow u |
 109 (THead _ t0 _) \Rightarrow t0])) (THead (Flat f) u t) (THead (Flat f) t2 t)
 110 (H (THead (Flat f) t2 t) (pr2_head_1 c u t2 H0 (Flat f) t))) in H1)))
 111 (\lambda (t2: T).(\lambda (H0: (pr2 c t t2)).(let H1 \def (f_equal T T
 112 (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
 113 \Rightarrow t | (TLRef _) \Rightarrow t | (THead _ _ t0) \Rightarrow t0]))
 114 (THead (Flat f) u t) (THead (Flat f) u t2) (H (THead (Flat f) u t2)
 115 (pr2_head_2 c u t t2 (Flat f) (pr2_cflat c t t2 H0 f u)))) in H1)))))))).
 116