matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.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/LambdaDelta-1/nf2/props".
  18
  19 include "nf2/defs.ma".
  20
  21 include "pr2/fwd.ma".
  22
  23 theorem nf2_sort:
  24  \forall (c: C).(\forall (n: nat).(nf2 c (TSort n)))
  25 \def
  26  \lambda (c: C).(\lambda (n: nat).(\lambda (t2: T).(\lambda (H: (pr2 c (TSort
  27 n) t2)).(eq_ind_r T (TSort n) (\lambda (t: T).(eq T (TSort n) t)) (refl_equal
  28 T (TSort n)) t2 (pr2_gen_sort c t2 n H))))).
  29
  30 theorem nf2_abst:
  31  \forall (c: C).(\forall (u: T).((nf2 c u) \to (\forall (b: B).(\forall (v:
  32 T).(\forall (t: T).((nf2 (CHead c (Bind b) v) t) \to (nf2 c (THead (Bind
  33 Abst) u t))))))))
  34 \def
  35  \lambda (c: C).(\lambda (u: T).(\lambda (H: ((\forall (t2: T).((pr2 c u t2)
  36 \to (eq T u t2))))).(\lambda (b: B).(\lambda (v: T).(\lambda (t: T).(\lambda
  37 (H0: ((\forall (t2: T).((pr2 (CHead c (Bind b) v) t t2) \to (eq T t
  38 t2))))).(\lambda (t2: T).(\lambda (H1: (pr2 c (THead (Bind Abst) u t)
  39 t2)).(let H2 \def (pr2_gen_abst c u t t2 H1) in (ex3_2_ind T T (\lambda (u2:
  40 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abst) u2 t3)))) (\lambda (u2:
  41 T).(\lambda (_: T).(pr2 c u u2))) (\lambda (_: T).(\lambda (t3: T).(\forall
  42 (b0: B).(\forall (u0: T).(pr2 (CHead c (Bind b0) u0) t t3))))) (eq T (THead
  43 (Bind Abst) u t) t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H3: (eq T t2
  44 (THead (Bind Abst) x0 x1))).(\lambda (H4: (pr2 c u x0)).(\lambda (H5:
  45 ((\forall (b0: B).(\forall (u0: T).(pr2 (CHead c (Bind b0) u0) t
  46 x1))))).(eq_ind_r T (THead (Bind Abst) x0 x1) (\lambda (t0: T).(eq T (THead
  47 (Bind Abst) u t) t0)) (f_equal3 K T T T THead (Bind Abst) (Bind Abst) u x0 t
  48 x1 (refl_equal K (Bind Abst)) (H x0 H4) (H0 x1 (H5 b v))) t2 H3))))))
  49 H2)))))))))).
  50
  51 theorem nf2_abst_shift:
  52  \forall (c: C).(\forall (u: T).((nf2 c u) \to (\forall (t: T).((nf2 (CHead c
  53 (Bind Abst) u) t) \to (nf2 c (THead (Bind Abst) u t))))))
  54 \def
  55  \lambda (c: C).(\lambda (u: T).(\lambda (H: ((\forall (t2: T).((pr2 c u t2)
  56 \to (eq T u t2))))).(\lambda (t: T).(\lambda (H0: ((\forall (t2: T).((pr2
  57 (CHead c (Bind Abst) u) t t2) \to (eq T t t2))))).(\lambda (t2: T).(\lambda
  58 (H1: (pr2 c (THead (Bind Abst) u t) t2)).(let H2 \def (pr2_gen_abst c u t t2
  59 H1) in (ex3_2_ind T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
  60 Abst) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c u u2))) (\lambda (_:
  61 T).(\lambda (t3: T).(\forall (b: B).(\forall (u0: T).(pr2 (CHead c (Bind b)
  62 u0) t t3))))) (eq T (THead (Bind Abst) u t) t2) (\lambda (x0: T).(\lambda
  63 (x1: T).(\lambda (H3: (eq T t2 (THead (Bind Abst) x0 x1))).(\lambda (H4: (pr2
  64 c u x0)).(\lambda (H5: ((\forall (b: B).(\forall (u0: T).(pr2 (CHead c (Bind
  65 b) u0) t x1))))).(eq_ind_r T (THead (Bind Abst) x0 x1) (\lambda (t0: T).(eq T
  66 (THead (Bind Abst) u t) t0)) (f_equal3 K T T T THead (Bind Abst) (Bind Abst)
  67 u x0 t x1 (refl_equal K (Bind Abst)) (H x0 H4) (H0 x1 (H5 Abst u))) t2
  68 H3)))))) H2)))))))).
  69
  70 theorem nf2_appl_lref:
  71  \forall (c: C).(\forall (u: T).((nf2 c u) \to (\forall (i: nat).((nf2 c
  72 (TLRef i)) \to (nf2 c (THead (Flat Appl) u (TLRef i)))))))
  73 \def
  74  \lambda (c: C).(\lambda (u: T).(\lambda (H: ((\forall (t2: T).((pr2 c u t2)
  75 \to (eq T u t2))))).(\lambda (i: nat).(\lambda (H0: ((\forall (t2: T).((pr2 c
  76 (TLRef i) t2) \to (eq T (TLRef i) t2))))).(\lambda (t2: T).(\lambda (H1: (pr2
  77 c (THead (Flat Appl) u (TLRef i)) t2)).(let H2 \def (pr2_gen_appl c u (TLRef
  78 i) t2 H1) in (or3_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2
  79 (THead (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c u u2)))
  80 (\lambda (_: T).(\lambda (t3: T).(pr2 c (TLRef i) t3)))) (ex4_4 T T T T
  81 (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
  82 (TLRef i) (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_:
  83 T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3))))))
  84 (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c u
  85 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3:
  86 T).(\forall (b: B).(\forall (u0: T).(pr2 (CHead c (Bind b) u0) z1 t3))))))))
  87 (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
  88 (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
  89 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
  90 (_: T).(eq T (TLRef i) (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda
  91 (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq
  92 T t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)))))))))
  93 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
  94 T).(\lambda (_: T).(pr2 c u u2))))))) (\lambda (_: B).(\lambda (y1:
  95 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1
  96 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2:
  97 T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))))
  98 (eq T (THead (Flat Appl) u (TLRef i)) t2) (\lambda (H3: (ex3_2 T T (\lambda
  99 (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2:
 100 T).(\lambda (_: T).(pr2 c u u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c
 101 (TLRef i) t3))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2
 102 (THead (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c u u2)))
 103 (\lambda (_: T).(\lambda (t3: T).(pr2 c (TLRef i) t3))) (eq T (THead (Flat
 104 Appl) u (TLRef i)) t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H4: (eq T
 105 t2 (THead (Flat Appl) x0 x1))).(\lambda (H5: (pr2 c u x0)).(\lambda (H6: (pr2
 106 c (TLRef i) x1)).(eq_ind_r T (THead (Flat Appl) x0 x1) (\lambda (t: T).(eq T
 107 (THead (Flat Appl) u (TLRef i)) t)) (let H7 \def (eq_ind_r T x1 (\lambda (t:
 108 T).(pr2 c (TLRef i) t)) H6 (TLRef i) (H0 x1 H6)) in (eq_ind T (TLRef i)
 109 (\lambda (t: T).(eq T (THead (Flat Appl) u (TLRef i)) (THead (Flat Appl) x0
 110 t))) (let H8 \def (eq_ind_r T x0 (\lambda (t: T).(pr2 c u t)) H5 u (H x0 H5))
 111 in (eq_ind T u (\lambda (t: T).(eq T (THead (Flat Appl) u (TLRef i)) (THead
 112 (Flat Appl) t (TLRef i)))) (refl_equal T (THead (Flat Appl) u (TLRef i))) x0
 113 (H x0 H5))) x1 (H0 x1 H6))) t2 H4)))))) H3)) (\lambda (H3: (ex4_4 T T T T
 114 (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
 115 (TLRef i) (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_:
 116 T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3))))))
 117 (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c u
 118 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3:
 119 T).(\forall (b: B).(\forall (u0: T).(pr2 (CHead c (Bind b) u0) z1
 120 t3))))))))).(ex4_4_ind T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
 121 T).(\lambda (_: T).(eq T (TLRef i) (THead (Bind Abst) y1 z1)))))) (\lambda
 122 (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead
 123 (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
 124 T).(\lambda (_: T).(pr2 c u u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda
 125 (_: T).(\lambda (t3: T).(\forall (b: B).(\forall (u0: T).(pr2 (CHead c (Bind
 126 b) u0) z1 t3))))))) (eq T (THead (Flat Appl) u (TLRef i)) t2) (\lambda (x0:
 127 T).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3: T).(\lambda (H4: (eq T
 128 (TLRef i) (THead (Bind Abst) x0 x1))).(\lambda (H5: (eq T t2 (THead (Bind
 129 Abbr) x2 x3))).(\lambda (_: (pr2 c u x2)).(\lambda (_: ((\forall (b:
 130 B).(\forall (u0: T).(pr2 (CHead c (Bind b) u0) x1 x3))))).(eq_ind_r T (THead
 131 (Bind Abbr) x2 x3) (\lambda (t: T).(eq T (THead (Flat Appl) u (TLRef i)) t))
 132 (let H8 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return
 133 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
 134 \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Bind Abst) x0
 135 x1) H4) in (False_ind (eq T (THead (Flat Appl) u (TLRef i)) (THead (Bind
 136 Abbr) x2 x3)) H8)) t2 H5))))))))) H3)) (\lambda (H3: (ex6_6 B T T T T T
 137 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
 138 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
 139 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T
 140 (TLRef i) (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
 141 T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T
 142 t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)))))))))
 143 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
 144 T).(\lambda (_: T).(pr2 c u u2))))))) (\lambda (_: B).(\lambda (y1:
 145 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1
 146 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2:
 147 T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1
 148 z2))))))))).(ex6_6_ind B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda
 149 (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b
 150 Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
 151 T).(\lambda (_: T).(\lambda (_: T).(eq T (TLRef i) (THead (Bind b) y1
 152 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2:
 153 T).(\lambda (u2: T).(\lambda (y2: T).(eq T t2 (THead (Bind b) y2 (THead (Flat
 154 Appl) (lift (S O) O u2) z2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda
 155 (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c u u2)))))))
 156 (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
 157 T).(\lambda (y2: T).(pr2 c y1 y2))))))) (\lambda (b: B).(\lambda (_:
 158 T).(\lambda (z1: T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr2
 159 (CHead c (Bind b) y2) z1 z2))))))) (eq T (THead (Flat Appl) u (TLRef i)) t2)
 160 (\lambda (x0: B).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3: T).(\lambda
 161 (x4: T).(\lambda (x5: T).(\lambda (_: (not (eq B x0 Abst))).(\lambda (H5: (eq
 162 T (TLRef i) (THead (Bind x0) x1 x2))).(\lambda (H6: (eq T t2 (THead (Bind x0)
 163 x5 (THead (Flat Appl) (lift (S O) O x4) x3)))).(\lambda (_: (pr2 c u
 164 x4)).(\lambda (_: (pr2 c x1 x5)).(\lambda (_: (pr2 (CHead c (Bind x0) x5) x2
 165 x3)).(eq_ind_r T (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4)
 166 x3)) (\lambda (t: T).(eq T (THead (Flat Appl) u (TLRef i)) t)) (let H10 \def
 167 (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_:
 168 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
 169 (THead _ _ _) \Rightarrow False])) I (THead (Bind x0) x1 x2) H5) in
 170 (False_ind (eq T (THead (Flat Appl) u (TLRef i)) (THead (Bind x0) x5 (THead
 171 (Flat Appl) (lift (S O) O x4) x3))) H10)) t2 H6))))))))))))) H3)) H2)))))))).
 172
 173 theorem nf2_lref_abst:
 174  \forall (c: C).(\forall (e: C).(\forall (u: T).(\forall (i: nat).((getl i c
 175 (CHead e (Bind Abst) u)) \to (nf2 c (TLRef i))))))
 176 \def
 177  \lambda (c: C).(\lambda (e: C).(\lambda (u: T).(\lambda (i: nat).(\lambda
 178 (H: (getl i c (CHead e (Bind Abst) u))).(\lambda (t2: T).(\lambda (H0: (pr2 c
 179 (TLRef i) t2)).(let H1 \def (pr2_gen_lref c t2 i H0) in (or_ind (eq T t2
 180 (TLRef i)) (ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i c (CHead d
 181 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(eq T t2 (lift (S i) O
 182 u0))))) (eq T (TLRef i) t2) (\lambda (H2: (eq T t2 (TLRef i))).(eq_ind_r T
 183 (TLRef i) (\lambda (t: T).(eq T (TLRef i) t)) (refl_equal T (TLRef i)) t2
 184 H2)) (\lambda (H2: (ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i c
 185 (CHead d (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(eq T t2 (lift
 186 (S i) O u0)))))).(ex2_2_ind C T (\lambda (d: C).(\lambda (u0: T).(getl i c
 187 (CHead d (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(eq T t2 (lift
 188 (S i) O u0)))) (eq T (TLRef i) t2) (\lambda (x0: C).(\lambda (x1: T).(\lambda
 189 (H3: (getl i c (CHead x0 (Bind Abbr) x1))).(\lambda (H4: (eq T t2 (lift (S i)
 190 O x1))).(eq_ind_r T (lift (S i) O x1) (\lambda (t: T).(eq T (TLRef i) t))
 191 (let H5 \def (eq_ind C (CHead e (Bind Abst) u) (\lambda (c0: C).(getl i c
 192 c0)) H (CHead x0 (Bind Abbr) x1) (getl_mono c (CHead e (Bind Abst) u) i H
 193 (CHead x0 (Bind Abbr) x1) H3)) in (let H6 \def (eq_ind C (CHead e (Bind Abst)
 194 u) (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort
 195 _) \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return
 196 (\lambda (_: K).Prop) with [(Bind b) \Rightarrow (match b in B return
 197 (\lambda (_: B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow True |
 198 Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead x0 (Bind
 199 Abbr) x1) (getl_mono c (CHead e (Bind Abst) u) i H (CHead x0 (Bind Abbr) x1)
 200 H3)) in (False_ind (eq T (TLRef i) (lift (S i) O x1)) H6))) t2 H4))))) H2))
 201 H1)))))))).
 202
 203 theorem nf2_lift:
 204  \forall (d: C).(\forall (t: T).((nf2 d t) \to (\forall (c: C).(\forall (h:
 205 nat).(\forall (i: nat).((drop h i c d) \to (nf2 c (lift h i t))))))))
 206 \def
 207  \lambda (d: C).(\lambda (t: T).(\lambda (H: ((\forall (t2: T).((pr2 d t t2)
 208 \to (eq T t t2))))).(\lambda (c: C).(\lambda (h: nat).(\lambda (i:
 209 nat).(\lambda (H0: (drop h i c d)).(\lambda (t2: T).(\lambda (H1: (pr2 c
 210 (lift h i t) t2)).(let H2 \def (pr2_gen_lift c t t2 h i H1 d H0) in (ex2_ind
 211 T (\lambda (t3: T).(eq T t2 (lift h i t3))) (\lambda (t3: T).(pr2 d t t3))
 212 (eq T (lift h i t) t2) (\lambda (x: T).(\lambda (H3: (eq T t2 (lift h i
 213 x))).(\lambda (H4: (pr2 d t x)).(eq_ind_r T (lift h i x) (\lambda (t0: T).(eq
 214 T (lift h i t) t0)) (let H_y \def (H x H4) in (let H5 \def (eq_ind_r T x
 215 (\lambda (t0: T).(pr2 d t t0)) H4 t H_y) in (eq_ind T t (\lambda (t0: T).(eq
 216 T (lift h i t) (lift h i t0))) (refl_equal T (lift h i t)) x H_y))) t2 H3))))
 217 H2)))))))))).
 218