1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground_2/tri.ma".
16 include "basic_2/substitution/lift.ma".
17 include "apps_2/functional/notation.ma".
19 (* RELOCATION ***************************************************************)
21 let rec flift d e U on U ≝ match U with
22 [ TAtom I ⇒ match I with
24 | LRef i ⇒ #(tri … i d i (i + e) (i + e))
27 | TPair I V T ⇒ match I with
28 [ Bind2 a I ⇒ ⓑ{a,I} (flift d e V). (flift (d+1) e T)
29 | Flat2 I ⇒ ⓕ{I} (flift d e V). (flift d e T)
33 interpretation "functional relocation" 'Lift d e T = (flift d e T).
35 (* Main properties **********************************************************)
37 theorem flift_lift: ∀T,d,e. ⇧[d, e] T ≡ ↑[d, e] T.
40 elim (lt_or_eq_or_gt i d) #Hid normalize
41 [ >(tri_lt ?????? Hid) /2 width=1/
43 | >(tri_gt ?????? Hid) /3 width=2/
49 (* Main inversion properties ************************************************)
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) //
55 elim (le_to_or_lt_eq … Hid) -Hid #Hid
56 [ >(tri_gt ?????? Hid) //
62 (* Derived properties *******************************************************)
64 lemma flift_join: ∀e1,e2,T. ⇧[e1, e2] ↑[0, e1] T ≡ ↑[0, 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 //