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 "trichotomy.ma".
18 (* RELOCATION ***************************************************************)
20 (* Policy: depth (level) metavariables: d, e
21 height metavariables : h, k
23 (* Note: indexes start at zero *)
24 let rec lift d h M on M ≝ match M with
25 [ VRef i ⇒ #(tri … i d i (i + h) (i + h))
26 | Abst A ⇒ 𝛌. (lift (d+1) h A)
27 | Appl B A ⇒ @(lift d h B). (lift d h A)
30 interpretation "relocation" 'Lift d h M = (lift d h M).
32 notation "hvbox( ↑ [ d , break h ] break term 55 M )"
33 non associative with precedence 55
34 for @{ 'Lift $d $h $M }.
36 notation > "hvbox( ↑ [ h ] break term 55 M )"
37 non associative with precedence 55
38 for @{ 'Lift 0 $h $M }.
40 notation > "hvbox( ↑ term 55 M )"
41 non associative with precedence 55
42 for @{ 'Lift 0 1 $M }.
44 lemma lift_vref_lt: ∀d,h,i. i < d → ↑[d, h] #i = #i.
48 lemma lift_vref_ge: ∀d,h,i. d ≤ i → ↑[d, h] #i = #(i+h).
49 #d #h #i #H elim (le_to_or_lt_eq … H) -H
50 normalize // /3 width=1/
53 lemma lift_inv_abst: ∀C,d,h,M. ↑[d, h] M = 𝛌.C →
54 ∃∃A. ↑[d+1, h] A = C & M = 𝛌.A.
57 | #A #H destruct /2 width=3/
62 lemma lift_inv_appl: ∀D,C,d,h,M. ↑[d, h] M = @D.C →
63 ∃∃B,A. ↑[d, h] B = D & ↑[d, h] A = C & M = @B.A.
64 #D #C #d #h * normalize
67 | #B #A #H destruct /2 width=5/