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/relocation/mr2_at.ma".
16 include "ground/relocation/mr2_plus.ma".
17 include "basic_2A/notation/relations/rliftstar_3.ma".
18 include "basic_2A/substitution/lift.ma".
20 (* GENERIC TERM RELOCATION **************************************************)
22 inductive lifts: mr2 → relation term ≝
23 | lifts_nil : ∀T. lifts (𝐞) T T
24 | lifts_cons: ∀T1,T,T2,cs,l,m.
25 ⬆[l,m] T1 ≡ T → lifts cs T T2 → lifts (❨l, m❩; cs) T1 T2
28 interpretation "generic relocation (term)"
29 'RLiftStar cs T1 T2 = (lifts cs T1 T2).
31 (* Basic inversion lemmas ***************************************************)
33 fact lifts_inv_nil_aux: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 → cs = 𝐞 → T1 = T2.
34 #T1 #T2 #cs * -T1 -T2 -cs //
35 #T1 #T #T2 #l #m #cs #_ #_ #H destruct
38 lemma lifts_inv_nil: ∀T1,T2. ⬆*[𝐞] T1 ≡ T2 → T1 = T2.
39 /2 width=3 by lifts_inv_nil_aux/ qed-.
41 fact lifts_inv_cons_aux: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 →
42 ∀l,m,tl. cs = ❨l, m❩; tl →
43 ∃∃T. ⬆[l, m] T1 ≡ T & ⬆*[tl] T ≡ T2.
44 #T1 #T2 #cs * -T1 -T2 -cs
45 [ #T #l #m #tl #H destruct
46 | #T1 #T #T2 #cs #l #m #HT1 #HT2 #l0 #m0 #tl #H destruct
47 /2 width=3 by ex2_intro/
50 lemma lifts_inv_cons: ∀T1,T2,l,m,cs. ⬆*[❨l, m❩; cs] T1 ≡ T2 →
51 ∃∃T. ⬆[l, m] T1 ≡ T & ⬆*[cs] T ≡ T2.
52 /2 width=3 by lifts_inv_cons_aux/ qed-.
54 lemma lifts_inv_sort1: ∀T2,k,cs. ⬆*[cs] ⋆k ≡ T2 → T2 = ⋆k.
55 #T2 #k #cs elim cs -cs
56 [ #H <(lifts_inv_nil … H) -H //
58 elim (lifts_inv_cons … H) -H #X #H
59 >(lift_inv_sort1 … H) -H /2 width=1 by/
63 lemma lifts_inv_lref1: ∀T2,cs,i1. ⬆*[cs] #i1 ≡ T2 →
64 ∃∃i2. @❪i1, cs❫ ≘ i2 & T2 = #i2.
66 [ #i1 #H <(lifts_inv_nil … H) -H /2 width=3 by at_nil, ex2_intro/
67 | #l #m #cs #IH #i1 #H
68 elim (lifts_inv_cons … H) -H #X #H1 #H2
69 elim (lift_inv_lref1 … H1) -H1 * #Hli1 #H destruct
70 elim (IH … H2) -IH -H2 /3 width=3 by at_lt, at_ge, ex2_intro/
74 lemma lifts_inv_gref1: ∀T2,p,cs. ⬆*[cs] §p ≡ T2 → T2 = §p.
75 #T2 #p #cs elim cs -cs
76 [ #H <(lifts_inv_nil … H) -H //
78 elim (lifts_inv_cons … H) -H #X #H
79 >(lift_inv_gref1 … H) -H /2 width=1 by/
83 lemma lifts_inv_bind1: ∀a,I,T2,cs,V1,U1. ⬆*[cs] ⓑ{a,I} V1. U1 ≡ T2 →
84 ∃∃V2,U2. ⬆*[cs] V1 ≡ V2 & ⬆*[cs + 1] U1 ≡ U2 &
86 #a #I #T2 #cs elim cs -cs
88 <(lifts_inv_nil … H) -H /2 width=5 by ex3_2_intro, lifts_nil/
89 | #l #m #cs #IHcs #V1 #U1 #H
90 elim (lifts_inv_cons … H) -H #X #H #HT2
91 elim (lift_inv_bind1 … H) -H #V #U #HV1 #HU1 #H destruct
92 elim (IHcs … HT2) -IHcs -HT2 #V2 #U2 #HV2 #HU2 #H destruct
93 /3 width=5 by ex3_2_intro, lifts_cons/
97 lemma lifts_inv_flat1: ∀I,T2,cs,V1,U1. ⬆*[cs] ⓕ{I} V1. U1 ≡ T2 →
98 ∃∃V2,U2. ⬆*[cs] V1 ≡ V2 & ⬆*[cs] U1 ≡ U2 &
100 #I #T2 #cs elim cs -cs
102 <(lifts_inv_nil … H) -H /2 width=5 by ex3_2_intro, lifts_nil/
103 | #l #m #cs #IHcs #V1 #U1 #H
104 elim (lifts_inv_cons … H) -H #X #H #HT2
105 elim (lift_inv_flat1 … H) -H #V #U #HV1 #HU1 #H destruct
106 elim (IHcs … HT2) -IHcs -HT2 #V2 #U2 #HV2 #HU2 #H destruct
107 /3 width=5 by ex3_2_intro, lifts_cons/
111 (* Basic forward lemmas *****************************************************)
113 lemma lifts_simple_dx: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
114 #T1 #T2 #cs #H elim H -T1 -T2 -cs /3 width=5 by lift_simple_dx/
117 lemma lifts_simple_sn: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
118 #T1 #T2 #cs #H elim H -T1 -T2 -cs /3 width=5 by lift_simple_sn/
121 (* Basic properties *********************************************************)
123 lemma lifts_bind: ∀a,I,T2,V1,V2,cs. ⬆*[cs] V1 ≡ V2 →
124 ∀T1. ⬆*[cs + 1] T1 ≡ T2 →
125 ⬆*[cs] ⓑ{a,I} V1. T1 ≡ ⓑ{a,I} V2. T2.
126 #a #I #T2 #V1 #V2 #cs #H elim H -V1 -V2 -cs
127 [ #V #T1 #H >(lifts_inv_nil … H) -H //
128 | #V1 #V #V2 #cs #l #m #HV1 #_ #IHV #T1 #H
129 elim (lifts_inv_cons … H) -H /3 width=3 by lift_bind, lifts_cons/
133 lemma lifts_flat: ∀I,T2,V1,V2,cs. ⬆*[cs] V1 ≡ V2 →
134 ∀T1. ⬆*[cs] T1 ≡ T2 →
135 ⬆*[cs] ⓕ{I} V1. T1 ≡ ⓕ{I} V2. T2.
136 #I #T2 #V1 #V2 #cs #H elim H -V1 -V2 -cs
137 [ #V #T1 #H >(lifts_inv_nil … H) -H //
138 | #V1 #V #V2 #cs #l #m #HV1 #_ #IHV #T1 #H
139 elim (lifts_inv_cons … H) -H /3 width=3 by lift_flat, lifts_cons/
143 lemma lifts_total: ∀cs,T1. ∃T2. ⬆*[cs] T1 ≡ T2.
144 #cs elim cs -cs /2 width=2 by lifts_nil, ex_intro/
145 #l #m #cs #IH #T1 elim (lift_total T1 l m)
146 #T #HT1 elim (IH T) -IH /3 width=4 by lifts_cons, ex_intro/