lift1/fwd lifts1_flat
lift1/fwd lifts1_nil
lift1/fwd lifts1_cons
-lift1/props lift1_lift1
-lift1/props lift1_xhg
-lift1/props lifts1_xhg
lift1/props lift1_free
lift/props thead_x_lift_y_y
lift/props lifts_tapp
axiom ldrops_lsubc_trans: ∀RP,L1,K1,des. ⇩*[des] L1 ≡ K1 → ∀K2. K1 [RP] ⊑ K2 →
∃∃L2. L1 [RP] ⊑ L2 & ⇩*[des] L2 ≡ K2.
-axiom lifts_trans: ∀T1,T,des1. ⇧*[des1] T1 ≡ T → ∀T2:term. ∀des2. ⇧*[des2] T ≡ T2 →
- ⇧*[des1 @ des2] T1 ≡ T2.
-
axiom ldrops_trans: ∀L1,L,des1. ⇩*[des1] L1 ≡ L → ∀L2,des2. ⇩*[des2] L ≡ L2 →
⇩*[des2 @ des1] L1 ≡ L2.
(**************************************************************************)
include "Basic_2/grammar/aarity.ma".
-include "Basic_2/unfold/lifts_vector.ma".
+include "Basic_2/unfold/lifts_lifts_vector.ma".
include "Basic_2/computation/acp.ma".
(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
@conj /2 width=1/ /2 width=6 by rp_lifts/
qed.
-axiom aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
+lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
∀A. acr RR RS RP (aacr RP A).
-(*
#RR #RS #RP #H1RP #H2RP #A elim A -A normalize //
#B #A #IHB #IHA @mk_acr normalize
[ #L #T #H
- lapply (H ? (⋆0) ? ⟠ ? ? ?) -H
+ lapply (H ? (⋆0) ? ⟠ ? ? ?) -H
[1,3: // |2,4: skip
| @(s2 … IHB … ◊) // /2 width=2/
| #H @(cp3 … H1RP … 0) @(s1 … IHA) //
@(HA … (ss des)) /2 width=1/
[ @(s7 … IHB … HB … HV120) /2 width=1/
| @liftsv_applv //
+ elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s
+ >(liftv_mono … HV12s … HV10s) -V1s //
]
| #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct
- @(s6 … IHA … (V0 :: V0s)) /2 width=6 by rp_lifts/ /3 width=4/
+ @(s6 … IHA … (V0 :: V0s)) /2 width=6 by rp_lifts/ /3 width=4/
| /3 width=7/
]
qed.
-*)
+
lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
∀L,W,T,A,B. RP L W → (
∀L0,V0,T0,des. ⇩*[des] L0 ≡ L → ⇧*[ss des] T ≡ T0 →
- ⦃L0, V0⦄ [RP] ϵ 〚B〛→ ⦃L0. 𝕓{Abbr} V0, T0⦄ [RP] ϵ 〚A〛
+ ⦃L0, V0⦄ [RP] ϵ 〚B〛 → ⦃L0. 𝕓{Abbr} V0, T0⦄ [RP] ϵ 〚A〛
) →
⦃L, 𝕓{Abst} W. T⦄ [RP] ϵ 〚𝕔 B. A〛.
#RR #RS #RP #H1RP #H2RP #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HB #HL0 #H
lapply (aacr_acr … H1RP H2RP A) #HCA
lapply (aacr_acr … H1RP H2RP B) #HCB
elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
-lapply (s1 … HCB) -HCB #HCB
+lapply (s1 … HCB) -HCB #HCB
@(s3 … HCA … ◊) /2 width=6 by rp_lifts/
@(s5 … HCA … ◊ ◊) // /2 width=1/ /2 width=3/
qed.
(* Main properies ***********************************************************)
(* Basic_1: was: lift_inj *)
-theorem lift_inj: ∀d,e,T1,U. ⇧[d,e] T1 ≡ U → ∀T2. ⇧[d,e] T2 ≡ U → T1 = T2.
+theorem lift_inj: ∀d,e,T1,U. ⇧[d,e] T1 ≡ U → ∀T2. ⇧[d,e] T2 ≡ U → T1 = T2.
#d #e #T1 #U #H elim H -d -e -T1 -U
[ #k #d #e #X #HX
lapply (lift_inv_sort2 … HX) -HX //
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic_2/substitution/lift_lift.ma".
+include "Basic_2/substitution/lift_vector.ma".
+
+(* RELOCATION ***************************************************************)
+
+(* Main properies ***********************************************************)
+
+theorem liftv_mono: ∀Ts,U1s,d,e. ⇧[d,e] Ts ≡ U1s →
+ ∀U2s:list term. ⇧[d,e] Ts ≡ U2s → U1s = U2s.
+#Ts #U1s #d #e #H elim H -Ts -U1s
+[ #U2s #H >(liftv_inv_nil1 … H) -H //
+| #Ts #U1s #T #U1 #HTU1 #_ #IHTU1s #X #H destruct
+ elim (liftv_inv_cons1 … H) -H #U2 #U2s #HTU2 #HTU2s #H destruct
+ >(lift_mono … HTU1 … HTU2) -T /3 width=1/
+]
+qed.
interpretation "relocation (vector)" 'RLift d e T1s T2s = (liftv d e T1s T2s).
+(* Basic inversion lemmas ***************************************************)
+
+fact liftv_inv_nil1_aux: ∀T1s,T2s,d,e. ⇧[d, e] T1s ≡ T2s → T1s = ◊ → T2s = ◊.
+#T1s #T2s #d #e * -T1s -T2s //
+#T1s #T2s #T1 #T2 #_ #_ #H destruct
+qed.
+
+lemma liftv_inv_nil1: ∀T2s,d,e. ⇧[d, e] ◊ ≡ T2s → T2s = ◊.
+/2 width=5/ qed-.
+
+fact liftv_inv_cons1_aux: ∀T1s,T2s,d,e. ⇧[d, e] T1s ≡ T2s →
+ ∀U1,U1s. T1s = U1 :: U1s →
+ ∃∃U2,U2s. ⇧[d, e] U1 ≡ U2 & ⇧[d, e] U1s ≡ U2s &
+ T2s = U2 :: U2s.
+#T1s #T2s #d #e * -T1s -T2s
+[ #U1 #U1s #H destruct
+| #T1s #T2s #T1 #T2 #HT12 #HT12s #U1 #U1s #H destruct /2 width=5/
+]
+qed.
+
+lemma liftv_inv_cons1: ∀U1,U1s,T2s,d,e. ⇧[d, e] U1 :: U1s ≡ T2s →
+ ∃∃U2,U2s. ⇧[d, e] U1 ≡ U2 & ⇧[d, e] U1s ≡ U2s &
+ T2s = U2 :: U2s.
+/2 width=3/ qed-.
+
(* Basic properties *********************************************************)
lemma liftv_total: ∀d,e. ∀T1s:list term. ∃T2s. ⇧[d, e] T1s ≡ T2s.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic_2/substitution/lift_lift.ma".
+include "Basic_2/unfold/lifts.ma".
+
+(* GENERIC RELOCATION *******************************************************)
+
+(* Main properties **********************************************************)
+
+(* Basic_1: was: lift1_xhg *)
+lemma lifts_lift_trans_le: ∀T1,T,des. ⇧*[des] T1 ≡ T → ∀T2. ⇧[0, 1] T ≡ T2 →
+ ∃∃T0. ⇧[0, 1] T1 ≡ T0 & ⇧*[ss des] T0 ≡ T2.
+#T1 #T #des #H elim H -T1 -T -des
+[ /2 width=3/
+| #T1 #T3 #T #des #d #e #HT13 #_ #IHT13 #T2 #HT2
+ elim (IHT13 … HT2) -T #T #HT3 #HT2
+ elim (lift_trans_le … HT13 … HT3 ?) -T3 // /3 width=5/
+]
+qed-.
+
+(* Basic_1: was: lift1_lift1 *)
+theorem lifts_trans: ∀T1,T,des1. ⇧*[des1] T1 ≡ T → ∀T2:term. ∀des2. ⇧*[des2] T ≡ T2 →
+ ⇧*[des1 @ des2] T1 ≡ T2.
+#T1 #T #des1 #H elim H -T1 -T -des1 // /3 width=3/
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic_2/substitution/lift_lift_vector.ma".
+include "Basic_2/unfold/lifts_lifts.ma".
+include "Basic_2/unfold/lifts_vector.ma".
+
+(* GENERIC RELOCATION *******************************************************)
+
+(* Main properties **********************************************************)
+
+(* Basic_1: was: lifts1_xhg *)
+lemma liftsv_liftv_trans_le: ∀T1s,Ts,des. ⇧*[des] T1s ≡ Ts →
+ ∀T2s:list term. ⇧[0, 1] Ts ≡ T2s →
+ ∃∃T0s. ⇧[0, 1] T1s ≡ T0s & ⇧*[ss des] T0s ≡ T2s.
+#T1s #Ts #des #H elim H -T1s -Ts
+[ #T1s #H
+ >(liftv_inv_nil1 … H) -T1s /2 width=3/
+| #T1s #Ts #T1 #T #HT1 #_ #IHT1s #X #H
+ elim (liftv_inv_cons1 … H) -H #T2 #T2s #HT2 #HT2s #H destruct
+ elim (IHT1s … HT2s) -Ts #Ts #HT1s #HT2s
+ elim (lifts_lift_trans_le … HT1 … HT2) -T /3 width=5/
+]
+qed-.
| nil2 : list2 A1 A2
| cons2: A1 → A2 → list2 A1 A2 → list2 A1 A2.
-interpretation "nil (list of pairs)" 'Nil2 = (nil2 ? ?). (**) (* 'Nil causes unification error in aacr_abst *)
+interpretation "nil (list of pairs)" 'Nil2 = (nil2 ? ?).
interpretation "cons (list of pairs)" 'Cons hd1 hd2 tl = (cons2 ? ? hd1 hd2 tl).
projects / helm.git / commitdiff