]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma
- notation fix for reducible and normal forms
[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / unfold / lifts.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "Basic_2/substitution/lift.ma".
16 include "Basic_2/unfold/gr2_plus.ma".
17
18 (* GENERIC TERM RELOCATION **************************************************)
19
20 inductive lifts: list2 nat nat → relation term ≝
21 | lifts_nil : ∀T. lifts ⟠ T T
22 | lifts_cons: ∀T1,T,T2,des,d,e.
23               ⇧[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} :: des) T1 T2
24 .
25
26 interpretation "generic relocation (term)"
27    'RLiftStar des T1 T2 = (lifts des T1 T2).
28
29 (* Basic inversion lemmas ***************************************************)
30
31 fact lifts_inv_nil_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → des = ⟠ → T1 = T2.
32 #T1 #T2 #des * -T1 -T2 -des //
33 #T1 #T #T2 #d #e #des #_ #_ #H destruct
34 qed.
35
36 lemma lifts_inv_nil: ∀T1,T2. ⇧*[⟠] T1 ≡ T2 → T1 = T2.
37 /2 width=3/ qed-.
38
39 fact lifts_inv_cons_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 →
40                          ∀d,e,tl. des = {d, e} :: tl →
41                          ∃∃T. ⇧[d, e] T1 ≡ T & ⇧*[tl] T ≡ T2.
42 #T1 #T2 #des * -T1 -T2 -des
43 [ #T #d #e #tl #H destruct
44 | #T1 #T #T2 #des #d #e #HT1 #HT2 #hd #he #tl #H destruct
45   /2 width=3/
46 qed.
47
48 lemma lifts_inv_cons: ∀T1,T2,d,e,des. ⇧*[{d, e} :: des] T1 ≡ T2 →
49                       ∃∃T. ⇧[d, e] T1 ≡ T & ⇧*[des] T ≡ T2.
50 /2 width=3/ qed-.
51
52 (* Basic_1: was: lift1_sort *)
53 lemma lifts_inv_sort1: ∀T2,k,des. ⇧*[des] ⋆k ≡ T2 → T2 = ⋆k.
54 #T2 #k #des elim des -des
55 [ #H <(lifts_inv_nil … H) -H //
56 | #d #e #des #IH #H
57   elim (lifts_inv_cons … H) -H #X #H
58   >(lift_inv_sort1 … H) -H /2 width=1/
59 ]
60 qed-.
61
62 (* Basic_1: was: lift1_lref *)
63 lemma lifts_inv_lref1: ∀T2,des,i1. ⇧*[des] #i1 ≡ T2 →
64                        ∃∃i2. @[i1] des ≡ i2 & T2 = #i2.
65 #T2 #des elim des -des
66 [ #i1 #H <(lifts_inv_nil … H) -H /2 width=3/
67 | #d #e #des #IH #i1 #H
68   elim (lifts_inv_cons … H) -H #X #H1 #H2
69   elim (lift_inv_lref1 … H1) -H1 * #Hdi1 #H destruct
70   elim (IH … H2) -IH -H2 /3 width=3/
71 ]
72 qed-.
73
74 lemma lifts_inv_gref1: ∀T2,p,des. ⇧*[des] §p ≡ T2 → T2 = §p.
75 #T2 #p #des elim des -des
76 [ #H <(lifts_inv_nil … H) -H //
77 | #d #e #des #IH #H
78   elim (lifts_inv_cons … H) -H #X #H
79   >(lift_inv_gref1 … H) -H /2 width=1/
80 ]
81 qed-.
82
83 (* Basic_1: was: lift1_bind *)
84 lemma lifts_inv_bind1: ∀I,T2,des,V1,U1. ⇧*[des] ⓑ{I} V1. U1 ≡ T2 →
85                        ∃∃V2,U2. ⇧*[des] V1 ≡ V2 & ⇧*[des + 1] U1 ≡ U2 &
86                                 T2 = ⓑ{I} V2. U2.
87 #I #T2 #des elim des -des
88 [ #V1 #U1 #H
89   <(lifts_inv_nil … H) -H /2 width=5/
90 | #d #e #des #IHdes #V1 #U1 #H
91   elim (lifts_inv_cons … H) -H #X #H #HT2
92   elim (lift_inv_bind1 … H) -H #V #U #HV1 #HU1 #H destruct
93   elim (IHdes … HT2) -IHdes -HT2 #V2 #U2 #HV2 #HU2 #H destruct
94   /3 width=5/
95 ]
96 qed-.
97
98 (* Basic_1: was: lift1_flat *)
99 lemma lifts_inv_flat1: ∀I,T2,des,V1,U1. ⇧*[des] ⓕ{I} V1. U1 ≡ T2 →
100                        ∃∃V2,U2. ⇧*[des] V1 ≡ V2 & ⇧*[des] U1 ≡ U2 &
101                                 T2 = ⓕ{I} V2. U2.
102 #I #T2 #des elim des -des
103 [ #V1 #U1 #H
104   <(lifts_inv_nil … H) -H /2 width=5/
105 | #d #e #des #IHdes #V1 #U1 #H
106   elim (lifts_inv_cons … H) -H #X #H #HT2
107   elim (lift_inv_flat1 … H) -H #V #U #HV1 #HU1 #H destruct
108   elim (IHdes … HT2) -IHdes -HT2 #V2 #U2 #HV2 #HU2 #H destruct
109   /3 width=5/
110 ]
111 qed-.
112
113 (* Basic forward lemmas *****************************************************)
114
115 lemma lifts_simple_dx: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒[T1] → 𝐒[T2].
116 #T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_dx/
117 qed-.
118
119 lemma lifts_simple_sn: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒[T2] → 𝐒[T1].
120 #T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_sn/
121 qed-.
122
123 (* Basic properties *********************************************************)
124
125 lemma lifts_bind: ∀I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 →
126                   ∀T1. ⇧*[des + 1] T1 ≡ T2 →
127                   ⇧*[des] ⓑ{I} V1. T1 ≡ ⓑ{I} V2. T2.
128 #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
129 [ #V #T1 #H >(lifts_inv_nil … H) -H //
130 | #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
131   elim (lifts_inv_cons … H) -H /3 width=3/
132 ]
133 qed.
134
135 lemma lifts_flat: ∀I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 →
136                   ∀T1. ⇧*[des] T1 ≡ T2 →
137                   ⇧*[des] ⓕ{I} V1. T1 ≡ ⓕ{I} V2. T2.
138 #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
139 [ #V #T1 #H >(lifts_inv_nil … H) -H //
140 | #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
141   elim (lifts_inv_cons … H) -H /3 width=3/
142 ]
143 qed.
144
145 lemma lifts_total: ∀des,T1. ∃T2. ⇧*[des] T1 ≡ T2.
146 #des elim des -des /2 width=2/
147 #d #e #des #IH #T1
148 elim (lift_total T1 d e) #T #HT1
149 elim (IH T) -IH /3 width=4/
150 qed.