matita/matita/contribs/lambdadelta/apps_2/functional/lift.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 "basic_2/substitution/lift.ma".
  16 include "apps_2/functional/notation.ma".
  17
  18 (* FUNCTIONAL RELOCATION ****************************************************)
  19
  20 let rec flift d e U on U ≝ match U with
  21 [ TAtom I     ⇒ match I with
  22   [ Sort _ ⇒ U
  23   | LRef i ⇒ #(tri … i d i (i + e) (i + e))
  24   | GRef _ ⇒ U
  25   ]
  26 | TPair I V T ⇒ match I with
  27   [ Bind2 a I ⇒ ⓑ{a,I} (flift d e V). (flift (d+1) e T)
  28   | Flat2 I   ⇒ ⓕ{I} (flift d e V). (flift d e T)
  29   ]
  30 ].
  31
  32 interpretation "functional relocation" 'Lift d e T = (flift d e T).
  33
  34 (* Main properties **********************************************************)
  35
  36 theorem flift_lift: ∀T,d,e. ⬆[d, e] T ≡ ↑[d, e] T.
  37 #T elim T -T
  38 [ * #i #d #e //
  39   elim (lt_or_eq_or_gt i d) #Hid normalize
  40   [ >(tri_lt ?????? Hid) /2 width=1/
  41   | /2 width=1/
  42   | >(tri_gt ?????? Hid) /3 width=2/
  43   ]
  44 | * /2/
  45 ]
  46 qed.
  47
  48 (* Main inversion properties ************************************************)
  49
  50 theorem flift_inv_lift: ∀d,e,T1,T2. ⬆[d, e] T1 ≡ T2 → ↑[d, e] T1 = T2.
  51 #d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize //
  52 [ #i #d #e #Hid >(tri_lt ?????? Hid) //
  53 | #i #d #e #Hid
  54   elim (le_to_or_lt_eq … Hid) -Hid #Hid
  55   [ >(tri_gt ?????? Hid) //
  56   | destruct //
  57   ]
  58 ]
  59 qed-.
  60
  61 (* Derived properties *******************************************************)
  62
  63 lemma flift_join: ∀e1,e2,T. ⬆[e1, e2] ↑[0, e1] T ≡ ↑[0, e1 + e2] T.
  64 #e1 #e2 #T
  65 lapply (flift_lift T 0 (e1+e2)) #H
  66 elim (lift_split … H e1 e1) -H // #U #H
  67 >(flift_inv_lift … H) -H //
  68 qed.