matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/clear.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/getl/clear".
  18
  19 include "getl/props.ma".
  20
  21 include "clear/drop.ma".
  22
  23 theorem clear_getl_trans:
  24  \forall (i: nat).(\forall (c2: C).(\forall (c3: C).((getl i c2 c3) \to
  25 (\forall (c1: C).((clear c1 c2) \to (getl i c1 c3))))))
  26 \def
  27  \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c2: C).(\forall (c3:
  28 C).((getl n c2 c3) \to (\forall (c1: C).((clear c1 c2) \to (getl n c1
  29 c3))))))) (\lambda (c2: C).(\lambda (c3: C).(\lambda (H: (getl O c2
  30 c3)).(\lambda (c1: C).(\lambda (H0: (clear c1 c2)).(getl_intro O c1 c3 c1
  31 (drop_refl c1) (clear_trans c1 c2 H0 c3 (getl_gen_O c2 c3 H)))))))) (\lambda
  32 (n: nat).(\lambda (_: ((\forall (c2: C).(\forall (c3: C).((getl n c2 c3) \to
  33 (\forall (c1: C).((clear c1 c2) \to (getl n c1 c3)))))))).(\lambda (c2:
  34 C).(C_ind (\lambda (c: C).(\forall (c3: C).((getl (S n) c c3) \to (\forall
  35 (c1: C).((clear c1 c) \to (getl (S n) c1 c3)))))) (\lambda (n0: nat).(\lambda
  36 (c3: C).(\lambda (H0: (getl (S n) (CSort n0) c3)).(\lambda (c1: C).(\lambda
  37 (_: (clear c1 (CSort n0))).(getl_gen_sort n0 (S n) c3 H0 (getl (S n) c1
  38 c3))))))) (\lambda (c: C).(\lambda (_: ((\forall (c3: C).((getl (S n) c c3)
  39 \to (\forall (c1: C).((clear c1 c) \to (getl (S n) c1 c3))))))).(\lambda (k:
  40 K).(\lambda (t: T).(\lambda (c3: C).(\lambda (H1: (getl (S n) (CHead c k t)
  41 c3)).(\lambda (c1: C).(\lambda (H2: (clear c1 (CHead c k t))).((match k in K
  42 return (\lambda (k0: K).((getl (S n) (CHead c k0 t) c3) \to ((clear c1 (CHead
  43 c k0 t)) \to (getl (S n) c1 c3)))) with [(Bind b) \Rightarrow (\lambda (H3:
  44 (getl (S n) (CHead c (Bind b) t) c3)).(\lambda (H4: (clear c1 (CHead c (Bind
  45 b) t))).(let H5 \def (getl_gen_all c c3 (r (Bind b) n) (getl_gen_S (Bind b) c
  46 c3 t n H3)) in (ex2_ind C (\lambda (e: C).(drop n O c e)) (\lambda (e:
  47 C).(clear e c3)) (getl (S n) c1 c3) (\lambda (x: C).(\lambda (H6: (drop n O c
  48 x)).(\lambda (H7: (clear x c3)).(getl_intro (S n) c1 c3 x (drop_clear_O b c1
  49 c t H4 x n H6) H7)))) H5)))) | (Flat f) \Rightarrow (\lambda (_: (getl (S n)
  50 (CHead c (Flat f) t) c3)).(\lambda (H4: (clear c1 (CHead c (Flat f)
  51 t))).(clear_gen_flat_r f c1 c t H4 (getl (S n) c1 c3))))]) H1 H2)))))))))
  52 c2)))) i).
  53
  54 theorem getl_clear_trans:
  55  \forall (i: nat).(\forall (c1: C).(\forall (c2: C).((getl i c1 c2) \to
  56 (\forall (c3: C).((clear c2 c3) \to (getl i c1 c3))))))
  57 \def
  58  \lambda (i: nat).(\lambda (c1: C).(\lambda (c2: C).(\lambda (H: (getl i c1
  59 c2)).(\lambda (c3: C).(\lambda (H0: (clear c2 c3)).(let H1 \def (getl_gen_all
  60 c1 c2 i H) in (ex2_ind C (\lambda (e: C).(drop i O c1 e)) (\lambda (e:
  61 C).(clear e c2)) (getl i c1 c3) (\lambda (x: C).(\lambda (H2: (drop i O c1
  62 x)).(\lambda (H3: (clear x c2)).(let H4 \def (clear_gen_all x c2 H3) in
  63 (ex_3_ind B C T (\lambda (b: B).(\lambda (e: C).(\lambda (u: T).(eq C c2
  64 (CHead e (Bind b) u))))) (getl i c1 c3) (\lambda (x0: B).(\lambda (x1:
  65 C).(\lambda (x2: T).(\lambda (H5: (eq C c2 (CHead x1 (Bind x0) x2))).(let H6
  66 \def (eq_ind C c2 (\lambda (c: C).(clear x c)) H3 (CHead x1 (Bind x0) x2) H5)
  67 in (let H7 \def (eq_ind C c2 (\lambda (c: C).(clear c c3)) H0 (CHead x1 (Bind
  68 x0) x2) H5) in (eq_ind_r C (CHead x1 (Bind x0) x2) (\lambda (c: C).(getl i c1
  69 c)) (getl_intro i c1 (CHead x1 (Bind x0) x2) x H2 H6) c3 (clear_gen_bind x0
  70 x1 c3 x2 H7)))))))) H4))))) H1))))))).
  71
  72 theorem getl_clear_bind:
  73  \forall (b: B).(\forall (c: C).(\forall (e1: C).(\forall (v: T).((clear c
  74 (CHead e1 (Bind b) v)) \to (\forall (e2: C).(\forall (n: nat).((getl n e1 e2)
  75 \to (getl (S n) c e2))))))))
  76 \def
  77  \lambda (b: B).(\lambda (c: C).(C_ind (\lambda (c0: C).(\forall (e1:
  78 C).(\forall (v: T).((clear c0 (CHead e1 (Bind b) v)) \to (\forall (e2:
  79 C).(\forall (n: nat).((getl n e1 e2) \to (getl (S n) c0 e2)))))))) (\lambda
  80 (n: nat).(\lambda (e1: C).(\lambda (v: T).(\lambda (H: (clear (CSort n)
  81 (CHead e1 (Bind b) v))).(\lambda (e2: C).(\lambda (n0: nat).(\lambda (_:
  82 (getl n0 e1 e2)).(clear_gen_sort (CHead e1 (Bind b) v) n H (getl (S n0)
  83 (CSort n) e2))))))))) (\lambda (c0: C).(\lambda (H: ((\forall (e1:
  84 C).(\forall (v: T).((clear c0 (CHead e1 (Bind b) v)) \to (\forall (e2:
  85 C).(\forall (n: nat).((getl n e1 e2) \to (getl (S n) c0 e2))))))))).(\lambda
  86 (k: K).(\lambda (t: T).(\lambda (e1: C).(\lambda (v: T).(\lambda (H0: (clear
  87 (CHead c0 k t) (CHead e1 (Bind b) v))).(\lambda (e2: C).(\lambda (n:
  88 nat).(\lambda (H1: (getl n e1 e2)).((match k in K return (\lambda (k0:
  89 K).((clear (CHead c0 k0 t) (CHead e1 (Bind b) v)) \to (getl (S n) (CHead c0
  90 k0 t) e2))) with [(Bind b0) \Rightarrow (\lambda (H2: (clear (CHead c0 (Bind
  91 b0) t) (CHead e1 (Bind b) v))).(let H3 \def (f_equal C C (\lambda (e:
  92 C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow e1 |
  93 (CHead c _ _) \Rightarrow c])) (CHead e1 (Bind b) v) (CHead c0 (Bind b0) t)
  94 (clear_gen_bind b0 c0 (CHead e1 (Bind b) v) t H2)) in ((let H4 \def (f_equal
  95 C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with [(CSort _)
  96 \Rightarrow b | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_:
  97 K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow b])])) (CHead e1
  98 (Bind b) v) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0 (CHead e1 (Bind b)
  99 v) t H2)) in ((let H5 \def (f_equal C T (\lambda (e: C).(match e in C return
 100 (\lambda (_: C).T) with [(CSort _) \Rightarrow v | (CHead _ _ t) \Rightarrow
 101 t])) (CHead e1 (Bind b) v) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0
 102 (CHead e1 (Bind b) v) t H2)) in (\lambda (H6: (eq B b b0)).(\lambda (H7: (eq
 103 C e1 c0)).(let H8 \def (eq_ind C e1 (\lambda (c: C).(getl n c e2)) H1 c0 H7)
 104 in (eq_ind B b (\lambda (b1: B).(getl (S n) (CHead c0 (Bind b1) t) e2))
 105 (getl_head (Bind b) n c0 e2 H8 t) b0 H6))))) H4)) H3))) | (Flat f)
 106 \Rightarrow (\lambda (H2: (clear (CHead c0 (Flat f) t) (CHead e1 (Bind b)
 107 v))).(getl_flat c0 e2 (S n) (H e1 v (clear_gen_flat f c0 (CHead e1 (Bind b)
 108 v) t H2) e2 n H1) f t))]) H0))))))))))) c)).
 109