matita/matita/contribs/lambdadelta/basic_1A/tlt/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_1A/T/fwd.ma".
  18
  19 include "basic_1A/tlt/defs.ma".
  20
  21 lemma wadd_le:
  22  \forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n:
  23 nat).(le (f n) (g n)))) \to (\forall (v: nat).(\forall (w: nat).((le v w) \to
  24 (\forall (n: nat).(le (wadd f v n) (wadd g w n))))))))
  25 \def
  26  \lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H:
  27 ((\forall (n: nat).(le (f n) (g n))))).(\lambda (v: nat).(\lambda (w:
  28 nat).(\lambda (H0: (le v w)).(\lambda (n: nat).(nat_ind (\lambda (n0:
  29 nat).(le (wadd f v n0) (wadd g w n0))) H0 (\lambda (n0: nat).(\lambda (_: (le
  30 (wadd f v n0) (wadd g w n0))).(H n0))) n))))))).
  31
  32 lemma wadd_lt:
  33  \forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n:
  34 nat).(le (f n) (g n)))) \to (\forall (v: nat).(\forall (w: nat).((lt v w) \to
  35 (\forall (n: nat).(le (wadd f v n) (wadd g w n))))))))
  36 \def
  37  \lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H:
  38 ((\forall (n: nat).(le (f n) (g n))))).(\lambda (v: nat).(\lambda (w:
  39 nat).(\lambda (H0: (lt v w)).(\lambda (n: nat).(nat_ind (\lambda (n0:
  40 nat).(le (wadd f v n0) (wadd g w n0))) (le_S_n v w (le_S_n (S v) (S w) (le_S
  41 (S (S v)) (S w) (le_n_S (S v) w H0)))) (\lambda (n0: nat).(\lambda (_: (le
  42 (wadd f v n0) (wadd g w n0))).(H n0))) n))))))).
  43
  44 lemma wadd_O:
  45  \forall (n: nat).(eq nat (wadd (\lambda (_: nat).O) O n) O)
  46 \def
  47  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat (wadd (\lambda (_:
  48 nat).O) O n0) O)) (refl_equal nat O) (\lambda (n0: nat).(\lambda (_: (eq nat
  49 (wadd (\lambda (_: nat).O) O n0) O)).(refl_equal nat O))) n).
  50
  51 lemma weight_le:
  52  \forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
  53 nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t)
  54 (weight_map g t)))))
  55 \def
  56  \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (f: ((nat \to
  57 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
  58 \to (le (weight_map f t0) (weight_map g t0)))))) (\lambda (n: nat).(\lambda
  59 (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (_: ((\forall
  60 (n0: nat).(le (f n0) (g n0))))).(le_O_n (weight_map g (TSort n)))))))
  61 (\lambda (n: nat).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
  62 nat))).(\lambda (H: ((\forall (n0: nat).(le (f n0) (g n0))))).(H n)))))
  63 (\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t0: T).(((\forall (f: ((nat
  64 \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g
  65 n)))) \to (le (weight_map f t0) (weight_map g t0)))))) \to (\forall (t1:
  66 T).(((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
  67 (n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g t1))))))
  68 \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
  69 (n: nat).(le (f n) (g n)))) \to (le (weight_map f (THead k0 t0 t1))
  70 (weight_map g (THead k0 t0 t1))))))))))) (\lambda (b: B).(B_ind (\lambda (b0:
  71 B).(\forall (t0: T).(((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
  72 nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t0)
  73 (weight_map g t0)))))) \to (\forall (t1: T).(((\forall (f: ((nat \to
  74 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
  75 \to (le (weight_map f t1) (weight_map g t1)))))) \to (\forall (f: ((nat \to
  76 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
  77 \to (le (match b0 with [Abbr \Rightarrow (S (plus (weight_map f t0)
  78 (weight_map (wadd f (S (weight_map f t0))) t1))) | Abst \Rightarrow (S (plus
  79 (weight_map f t0) (weight_map (wadd f O) t1))) | Void \Rightarrow (S (plus
  80 (weight_map f t0) (weight_map (wadd f O) t1)))]) (match b0 with [Abbr
  81 \Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g (S (weight_map g
  82 t0))) t1))) | Abst \Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g
  83 O) t1))) | Void \Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g O)
  84 t1)))])))))))))) (\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to
  85 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
  86 \to (le (weight_map f t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda
  87 (H0: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
  88 (n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g
  89 t1))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
  90 nat))).(\lambda (H1: ((\forall (n: nat).(le (f n) (g n))))).(le_n_S (plus
  91 (weight_map f t0) (weight_map (wadd f (S (weight_map f t0))) t1)) (plus
  92 (weight_map g t0) (weight_map (wadd g (S (weight_map g t0))) t1))
  93 (le_plus_plus (weight_map f t0) (weight_map g t0) (weight_map (wadd f (S
  94 (weight_map f t0))) t1) (weight_map (wadd g (S (weight_map g t0))) t1) (H f g
  95 H1) (H0 (wadd f (S (weight_map f t0))) (wadd g (S (weight_map g t0)))
  96 (\lambda (n: nat).(wadd_le f g H1 (S (weight_map f t0)) (S (weight_map g t0))
  97 (le_n_S (weight_map f t0) (weight_map g t0) (H f g H1)) n))))))))))))
  98 (\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to nat))).(\forall (g:
  99 ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f
 100 t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f:
 101 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n)
 102 (g n)))) \to (le (weight_map f t1) (weight_map g t1))))))).(\lambda (f: ((nat
 103 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: nat).(le
 104 (f n) (g n))))).(le_n_S (plus (weight_map f t0) (weight_map (wadd f O) t1))
 105 (plus (weight_map g t0) (weight_map (wadd g O) t1)) (le_plus_plus (weight_map
 106 f t0) (weight_map g t0) (weight_map (wadd f O) t1) (weight_map (wadd g O) t1)
 107 (H f g H1) (H0 (wadd f O) (wadd g O) (\lambda (n: nat).(wadd_le f g H1 O O
 108 (le_O_n O) n)))))))))))) (\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat
 109 \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g
 110 n)))) \to (le (weight_map f t0) (weight_map g t0))))))).(\lambda (t1:
 111 T).(\lambda (H0: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
 112 nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t1)
 113 (weight_map g t1))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
 114 nat))).(\lambda (H1: ((\forall (n: nat).(le (f n) (g n))))).(le_n_S (plus
 115 (weight_map f t0) (weight_map (wadd f O) t1)) (plus (weight_map g t0)
 116 (weight_map (wadd g O) t1)) (le_plus_plus (weight_map f t0) (weight_map g t0)
 117 (weight_map (wadd f O) t1) (weight_map (wadd g O) t1) (H f g H1) (H0 (wadd f
 118 O) (wadd g O) (\lambda (n: nat).(wadd_le f g H1 O O (le_O_n O) n))))))))))))
 119 b)) (\lambda (_: F).(\lambda (t0: T).(\lambda (H: ((\forall (f0: ((nat \to
 120 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f0 n) (g n))))
 121 \to (le (weight_map f0 t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda
 122 (H0: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
 123 (n: nat).(le (f0 n) (g n)))) \to (le (weight_map f0 t1) (weight_map g
 124 t1))))))).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat \to
 125 nat))).(\lambda (H1: ((\forall (n: nat).(le (f0 n) (g n))))).(le_n_S (plus
 126 (weight_map f0 t0) (weight_map f0 t1)) (plus (weight_map g t0) (weight_map g
 127 t1)) (le_plus_plus (weight_map f0 t0) (weight_map g t0) (weight_map f0 t1)
 128 (weight_map g t1) (H f0 g H1) (H0 f0 g H1))))))))))) k)) t).
 129
 130 lemma weight_eq:
 131  \forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
 132 nat))).(((\forall (n: nat).(eq nat (f n) (g n)))) \to (eq nat (weight_map f
 133 t) (weight_map g t)))))
 134 \def
 135  \lambda (t: T).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
 136 nat))).(\lambda (H: ((\forall (n: nat).(eq nat (f n) (g n))))).(le_antisym
 137 (weight_map f t) (weight_map g t) (weight_le t f g (\lambda (n:
 138 nat).(eq_ind_r nat (g n) (\lambda (n0: nat).(le n0 (g n))) (le_n (g n)) (f n)
 139 (H n)))) (weight_le t g f (\lambda (n: nat).(eq_ind_r nat (g n) (\lambda (n0:
 140 nat).(le (g n) n0)) (le_n (g n)) (f n) (H n)))))))).
 141
 142 lemma weight_add_O:
 143  \forall (t: T).(eq nat (weight_map (wadd (\lambda (_: nat).O) O) t)
 144 (weight_map (\lambda (_: nat).O) t))
 145 \def
 146  \lambda (t: T).(weight_eq t (wadd (\lambda (_: nat).O) O) (\lambda (_:
 147 nat).O) (\lambda (n: nat).(wadd_O n))).
 148
 149 lemma weight_add_S:
 150  \forall (t: T).(\forall (m: nat).(le (weight_map (wadd (\lambda (_: nat).O)
 151 O) t) (weight_map (wadd (\lambda (_: nat).O) (S m)) t)))
 152 \def
 153  \lambda (t: T).(\lambda (m: nat).(weight_le t (wadd (\lambda (_: nat).O) O)
 154 (wadd (\lambda (_: nat).O) (S m)) (\lambda (n: nat).(wadd_le (\lambda (_:
 155 nat).O) (\lambda (_: nat).O) (\lambda (_: nat).(le_O_n O)) O (S m) (le_O_n (S
 156 m)) n)))).
 157
 158 theorem tlt_trans:
 159  \forall (v: T).(\forall (u: T).(\forall (t: T).((tlt u v) \to ((tlt v t) \to
 160 (tlt u t)))))
 161 \def
 162  \lambda (v: T).(\lambda (u: T).(\lambda (t: T).(\lambda (H: (lt (weight u)
 163 (weight v))).(\lambda (H0: (lt (weight v) (weight t))).(lt_trans (weight u)
 164 (weight v) (weight t) H H0))))).
 165
 166 lemma tlt_head_sx:
 167  \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt u (THead k u t))))
 168 \def
 169  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (t: T).(lt
 170 (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) (THead
 171 k0 u t)))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (u: T).(\forall
 172 (t: T).(lt (weight_map (\lambda (_: nat).O) u) (match b0 with [Abbr
 173 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
 174 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) | Abst
 175 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
 176 (\lambda (_: nat).O) O) t))) | Void \Rightarrow (S (plus (weight_map (\lambda
 177 (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)))]))))) (\lambda
 178 (u: T).(\lambda (t: T).(le_n_S (weight_map (\lambda (_: nat).O) u) (plus
 179 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S
 180 (weight_map (\lambda (_: nat).O) u))) t)) (le_plus_l (weight_map (\lambda (_:
 181 nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_:
 182 nat).O) u))) t))))) (\lambda (u: T).(\lambda (t: T).(le_n_S (weight_map
 183 (\lambda (_: nat).O) u) (plus (weight_map (\lambda (_: nat).O) u) (weight_map
 184 (wadd (\lambda (_: nat).O) O) t)) (le_plus_l (weight_map (\lambda (_: nat).O)
 185 u) (weight_map (wadd (\lambda (_: nat).O) O) t))))) (\lambda (u: T).(\lambda
 186 (t: T).(le_n_S (weight_map (\lambda (_: nat).O) u) (plus (weight_map (\lambda
 187 (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)) (le_plus_l
 188 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O)
 189 t))))) b)) (\lambda (_: F).(\lambda (u: T).(\lambda (t: T).(le_n_S
 190 (weight_map (\lambda (_: nat).O) u) (plus (weight_map (\lambda (_: nat).O) u)
 191 (weight_map (\lambda (_: nat).O) t)) (le_plus_l (weight_map (\lambda (_:
 192 nat).O) u) (weight_map (\lambda (_: nat).O) t)))))) k).
 193
 194 lemma tlt_head_dx:
 195  \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt t (THead k u t))))
 196 \def
 197  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (t: T).(lt
 198 (weight_map (\lambda (_: nat).O) t) (weight_map (\lambda (_: nat).O) (THead
 199 k0 u t)))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (u: T).(\forall
 200 (t: T).(lt (weight_map (\lambda (_: nat).O) t) (match b0 with [Abbr
 201 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
 202 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) | Abst
 203 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
 204 (\lambda (_: nat).O) O) t))) | Void \Rightarrow (S (plus (weight_map (\lambda
 205 (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)))]))))) (\lambda
 206 (u: T).(\lambda (t: T).(lt_le_trans (weight_map (\lambda (_: nat).O) t) (S
 207 (weight_map (\lambda (_: nat).O) t)) (S (plus (weight_map (\lambda (_:
 208 nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_:
 209 nat).O) u))) t))) (lt_n_Sn (weight_map (\lambda (_: nat).O) t)) (le_n_S
 210 (weight_map (\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u)
 211 (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O)
 212 u))) t)) (le_trans (weight_map (\lambda (_: nat).O) t) (weight_map (wadd
 213 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t) (plus
 214 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S
 215 (weight_map (\lambda (_: nat).O) u))) t)) (eq_ind nat (weight_map (wadd
 216 (\lambda (_: nat).O) O) t) (\lambda (n: nat).(le n (weight_map (wadd (\lambda
 217 (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) (weight_add_S t
 218 (weight_map (\lambda (_: nat).O) u)) (weight_map (\lambda (_: nat).O) t)
 219 (weight_add_O t)) (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map
 220 (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t)))))))
 221 (\lambda (u: T).(\lambda (t: T).(eq_ind_r nat (weight_map (\lambda (_:
 222 nat).O) t) (\lambda (n: nat).(lt (weight_map (\lambda (_: nat).O) t) (S (plus
 223 (weight_map (\lambda (_: nat).O) u) n)))) (le_n_S (weight_map (\lambda (_:
 224 nat).O) t) (plus (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_:
 225 nat).O) t)) (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map
 226 (\lambda (_: nat).O) t))) (weight_map (wadd (\lambda (_: nat).O) O) t)
 227 (weight_add_O t)))) (\lambda (u: T).(\lambda (t: T).(eq_ind_r nat (weight_map
 228 (\lambda (_: nat).O) t) (\lambda (n: nat).(lt (weight_map (\lambda (_:
 229 nat).O) t) (S (plus (weight_map (\lambda (_: nat).O) u) n)))) (le_n_S
 230 (weight_map (\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u)
 231 (weight_map (\lambda (_: nat).O) t)) (le_plus_r (weight_map (\lambda (_:
 232 nat).O) u) (weight_map (\lambda (_: nat).O) t))) (weight_map (wadd (\lambda
 233 (_: nat).O) O) t) (weight_add_O t)))) b)) (\lambda (_: F).(\lambda (u:
 234 T).(\lambda (t: T).(le_n_S (weight_map (\lambda (_: nat).O) t) (plus
 235 (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t))
 236 (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_:
 237 nat).O) t)))))) k).
 238