matita/matita/contribs/lambdadelta/basic_1/lift1/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/lift1/defs.ma".
  18
  19 include "basic_1/lift/props.ma".
  20
  21 lemma lift1_sort:
  22  \forall (n: nat).(\forall (is: PList).(eq T (lift1 is (TSort n)) (TSort n)))
  23 \def
  24  \lambda (n: nat).(\lambda (is: PList).(PList_ind (\lambda (p: PList).(eq T
  25 (lift1 p (TSort n)) (TSort n))) (refl_equal T (TSort n)) (\lambda (n0:
  26 nat).(\lambda (n1: nat).(\lambda (p: PList).(\lambda (H: (eq T (lift1 p
  27 (TSort n)) (TSort n))).(eq_ind_r T (TSort n) (\lambda (t: T).(eq T (lift n0
  28 n1 t) (TSort n))) (refl_equal T (TSort n)) (lift1 p (TSort n)) H))))) is)).
  29
  30 lemma lift1_lref:
  31  \forall (hds: PList).(\forall (i: nat).(eq T (lift1 hds (TLRef i)) (TLRef
  32 (trans hds i))))
  33 \def
  34  \lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall (i: nat).(eq T
  35 (lift1 p (TLRef i)) (TLRef (trans p i))))) (\lambda (i: nat).(refl_equal T
  36 (TLRef i))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda
  37 (H: ((\forall (i: nat).(eq T (lift1 p (TLRef i)) (TLRef (trans p
  38 i)))))).(\lambda (i: nat).(eq_ind_r T (TLRef (trans p i)) (\lambda (t: T).(eq
  39 T (lift n n0 t) (TLRef (match (blt (trans p i) n0) with [true \Rightarrow
  40 (trans p i) | false \Rightarrow (plus (trans p i) n)])))) (refl_equal T
  41 (TLRef (match (blt (trans p i) n0) with [true \Rightarrow (trans p i) | false
  42 \Rightarrow (plus (trans p i) n)]))) (lift1 p (TLRef i)) (H i))))))) hds).
  43
  44 lemma lift1_bind:
  45  \forall (b: B).(\forall (hds: PList).(\forall (u: T).(\forall (t: T).(eq T
  46 (lift1 hds (THead (Bind b) u t)) (THead (Bind b) (lift1 hds u) (lift1 (Ss
  47 hds) t))))))
  48 \def
  49  \lambda (b: B).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall
  50 (u: T).(\forall (t: T).(eq T (lift1 p (THead (Bind b) u t)) (THead (Bind b)
  51 (lift1 p u) (lift1 (Ss p) t)))))) (\lambda (u: T).(\lambda (t: T).(refl_equal
  52 T (THead (Bind b) u t)))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p:
  53 PList).(\lambda (H: ((\forall (u: T).(\forall (t: T).(eq T (lift1 p (THead
  54 (Bind b) u t)) (THead (Bind b) (lift1 p u) (lift1 (Ss p) t))))))).(\lambda
  55 (u: T).(\lambda (t: T).(eq_ind_r T (THead (Bind b) (lift1 p u) (lift1 (Ss p)
  56 t)) (\lambda (t0: T).(eq T (lift n n0 t0) (THead (Bind b) (lift n n0 (lift1 p
  57 u)) (lift n (S n0) (lift1 (Ss p) t))))) (eq_ind_r T (THead (Bind b) (lift n
  58 n0 (lift1 p u)) (lift n (S n0) (lift1 (Ss p) t))) (\lambda (t0: T).(eq T t0
  59 (THead (Bind b) (lift n n0 (lift1 p u)) (lift n (S n0) (lift1 (Ss p) t)))))
  60 (refl_equal T (THead (Bind b) (lift n n0 (lift1 p u)) (lift n (S n0) (lift1
  61 (Ss p) t)))) (lift n n0 (THead (Bind b) (lift1 p u) (lift1 (Ss p) t)))
  62 (lift_bind b (lift1 p u) (lift1 (Ss p) t) n n0)) (lift1 p (THead (Bind b) u
  63 t)) (H u t)))))))) hds)).
  64
  65 lemma lift1_flat:
  66  \forall (f: F).(\forall (hds: PList).(\forall (u: T).(\forall (t: T).(eq T
  67 (lift1 hds (THead (Flat f) u t)) (THead (Flat f) (lift1 hds u) (lift1 hds
  68 t))))))
  69 \def
  70  \lambda (f: F).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall
  71 (u: T).(\forall (t: T).(eq T (lift1 p (THead (Flat f) u t)) (THead (Flat f)
  72 (lift1 p u) (lift1 p t)))))) (\lambda (u: T).(\lambda (t: T).(refl_equal T
  73 (THead (Flat f) u t)))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p:
  74 PList).(\lambda (H: ((\forall (u: T).(\forall (t: T).(eq T (lift1 p (THead
  75 (Flat f) u t)) (THead (Flat f) (lift1 p u) (lift1 p t))))))).(\lambda (u:
  76 T).(\lambda (t: T).(eq_ind_r T (THead (Flat f) (lift1 p u) (lift1 p t))
  77 (\lambda (t0: T).(eq T (lift n n0 t0) (THead (Flat f) (lift n n0 (lift1 p u))
  78 (lift n n0 (lift1 p t))))) (eq_ind_r T (THead (Flat f) (lift n n0 (lift1 p
  79 u)) (lift n n0 (lift1 p t))) (\lambda (t0: T).(eq T t0 (THead (Flat f) (lift
  80 n n0 (lift1 p u)) (lift n n0 (lift1 p t))))) (refl_equal T (THead (Flat f)
  81 (lift n n0 (lift1 p u)) (lift n n0 (lift1 p t)))) (lift n n0 (THead (Flat f)
  82 (lift1 p u) (lift1 p t))) (lift_flat f (lift1 p u) (lift1 p t) n n0)) (lift1
  83 p (THead (Flat f) u t)) (H u t)))))))) hds)).
  84
  85 lemma lift1_cons_tail:
  86  \forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (hds: PList).(eq
  87 T (lift1 (PConsTail hds h d) t) (lift1 hds (lift h d t))))))
  88 \def
  89  \lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda (hds:
  90 PList).(PList_ind (\lambda (p: PList).(eq T (lift1 (PConsTail p h d) t)
  91 (lift1 p (lift h d t)))) (refl_equal T (lift h d t)) (\lambda (n:
  92 nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda (H: (eq T (lift1
  93 (PConsTail p h d) t) (lift1 p (lift h d t)))).(eq_ind_r T (lift1 p (lift h d
  94 t)) (\lambda (t0: T).(eq T (lift n n0 t0) (lift n n0 (lift1 p (lift h d
  95 t))))) (refl_equal T (lift n n0 (lift1 p (lift h d t)))) (lift1 (PConsTail p
  96 h d) t) H))))) hds)))).
  97
  98 lemma lifts1_flat:
  99  \forall (f: F).(\forall (hds: PList).(\forall (t: T).(\forall (ts:
 100 TList).(eq T (lift1 hds (THeads (Flat f) ts t)) (THeads (Flat f) (lifts1 hds
 101 ts) (lift1 hds t))))))
 102 \def
 103  \lambda (f: F).(\lambda (hds: PList).(\lambda (t: T).(\lambda (ts:
 104 TList).(TList_ind (\lambda (t0: TList).(eq T (lift1 hds (THeads (Flat f) t0
 105 t)) (THeads (Flat f) (lifts1 hds t0) (lift1 hds t)))) (refl_equal T (lift1
 106 hds t)) (\lambda (t0: T).(\lambda (t1: TList).(\lambda (H: (eq T (lift1 hds
 107 (THeads (Flat f) t1 t)) (THeads (Flat f) (lifts1 hds t1) (lift1 hds
 108 t)))).(eq_ind_r T (THead (Flat f) (lift1 hds t0) (lift1 hds (THeads (Flat f)
 109 t1 t))) (\lambda (t2: T).(eq T t2 (THead (Flat f) (lift1 hds t0) (THeads
 110 (Flat f) (lifts1 hds t1) (lift1 hds t))))) (eq_ind_r T (THeads (Flat f)
 111 (lifts1 hds t1) (lift1 hds t)) (\lambda (t2: T).(eq T (THead (Flat f) (lift1
 112 hds t0) t2) (THead (Flat f) (lift1 hds t0) (THeads (Flat f) (lifts1 hds t1)
 113 (lift1 hds t))))) (refl_equal T (THead (Flat f) (lift1 hds t0) (THeads (Flat
 114 f) (lifts1 hds t1) (lift1 hds t)))) (lift1 hds (THeads (Flat f) t1 t)) H)
 115 (lift1 hds (THead (Flat f) t0 (THeads (Flat f) t1 t))) (lift1_flat f hds t0
 116 (THeads (Flat f) t1 t)))))) ts)))).
 117
 118 lemma lifts1_nil:
 119  \forall (ts: TList).(eq TList (lifts1 PNil ts) ts)
 120 \def
 121  \lambda (ts: TList).(TList_ind (\lambda (t: TList).(eq TList (lifts1 PNil t)
 122 t)) (refl_equal TList TNil) (\lambda (t: T).(\lambda (t0: TList).(\lambda (H:
 123 (eq TList (lifts1 PNil t0) t0)).(eq_ind_r TList t0 (\lambda (t1: TList).(eq
 124 TList (TCons t t1) (TCons t t0))) (refl_equal TList (TCons t t0)) (lifts1
 125 PNil t0) H)))) ts).
 126
 127 lemma lifts1_cons:
 128  \forall (h: nat).(\forall (d: nat).(\forall (hds: PList).(\forall (ts:
 129 TList).(eq TList (lifts1 (PCons h d hds) ts) (lifts h d (lifts1 hds ts))))))
 130 \def
 131  \lambda (h: nat).(\lambda (d: nat).(\lambda (hds: PList).(\lambda (ts:
 132 TList).(TList_ind (\lambda (t: TList).(eq TList (lifts1 (PCons h d hds) t)
 133 (lifts h d (lifts1 hds t)))) (refl_equal TList TNil) (\lambda (t: T).(\lambda
 134 (t0: TList).(\lambda (H: (eq TList (lifts1 (PCons h d hds) t0) (lifts h d
 135 (lifts1 hds t0)))).(eq_ind_r TList (lifts h d (lifts1 hds t0)) (\lambda (t1:
 136 TList).(eq TList (TCons (lift h d (lift1 hds t)) t1) (TCons (lift h d (lift1
 137 hds t)) (lifts h d (lifts1 hds t0))))) (refl_equal TList (TCons (lift h d
 138 (lift1 hds t)) (lifts h d (lifts1 hds t0)))) (lifts1 (PCons h d hds) t0)
 139 H)))) ts)))).
 140