matita/matita/contribs/lambdadelta/basic_1/sty0/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 include "basic_1/sty0/fwd.ma".
  18
  19 include "basic_1/getl/drop.ma".
  20
  21 lemma sty0_lift:
  22  \forall (g: G).(\forall (e: C).(\forall (t1: T).(\forall (t2: T).((sty0 g e
  23 t1 t2) \to (\forall (c: C).(\forall (h: nat).(\forall (d: nat).((drop h d c
  24 e) \to (sty0 g c (lift h d t1) (lift h d t2))))))))))
  25 \def
  26  \lambda (g: G).(\lambda (e: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda
  27 (H: (sty0 g e t1 t2)).(sty0_ind g (\lambda (c: C).(\lambda (t: T).(\lambda
  28 (t0: T).(\forall (c0: C).(\forall (h: nat).(\forall (d: nat).((drop h d c0 c)
  29 \to (sty0 g c0 (lift h d t) (lift h d t0))))))))) (\lambda (c: C).(\lambda
  30 (n: nat).(\lambda (c0: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (_:
  31 (drop h d c0 c)).(eq_ind_r T (TSort n) (\lambda (t: T).(sty0 g c0 t (lift h d
  32 (TSort (next g n))))) (eq_ind_r T (TSort (next g n)) (\lambda (t: T).(sty0 g
  33 c0 (TSort n) t)) (sty0_sort g c0 n) (lift h d (TSort (next g n))) (lift_sort
  34 (next g n) h d)) (lift h d (TSort n)) (lift_sort n h d)))))))) (\lambda (c:
  35 C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (H0: (getl i c
  36 (CHead d (Bind Abbr) v))).(\lambda (w: T).(\lambda (H1: (sty0 g d v
  37 w)).(\lambda (H2: ((\forall (c0: C).(\forall (h: nat).(\forall (d0:
  38 nat).((drop h d0 c0 d) \to (sty0 g c0 (lift h d0 v) (lift h d0
  39 w)))))))).(\lambda (c0: C).(\lambda (h: nat).(\lambda (d0: nat).(\lambda (H3:
  40 (drop h d0 c0 c)).(lt_le_e i d0 (sty0 g c0 (lift h d0 (TLRef i)) (lift h d0
  41 (lift (S i) O w))) (\lambda (H4: (lt i d0)).(let H5 \def (drop_getl_trans_le
  42 i d0 (le_S_n i d0 (le_S_n (S i) (S d0) (le_S (S (S i)) (S d0) (le_n_S (S i)
  43 d0 H4)))) c0 c h H3 (CHead d (Bind Abbr) v) H0) in (ex3_2_ind C C (\lambda
  44 (e0: C).(\lambda (_: C).(drop i O c0 e0))) (\lambda (e0: C).(\lambda (e1:
  45 C).(drop h (minus d0 i) e0 e1))) (\lambda (_: C).(\lambda (e1: C).(clear e1
  46 (CHead d (Bind Abbr) v)))) (sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift
  47 (S i) O w))) (\lambda (x0: C).(\lambda (x1: C).(\lambda (H6: (drop i O c0
  48 x0)).(\lambda (H7: (drop h (minus d0 i) x0 x1)).(\lambda (H8: (clear x1
  49 (CHead d (Bind Abbr) v))).(let H9 \def (eq_ind nat (minus d0 i) (\lambda (n:
  50 nat).(drop h n x0 x1)) H7 (S (minus d0 (S i))) (minus_x_Sy d0 i H4)) in (let
  51 H10 \def (drop_clear_S x1 x0 h (minus d0 (S i)) H9 Abbr d v H8) in (ex2_ind C
  52 (\lambda (c1: C).(clear x0 (CHead c1 (Bind Abbr) (lift h (minus d0 (S i))
  53 v)))) (\lambda (c1: C).(drop h (minus d0 (S i)) c1 d)) (sty0 g c0 (lift h d0
  54 (TLRef i)) (lift h d0 (lift (S i) O w))) (\lambda (x: C).(\lambda (H11:
  55 (clear x0 (CHead x (Bind Abbr) (lift h (minus d0 (S i)) v)))).(\lambda (H12:
  56 (drop h (minus d0 (S i)) x d)).(eq_ind_r T (TLRef i) (\lambda (t: T).(sty0 g
  57 c0 t (lift h d0 (lift (S i) O w)))) (eq_ind nat (plus (S i) (minus d0 (S i)))
  58 (\lambda (n: nat).(sty0 g c0 (TLRef i) (lift h n (lift (S i) O w))))
  59 (eq_ind_r T (lift (S i) O (lift h (minus d0 (S i)) w)) (\lambda (t: T).(sty0
  60 g c0 (TLRef i) t)) (eq_ind nat d0 (\lambda (_: nat).(sty0 g c0 (TLRef i)
  61 (lift (S i) O (lift h (minus d0 (S i)) w)))) (sty0_abbr g c0 x (lift h (minus
  62 d0 (S i)) v) i (getl_intro i c0 (CHead x (Bind Abbr) (lift h (minus d0 (S i))
  63 v)) x0 H6 H11) (lift h (minus d0 (S i)) w) (H2 x h (minus d0 (S i)) H12))
  64 (plus (S i) (minus d0 (S i))) (le_plus_minus (S i) d0 H4)) (lift h (plus (S
  65 i) (minus d0 (S i))) (lift (S i) O w)) (lift_d w h (S i) (minus d0 (S i)) O
  66 (le_O_n (minus d0 (S i))))) d0 (le_plus_minus_r (S i) d0 H4)) (lift h d0
  67 (TLRef i)) (lift_lref_lt i h d0 H4))))) H10)))))))) H5))) (\lambda (H4: (le
  68 d0 i)).(eq_ind_r T (TLRef (plus i h)) (\lambda (t: T).(sty0 g c0 t (lift h d0
  69 (lift (S i) O w)))) (eq_ind nat (S i) (\lambda (_: nat).(sty0 g c0 (TLRef
  70 (plus i h)) (lift h d0 (lift (S i) O w)))) (eq_ind_r T (lift (plus h (S i)) O
  71 w) (\lambda (t: T).(sty0 g c0 (TLRef (plus i h)) t)) (eq_ind_r nat (plus (S
  72 i) h) (\lambda (n: nat).(sty0 g c0 (TLRef (plus i h)) (lift n O w)))
  73 (sty0_abbr g c0 d v (plus i h) (drop_getl_trans_ge i c0 c d0 h H3 (CHead d
  74 (Bind Abbr) v) H0 H4) w H1) (plus h (S i)) (plus_sym h (S i))) (lift h d0
  75 (lift (S i) O w)) (lift_free w (S i) h O d0 (le_S_n d0 (S i) (le_S (S d0) (S
  76 i) (le_n_S d0 i H4))) (le_O_n d0))) (plus i (S O)) (eq_ind_r nat (plus (S O)
  77 i) (\lambda (n: nat).(eq nat (S i) n)) (le_antisym (S i) (plus (S O) i) (le_n
  78 (plus (S O) i)) (le_n (S i))) (plus i (S O)) (plus_sym i (S O)))) (lift h d0
  79 (TLRef i)) (lift_lref_ge i h d0 H4)))))))))))))))) (\lambda (c: C).(\lambda
  80 (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (H0: (getl i c (CHead d
  81 (Bind Abst) v))).(\lambda (w: T).(\lambda (H1: (sty0 g d v w)).(\lambda (H2:
  82 ((\forall (c0: C).(\forall (h: nat).(\forall (d0: nat).((drop h d0 c0 d) \to
  83 (sty0 g c0 (lift h d0 v) (lift h d0 w)))))))).(\lambda (c0: C).(\lambda (h:
  84 nat).(\lambda (d0: nat).(\lambda (H3: (drop h d0 c0 c)).(lt_le_e i d0 (sty0 g
  85 c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O v))) (\lambda (H4: (lt i
  86 d0)).(let H5 \def (drop_getl_trans_le i d0 (le_S_n i d0 (le_S_n (S i) (S d0)
  87 (le_S (S (S i)) (S d0) (le_n_S (S i) d0 H4)))) c0 c h H3 (CHead d (Bind Abst)
  88 v) H0) in (ex3_2_ind C C (\lambda (e0: C).(\lambda (_: C).(drop i O c0 e0)))
  89 (\lambda (e0: C).(\lambda (e1: C).(drop h (minus d0 i) e0 e1))) (\lambda (_:
  90 C).(\lambda (e1: C).(clear e1 (CHead d (Bind Abst) v)))) (sty0 g c0 (lift h
  91 d0 (TLRef i)) (lift h d0 (lift (S i) O v))) (\lambda (x0: C).(\lambda (x1:
  92 C).(\lambda (H6: (drop i O c0 x0)).(\lambda (H7: (drop h (minus d0 i) x0
  93 x1)).(\lambda (H8: (clear x1 (CHead d (Bind Abst) v))).(let H9 \def (eq_ind
  94 nat (minus d0 i) (\lambda (n: nat).(drop h n x0 x1)) H7 (S (minus d0 (S i)))
  95 (minus_x_Sy d0 i H4)) in (let H10 \def (drop_clear_S x1 x0 h (minus d0 (S i))
  96 H9 Abst d v H8) in (ex2_ind C (\lambda (c1: C).(clear x0 (CHead c1 (Bind
  97 Abst) (lift h (minus d0 (S i)) v)))) (\lambda (c1: C).(drop h (minus d0 (S
  98 i)) c1 d)) (sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O v)))
  99 (\lambda (x: C).(\lambda (H11: (clear x0 (CHead x (Bind Abst) (lift h (minus
 100 d0 (S i)) v)))).(\lambda (H12: (drop h (minus d0 (S i)) x d)).(eq_ind_r T
 101 (TLRef i) (\lambda (t: T).(sty0 g c0 t (lift h d0 (lift (S i) O v)))) (eq_ind
 102 nat (plus (S i) (minus d0 (S i))) (\lambda (n: nat).(sty0 g c0 (TLRef i)
 103 (lift h n (lift (S i) O v)))) (eq_ind_r T (lift (S i) O (lift h (minus d0 (S
 104 i)) v)) (\lambda (t: T).(sty0 g c0 (TLRef i) t)) (eq_ind nat d0 (\lambda (_:
 105 nat).(sty0 g c0 (TLRef i) (lift (S i) O (lift h (minus d0 (S i)) v))))
 106 (sty0_abst g c0 x (lift h (minus d0 (S i)) v) i (getl_intro i c0 (CHead x
 107 (Bind Abst) (lift h (minus d0 (S i)) v)) x0 H6 H11) (lift h (minus d0 (S i))
 108 w) (H2 x h (minus d0 (S i)) H12)) (plus (S i) (minus d0 (S i)))
 109 (le_plus_minus (S i) d0 H4)) (lift h (plus (S i) (minus d0 (S i))) (lift (S
 110 i) O v)) (lift_d v h (S i) (minus d0 (S i)) O (le_O_n (minus d0 (S i))))) d0
 111 (le_plus_minus_r (S i) d0 H4)) (lift h d0 (TLRef i)) (lift_lref_lt i h d0
 112 H4))))) H10)))))))) H5))) (\lambda (H4: (le d0 i)).(eq_ind_r T (TLRef (plus i
 113 h)) (\lambda (t: T).(sty0 g c0 t (lift h d0 (lift (S i) O v)))) (eq_ind nat
 114 (S i) (\lambda (_: nat).(sty0 g c0 (TLRef (plus i h)) (lift h d0 (lift (S i)
 115 O v)))) (eq_ind_r T (lift (plus h (S i)) O v) (\lambda (t: T).(sty0 g c0
 116 (TLRef (plus i h)) t)) (eq_ind_r nat (plus (S i) h) (\lambda (n: nat).(sty0 g
 117 c0 (TLRef (plus i h)) (lift n O v))) (sty0_abst g c0 d v (plus i h)
 118 (drop_getl_trans_ge i c0 c d0 h H3 (CHead d (Bind Abst) v) H0 H4) w H1) (plus
 119 h (S i)) (plus_sym h (S i))) (lift h d0 (lift (S i) O v)) (lift_free v (S i)
 120 h O d0 (le_S_n d0 (S i) (le_S (S d0) (S i) (le_n_S d0 i H4))) (le_O_n d0)))
 121 (plus i (S O)) (eq_ind_r nat (plus (S O) i) (\lambda (n: nat).(eq nat (S i)
 122 n)) (le_antisym (S i) (plus (S O) i) (le_n (plus (S O) i)) (le_n (S i)))
 123 (plus i (S O)) (plus_sym i (S O)))) (lift h d0 (TLRef i)) (lift_lref_ge i h
 124 d0 H4)))))))))))))))) (\lambda (b: B).(\lambda (c: C).(\lambda (v:
 125 T).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (sty0 g (CHead c (Bind b)
 126 v) t3 t4)).(\lambda (H1: ((\forall (c0: C).(\forall (h: nat).(\forall (d:
 127 nat).((drop h d c0 (CHead c (Bind b) v)) \to (sty0 g c0 (lift h d t3) (lift h
 128 d t4)))))))).(\lambda (c0: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda
 129 (H2: (drop h d c0 c)).(eq_ind_r T (THead (Bind b) (lift h d v) (lift h (s
 130 (Bind b) d) t3)) (\lambda (t: T).(sty0 g c0 t (lift h d (THead (Bind b) v
 131 t4)))) (eq_ind_r T (THead (Bind b) (lift h d v) (lift h (s (Bind b) d) t4))
 132 (\lambda (t: T).(sty0 g c0 (THead (Bind b) (lift h d v) (lift h (s (Bind b)
 133 d) t3)) t)) (sty0_bind g b c0 (lift h d v) (lift h (S d) t3) (lift h (S d)
 134 t4) (H1 (CHead c0 (Bind b) (lift h d v)) h (S d) (drop_skip_bind h d c0 c H2
 135 b v))) (lift h d (THead (Bind b) v t4)) (lift_head (Bind b) v t4 h d)) (lift
 136 h d (THead (Bind b) v t3)) (lift_head (Bind b) v t3 h d))))))))))))) (\lambda
 137 (c: C).(\lambda (v: T).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (sty0 g
 138 c t3 t4)).(\lambda (H1: ((\forall (c0: C).(\forall (h: nat).(\forall (d:
 139 nat).((drop h d c0 c) \to (sty0 g c0 (lift h d t3) (lift h d
 140 t4)))))))).(\lambda (c0: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H2:
 141 (drop h d c0 c)).(eq_ind_r T (THead (Flat Appl) (lift h d v) (lift h (s (Flat
 142 Appl) d) t3)) (\lambda (t: T).(sty0 g c0 t (lift h d (THead (Flat Appl) v
 143 t4)))) (eq_ind_r T (THead (Flat Appl) (lift h d v) (lift h (s (Flat Appl) d)
 144 t4)) (\lambda (t: T).(sty0 g c0 (THead (Flat Appl) (lift h d v) (lift h (s
 145 (Flat Appl) d) t3)) t)) (sty0_appl g c0 (lift h d v) (lift h (s (Flat Appl)
 146 d) t3) (lift h (s (Flat Appl) d) t4) (H1 c0 h (s (Flat Appl) d) H2)) (lift h
 147 d (THead (Flat Appl) v t4)) (lift_head (Flat Appl) v t4 h d)) (lift h d
 148 (THead (Flat Appl) v t3)) (lift_head (Flat Appl) v t3 h d))))))))))))
 149 (\lambda (c: C).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (sty0 g c v1
 150 v2)).(\lambda (H1: ((\forall (c0: C).(\forall (h: nat).(\forall (d:
 151 nat).((drop h d c0 c) \to (sty0 g c0 (lift h d v1) (lift h d
 152 v2)))))))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (sty0 g c t3
 153 t4)).(\lambda (H3: ((\forall (c0: C).(\forall (h: nat).(\forall (d:
 154 nat).((drop h d c0 c) \to (sty0 g c0 (lift h d t3) (lift h d
 155 t4)))))))).(\lambda (c0: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H4:
 156 (drop h d c0 c)).(eq_ind_r T (THead (Flat Cast) (lift h d v1) (lift h (s
 157 (Flat Cast) d) t3)) (\lambda (t: T).(sty0 g c0 t (lift h d (THead (Flat Cast)
 158 v2 t4)))) (eq_ind_r T (THead (Flat Cast) (lift h d v2) (lift h (s (Flat Cast)
 159 d) t4)) (\lambda (t: T).(sty0 g c0 (THead (Flat Cast) (lift h d v1) (lift h
 160 (s (Flat Cast) d) t3)) t)) (sty0_cast g c0 (lift h d v1) (lift h d v2) (H1 c0
 161 h d H4) (lift h (s (Flat Cast) d) t3) (lift h (s (Flat Cast) d) t4) (H3 c0 h
 162 (s (Flat Cast) d) H4)) (lift h d (THead (Flat Cast) v2 t4)) (lift_head (Flat
 163 Cast) v2 t4 h d)) (lift h d (THead (Flat Cast) v1 t3)) (lift_head (Flat Cast)
 164 v1 t3 h d))))))))))))))) e t1 t2 H))))).
 165
 166 lemma sty0_correct:
 167  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t: T).((sty0 g c
 168 t1 t) \to (ex T (\lambda (t2: T).(sty0 g c t t2)))))))
 169 \def
 170  \lambda (g: G).(\lambda (c: C).(\lambda (t1: T).(\lambda (t: T).(\lambda (H:
 171 (sty0 g c t1 t)).(sty0_ind g (\lambda (c0: C).(\lambda (_: T).(\lambda (t2:
 172 T).(ex T (\lambda (t3: T).(sty0 g c0 t2 t3)))))) (\lambda (c0: C).(\lambda
 173 (n: nat).(ex_intro T (\lambda (t2: T).(sty0 g c0 (TSort (next g n)) t2))
 174 (TSort (next g (next g n))) (sty0_sort g c0 (next g n))))) (\lambda (c0:
 175 C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (H0: (getl i c0
 176 (CHead d (Bind Abbr) v))).(\lambda (w: T).(\lambda (_: (sty0 g d v
 177 w)).(\lambda (H2: (ex T (\lambda (t2: T).(sty0 g d w t2)))).(let H3 \def H2
 178 in (ex_ind T (\lambda (t2: T).(sty0 g d w t2)) (ex T (\lambda (t2: T).(sty0 g
 179 c0 (lift (S i) O w) t2))) (\lambda (x: T).(\lambda (H4: (sty0 g d w
 180 x)).(ex_intro T (\lambda (t2: T).(sty0 g c0 (lift (S i) O w) t2)) (lift (S i)
 181 O x) (sty0_lift g d w x H4 c0 (S i) O (getl_drop Abbr c0 d v i H0)))))
 182 H3)))))))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i:
 183 nat).(\lambda (H0: (getl i c0 (CHead d (Bind Abst) v))).(\lambda (w:
 184 T).(\lambda (H1: (sty0 g d v w)).(\lambda (H2: (ex T (\lambda (t2: T).(sty0 g
 185 d w t2)))).(let H3 \def H2 in (ex_ind T (\lambda (t2: T).(sty0 g d w t2)) (ex
 186 T (\lambda (t2: T).(sty0 g c0 (lift (S i) O v) t2))) (\lambda (x: T).(\lambda
 187 (_: (sty0 g d w x)).(ex_intro T (\lambda (t2: T).(sty0 g c0 (lift (S i) O v)
 188 t2)) (lift (S i) O w) (sty0_lift g d v w H1 c0 (S i) O (getl_drop Abst c0 d v
 189 i H0))))) H3)))))))))) (\lambda (b: B).(\lambda (c0: C).(\lambda (v:
 190 T).(\lambda (t2: T).(\lambda (t3: T).(\lambda (_: (sty0 g (CHead c0 (Bind b)
 191 v) t2 t3)).(\lambda (H1: (ex T (\lambda (t4: T).(sty0 g (CHead c0 (Bind b) v)
 192 t3 t4)))).(let H2 \def H1 in (ex_ind T (\lambda (t4: T).(sty0 g (CHead c0
 193 (Bind b) v) t3 t4)) (ex T (\lambda (t4: T).(sty0 g c0 (THead (Bind b) v t3)
 194 t4))) (\lambda (x: T).(\lambda (H3: (sty0 g (CHead c0 (Bind b) v) t3
 195 x)).(ex_intro T (\lambda (t4: T).(sty0 g c0 (THead (Bind b) v t3) t4)) (THead
 196 (Bind b) v x) (sty0_bind g b c0 v t3 x H3)))) H2))))))))) (\lambda (c0:
 197 C).(\lambda (v: T).(\lambda (t2: T).(\lambda (t3: T).(\lambda (_: (sty0 g c0
 198 t2 t3)).(\lambda (H1: (ex T (\lambda (t4: T).(sty0 g c0 t3 t4)))).(let H2
 199 \def H1 in (ex_ind T (\lambda (t4: T).(sty0 g c0 t3 t4)) (ex T (\lambda (t4:
 200 T).(sty0 g c0 (THead (Flat Appl) v t3) t4))) (\lambda (x: T).(\lambda (H3:
 201 (sty0 g c0 t3 x)).(ex_intro T (\lambda (t4: T).(sty0 g c0 (THead (Flat Appl)
 202 v t3) t4)) (THead (Flat Appl) v x) (sty0_appl g c0 v t3 x H3)))) H2))))))))
 203 (\lambda (c0: C).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (sty0 g c0 v1
 204 v2)).(\lambda (H1: (ex T (\lambda (t2: T).(sty0 g c0 v2 t2)))).(\lambda (t2:
 205 T).(\lambda (t3: T).(\lambda (_: (sty0 g c0 t2 t3)).(\lambda (H3: (ex T
 206 (\lambda (t4: T).(sty0 g c0 t3 t4)))).(let H4 \def H1 in (ex_ind T (\lambda
 207 (t4: T).(sty0 g c0 v2 t4)) (ex T (\lambda (t4: T).(sty0 g c0 (THead (Flat
 208 Cast) v2 t3) t4))) (\lambda (x: T).(\lambda (H5: (sty0 g c0 v2 x)).(let H6
 209 \def H3 in (ex_ind T (\lambda (t4: T).(sty0 g c0 t3 t4)) (ex T (\lambda (t4:
 210 T).(sty0 g c0 (THead (Flat Cast) v2 t3) t4))) (\lambda (x0: T).(\lambda (H7:
 211 (sty0 g c0 t3 x0)).(ex_intro T (\lambda (t4: T).(sty0 g c0 (THead (Flat Cast)
 212 v2 t3) t4)) (THead (Flat Cast) x x0) (sty0_cast g c0 v2 x H5 t3 x0 H7))))
 213 H6)))) H4))))))))))) c t1 t H))))).
 214