matita/matita/lib/lambda-delta/substitution/lift_fun.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 include "lambda-delta/substitution/lift_defs.ma".
  16
  17 (* RELOCATION ***************************************************************)
  18
  19 (* the functional properties ************************************************)
  20
  21 lemma lift_total: ∀T1,d,e. ∃T2. ↑[d,e] T1 ≡ T2.
  22 #T1 elim T1 -T1
  23 [ /2/
  24 | #i #d #e elim (lt_or_ge i d) /3/
  25 | * #I #V1 #T1 #IHV1 #IHT1 #d #e
  26   elim (IHV1 d e) -IHV1 #V2 #HV12
  27   [ elim (IHT1 (d+1) e) -IHT1 /3/
  28   | elim (IHT1 d e) -IHT1 /3/
  29   ]
  30 ]
  31 qed.
  32
  33 lemma lift_mono:  ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 → U1 = U2.
  34 #d #e #T #U1 #H elim H -H d e T U1
  35 [ #k #d #e #X #HX
  36   lapply (lift_inv_sort1 … HX) -HX //
  37 | #i #d #e #Hid #X #HX
  38   lapply (lift_inv_lref1_lt … HX ?) -HX //
  39 | #i #d #e #Hdi #X #HX
  40   lapply (lift_inv_lref1_ge … HX ?) -HX //
  41 | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
  42   elim (lift_inv_bind1 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
  43 | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
  44   elim (lift_inv_flat1 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
  45 ]
  46 qed.
  47
  48 lemma lift_inj:  ∀d,e,T1,U. ↑[d,e] T1 ≡ U → ∀T2. ↑[d,e] T2 ≡ U → T1 = T2.
  49 #d #e #T1 #U #H elim H -H d e T1 U
  50 [ #k #d #e #X #HX
  51   lapply (lift_inv_sort2 … HX) -HX //
  52 | #i #d #e #Hid #X #HX
  53   lapply (lift_inv_lref2_lt … HX ?) -HX //
  54 | #i #d #e #Hdi #X #HX
  55   lapply (lift_inv_lref2_ge … HX ?) -HX /2/
  56 | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
  57   elim (lift_inv_bind2 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
  58 | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
  59   elim (lift_inv_flat2 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
  60 ]
  61 qed.