(* *)
(**************************************************************************)
-include "Basic_2/grammar/term_vector.ma".
include "Basic_2/substitution/lift.ma".
+include "Basic_2/unfold/gr2_plus.ma".
-(* GENERIC RELOCATION *******************************************************)
-
-let rec ss (des:list2 nat nat) ≝ match des with
-[ nil2 ⇒ ⟠
-| cons2 d e des ⇒ {d + 1, e} :: ss des
-].
+(* GENERIC TERM RELOCATION **************************************************)
inductive lifts: list2 nat nat → relation term ≝
| lifts_nil : ∀T. lifts ⟠ T T
| lifts_cons: ∀T1,T,T2,des,d,e.
- â\87\91[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} :: des) T1 T2
+ â\87§[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} :: des) T1 T2
.
-interpretation "generic relocation" 'RLift des T1 T2 = (lifts des T1 T2).
+interpretation "generic relocation (term)"
+ 'RLiftStar des T1 T2 = (lifts des T1 T2).
(* Basic inversion lemmas ***************************************************)
-fact lifts_inv_nil_aux: â\88\80T1,T2,des. â\87\91[des] T1 ≡ T2 → des = ⟠ → T1 = T2.
+fact lifts_inv_nil_aux: â\88\80T1,T2,des. â\87§*[des] T1 ≡ T2 → des = ⟠ → T1 = T2.
#T1 #T2 #des * -T1 -T2 -des //
#T1 #T #T2 #d #e #des #_ #_ #H destruct
qed.
-lemma lifts_inv_nil: â\88\80T1,T2. â\87\91[⟠] T1 ≡ T2 → T1 = T2.
+lemma lifts_inv_nil: â\88\80T1,T2. â\87§*[⟠] T1 ≡ T2 → T1 = T2.
/2 width=3/ qed-.
-fact lifts_inv_cons_aux: â\88\80T1,T2,des. â\87\91[des] T1 ≡ T2 →
+fact lifts_inv_cons_aux: â\88\80T1,T2,des. â\87§*[des] T1 ≡ T2 →
∀d,e,tl. des = {d, e} :: tl →
- â\88\83â\88\83T. â\87\91[d, e] T1 â\89¡ T & â\87\91[tl] T ≡ T2.
+ â\88\83â\88\83T. â\87§[d, e] T1 â\89¡ T & â\87§*[tl] T ≡ T2.
#T1 #T2 #des * -T1 -T2 -des
[ #T #d #e #tl #H destruct
| #T1 #T #T2 #des #d #e #HT1 #HT2 #hd #he #tl #H destruct
/2 width=3/
qed.
-lemma lifts_inv_cons: â\88\80T1,T2,d,e,des. â\87\91[{d, e} :: des] T1 ≡ T2 →
- â\88\83â\88\83T. â\87\91[d, e] T1 â\89¡ T & â\87\91[des] T ≡ T2.
+lemma lifts_inv_cons: â\88\80T1,T2,d,e,des. â\87§*[{d, e} :: des] T1 ≡ T2 →
+ â\88\83â\88\83T. â\87§[d, e] T1 â\89¡ T & â\87§*[des] T ≡ T2.
/2 width=3/ qed-.
-lemma lifts_inv_bind1: ∀I,T2,des,V1,U1. ⇑[des] 𝕓{I} V1. U1 ≡ T2 →
- ∃∃V2,U2. ⇑[des] V1 ≡ V2 & ⇑[ss des] U1 ≡ U2 &
- T2 = 𝕓{I} V2. U2.
+(* Basic_1: was: lift1_sort *)
+lemma lifts_inv_sort1: ∀T2,k,des. ⇧*[des] ⋆k ≡ T2 → T2 = ⋆k.
+#T2 #k #des elim des -des
+[ #H <(lifts_inv_nil … H) -H //
+| #d #e #des #IH #H
+ elim (lifts_inv_cons … H) -H #X #H
+ >(lift_inv_sort1 … H) -H /2 width=1/
+]
+qed-.
+
+(* Basic_1: was: lift1_lref *)
+lemma lifts_inv_lref1: ∀T2,des,i1. ⇧*[des] #i1 ≡ T2 →
+ ∃∃i2. @[i1] des ≡ i2 & T2 = #i2.
+#T2 #des elim des -des
+[ #i1 #H <(lifts_inv_nil … H) -H /2 width=3/
+| #d #e #des #IH #i1 #H
+ elim (lifts_inv_cons … H) -H #X #H1 #H2
+ elim (lift_inv_lref1 … H1) -H1 * #Hdi1 #H destruct
+ elim (IH … H2) -IH -H2 /3 width=3/
+]
+qed-.
+
+lemma lifts_inv_gref1: ∀T2,p,des. ⇧*[des] §p ≡ T2 → T2 = §p.
+#T2 #p #des elim des -des
+[ #H <(lifts_inv_nil … H) -H //
+| #d #e #des #IH #H
+ elim (lifts_inv_cons … H) -H #X #H
+ >(lift_inv_gref1 … H) -H /2 width=1/
+]
+qed-.
+
+(* Basic_1: was: lift1_bind *)
+lemma lifts_inv_bind1: ∀I,T2,des,V1,U1. ⇧*[des] ⓑ{I} V1. U1 ≡ T2 →
+ ∃∃V2,U2. ⇧*[des] V1 ≡ V2 & ⇧*[des + 1] U1 ≡ U2 &
+ T2 = ⓑ{I} V2. U2.
#I #T2 #des elim des -des
[ #V1 #U1 #H
<(lifts_inv_nil … H) -H /2 width=5/
]
qed-.
-lemma lifts_inv_flat1: ∀I,T2,des,V1,U1. ⇑[des] 𝕗{I} V1. U1 ≡ T2 →
- ∃∃V2,U2. ⇑[des] V1 ≡ V2 & ⇑[des] U1 ≡ U2 &
- T2 = 𝕗{I} V2. U2.
+(* Basic_1: was: lift1_flat *)
+lemma lifts_inv_flat1: ∀I,T2,des,V1,U1. ⇧*[des] ⓕ{I} V1. U1 ≡ T2 →
+ ∃∃V2,U2. ⇧*[des] V1 ≡ V2 & ⇧*[des] U1 ≡ U2 &
+ T2 = ⓕ{I} V2. U2.
#I #T2 #des elim des -des
[ #V1 #U1 #H
<(lifts_inv_nil … H) -H /2 width=5/
(* Basic forward lemmas *****************************************************)
-lemma lifts_simple_dx: â\88\80T1,T2,des. â\87\91[des] T1 ≡ T2 → 𝕊[T1] → 𝕊[T2].
+lemma lifts_simple_dx: â\88\80T1,T2,des. â\87§*[des] T1 ≡ T2 → 𝕊[T1] → 𝕊[T2].
#T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_dx/
qed-.
-lemma lifts_simple_sn: â\88\80T1,T2,des. â\87\91[des] T1 ≡ T2 → 𝕊[T2] → 𝕊[T1].
+lemma lifts_simple_sn: â\88\80T1,T2,des. â\87§*[des] T1 ≡ T2 → 𝕊[T2] → 𝕊[T1].
#T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_sn/
qed-.
(* Basic properties *********************************************************)
-lemma lifts_bind: â\88\80I,T2,V1,V2,des. â\87\91[des] V1 ≡ V2 →
- â\88\80T1. â\87\91[ss des] T1 ≡ T2 →
- â\87\91[des] ð\9d\95\93{I} V1. T1 â\89¡ ð\9d\95\93{I} V2. T2.
+lemma lifts_bind: â\88\80I,T2,V1,V2,des. â\87§*[des] V1 ≡ V2 →
+ â\88\80T1. â\87§*[des + 1] T1 ≡ T2 →
+ â\87§*[des] â\93\91{I} V1. T1 â\89¡ â\93\91{I} V2. T2.
#I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
[ #V #T1 #H >(lifts_inv_nil … H) -H //
| #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
]
qed.
-lemma lifts_flat: â\88\80I,T2,V1,V2,des. â\87\91[des] V1 ≡ V2 →
- â\88\80T1. â\87\91[des] T1 ≡ T2 →
- â\87\91[des] ð\9d\95\97{I} V1. T1 â\89¡ ð\9d\95\97{I} V2. T2.
+lemma lifts_flat: â\88\80I,T2,V1,V2,des. â\87§*[des] V1 ≡ V2 →
+ â\88\80T1. â\87§*[des] T1 ≡ T2 →
+ â\87§*[des] â\93\95{I} V1. T1 â\89¡ â\93\95{I} V2. T2.
#I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
[ #V #T1 #H >(lifts_inv_nil … H) -H //
| #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
]
qed.
-lemma lifts_total: â\88\80des,T1. â\88\83T2. â\87\91[des] T1 ≡ T2.
+lemma lifts_total: â\88\80des,T1. â\88\83T2. â\87§*[des] T1 ≡ T2.
#des elim des -des /2 width=2/
#d #e #des #IH #T1
elim (lift_total T1 d e) #T #HT1