matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clear/drop.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/clear/drop".
  18
  19 include "clear/fwd.ma".
  20
  21 include "drop/fwd.ma".
  22
  23 theorem drop_clear:
  24  \forall (c1: C).(\forall (c2: C).(\forall (i: nat).((drop (S i) O c1 c2) \to
  25 (ex2_3 B C T (\lambda (b: B).(\lambda (e: C).(\lambda (v: T).(clear c1 (CHead
  26 e (Bind b) v))))) (\lambda (_: B).(\lambda (e: C).(\lambda (_: T).(drop i O e
  27 c2))))))))
  28 \def
  29  \lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c2: C).(\forall (i:
  30 nat).((drop (S i) O c c2) \to (ex2_3 B C T (\lambda (b: B).(\lambda (e:
  31 C).(\lambda (v: T).(clear c (CHead e (Bind b) v))))) (\lambda (_: B).(\lambda
  32 (e: C).(\lambda (_: T).(drop i O e c2))))))))) (\lambda (n: nat).(\lambda
  33 (c2: C).(\lambda (i: nat).(\lambda (H: (drop (S i) O (CSort n) c2)).(and3_ind
  34 (eq C c2 (CSort n)) (eq nat (S i) O) (eq nat O O) (ex2_3 B C T (\lambda (b:
  35 B).(\lambda (e: C).(\lambda (v: T).(clear (CSort n) (CHead e (Bind b) v)))))
  36 (\lambda (_: B).(\lambda (e: C).(\lambda (_: T).(drop i O e c2))))) (\lambda
  37 (_: (eq C c2 (CSort n))).(\lambda (H1: (eq nat (S i) O)).(\lambda (_: (eq nat
  38 O O)).(let H3 \def (eq_ind nat (S i) (\lambda (ee: nat).(match ee in nat
  39 return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow
  40 True])) I O H1) in (False_ind (ex2_3 B C T (\lambda (b: B).(\lambda (e:
  41 C).(\lambda (v: T).(clear (CSort n) (CHead e (Bind b) v))))) (\lambda (_:
  42 B).(\lambda (e: C).(\lambda (_: T).(drop i O e c2))))) H3))))) (drop_gen_sort
  43 n (S i) O c2 H)))))) (\lambda (c: C).(\lambda (H: ((\forall (c2: C).(\forall
  44 (i: nat).((drop (S i) O c c2) \to (ex2_3 B C T (\lambda (b: B).(\lambda (e:
  45 C).(\lambda (v: T).(clear c (CHead e (Bind b) v))))) (\lambda (_: B).(\lambda
  46 (e: C).(\lambda (_: T).(drop i O e c2)))))))))).(\lambda (k: K).(\lambda (t:
  47 T).(\lambda (c2: C).(\lambda (i: nat).(\lambda (H0: (drop (S i) O (CHead c k
  48 t) c2)).((match k in K return (\lambda (k0: K).((drop (r k0 i) O c c2) \to
  49 (ex2_3 B C T (\lambda (b: B).(\lambda (e: C).(\lambda (v: T).(clear (CHead c
  50 k0 t) (CHead e (Bind b) v))))) (\lambda (_: B).(\lambda (e: C).(\lambda (_:
  51 T).(drop i O e c2))))))) with [(Bind b) \Rightarrow (\lambda (H1: (drop (r
  52 (Bind b) i) O c c2)).(ex2_3_intro B C T (\lambda (b0: B).(\lambda (e:
  53 C).(\lambda (v: T).(clear (CHead c (Bind b) t) (CHead e (Bind b0) v)))))
  54 (\lambda (_: B).(\lambda (e: C).(\lambda (_: T).(drop i O e c2)))) b c t
  55 (clear_bind b c t) H1)) | (Flat f) \Rightarrow (\lambda (H1: (drop (r (Flat
  56 f) i) O c c2)).(let H2 \def (H c2 i H1) in (ex2_3_ind B C T (\lambda (b:
  57 B).(\lambda (e: C).(\lambda (v: T).(clear c (CHead e (Bind b) v))))) (\lambda
  58 (_: B).(\lambda (e: C).(\lambda (_: T).(drop i O e c2)))) (ex2_3 B C T
  59 (\lambda (b: B).(\lambda (e: C).(\lambda (v: T).(clear (CHead c (Flat f) t)
  60 (CHead e (Bind b) v))))) (\lambda (_: B).(\lambda (e: C).(\lambda (_:
  61 T).(drop i O e c2))))) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2:
  62 T).(\lambda (H3: (clear c (CHead x1 (Bind x0) x2))).(\lambda (H4: (drop i O
  63 x1 c2)).(ex2_3_intro B C T (\lambda (b: B).(\lambda (e: C).(\lambda (v:
  64 T).(clear (CHead c (Flat f) t) (CHead e (Bind b) v))))) (\lambda (_:
  65 B).(\lambda (e: C).(\lambda (_: T).(drop i O e c2)))) x0 x1 x2 (clear_flat c
  66 (CHead x1 (Bind x0) x2) H3 f t) H4)))))) H2)))]) (drop_gen_drop k c c2 t i
  67 H0))))))))) c1).
  68
  69 theorem drop_clear_O:
  70  \forall (b: B).(\forall (c: C).(\forall (e1: C).(\forall (u: T).((clear c
  71 (CHead e1 (Bind b) u)) \to (\forall (e2: C).(\forall (i: nat).((drop i O e1
  72 e2) \to (drop (S i) O c e2))))))))
  73 \def
  74  \lambda (b: B).(\lambda (c: C).(C_ind (\lambda (c0: C).(\forall (e1:
  75 C).(\forall (u: T).((clear c0 (CHead e1 (Bind b) u)) \to (\forall (e2:
  76 C).(\forall (i: nat).((drop i O e1 e2) \to (drop (S i) O c0 e2))))))))
  77 (\lambda (n: nat).(\lambda (e1: C).(\lambda (u: T).(\lambda (H: (clear (CSort
  78 n) (CHead e1 (Bind b) u))).(\lambda (e2: C).(\lambda (i: nat).(\lambda (_:
  79 (drop i O e1 e2)).(clear_gen_sort (CHead e1 (Bind b) u) n H (drop (S i) O
  80 (CSort n) e2))))))))) (\lambda (c0: C).(\lambda (H: ((\forall (e1:
  81 C).(\forall (u: T).((clear c0 (CHead e1 (Bind b) u)) \to (\forall (e2:
  82 C).(\forall (i: nat).((drop i O e1 e2) \to (drop (S i) O c0
  83 e2))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (e1: C).(\lambda (u:
  84 T).(\lambda (H0: (clear (CHead c0 k t) (CHead e1 (Bind b) u))).(\lambda (e2:
  85 C).(\lambda (i: nat).(\lambda (H1: (drop i O e1 e2)).((match k in K return
  86 (\lambda (k0: K).((clear (CHead c0 k0 t) (CHead e1 (Bind b) u)) \to (drop (S
  87 i) O (CHead c0 k0 t) e2))) with [(Bind b0) \Rightarrow (\lambda (H2: (clear
  88 (CHead c0 (Bind b0) t) (CHead e1 (Bind b) u))).(let H3 \def (f_equal C C
  89 (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
  90 \Rightarrow e1 | (CHead c _ _) \Rightarrow c])) (CHead e1 (Bind b) u) (CHead
  91 c0 (Bind b0) t) (clear_gen_bind b0 c0 (CHead e1 (Bind b) u) t H2)) in ((let
  92 H4 \def (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_: C).B)
  93 with [(CSort _) \Rightarrow b | (CHead _ k _) \Rightarrow (match k in K
  94 return (\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow
  95 b])])) (CHead e1 (Bind b) u) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0
  96 (CHead e1 (Bind b) u) t H2)) in ((let H5 \def (f_equal C T (\lambda (e:
  97 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
  98 (CHead _ _ t) \Rightarrow t])) (CHead e1 (Bind b) u) (CHead c0 (Bind b0) t)
  99 (clear_gen_bind b0 c0 (CHead e1 (Bind b) u) t H2)) in (\lambda (H6: (eq B b
 100 b0)).(\lambda (H7: (eq C e1 c0)).(let H8 \def (eq_ind C e1 (\lambda (c:
 101 C).(drop i O c e2)) H1 c0 H7) in (eq_ind B b (\lambda (b1: B).(drop (S i) O
 102 (CHead c0 (Bind b1) t) e2)) (drop_drop (Bind b) i c0 e2 H8 t) b0 H6))))) H4))
 103 H3))) | (Flat f) \Rightarrow (\lambda (H2: (clear (CHead c0 (Flat f) t)
 104 (CHead e1 (Bind b) u))).(drop_drop (Flat f) i c0 e2 (H e1 u (clear_gen_flat f
 105 c0 (CHead e1 (Bind b) u) t H2) e2 i H1) t))]) H0))))))))))) c)).
 106
 107 theorem drop_clear_S:
 108  \forall (x2: C).(\forall (x1: C).(\forall (h: nat).(\forall (d: nat).((drop
 109 h (S d) x1 x2) \to (\forall (b: B).(\forall (c2: C).(\forall (u: T).((clear
 110 x2 (CHead c2 (Bind b) u)) \to (ex2 C (\lambda (c1: C).(clear x1 (CHead c1
 111 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 c2)))))))))))
 112 \def
 113  \lambda (x2: C).(C_ind (\lambda (c: C).(\forall (x1: C).(\forall (h:
 114 nat).(\forall (d: nat).((drop h (S d) x1 c) \to (\forall (b: B).(\forall (c2:
 115 C).(\forall (u: T).((clear c (CHead c2 (Bind b) u)) \to (ex2 C (\lambda (c1:
 116 C).(clear x1 (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1
 117 c2)))))))))))) (\lambda (n: nat).(\lambda (x1: C).(\lambda (h: nat).(\lambda
 118 (d: nat).(\lambda (_: (drop h (S d) x1 (CSort n))).(\lambda (b: B).(\lambda
 119 (c2: C).(\lambda (u: T).(\lambda (H0: (clear (CSort n) (CHead c2 (Bind b)
 120 u))).(clear_gen_sort (CHead c2 (Bind b) u) n H0 (ex2 C (\lambda (c1:
 121 C).(clear x1 (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1
 122 c2))))))))))))) (\lambda (c: C).(\lambda (H: ((\forall (x1: C).(\forall (h:
 123 nat).(\forall (d: nat).((drop h (S d) x1 c) \to (\forall (b: B).(\forall (c2:
 124 C).(\forall (u: T).((clear c (CHead c2 (Bind b) u)) \to (ex2 C (\lambda (c1:
 125 C).(clear x1 (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1
 126 c2))))))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (x1: C).(\lambda (h:
 127 nat).(\lambda (d: nat).(\lambda (H0: (drop h (S d) x1 (CHead c k
 128 t))).(\lambda (b: B).(\lambda (c2: C).(\lambda (u: T).(\lambda (H1: (clear
 129 (CHead c k t) (CHead c2 (Bind b) u))).(ex2_ind C (\lambda (e: C).(eq C x1
 130 (CHead e k (lift h (r k d) t)))) (\lambda (e: C).(drop h (r k d) e c)) (ex2 C
 131 (\lambda (c1: C).(clear x1 (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1:
 132 C).(drop h d c1 c2))) (\lambda (x: C).(\lambda (H2: (eq C x1 (CHead x k (lift
 133 h (r k d) t)))).(\lambda (H3: (drop h (r k d) x c)).(eq_ind_r C (CHead x k
 134 (lift h (r k d) t)) (\lambda (c0: C).(ex2 C (\lambda (c1: C).(clear c0 (CHead
 135 c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 c2)))) ((match k in
 136 K return (\lambda (k0: K).((clear (CHead c k0 t) (CHead c2 (Bind b) u)) \to
 137 ((drop h (r k0 d) x c) \to (ex2 C (\lambda (c1: C).(clear (CHead x k0 (lift h
 138 (r k0 d) t)) (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1
 139 c2)))))) with [(Bind b0) \Rightarrow (\lambda (H4: (clear (CHead c (Bind b0)
 140 t) (CHead c2 (Bind b) u))).(\lambda (H5: (drop h (r (Bind b0) d) x c)).(let
 141 H6 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C)
 142 with [(CSort _) \Rightarrow c2 | (CHead c _ _) \Rightarrow c])) (CHead c2
 143 (Bind b) u) (CHead c (Bind b0) t) (clear_gen_bind b0 c (CHead c2 (Bind b) u)
 144 t H4)) in ((let H7 \def (f_equal C B (\lambda (e: C).(match e in C return
 145 (\lambda (_: C).B) with [(CSort _) \Rightarrow b | (CHead _ k _) \Rightarrow
 146 (match k in K return (\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat
 147 _) \Rightarrow b])])) (CHead c2 (Bind b) u) (CHead c (Bind b0) t)
 148 (clear_gen_bind b0 c (CHead c2 (Bind b) u) t H4)) in ((let H8 \def (f_equal C
 149 T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _)
 150 \Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead c2 (Bind b) u) (CHead c
 151 (Bind b0) t) (clear_gen_bind b0 c (CHead c2 (Bind b) u) t H4)) in (\lambda
 152 (H9: (eq B b b0)).(\lambda (H10: (eq C c2 c)).(eq_ind_r T t (\lambda (t0:
 153 T).(ex2 C (\lambda (c1: C).(clear (CHead x (Bind b0) (lift h (r (Bind b0) d)
 154 t)) (CHead c1 (Bind b) (lift h d t0)))) (\lambda (c1: C).(drop h d c1 c2))))
 155 (eq_ind_r C c (\lambda (c0: C).(ex2 C (\lambda (c1: C).(clear (CHead x (Bind
 156 b0) (lift h (r (Bind b0) d) t)) (CHead c1 (Bind b) (lift h d t)))) (\lambda
 157 (c1: C).(drop h d c1 c0)))) (eq_ind_r B b0 (\lambda (b1: B).(ex2 C (\lambda
 158 (c1: C).(clear (CHead x (Bind b0) (lift h (r (Bind b0) d) t)) (CHead c1 (Bind
 159 b1) (lift h d t)))) (\lambda (c1: C).(drop h d c1 c)))) (ex_intro2 C (\lambda
 160 (c1: C).(clear (CHead x (Bind b0) (lift h (r (Bind b0) d) t)) (CHead c1 (Bind
 161 b0) (lift h d t)))) (\lambda (c1: C).(drop h d c1 c)) x (clear_bind b0 x
 162 (lift h d t)) H5) b H9) c2 H10) u H8)))) H7)) H6)))) | (Flat f) \Rightarrow
 163 (\lambda (H4: (clear (CHead c (Flat f) t) (CHead c2 (Bind b) u))).(\lambda
 164 (H5: (drop h (r (Flat f) d) x c)).(let H6 \def (H x h d H5 b c2 u
 165 (clear_gen_flat f c (CHead c2 (Bind b) u) t H4)) in (ex2_ind C (\lambda (c1:
 166 C).(clear x (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1
 167 c2)) (ex2 C (\lambda (c1: C).(clear (CHead x (Flat f) (lift h (r (Flat f) d)
 168 t)) (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 c2)))
 169 (\lambda (x0: C).(\lambda (H7: (clear x (CHead x0 (Bind b) (lift h d
 170 u)))).(\lambda (H8: (drop h d x0 c2)).(ex_intro2 C (\lambda (c1: C).(clear
 171 (CHead x (Flat f) (lift h (r (Flat f) d) t)) (CHead c1 (Bind b) (lift h d
 172 u)))) (\lambda (c1: C).(drop h d c1 c2)) x0 (clear_flat x (CHead x0 (Bind b)
 173 (lift h d u)) H7 f (lift h (r (Flat f) d) t)) H8)))) H6))))]) H1 H3) x1
 174 H2)))) (drop_gen_skip_r c x1 t h d k H0)))))))))))))) x2).
 175