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 "static_2/syntax/term_vector.ma".
16 include "static_2/relocation/lifts.ma".
18 (* GENERIC RELOCATION FOR TERM VECTORS *************************************)
20 (* Basic_2A1: includes: liftv_nil liftv_cons *)
21 inductive liftsv (f): relation … ≝
22 | liftsv_nil : liftsv f (ⓔ) (ⓔ)
23 | liftsv_cons: ∀T1s,T2s,T1,T2.
24 ⇧*[f] T1 ≘ T2 → liftsv f T1s T2s →
25 liftsv f (T1 ⨮ T1s) (T2 ⨮ T2s)
28 interpretation "generic relocation (term vector)"
29 'RLiftStar f T1s T2s = (liftsv f T1s T2s).
31 interpretation "uniform relocation (term vector)"
32 'RLift i T1s T2s = (liftsv (pr_uni i) T1s T2s).
34 (* Basic inversion lemmas ***************************************************)
36 fact liftsv_inv_nil1_aux (f):
37 ∀X,Y. ⇧*[f] X ≘ Y → X = ⓔ → Y = ⓔ.
39 #T1s #T2s #T1 #T2 #_ #_ #H destruct
42 (* Basic_2A1: includes: liftv_inv_nil1 *)
43 lemma liftsv_inv_nil1 (f):
44 ∀Y. ⇧*[f] ⓔ ≘ Y → Y = ⓔ.
45 /2 width=5 by liftsv_inv_nil1_aux/ qed-.
47 fact liftsv_inv_cons1_aux (f):
48 ∀X,Y. ⇧*[f] X ≘ Y → ∀T1,T1s. X = T1 ⨮ T1s →
49 ∃∃T2,T2s. ⇧*[f] T1 ≘ T2 & ⇧*[f] T1s ≘ T2s & Y = T2 ⨮ T2s.
51 [ #U1 #U1s #H destruct
52 | #T1s #T2s #T1 #T2 #HT12 #HT12s #U1 #U1s #H destruct /2 width=5 by ex3_2_intro/
56 (* Basic_2A1: includes: liftv_inv_cons1 *)
57 lemma liftsv_inv_cons1 (f):
58 ∀T1,T1s,Y. ⇧*[f] T1 ⨮ T1s ≘ Y →
59 ∃∃T2,T2s. ⇧*[f] T1 ≘ T2 & ⇧*[f] T1s ≘ T2s & Y = T2 ⨮ T2s.
60 /2 width=3 by liftsv_inv_cons1_aux/ qed-.
62 fact liftsv_inv_nil2_aux (f):
63 ∀X,Y. ⇧*[f] X ≘ Y → Y = ⓔ → X = ⓔ.
65 #T1s #T2s #T1 #T2 #_ #_ #H destruct
68 lemma liftsv_inv_nil2 (f):
69 ∀X. ⇧*[f] X ≘ ⓔ → X = ⓔ.
70 /2 width=5 by liftsv_inv_nil2_aux/ qed-.
72 fact liftsv_inv_cons2_aux (f):
73 ∀X,Y. ⇧*[f] X ≘ Y → ∀T2,T2s. Y = T2 ⨮ T2s →
74 ∃∃T1,T1s. ⇧*[f] T1 ≘ T2 & ⇧*[f] T1s ≘ T2s & X = T1 ⨮ T1s.
76 [ #U2 #U2s #H destruct
77 | #T1s #T2s #T1 #T2 #HT12 #HT12s #U2 #U2s #H destruct /2 width=5 by ex3_2_intro/
81 lemma liftsv_inv_cons2 (f):
82 ∀X,T2,T2s. ⇧*[f] X ≘ T2 ⨮ T2s →
83 ∃∃T1,T1s. ⇧*[f] T1 ≘ T2 & ⇧*[f] T1s ≘ T2s & X = T1 ⨮ T1s.
84 /2 width=3 by liftsv_inv_cons2_aux/ qed-.
86 (* Basic_1: was: lifts1_flat (left to right) *)
87 lemma lifts_inv_applv1 (f):
88 ∀V1s,U1,T2. ⇧*[f] Ⓐ V1s.U1 ≘ T2 →
89 ∃∃V2s,U2. ⇧*[f] V1s ≘ V2s & ⇧*[f] U1 ≘ U2 & T2 = Ⓐ V2s.U2.
91 [ /3 width=5 by ex3_2_intro, liftsv_nil/
92 | #V1 #V1s #IHV1s #T1 #X #H elim (lifts_inv_flat1 … H) -H
93 #V2 #Y #HV12 #HY #H destruct elim (IHV1s … HY) -IHV1s -HY
94 #V2s #T2 #HV12s #HT12 #H destruct /3 width=5 by ex3_2_intro, liftsv_cons/
98 lemma lifts_inv_applv2 (f):
99 ∀V2s,U2,T1. ⇧*[f] T1 ≘ Ⓐ V2s.U2 →
100 ∃∃V1s,U1. ⇧*[f] V1s ≘ V2s & ⇧*[f] U1 ≘ U2 & T1 = Ⓐ V1s.U1.
101 #f #V2s elim V2s -V2s
102 [ /3 width=5 by ex3_2_intro, liftsv_nil/
103 | #V2 #V2s #IHV2s #T2 #X #H elim (lifts_inv_flat2 … H) -H
104 #V1 #Y #HV12 #HY #H destruct elim (IHV2s … HY) -IHV2s -HY
105 #V1s #T1 #HV12s #HT12 #H destruct /3 width=5 by ex3_2_intro, liftsv_cons/
109 (* Basic properties *********************************************************)
111 (* Basic_2A1: includes: liftv_total *)
112 lemma liftsv_total (f):
113 ∀T1s. ∃T2s. ⇧*[f] T1s ≘ T2s.
114 #f #T1s elim T1s -T1s
115 [ /2 width=2 by liftsv_nil, ex_intro/
116 | #T1 #T1s * #T2s #HT12s
117 elim (lifts_total T1 f) /3 width=2 by liftsv_cons, ex_intro/
121 (* Basic_1: was: lifts1_flat (right to left) *)
122 lemma lifts_applv (f):
123 ∀V1s,V2s. ⇧*[f] V1s ≘ V2s → ∀T1,T2. ⇧*[f] T1 ≘ T2 →
124 ⇧*[f] Ⓐ V1s.T1 ≘ Ⓐ V2s.T2.
125 #f #V1s #V2s #H elim H -V1s -V2s /3 width=1 by lifts_flat/
128 lemma liftsv_split_trans (f):
129 ∀T1s,T2s. ⇧*[f] T1s ≘ T2s → ∀f1,f2. f2 ⊚ f1 ≘ f →
130 ∃∃Ts. ⇧*[f1] T1s ≘ Ts & ⇧*[f2] Ts ≘ T2s.
131 #f #T1s #T2s #H elim H -T1s -T2s
132 [ /2 width=3 by liftsv_nil, ex2_intro/
133 | #T1s #T2s #T1 #T2 #HT12 #_ #IH #f1 #f2 #Hf
135 elim (lifts_split_trans … HT12 … Hf) -HT12 -Hf
136 /3 width=5 by liftsv_cons, ex2_intro/
140 (* Basic_1: removed theorems 2: lifts1_nil lifts1_cons *)