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" 'RLift des T1 T2 = (lifts des T1 T2).
33 (* Basic inversion lemmas ***************************************************)
35 fact lifts_inv_nil_aux: ∀T1,T2,des. ⇑[des] T1 ≡ T2 → des = ⟠ → T1 = T2.
36 #T1 #T2 #des * -T1 -T2 -des //
37 #T1 #T #T2 #d #e #des #_ #_ #H destruct
40 lemma lifts_inv_nil: ∀T1,T2. ⇑[⟠] T1 ≡ T2 → T1 = T2.
43 fact lifts_inv_cons_aux: ∀T1,T2,des. ⇑[des] T1 ≡ T2 →
44 ∀d,e,tl. des = {d, e} :: tl →
45 ∃∃T. ⇑[d, e] T1 ≡ T & ⇑[tl] T ≡ T2.
46 #T1 #T2 #des * -T1 -T2 -des
47 [ #T #d #e #tl #H destruct
48 | #T1 #T #T2 #des #d #e #HT1 #HT2 #hd #he #tl #H destruct
52 lemma lifts_inv_cons: ∀T1,T2,d,e,des. ⇑[{d, e} :: des] T1 ≡ T2 →
53 ∃∃T. ⇑[d, e] T1 ≡ T & ⇑[des] T ≡ T2.
56 lemma lifts_inv_bind1: ∀I,T2,des,V1,U1. ⇑[des] 𝕓{I} V1. U1 ≡ T2 →
57 ∃∃V2,U2. ⇑[des] V1 ≡ V2 & ⇑[ss des] U1 ≡ U2 &
59 #I #T2 #des elim des -des
61 <(lifts_inv_nil … H) -H /2 width=5/
62 | #d #e #des #IHdes #V1 #U1 #H
63 elim (lifts_inv_cons … H) -H #X #H #HT2
64 elim (lift_inv_bind1 … H) -H #V #U #HV1 #HU1 #H destruct
65 elim (IHdes … HT2) -IHdes -HT2 #V2 #U2 #HV2 #HU2 #H destruct
70 lemma lifts_inv_flat1: ∀I,T2,des,V1,U1. ⇑[des] 𝕗{I} V1. U1 ≡ T2 →
71 ∃∃V2,U2. ⇑[des] V1 ≡ V2 & ⇑[des] U1 ≡ U2 &
73 #I #T2 #des elim des -des
75 <(lifts_inv_nil … H) -H /2 width=5/
76 | #d #e #des #IHdes #V1 #U1 #H
77 elim (lifts_inv_cons … H) -H #X #H #HT2
78 elim (lift_inv_flat1 … H) -H #V #U #HV1 #HU1 #H destruct
79 elim (IHdes … HT2) -IHdes -HT2 #V2 #U2 #HV2 #HU2 #H destruct
84 (* Basic forward lemmas *****************************************************)
86 lemma lifts_simple_dx: ∀T1,T2,des. ⇑[des] T1 ≡ T2 → 𝕊[T1] → 𝕊[T2].
87 #T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_dx/
90 lemma lifts_simple_sn: ∀T1,T2,des. ⇑[des] T1 ≡ T2 → 𝕊[T2] → 𝕊[T1].
91 #T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_sn/
94 (* Basic properties *********************************************************)
96 lemma lifts_bind: ∀I,T2,V1,V2,des. ⇑[des] V1 ≡ V2 →
97 ∀T1. ⇑[ss des] T1 ≡ T2 →
98 ⇑[des] 𝕓{I} V1. T1 ≡ 𝕓{I} V2. T2.
99 #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
100 [ #V #T1 #H >(lifts_inv_nil … H) -H //
101 | #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
102 elim (lifts_inv_cons … H) -H /3 width=3/
106 lemma lifts_flat: ∀I,T2,V1,V2,des. ⇑[des] V1 ≡ V2 →
107 ∀T1. ⇑[des] T1 ≡ T2 →
108 ⇑[des] 𝕗{I} V1. T1 ≡ 𝕗{I} V2. T2.
109 #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
110 [ #V #T1 #H >(lifts_inv_nil … H) -H //
111 | #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
112 elim (lifts_inv_cons … H) -H /3 width=3/
116 lemma lifts_total: ∀des,T1. ∃T2. ⇑[des] T1 ≡ T2.
117 #des elim des -des /2 width=2/
119 elim (lift_total T1 d e) #T #HT1
120 elim (IH T) -IH /3 width=4/