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