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 (**************************************************************************)
17 (* RELOCATION ***************************************************************)
19 (* Policy: depth (level) metavariables: d, e
20 height metavariables : h, k
22 (* Note: indexes start at zero *)
23 let rec lift d h M on M ≝ match M with
24 [ VRef i ⇒ #(tri … i d i (i + h) (i + h))
25 | Abst A ⇒ 𝛌. (lift (d+1) h A)
26 | Appl B A ⇒ @(lift d h B). (lift d h A)
29 interpretation "relocation" 'Lift d h M = (lift d h M).
31 notation "hvbox( ↑ [ d , break h ] break term 55 M )"
32 non associative with precedence 55
33 for @{ 'Lift $d $h $M }.
35 notation > "hvbox( ↑ [ h ] break term 55 M )"
36 non associative with precedence 55
37 for @{ 'Lift 0 $h $M }.
39 notation > "hvbox( ↑ term 55 M )"
40 non associative with precedence 55
41 for @{ 'Lift 0 1 $M }.
43 lemma lift_vref_lt: ∀d,h,i. i < d → ↑[d, h] #i = #i.
47 lemma lift_vref_ge: ∀d,h,i. d ≤ i → ↑[d, h] #i = #(i+h).
48 #d #h #i #H elim (le_to_or_lt_eq … H) -H
49 normalize // /3 width=1/
52 lemma lift_inv_vref_lt: ∀j,d. j < d → ∀h,M. ↑[d, h] M = #j → M = #j.
53 #j #d #Hjd #h * normalize
54 [ #i elim (lt_or_eq_or_gt i d) #Hid
55 [ >(tri_lt ???? … Hid) -Hid -Hjd //
56 | #H destruct >tri_eq in Hjd; #H
57 elim (plus_lt_false … H)
58 | >(tri_gt ???? … Hid)
59 lapply (transitive_lt … Hjd Hid) -Hjd -Hid #H #H0 destruct
60 elim (plus_lt_false … H)
67 lemma lift_inv_abst: ∀C,d,h,M. ↑[d, h] M = 𝛌.C →
68 ∃∃A. ↑[d+1, h] A = C & M = 𝛌.A.
71 | #A #H destruct /2 width=3/
76 lemma lift_inv_appl: ∀D,C,d,h,M. ↑[d, h] M = @D.C →
77 ∃∃B,A. ↑[d, h] B = D & ↑[d, h] A = C & M = @B.A.
78 #D #C #d #h * normalize
81 | #B #A #H destruct /2 width=5/