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 "Basic_2/grammar/term_vector.ma".
16 include "Basic_2/substitution/lift.ma".
18 (* GENERIC RELOCATION *******************************************************)
20 let rec ss (des:list2 nat nat) ≝ match des with
22 | cons2 d e des ⇒ {d + 1, e} :: ss des
25 inductive lifts: list2 nat nat → relation term ≝
26 | lifts_nil : ∀T. lifts ⟠ T T
27 | lifts_cons: ∀T1,T,T2,des,d,e.
28 ⇧[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} :: des) T1 T2
31 interpretation "generic relocation"
32 'RLiftStar des T1 T2 = (lifts des T1 T2).
34 (* Basic inversion lemmas ***************************************************)
36 fact lifts_inv_nil_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → des = ⟠ → T1 = T2.
37 #T1 #T2 #des * -T1 -T2 -des //
38 #T1 #T #T2 #d #e #des #_ #_ #H destruct
41 lemma lifts_inv_nil: ∀T1,T2. ⇧*[⟠] T1 ≡ T2 → T1 = T2.
44 fact lifts_inv_cons_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 →
45 ∀d,e,tl. des = {d, e} :: tl →
46 ∃∃T. ⇧[d, e] T1 ≡ T & ⇧*[tl] T ≡ T2.
47 #T1 #T2 #des * -T1 -T2 -des
48 [ #T #d #e #tl #H destruct
49 | #T1 #T #T2 #des #d #e #HT1 #HT2 #hd #he #tl #H destruct
53 lemma lifts_inv_cons: ∀T1,T2,d,e,des. ⇧*[{d, e} :: des] T1 ≡ T2 →
54 ∃∃T. ⇧[d, e] T1 ≡ T & ⇧*[des] T ≡ T2.
57 lemma lifts_inv_bind1: ∀I,T2,des,V1,U1. ⇧*[des] 𝕓{I} V1. U1 ≡ T2 →
58 ∃∃V2,U2. ⇧*[des] V1 ≡ V2 & ⇧*[ss des] U1 ≡ U2 &
60 #I #T2 #des elim des -des
62 <(lifts_inv_nil … H) -H /2 width=5/
63 | #d #e #des #IHdes #V1 #U1 #H
64 elim (lifts_inv_cons … H) -H #X #H #HT2
65 elim (lift_inv_bind1 … H) -H #V #U #HV1 #HU1 #H destruct
66 elim (IHdes … HT2) -IHdes -HT2 #V2 #U2 #HV2 #HU2 #H destruct
71 lemma lifts_inv_flat1: ∀I,T2,des,V1,U1. ⇧*[des] 𝕗{I} V1. U1 ≡ T2 →
72 ∃∃V2,U2. ⇧*[des] V1 ≡ V2 & ⇧*[des] U1 ≡ U2 &
74 #I #T2 #des elim des -des
76 <(lifts_inv_nil … H) -H /2 width=5/
77 | #d #e #des #IHdes #V1 #U1 #H
78 elim (lifts_inv_cons … H) -H #X #H #HT2
79 elim (lift_inv_flat1 … H) -H #V #U #HV1 #HU1 #H destruct
80 elim (IHdes … HT2) -IHdes -HT2 #V2 #U2 #HV2 #HU2 #H destruct
85 (* Basic forward lemmas *****************************************************)
87 lemma lifts_simple_dx: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝕊[T1] → 𝕊[T2].
88 #T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_dx/
91 lemma lifts_simple_sn: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝕊[T2] → 𝕊[T1].
92 #T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_sn/
95 (* Basic properties *********************************************************)
97 lemma lifts_bind: ∀I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 →
98 ∀T1. ⇧*[ss des] T1 ≡ T2 →
99 ⇧*[des] 𝕓{I} V1. T1 ≡ 𝕓{I} V2. T2.
100 #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
101 [ #V #T1 #H >(lifts_inv_nil … H) -H //
102 | #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
103 elim (lifts_inv_cons … H) -H /3 width=3/
107 lemma lifts_flat: ∀I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 →
108 ∀T1. ⇧*[des] T1 ≡ T2 →
109 ⇧*[des] 𝕗{I} V1. T1 ≡ 𝕗{I} V2. T2.
110 #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
111 [ #V #T1 #H >(lifts_inv_nil … H) -H //
112 | #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
113 elim (lifts_inv_cons … H) -H /3 width=3/
117 lemma lifts_total: ∀des,T1. ∃T2. ⇧*[des] T1 ≡ T2.
118 #des elim des -des /2 width=2/
120 elim (lift_total T1 d e) #T #HT1
121 elim (IH T) -IH /3 width=4/