(mk_rtm G u E S T)
| rtm_appl : ∀G,u,E,S,V,T.
rtm_step (mk_rtm G u E S (ⓐV. T))
- (mk_rtm G u E ({E, V} :: S) T)
+ (mk_rtm G u E ({E, V} @ S) T)
| rtm_beta : ∀G,u,E,F,V,S,W,T.
- rtm_step (mk_rtm G u E ({F, V} :: S) (ⓛW. T))
+ rtm_step (mk_rtm G u E ({F, V} @ S) (ⓛW. T))
(mk_rtm G u (E. ④{Abbr} {u, F, V}) S T)
| rtm_push : ∀G,u,E,W,T.
rtm_step (mk_rtm G u E ⟠ (ⓛW. T))
pc3/props pc3_pr2_pr3_t
pc3/props pc3_pr3_pc3_t
pc3/props pc3_eta
-pc3/subst1 pc3_gen_cabbr
pc3/wcpr0 pc3_wcpr0__pc3_wcpr0_t_aux
pc3/wcpr0 pc3_wcpr0_t
pc3/wcpr0 pc3_wcpr0
pr1/props pr1_comp
pr1/props pr1_eta
pr2/fwd pr2_gen_void
-pr2/subst1 pr2_gen_cabbr
pr3/fwd pr3_gen_void
pr3/pr1 pr3_pr1
pr3/props pr3_eta
-pr3/subst1 pr3_gen_cabbr
sn3/props sns3_lifts
sty1/cnt sty1_cnt
sty1/props sty1_trans
ty3/pr3_props ty3_sconv_pc3
ty3/pr3_props ty3_sred_back
ty3/pr3_props ty3_sconv
-ty3/props ty3_unique
ty3/props ty3_gen_abst_abst
ty3/sty0 ty3_sty0
ty3/subst1 ty3_gen_cabbr
#L3 #V3 #T3 #des3 #HL32 #HT03 #HB
elim (lifts_total des3 W0) #W2 #HW02
elim (ldrops_lsubc_trans … H1RP H2RP … HL32 … HL02) -L2 #L2 #HL32 #HL20
- lapply (aaa_lifts … L2 W2 … (des @ des3) … HLWB) -HLWB /2 width=3/ #HLW2B
- @(IHA (L2. ⓛW2) … (des + 1 @ des3 + 1)) -IHA
+ lapply (aaa_lifts … L2 W2 … (des @@ des3) … HLWB) -HLWB /2 width=3/ #HLW2B
+ @(IHA (L2. ⓛW2) … (des + 1 @@ des3 + 1)) -IHA
/2 width=3/ /3 width=5/
]
| #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
| #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct
lapply (s1 … IHB … HB) #HV0
- @(s2 … IHA … (V0 :: V0s)) /2 width=4 by lifts_simple_dx/ /3 width=6/
+ @(s2 … IHA … (V0 @ V0s)) /2 width=4 by lifts_simple_dx/ /3 width=6/
| #L #Vs #U #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 #U0 #X #HU0 #HX #H destruct
elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct
- @(s3 … IHA … (V0 :: V0s)) /2 width=6 by rp_lifts/ /4 width=5/
+ @(s3 … IHA … (V0 @ V0s)) /2 width=6 by rp_lifts/ /4 width=5/
| #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct
elim (lift_total W1 0 (i0 + 1)) #W2 #HW12
elim (lifts_lift_trans … Hdes0 … HVW1 … HW12) // -Hdes0 -Hi0 #V3 #HV13 #HVW2
>(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2
- @(s4 … IHA … (V0 :: V0s) … HW12 HL02) /3 width=4/
+ @(s4 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=4/
| #L #V1s #V2s #HV12s #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct
elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct
elim (lift_total V10 0 1) #V20 #HV120
elim (liftv_total 0 1 V10s) #V20s #HV120s
- @(s5 … IHA … (V10 :: V10s) (V20 :: V20s)) /2 width=1/ /2 width=6 by rp_lifts/
+ @(s5 … IHA … (V10 @ V10s) (V20 @ V20s)) /2 width=1/ /2 width=6 by rp_lifts/
@(HA … (des + 1)) /2 width=1/
[ @(s7 … IHB … HB … HV120) /2 width=1/
| @lifts_applv //
| #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.
--- /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/reducibility/cpr_delift.ma".
+include "basic_2/computation/cprs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
+
+(* Properties on inverse basic term relocation ******************************)
+
+(* Basic_1: was only: pr3_gen_cabbr *)
+lemma thin_cprs_delift_conf: ∀L,U1,U2. L ⊢ U1 ➡* U2 →
+ ∀K,d,e. L [d, e] ≡ K → ∀T1. L ⊢ U1 [d, e] ≡ T1 →
+ ∃∃T2. K ⊢ T1 ➡* T2 & L ⊢ U2 [d, e] ≡ T2.
+#L #U1 #U2 #H @(cprs_ind … H) -U2 /2 width=3/
+#U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1
+elim (IHU1 … HLK … HTU1) -U1 #T #HT1 #HUT
+elim (thin_cpr_delift_conf … HU2 … HLK … HUT) -U -HLK /3 width=3/
+qed.
lapply (csn_fwd_pair_sn … H) #HW1
lapply (csn_fwd_flat_dx … H) #H1
@csn_appl_simple_tstc // -HW1 /2 width=3/ -IHV12s -HV -H1 #X #H1 #H2
-elim (cprs_fwd_theta_vector … (V2::V2s) … H1) -H1 /2 width=1/ -HV12s -HV12
+elim (cprs_fwd_theta_vector … (V2@V2s) … H1) -H1 /2 width=1/ -HV12s -HV12
[ -H #H elim (H2 ?) -H2 //
| -H2 #H1 @(csn_cprs_trans … H) -H /2 width=1/
]
(* Basic inversion lemmas ***************************************************)
-lemma csnv_inv_cons: ∀L,T,Ts. L ⊢ ⬇* T :: Ts → L ⊢ ⬇* T ∧ L ⊢ ⬇* Ts.
+lemma csnv_inv_cons: ∀L,T,Ts. L ⊢ ⬇* T @ Ts → L ⊢ ⬇* T ∧ L ⊢ ⬇* Ts.
normalize // 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/equivalence/cpcs_cpcs.ma".
+include "basic_2/dynamic/nta.ma".
+
+(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
+
+(* alternative definition of nta *)
+inductive ntaa (h:sh): lenv → relation term ≝
+| ntaa_sort: ∀L,k. ntaa h L (⋆k) (⋆(next h k))
+| ntaa_ldef: ∀L,K,V,W,U,i. ⇩[0, i] L ≡ K. ⓓV → ntaa h K V W →
+ ⇧[0, i + 1] W ≡ U → ntaa h L (#i) U
+| ntaa_ldec: ∀L,K,W,V,U,i. ⇩[0, i] L ≡ K. ⓛW → ntaa h K W V →
+ ⇧[0, i + 1] W ≡ U → ntaa h L (#i) U
+| ntaa_bind: ∀I,L,V,W,T,U. ntaa h L V W → ntaa h (L. ⓑ{I} V) T U →
+ ntaa h L (ⓑ{I}V.T) (ⓑ{I}V.U)
+| ntaa_appl: ∀L,V,W,T,U. ntaa h L V W → ntaa h L (ⓛW.T) (ⓛW.U) →
+ ntaa h L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U)
+| ntaa_pure: ∀L,V,W,T,U. ntaa h L T U → ntaa h L (ⓐV.U) W →
+ ntaa h L (ⓐV.T) (ⓐV.U)
+| ntaa_cast: ∀L,T,U,W. ntaa h L T U → ntaa h L U W → ntaa h L (ⓣU. T) U
+| ntaa_conv: ∀L,T,U1,U2,V2. ntaa h L T U1 → L ⊢ U1 ⬌* U2 → ntaa h L U2 V2 →
+ ntaa h L T U2
+.
+
+interpretation "native type assignment (term) alternative"
+ 'NativeTypeAlt h L T U = (ntaa h L T U).
+
+(* Advanced inversion lemmas ************************************************)
+
+fact ntaa_inv_bind1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T :: U → ∀J,X,Y. T = ⓑ{J}Y.X →
+ ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y :: Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X :: Z2 &
+ L ⊢ ⓑ{J}Y.Z2 ⬌* U.
+#h #L #T #U #H elim H -L -T -U
+[ #L #k #J #X #Y #H destruct
+| #L #K #V #W #U #i #_ #_ #_ #_ #J #X #Y #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #_ #J #X #Y #H destruct
+| #I #L #V #W #T #U #HVW #HTU #_ #_ #J #X #Y #H destruct /2 width=3/
+| #L #V #W #T #U #_ #_ #_ #_ #J #X #Y #H destruct
+| #L #V #W #T #U #_ #_ #_ #_ #J #X #Y #H destruct
+| #L #T #U #W #_ #_ #_ #_ #J #X #Y #H destruct
+| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #J #X #Y #H destruct
+ elim (IHTU1 ????) -IHTU1 [5: // |2,3,4: skip ] #Z1 #Z2 #HZ1 #HZ2 #HU1
+ lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/
+]
+qed.
+
+lemma ntaa_inv_bind1: ∀h,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{J}Y.X :: U →
+ ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y :: Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X :: Z2 &
+ L ⊢ ⓑ{J}Y.Z2 ⬌* U.
+/2 width=3/ qed-.
+
+lemma ntaa_nta: ∀h,L,T,U. ⦃h, L⦄ ⊢ T :: U → ⦃h, L⦄ ⊢ T : U.
+#h #L #T #U #H elim H -L -T -U
+// /2 width=1/ /2 width=2/ /2 width=3/ /2 width=6/
+qed-.
+
+(* Properties on relocation *************************************************)
+
+lemma ntaa_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 :: U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
+ ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 :: U2.
+#h #L1 #T1 #U1 #H elim H -L1 -T1 -U1
+[ #L1 #k #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+ >(lift_inv_sort1 … H1) -X1
+ >(lift_inv_sort1 … H2) -X2 //
+| #L1 #K1 #V1 #W1 #W #i #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2
+ elim (lift_inv_lref1 … H) * #Hid #H destruct
+ [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2
+ elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
+ elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct
+ /3 width=8/
+ | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
+ lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
+ ]
+| #L1 #K1 #W1 #V1 #W #i #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2
+ elim (lift_inv_lref1 … H) * #Hid #H destruct
+ [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // <minus_plus #W #HW1 #HWU2
+ elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
+ elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #W2 #HK21 #HW12 #H destruct
+ lapply (lift_mono … HW1 … HW12) -HW1 #H destruct
+ elim (lift_total V1 (d-i-1) e) /3 width=8/
+ | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
+ lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
+ ]
+| #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+ elim (lift_inv_bind1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
+ elim (lift_inv_bind1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
+ lapply (lift_mono … H1 … HV12) -H1 #H destruct
+ elim (lift_total W1 d e) /4 width=6/
+| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+ elim (lift_inv_flat1 … H1) -H1 #V2 #X #HV12 #H1 #H destruct
+ elim (lift_inv_bind1 … H1) -H1 #W2 #T2 #HW12 #HT12 #H destruct
+ elim (lift_inv_flat1 … H2) -H2 #Y2 #X #HY #H2 #H destruct
+ elim (lift_inv_bind1 … H2) -H2 #X2 #U2 #HX #HU12 #H destruct
+ lapply (lift_mono … HY … HV12) -HY #H destruct
+ lapply (lift_mono … HX … HW12) -HX #H destruct /4 width=6/
+| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+ elim (lift_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
+ elim (lift_inv_flat1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
+ lapply (lift_mono … H1 … HV12) -H1 #H destruct
+ elim (lift_total W1 d e) /4 width=6/
+| #L1 #T1 #U1 #W1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL21 #X #H #U2 #HU12
+ elim (lift_inv_flat1 … H) -H #X2 #T2 #HUX2 #HT12 #H destruct
+ lapply (lift_mono … HUX2 … HU12) -HUX2 #H destruct
+ elim (lift_total W1 d e) /3 width=6/
+| #L1 #T1 #U11 #U12 #V12 #_ #HU112 #_ #IHTU11 #IHUV12 #L2 #d #e #HL21 #U1 #HTU1 #U2 #HU12
+ elim (lift_total U11 d e) #U #HU11
+ elim (lift_total V12 d e) #V22 #HV122
+ lapply (cpcs_lift … HL21 … HU11 … HU12 HU112) -HU112 /3 width=6/
+]
+qed.
+
+(* Advanced forvard lemmas **************************************************)
+
+lemma ntaa_fwd_correct: ∀h,L,T,U. ⦃h, L⦄ ⊢ T :: U → ∃T0. ⦃h, L⦄ ⊢ U :: T0.
+#h #L #T #U #H elim H -L -T -U
+[ /2 width=2/
+| #L #K #V #W #W0 #i #HLK #_ #HW0 * #V0 #HWV0
+ lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+ elim (lift_total V0 0 (i+1)) /3 width=10/
+| #L #K #W #V #V0 #i #HLK #HWV #HWV0 #_
+ lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+ elim (lift_total V 0 (i+1)) /3 width=10/
+| #I #L #V #W #T #U #HVW #_ #_ * /3 width=2/
+| #L #V #W #T #U #HVW #_ #_ * #X #H
+ elim (ntaa_inv_bind1 … H) -H /4 width=2/
+| #L #V #W #T #U #_ #HUW * #T0 #HUT0 /3 width=2/
+| /2 width=2/
+| /2 width=2/
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma nta_ntaa: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ T :: U.
+#h #L #T #U #H elim H -L -T -U
+// /2 width=1/ /2 width=2/ /2 width=3/ /2 width=6/
+#L #T #U #_ #HTU
+elim (ntaa_fwd_correct … HTU) /2 width=2/
+qed.
+
+(* Advanced eliminators *****************************************************)
+
+lemma nta_ind_alt: ∀h. ∀R:lenv→relation term.
+ (∀L,k. R L ⋆k ⋆(next h k)) →
+ (∀L,K,V,W,U,i.
+ ⇩[O, i] L ≡ K.ⓓV → ⦃h, K⦄ ⊢ V : W → ⇧[O, i + 1] W ≡ U →
+ R K V W → R L (#i) U
+ ) →
+ (∀L,K,W,V,U,i.
+ ⇩[O, i] L ≡ K.ⓛW → ⦃h, K⦄ ⊢ W : V → ⇧[O, i + 1] W ≡ U →
+ R K W V → R L (#i) U
+ ) →
+ (∀I,L,V,W,T,U.
+ ⦃h, L⦄ ⊢ V : W → ⦃h, L.ⓑ{I}V⦄ ⊢ T : U →
+ R L V W → R (L.ⓑ{I}V) T U → R L (ⓑ{I}V.T) (ⓑ{I}V.U)
+ ) →
+ (∀L,V,W,T,U.
+ ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ (ⓛW.T):(ⓛW.U) →
+ R L V W →R L (ⓛW.T) (ⓛW.U) →R L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U)
+ ) →
+ (∀L,V,W,T,U.
+ ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ (ⓐV.U) : W →
+ R L T U → R L (ⓐV.U) W → R L (ⓐV.T) (ⓐV.U)
+ ) →
+ (∀L,T,U,W.
+ ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W →
+ R L T U → R L U W → R L (ⓣU.T) U
+ ) →
+ (∀L,T,U1,U2,V2.
+ ⦃h, L⦄ ⊢ T : U1 → L ⊢ U1 ⬌* U2 → ⦃h, L⦄ ⊢ U2 : V2 →
+ R L T U1 →R L U2 V2 →R L T U2
+ ) →
+ ∀L,T,U. ⦃h, L⦄ ⊢ T : U → R L T U.
+#h #R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #L #T #U #H elim (nta_ntaa … H) -L -T -U
+// /3 width=1 by ntaa_nta/ /3 width=3 by ntaa_nta/ /3 width=4 by ntaa_nta/
+/3 width=7 by ntaa_nta/
+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/unfold/delift_lift.ma".
+include "basic_2/unfold/thin_ldrop.ma".
+include "basic_2/equivalence/cpcs_delift.ma".
+include "basic_2/dynamic/nta_nta.ma".
+
+(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
+
+(* Properties on reverse basic term relocation ******************************)
+
+(* Basic_1: was only: ty3_gen_cabbr *)
+axiom thin_nta_delift_conf: ∀h,L1,T1,X1. ⦃h, L1⦄ ⊢ T1 : X1 →
+ ∀L2,d,e. L1 [d, e] ≡ L2 →
+ ∀T2. L1 ⊢ T1 [d, e] ≡ T2 →
+ ∃∃U1,U2. ⦃h, L2⦄ ⊢ T2 : U2 & L1 ⊢ U1 [d, e] ≡ U2 &
+ L1 ⊢ U1 ⬌* X1.
+(*
+#h #L1 #T1 #U1 #H @(nta_ind_alt … H) -L1 -T1 -U1
+[ #L1 #k #L2 #d #e #HL12 #X #H
+ >(delift_inv_sort1 … H) -X /2 width=5/
+| #L1 #K1 #V1 #W1 #U1 #i #HLK1 #_ #HWU1 #IHVW1 #L2 #d #e #HL12 #X #H
+(*
+ elim (delift_inv_lref1 … H) -H *
+ [ #Hid #H destruct
+ elim (thin_ldrop_conf_le … HL12 … HLK1 ?) -HL12 /2 width=2/ #X #H #HLK2
+ lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 #HLK1
+ elim (thin_inv_delift1 … H ?) -H /2 width=1/ #K2 #V2 #HK12 #HV12 #H destruct
+ elim (IHVW1 … HK12 … HV12) -IHVW1 -HK12 -HV12 #W2 #HVW2 #HW12
+ elim (lift_total W2 0 (i+1)) #U2 #HWU2
+ @(ex2_1_intro … U2)
+ [ /2 width=6/
+ | -HVW2 -HLK2
+ ]
+ |
+ |
+ ]
+*)
+|
+|
+|
+| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHVW1 #L2 #d #e #HL12 #X #H
+ elim (delift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+(*
+ elim (IHTU1 … HL12 … HT12) -T1 #U2 #HTU2 #HU12
+ elim (IHVW1 … HL12 (ⓐV2.U2) ?) -IHVW1 -HL12
+ [ /3 width=5/ | /2 width=1/ ]
+*)
+| #L1 #T1 #X1 #Y1 #_ #_ #IHTX1 #IHXY1 #L2 #d #e #HL12 #X #H
+ elim (delift_inv_flat1 … H) -H #X2 #T2 #HX12 #HT12 #H destruct
+ elim (IHTX1 … HL12 … HT12) -T1 #U1 #U2 #HTU2 #HU12 #HUX1
+ elim (IHXY1 … HL12 … HX12) -IHXY1 #W1 #W2 #HXW2 #_ #_ -Y1 -W1
+ lapply (thin_cpcs_delift_mono … HUX1 … HL12 … HU12 … HX12) -HL12 -HX12 /4 width=5/
+| #L1 #T1 #X11 #X12 #V1 #_ #HX112 #_ #IHT1 #_ #L2 #d #e #HL12 #T2 #HT12
+ elim (IHT1 … HL12 … HT12) -T1 -HL12 #U21 #U22 #HTU22 #HU212 #HUX211
+ lapply (cpcs_trans … HUX211 … HX112) -X11 /2 width=5/
+]
+*)
+lemma nta_inv_lift1_delift: ∀h,L1,T1,X. ⦃h, L1⦄ ⊢ T1 : X →
+ ∀L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀T2. ⇧[d, e] T2 ≡ T1 →
+ ∃∃U1,U2. ⦃h, L2⦄ ⊢ T2 : U2 & L1 ⊢ U1 [d, e] ≡ U2 &
+ L1 ⊢ U1 ⬌* X.
+/3 width=3/ qed-.
+
+lemma nta_inv_lift1: ∀h,L1,T1,X. ⦃h, L1⦄ ⊢ T1 : X →
+ ∀L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀T2. ⇧[d, e] T2 ≡ T1 →
+ ∃∃U1,U2. ⦃h, L2⦄ ⊢ T2 : U2 & ⇧[d, e] U2 ≡ U1 &
+ L1 ⊢ U1 ⬌* X.
+#h #L1 #T1 #X #H #L2 #d #e #HL12 #T2 #HT21
+elim (nta_inv_lift1_delift … H … HL12 … HT21) -T1 -HL12 #U1 #U2 #HTU2 * #U #HU1 #HU2 #HU1X
+lapply (cpcs_cpr_conf … U … HU1X) -HU1X /2 width=3/ -U1 /2 width=5/
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/equivalence/cpcs_cpcs.ma".
-include "basic_2/dynamic/nta.ma".
+include "basic_2/dynamic/nta_alt.ma".
(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
).
/2 width=3/ qed-.
-fact nta_inv_bind1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀J,X,Y. T = ⓑ{J}Y.X →
- ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X : Z2 &
- L ⊢ ⓑ{J}Y.Z2 ⬌* U.
-#h #L #T #U #H elim H -L -T -U
-[ #L #k #J #X #Y #H destruct
-| #L #K #V #W #U #i #_ #_ #_ #_ #J #X #Y #H destruct
-| #L #K #W #V #U #i #_ #_ #_ #_ #J #X #Y #H destruct
-| #I #L #V #W #T #U #HVW #HTU #_ #_ #J #X #Y #H destruct /2 width=3/
-| #L #V #W #T #U #_ #_ #_ #_ #J #X #Y #H destruct
-| #L #V #W #T #U #_ #_ #_ #_ #J #X #Y #H destruct
-| #L #T #U #_ #_ #J #X #Y #H destruct
-| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #J #X #Y #H destruct
- elim (IHTU1 ????) -IHTU1 [5: // |2,3,4: skip ] #Z1 #Z2 #HZ1 #HZ2 #HU1
- lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/
-]
-qed.
-
(* Basic_1: was: ty3_gen_bind *)
-lemma nta_inv_bind1: ∀h,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{J}Y.X : U →
- ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X : Z2 &
- L ⊢ ⓑ{J}Y.Z2 ⬌* U.
-/2 width=3/ qed-.
+lemma nta_inv_bind1: ∀h,I,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{I}Y.X : U →
+ ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{I}Y⦄ ⊢ X : Z2 &
+ L ⊢ ⓑ{I}Y.Z2 ⬌* U.
+#h #I #L #Y #X #U #H
+elim (ntaa_inv_bind1 … (nta_ntaa … H)) -H /3 width=3 by ntaa_nta, ex3_2_intro/
+qed-.
fact nta_inv_cast1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓣY.X →
⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
lemma nta_inv_cast1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓣY.X : U → ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
/2 width=3/ qed-.
-(* Properties on relocation *************************************************)
+(* Advanced forvard lemmas **************************************************)
-(* Basic_1: was: ty3_lift *)
-lemma nta_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
- ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 : U2.
-#h #L1 #T1 #U1 #H elim H -L1 -T1 -U1
-[ #L1 #k #L2 #d #e #HL21 #X1 #H1 #X2 #H2
- >(lift_inv_sort1 … H1) -X1
- >(lift_inv_sort1 … H2) -X2 //
-| #L1 #K1 #V1 #W1 #W #i #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2
- elim (lift_inv_lref1 … H) * #Hid #H destruct
- [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2
- elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
- elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct
- /3 width=8/
- | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
- lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
- ]
-| #L1 #K1 #W1 #V1 #W #i #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2
- elim (lift_inv_lref1 … H) * #Hid #H destruct
- [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // <minus_plus #W #HW1 #HWU2
- elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
- elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #W2 #HK21 #HW12 #H destruct
- lapply (lift_mono … HW1 … HW12) -HW1 #H destruct
- elim (lift_total V1 (d-i-1) e) /3 width=8/
- | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
- lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
- ]
-| #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
- elim (lift_inv_bind1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
- elim (lift_inv_bind1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
- lapply (lift_mono … H1 … HV12) -H1 #H destruct
- elim (lift_total W1 d e) /4 width=6/
-| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
- elim (lift_inv_flat1 … H1) -H1 #V2 #X #HV12 #H1 #H destruct
- elim (lift_inv_bind1 … H1) -H1 #W2 #T2 #HW12 #HT12 #H destruct
- elim (lift_inv_flat1 … H2) -H2 #Y2 #X #HY #H2 #H destruct
- elim (lift_inv_bind1 … H2) -H2 #X2 #U2 #HX #HU12 #H destruct
- lapply (lift_mono … HY … HV12) -HY #H destruct
- lapply (lift_mono … HX … HW12) -HX #H destruct /4 width=6/
-| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
- elim (lift_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
- elim (lift_inv_flat1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
- lapply (lift_mono … H1 … HV12) -H1 #H destruct
- elim (lift_total W1 d e) /4 width=6/
-| #L1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL21 #X #H #U2 #HU12
- elim (lift_inv_flat1 … H) -H #X2 #T2 #HUX2 #HT12 #H destruct
- lapply (lift_mono … HUX2 … HU12) -HUX2 #H destruct /3 width=5/
-| #L1 #T1 #U11 #U12 #V12 #_ #HU112 #_ #IHTU11 #IHUV12 #L2 #d #e #HL21 #U1 #HTU1 #U2 #HU12
- elim (lift_total U11 d e) #U #HU11
- elim (lift_total V12 d e) #V22 #HV122
- lapply (cpcs_lift … HL21 … HU11 … HU12 HU112) -HU112 /3 width=6/
+fact nta_fwd_appl1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓐY.X →
+ ∃∃V,W. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V & L ⊢ ⓐY.V ⬌* U.
+#h #L #T #U #H elim H -L -T -U
+[ #L #k #X #Y #H destruct
+| #L #K #V #W #U #i #_ #_ #_ #_ #X #Y #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #_ #X #Y #H destruct
+| #I #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
+| #L #V #W #T #U #HVW #HTU #_ #_ #X #Y #H destruct /2 width=3/
+| #L #V #W #T #U #HTU #_ #_ #IHUW #X #Y #H destruct
+ elim (IHUW U Y ?) -IHUW // /2 width=3/
+| #L #T #U #_ #_ #X #Y #H destruct
+| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct
+ elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #V #W #HYW #HXV #HU1
+ lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/
]
qed.
-(* Advanced forvard lemmas **************************************************)
+lemma nta_fwd_appl1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓐY.X : U →
+ ∃∃V,W. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V & L ⊢ ⓐY.V ⬌* U.
+/2 width=3/ qed-.
(* Basic_1: was: ty3_correct *)
lemma nta_fwd_correct: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ U : T0.
-#h #L #T #U #H elim H -L -T -U
-[ /2 width=2/
-| #L #K #V #W #W0 #i #HLK #_ #HW0 * #V0 #HWV0
- lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
- elim (lift_total V0 0 (i+1)) /3 width=10/
-| #L #K #W #V #V0 #i #HLK #HWV #HWV0 #_
- lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
- elim (lift_total V 0 (i+1)) /3 width=10/
-| #I #L #V #W #T #U #HVW #_ #_ * /3 width=2/
-| #L #V #W #T #U #HVW #_ #_ * #X #H
- elim (nta_inv_bind1 … H) -H /4 width=2/
-| #L #V #W #T #U #_ #HUW * #T0 #HUT0 /3 width=2/
-| #L #T #U #_ * /2 width=2/
-| /2 width=2/
-]
+#h #L #T #U #H
+elim (ntaa_fwd_correct … (nta_ntaa … H)) -H /3 width=2 by ntaa_nta, ex_intro/
qed-.
(* Advanced properties ******************************************************)
elim (nta_fwd_correct … HTU) #X #H
elim (nta_inv_bind1 … H) -H /4 width=2/
qed.
+
+(* Properties on relocation *************************************************)
+
+(* Basic_1: was: ty3_lift *)
+lemma nta_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
+ ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 : U2.
+/4 width=9 by ntaa_nta, nta_ntaa, ntaa_lift/ 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/dynamic/nta_lift.ma".
+
+(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
+
+(* Main properties **********************************************************)
+
+(* Basic_1: was: ty3_unique *)
+theorem nta_mono: ∀h,L,T,U1. ⦃h, L⦄ ⊢ T : U1 → ∀U2. ⦃h, L⦄ ⊢ T : U2 →
+ L ⊢ U1 ⬌* U2.
+#h #L #T #U1 #H elim H -L -T -U1
+[ #L #k #X #H
+ lapply (nta_inv_sort1 … H) -H //
+| #L #K #V #W11 #W12 #i #HLK #_ #HW112 #IHVW11 #X #H
+ elim (nta_inv_lref1 … H) -H * #K0 #V0 #W21 #W22 #HLK0 #HVW21 #HW212 #HX
+ lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+ @(cpcs_trans … HX) -X /3 width=9 by cpcs_lift/ (**) (* to slow without trace *)
+| #L #K #W #V1 #V #i #HLK #_ #HWV #_ #X #H
+ elim (nta_inv_lref1 … H) -H * #K0 #W0 #V2 #V0 #HLK0 #_ #HWV0 #HX
+ lapply (ldrop_mono … HLK0 … HLK) -HLK0 -HLK #H destruct
+ lapply (lift_mono … HWV0 … HWV) -HWV0 -HWV #H destruct //
+| #I #L #V #W1 #T #U1 #_ #_ #_ #IHTU1 #X #H
+ elim (nta_inv_bind1 … H) -H #W2 #U2 #_ #HTU2 #H
+ @(cpcs_trans … H) -X /3 width=1/
+| #L #V #W1 #T #U1 #_ #_ #_ #IHTU1 #X #H
+ elim (nta_fwd_appl1 … H) -H #U2 #W2 #_ #HTU2 #H
+ @(cpcs_trans … H) -X /3 width=1/
+| #L #V #W1 #T #U1 #_ #_ #IHTU1 #_ #X #H
+ elim (nta_fwd_appl1 … H) -H #U2 #W2 #_ #HTU2 #H
+ @(cpcs_trans … H) -X /3 width=1/
+| #L #T #U1 #_ #_ #X #H
+ elim (nta_inv_cast1 … H) -H //
+| #L #T #U11 #U12 #V12 #_ #HU112 #_ #IHTU11 #_ #U2 #HTU2
+ @(cpcs_canc_sn … HU112) -U12 /2 width=1/
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma nta_cast_alt: ∀h,L,T,W,U. ⦃h, L⦄ ⊢ T : W → ⦃h, L⦄ ⊢ T : U →
+ ⦃h, L⦄ ⊢ ⓣW.T : U.
+#h #L #T #W #U #HTW #HTU
+lapply (nta_mono … HTW … HTU) #HWU
+elim (nta_fwd_correct … HTU) -HTU /3 width=3/
+qed.
lemma cpcs_refl: ∀L,T. L ⊢ T ⬌* T.
/2 width=1/ qed.
+lemma cpcs_sym: ∀L,T1,T2. L ⊢ T1 ⬌* T2 → L ⊢ T2 ⬌* T1.
+/3 width=1/ qed.
+
lemma cpcs_strap1: ∀L,T1,T,T2. L ⊢ T1 ⬌* T → L ⊢ T ⬌ T2 → L ⊢ T1 ⬌* T2.
/2 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/unfold/delift_delift.ma".
+include "basic_2/computation/cprs_delift.ma".
+include "basic_2/equivalence/cpcs_cpcs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
+
+(* Properties on inverse basic term relocation ******************************)
+
+(* Basic_1: was only: pc3_gen_cabbr *)
+lemma thin_cpcs_delift_mono: ∀L,U1,U2. L ⊢ U1 ⬌* U2 →
+ ∀K,d,e. L [d, e] ≡ K → ∀T1. L ⊢ U1 [d, e] ≡ T1 →
+ ∀T2. L ⊢ U2 [d, e] ≡ T2 → K ⊢ T1 ⬌* T2.
+#L #U1 #U2 #H #K #d #e #HLK #T1 #HTU1 #T2 #HTU2
+elim (cpcs_inv_cprs … H) -H #U #HU1 #HU2
+elim (thin_cprs_delift_conf … HU1 … HLK … HTU1) -U1 #T #HT1 #HUT
+elim (thin_cprs_delift_conf … HU2 … HLK … HTU2) -U2 -HLK #X #HT2 #H
+lapply (delift_mono … H … HUT) -L #H destruct /2 width=3/
+qed.
normalize //
qed.
-lemma tw_shift: ∀L,T. #[L, T] ≤ #[L @ T].
+lemma tw_shift: ∀L,T. #[L, T] ≤ #[L @@ T].
#L elim L //
#K #I #V #IHL #T
@transitive_le [3: @IHL |2: /2 width=2/ | skip ]
non associative with precedence 45
for @{ 'NativeType $h $L $T1 $T2 }.
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 :: break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'NativeTypeAlt $h $L $T1 $T2 }.
+
notation "hvbox( h ⊢ break term 46 L1 : ⊑ break term 46 L2 )"
non associative with precedence 45
for @{ 'CrSubEqN $h $L1 $L2 }.
(* Advanced forward lemmas **************************************************)
-lemma cpr_shift_fwd: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L @ T1 ➡ L @ T2.
+lemma cpr_shift_fwd: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L @@ T1 ➡ L @@ T2.
#L elim L -L
[ #T1 #T2 #HT12 @(cpr_inv_atom … HT12)
| normalize /3 width=1/
--- /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/unfold/thin_delift.ma".
+include "basic_2/reducibility/tpr_delift.ma".
+include "basic_2/reducibility/cpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
+
+(* Properties on inverse basic term relocation ******************************)
+
+(* Basic_1: was only: pr2_gen_cabbr *)
+lemma thin_cpr_delift_conf: ∀L,U1,U2. L ⊢ U1 ➡ U2 →
+ ∀K,d,e. L [d, e] ≡ K → ∀T1. L ⊢ U1 [d, e] ≡ T1 →
+ ∃∃T2. K ⊢ T1 ➡ T2 & L ⊢ U2 [d, e] ≡ T2.
+#L #U1 #U2 * #U #HU1 #HU2 #K #d #e #HLK #T1 #HTU1
+elim (tpr_delift_conf … HU1 … HTU1) -U1 #T #HT1 #HUT
+elim (le_or_ge (|L|) d) #Hd
+[ elim (thin_delift_tpss_conf_le … HU2 … HUT … HLK ?)
+| elim (le_or_ge (|L|) (d+e)) #Hde
+ [ elim (thin_delift_tpss_conf_le_up … HU2 … HUT … HLK ? ? ?)
+ | elim (thin_delift_tpss_conf_be … HU2 … HUT … HLK ? ?)
+ ]
+] -U -HLK // -Hd [2,3: -Hde] #T2 #HT2
+lapply (cpr_intro … HT1 HT2) -T /2 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/unfold/delift.ma".
+include "basic_2/reducibility/tpr_tpss.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
+
+(* Properties on inverse basic term relocation ******************************)
+
+lemma tpr_delift_conf: ∀U1,U2. U1 ➡ U2 → ∀L,T1,d,e. L ⊢ U1 [d, e] ≡ T1 →
+ ∃∃T2. T1 ➡ T2 & L ⊢ U2 [d, e] ≡ T2.
+#U1 #U2 #HU12 #L #T1 #d #e * #W1 #HUW1 #HTW1
+elim (tpr_tpss_conf … HU12 … HUW1) -U1 #U1 #HWU1 #HU21
+elim (tpr_inv_lift … HWU1 … HTW1) -W1 /3 width=5/
+qed.
lapply (tpss_trans_eq … HT2 … HTU2) -T /2 width=3/
]
qed.
+
+lemma tpr_tpss_conf: ∀T1,T2. T1 ➡ T2 →
+ ∀L,U1,d,e. L ⊢ T1 [d, e] ▶* U1 →
+ ∃∃U2. U1 ➡ U2 & L ⊢ T2 [d, e] ▶* U2.
+/2 width=5/ qed.
| liftv_nil : liftv d e ◊ ◊
| liftv_cons: ∀T1s,T2s,T1,T2.
⇧[d, e] T1 ≡ T2 → liftv d e T1s T2s →
- liftv d e (T1 :: T1s) (T2 :: T2s)
+ liftv d e (T1 @ T1s) (T2 @ T2s)
.
interpretation "relocation (vector)" 'RLift d e T1s T2s = (liftv d e T1s T2s).
/2 width=5/ qed-.
fact liftv_inv_cons1_aux: ∀T1s,T2s,d,e. ⇧[d, e] T1s ≡ T2s →
- ∀U1,U1s. T1s = U1 :: U1s →
+ ∀U1,U1s. T1s = U1 @ U1s →
∃∃U2,U2s. ⇧[d, e] U1 ≡ U2 & ⇧[d, e] U1s ≡ U2s &
- T2s = U2 :: 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 →
+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.
+ T2s = U2 @ U2s.
/2 width=3/ qed-.
(* Basic properties *********************************************************)
(le d i) -> (lt i (plus d h)) ->
(EX u1 | t1 = (lift (minus (plus d h) (S i)) (S i) u1)).
*)
-lemma tps_inv_lift1_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶ U2 →
- ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
- d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →
- ∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ▶ T2 & ⇧[d, e] T2 ≡ U2.
+lemma tps_inv_lift1_ge_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶ U2 →
+ ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+ d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →
+ ∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ▶ T2 & ⇧[d, e] T2 ≡ U2.
#L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
elim (tps_split_up … HU12 (d + e) ? ?) -HU12 // -Hdedet #U #HU1 #HU2
lapply (tps_weak … HU1 d e ? ?) -HU1 // [ >commutative_plus /2 width=1/ ] -Hddt -Hdtde #HU1
lapply (tps_weak … HU12 dt (d + e - dt) ? ?) -HU12 // /2 width=3/ -Hdetde #HU12
elim (tps_inv_lift1_be … HU12 … HLK … HTU1 ? ?) -U1 -L // /2 width=3/
qed.
+
+lemma tps_inv_lift1_le_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶ U2 →
+ ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+ dt ≤ d → d ≤ dt + et → dt + et ≤ d + e →
+ ∃∃T2. K ⊢ T1 [dt, d - dt] ▶ T2 & ⇧[d, e] T2 ≡ U2.
+#L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde
+elim (tps_split_up … HU12 d ? ?) -HU12 // #U #HU1 #HU2
+elim (tps_inv_lift1_le … HU1 … HLK … HTU1 ?) -U1 [2: >commutative_plus /2 width=1/ ] -Hdtd #T #HT1 #HTU
+lapply (tps_weak … HU2 d e ? ?) -HU2 // [ >commutative_plus <plus_minus_m_m // ] -Hddet -Hdetde #HU2
+lapply (tps_inv_lift1_eq … HU2 … HTU) -L #H destruct /2 width=3/
+qed.
include "basic_2/unfold/tpss.ma".
-(* INVERSE TERM RELOCATION *************************************************)
+(* INVERSE BASIC TERM RELOCATION *******************************************)
definition delift: nat → nat → lenv → relation term ≝
λd,e,L,T1,T2. ∃∃T. L ⊢ T1 [d, e] ▶* T & ⇧[d, e] T2 ≡ T.
-interpretation "inverse relocation (term)"
+interpretation "inverse basic relocation (term)"
'TSubst L T1 d e T2 = (delift d e L T1 T2).
(* Basic properties *********************************************************)
include "basic_2/unfold/delift_lift.ma".
-(* INVERSE TERM RELOCATION *************************************************)
+(* INVERSE BASIC TERM RELOCATION *******************************************)
-(* alternative definition of inverse relocation *)
+(* alternative definition of inverse basic term relocation *)
inductive delifta: nat → nat → lenv → relation term ≝
| delifta_sort : ∀L,d,e,k. delifta d e L (⋆k) (⋆k)
| delifta_lref_lt: ∀L,d,e,i. i < d → delifta d e L (#i) (#i)
delifta d e L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
.
-interpretation "inverse relocation (term) alternative"
+interpretation "inverse basic relocation (term) alternative"
'TSubstAlt L T1 d e T2 = (delifta d e L T1 T2).
(* Basic properties *********************************************************)
include "basic_2/unfold/tpss_tpss.ma".
include "basic_2/unfold/delift.ma".
-(* INVERSE TERM RELOCATION *************************************************)
+(* INVERSE BASIC TERM RELOCATION *******************************************)
(* Main properties **********************************************************)
include "basic_2/unfold/tpss_lift.ma".
include "basic_2/unfold/delift.ma".
-(* INVERSE TERM RELOCATION *************************************************)
+(* INVERSE BASIC TERM RELOCATION *******************************************)
(* Advanced properties ******************************************************)
/2 width=1/ /3 width=6/
qed.
-(* Advanced forward lemmas **************************************************)
+(* Advanced inversion lemmas ************************************************)
lemma delift_inv_lref1_lt: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 → i < d → U2 = #i.
#L #U2 #i #d #e * #U #HU #HU2 #Hid
]
qed-.
-(* Relocation properties ****************************************************)
+(* Properties on basic term relocation **************************************)
lemma delift_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≡ T2 →
∀L,U1,d,e. dt + et ≤ d → ⇩[d, e] L ≡ K →
include "basic_2/unfold/ltpss_ltpss.ma".
include "basic_2/unfold/delift.ma".
-(* INVERSE TERM RELOCATION *************************************************)
+(* INVERSE BASIC TERM RELOCATION *******************************************)
(* Properties on partial unfold on local environments ***********************)
include "basic_2/unfold/tpss_tpss.ma".
include "basic_2/unfold/delift.ma".
-(* INVERSE TERM RELOCATION *************************************************)
+(* INVERSE BASIC TERM RELOCATION *******************************************)
(* Properties on partial unfold on terms ************************************)
+lemma delift_tpss_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
+ ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+ ∀K. ⇩[dd, ee] L ≡ K → d + e ≤ dd →
+ ∃∃T2. K ⊢ T1 [d, e] ▶* T2 & L ⊢ U2 [dd, ee] ≡ T2.
+#L #U1 #U2 #d #e #HU12 #T1 #dd #ee * #X1 #HUX1 #HTX1 #K #HLK #H1
+elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1
+elim (tpss_inv_lift1_le … HXU1 … HLK … HTX1 ?) -X1 -HLK // -H1 /3 width=5/
+qed.
+
+lemma delift_tps_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 →
+ ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+ ∀K. ⇩[dd, ee] L ≡ K → d + e ≤ dd →
+ ∃∃T2. K ⊢ T1 [d, e] ▶* T2 & L ⊢ U2 [dd, ee] ≡ T2.
+/3 width=3/ qed.
+
+lemma delift_tpss_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
+ ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+ ∀K. ⇩[dd, ee] L ≡ K →
+ d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
+ ∃∃T2. K ⊢ T1 [d, dd - d] ▶* T2 &
+ L ⊢ U2 [dd, ee] ≡ T2.
+#L #U1 #U2 #d #e #HU12 #T1 #dd #ee * #X1 #HUX1 #HTX1 #K #HLK #H1 #H2 #H3
+elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1
+elim (tpss_inv_lift1_le_up … HXU1 … HLK … HTX1 ? ? ?) -X1 -HLK // -H1 -H2 -H3 /3 width=5/
+qed.
+
+lemma delift_tps_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 →
+ ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+ ∀K. ⇩[dd, ee] L ≡ K →
+ d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
+ ∃∃T2. K ⊢ T1 [d, dd - d] ▶* T2 &
+ L ⊢ U2 [dd, ee] ≡ T2.
+/3 width=6/ qed.
+
lemma delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
∀K. ⇩[dd, ee] L ≡ K → d ≤ dd → dd + ee ≤ d + e →
L ⊢ U2 [dd, ee] ≡ T2.
#L #U1 #U2 #d #e #HU12 #T1 #dd #ee * #X1 #HUX1 #HTX1 #K #HLK #H1 #H2
elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1
-elim (tpss_inv_lift1_be … HXU1 … HLK … HTX1 ? ?) -X1 -HLK // /3 width=5/
+elim (tpss_inv_lift1_be … HXU1 … HLK … HTX1 ? ?) -X1 -HLK // -H1 -H2 /3 width=5/
qed.
lemma delift_tps_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 →
inductive at: list2 nat nat → relation nat ≝
| at_nil: ∀i. at ⟠ i i
| at_lt : ∀des,d,e,i1,i2. i1 < d →
- at des i1 i2 → at ({d, e} :: des) i1 i2
+ at des i1 i2 → at ({d, e} @ des) i1 i2
| at_ge : ∀des,d,e,i1,i2. d ≤ i1 →
- at des (i1 + e) i2 → at ({d, e} :: des) i1 i2
+ at des (i1 + e) i2 → at ({d, e} @ des) i1 i2
.
interpretation "application (generic relocation with pairs)"
/2 width=3/ qed-.
fact at_inv_cons_aux: ∀des,i1,i2. @[i1] des ≡ i2 →
- ∀d,e,des0. des = {d, e} :: des0 →
+ ∀d,e,des0. des = {d, e} @ des0 →
i1 < d ∧ @[i1] des0 ≡ i2 ∨
d ≤ i1 ∧ @[i1 + e] des0 ≡ i2.
#des #i1 #i2 * -des -i1 -i2
]
qed.
-lemma at_inv_cons: ∀des,d,e,i1,i2. @[i1] {d, e} :: des ≡ i2 →
+lemma at_inv_cons: ∀des,d,e,i1,i2. @[i1] {d, e} @ des ≡ i2 →
i1 < d ∧ @[i1] des ≡ i2 ∨
d ≤ i1 ∧ @[i1 + e] des ≡ i2.
/2 width=3/ qed-.
-lemma at_inv_cons_lt: ∀des,d,e,i1,i2. @[i1] {d, e} :: des ≡ i2 →
+lemma at_inv_cons_lt: ∀des,d,e,i1,i2. @[i1] {d, e} @ des ≡ i2 →
i1 < d → @[i1] des ≡ i2.
#des #d #e #i1 #e2 #H
elim (at_inv_cons … H) -H * // #Hdi1 #_ #Hi1d
elim (lt_refl_false … Hd)
qed-.
-lemma at_inv_cons_ge: ∀des,d,e,i1,i2. @[i1] {d, e} :: des ≡ i2 →
+lemma at_inv_cons_ge: ∀des,d,e,i1,i2. @[i1] {d, e} @ des ≡ i2 →
d ≤ i1 → @[i1 + e] des ≡ i2.
#des #d #e #i1 #e2 #H
elim (at_inv_cons … H) -H * // #Hi1d #_ #Hdi1
inductive minuss: nat → relation (list2 nat nat) ≝
| minuss_nil: ∀i. minuss i ⟠ ⟠
| minuss_lt : ∀des1,des2,d,e,i. i < d → minuss i des1 des2 →
- minuss i ({d, e} :: des1) ({d - i, e} :: des2)
+ minuss i ({d, e} @ des1) ({d - i, e} @ des2)
| minuss_ge : ∀des1,des2,d,e,i. d ≤ i → minuss (e + i) des1 des2 →
- minuss i ({d, e} :: des1) des2
+ minuss i ({d, e} @ des1) des2
.
interpretation "minus (generic relocation with pairs)"
/2 width=4/ qed-.
fact minuss_inv_cons1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 →
- ∀d,e,des. des1 = {d, e} :: des →
+ ∀d,e,des. des1 = {d, e} @ des →
d ≤ i ∧ des ▭ e + i ≡ des2 ∨
∃∃des0. i < d & des ▭ i ≡ des0 &
- des2 = {d - i, e} :: des0.
+ des2 = {d - i, e} @ des0.
#des1 #des2 #i * -des1 -des2 -i
[ #i #d #e #des #H destruct
| #des1 #des #d1 #e1 #i1 #Hid1 #Hdes #d2 #e2 #des2 #H destruct /3 width=3/
]
qed.
-lemma minuss_inv_cons1: ∀des1,des2,d,e,i. {d, e} :: des1 ▭ i ≡ des2 →
+lemma minuss_inv_cons1: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 →
d ≤ i ∧ des1 ▭ e + i ≡ des2 ∨
∃∃des. i < d & des1 ▭ i ≡ des &
- des2 = {d - i, e} :: des.
+ des2 = {d - i, e} @ des.
/2 width=3/ qed-.
-lemma minuss_inv_cons1_ge: ∀des1,des2,d,e,i. {d, e} :: des1 ▭ i ≡ des2 →
+lemma minuss_inv_cons1_ge: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 →
d ≤ i → des1 ▭ e + i ≡ des2.
#des1 #des2 #d #e #i #H
elim (minuss_inv_cons1 … H) -H * // #des #Hid #_ #_ #Hdi
elim (lt_refl_false … Hi)
qed-.
-lemma minuss_inv_cons1_lt: ∀des1,des2,d,e,i. {d, e} :: des1 ▭ i ≡ des2 →
+lemma minuss_inv_cons1_lt: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 →
i < d →
- ∃∃des. des1 ▭ i ≡ des & des2 = {d - i, e} :: des.
+ ∃∃des. des1 ▭ i ≡ des & des2 = {d - i, e} @ des.
#des1 #des2 #d #e #i #H
elim (minuss_inv_cons1 … H) -H * /2 width=3/ #Hdi #_ #Hid
lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi #Hi
let rec pluss (des:list2 nat nat) (i:nat) on des ≝ match des with
[ nil2 ⇒ ⟠
-| cons2 d e des ⇒ {d + i, e} :: pluss des i
+| cons2 d e des ⇒ {d + i, e} @ pluss des i
].
interpretation "plus (generic relocation with pairs)"
#d #e #des #H destruct
qed.
-lemma pluss_inv_cons2: ∀i,d,e,des2,des. des + i = {d, e} :: des2 →
- ∃∃des1. des1 + i = des2 & des = {d - i, e} :: des1.
+lemma pluss_inv_cons2: ∀i,d,e,des2,des. des + i = {d, e} @ des2 →
+ ∃∃des1. des1 + i = des2 & des = {d - i, e} @ des1.
#i #d #e #des2 * normalize
[ #H destruct
| #d1 #e1 #des1 #H destruct /2 width=3/
inductive ldrops: list2 nat nat → relation lenv ≝
| ldrops_nil : ∀L. ldrops ⟠ L L
| ldrops_cons: ∀L1,L,L2,des,d,e.
- ldrops des L1 L → ⇩[d,e] L ≡ L2 → ldrops ({d, e} :: des) L1 L2
+ ldrops des L1 L → ⇩[d,e] L ≡ L2 → ldrops ({d, e} @ des) L1 L2
.
interpretation "generic local environment slicing"
/2 width=3/ qed-.
fact ldrops_inv_cons_aux: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 →
- ∀d,e,tl. des = {d, e} :: tl →
+ ∀d,e,tl. des = {d, e} @ tl →
∃∃L. ⇩*[tl] L1 ≡ L & ⇩[d, e] L ≡ L2.
#L1 #L2 #des * -L1 -L2 -des
[ #L #d #e #tl #H destruct
qed.
(* Basic_1: was: drop1_gen_pcons *)
-lemma ldrops_inv_cons: ∀L1,L2,d,e,des. ⇩*[{d, e} :: des] L1 ≡ L2 →
+lemma ldrops_inv_cons: ∀L1,L2,d,e,des. ⇩*[{d, e} @ des] L1 ≡ L2 →
∃∃L. ⇩*[des] L1 ≡ L & ⇩[d, e] L ≡ L2.
/2 width=3/ qed-.
(* Basic_1: was: drop1_trans *)
theorem ldrops_trans: ∀L,L2,des2. ⇩*[des2] L ≡ L2 → ∀L1,des1. ⇩*[des1] L1 ≡ L →
- ⇩*[des2 @ des1] L1 ≡ L2.
+ ⇩*[des2 @@ des1] L1 ≡ L2.
#L #L2 #des2 #H elim H -L -L2 -des2 // /3 width=3/
qed.
inductive lifts: list2 nat nat → relation term ≝
| lifts_nil : ∀T. lifts ⟠ T T
| lifts_cons: ∀T1,T,T2,des,d,e.
- ⇧[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} :: des) T1 T2
+ ⇧[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} @ des) T1 T2
.
interpretation "generic relocation (term)"
/2 width=3/ qed-.
fact lifts_inv_cons_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 →
- ∀d,e,tl. des = {d, e} :: tl →
+ ∀d,e,tl. des = {d, e} @ tl →
∃∃T. ⇧[d, e] T1 ≡ T & ⇧*[tl] T ≡ T2.
#T1 #T2 #des * -T1 -T2 -des
[ #T #d #e #tl #H destruct
/2 width=3/
qed.
-lemma lifts_inv_cons: ∀T1,T2,d,e,des. ⇧*[{d, e} :: des] T1 ≡ T2 →
+lemma lifts_inv_cons: ∀T1,T2,d,e,des. ⇧*[{d, e} @ des] T1 ≡ T2 →
∃∃T. ⇧[d, e] T1 ≡ T & ⇧*[des] T ≡ T2.
/2 width=3/ qed-.
(* Basic_1: was: lift1_lift1 (left to right) *)
theorem lifts_trans: ∀T1,T,des1. ⇧*[des1] T1 ≡ T → ∀T2:term. ∀des2. ⇧*[des2] T ≡ T2 →
- ⇧*[des1 @ des2] T1 ≡ T2.
+ ⇧*[des1 @@ des2] T1 ≡ T2.
#T1 #T #des1 #H elim H -T1 -T -des1 // /3 width=3/
qed.
| liftsv_nil : liftsv des ◊ ◊
| liftsv_cons: ∀T1s,T2s,T1,T2.
⇧*[des] T1 ≡ T2 → liftsv des T1s T2s →
- liftsv des (T1 :: T1s) (T2 :: T2s)
+ liftsv des (T1 @ T1s) (T2 @ T2s)
.
interpretation "generic relocation (vector)"
include "basic_2/unfold/ltpss.ma".
-(* LOCAL ENVIRONMENT THINNING ***********************************************)
+(* BASIC LOCAL ENVIRONMENT THINNING *****************************************)
definition thin: nat → nat → relation lenv ≝
λd,e,L1,L2. ∃∃L. L1 [d, e] ▶* L & ⇩[d, e] L ≡ L2.
-interpretation "thinning (local environment)"
+interpretation "basic thinning (local environment)"
'TSubst L1 d e L2 = (thin d e L1 L2).
(* Basic properties *********************************************************)
include "basic_2/unfold/delift_ltpss.ma".
include "basic_2/unfold/thin.ma".
-(* DELIFT ON LOCAL ENVIRONMENTS *********************************************)
+(* BASIC DELIFT ON LOCAL ENVIRONMENTS ***************************************)
-(* Properties on inverse term relocation ************************************)
+(* Inversion lemmas on inverse basic term relocation ************************)
+
+lemma thin_inv_delift1: ∀I,K1,V1,L2,d,e. K1. ⓑ{I} V1 [d, e] ≡ L2 → 0 < d →
+ ∃∃K2,V2. K1 [d - 1, e] ≡ K2 &
+ K1 ⊢ V1 [d - 1, e] ≡ V2 &
+ L2 = K2. ⓑ{I} V2.
+#I #K1 #V1 #L2 #d #e * #X #HK1 #HL2 #e
+elim (ltpss_inv_tpss11 … HK1 ?) -HK1 // #K #V #HK1 #HV1 #H destruct
+elim (ldrop_inv_skip1 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H destruct
+lapply (ltpss_tpss_trans_eq … HV1 … HK1) -HV1 /3 width=5/
+qed-.
+
+(* Properties on inverse basic term relocation ******************************)
lemma thin_delift1: ∀L1,L2,d,e. L1 [d, e] ≡ L2 → ∀V1,V2. L1 ⊢ V1 [d, e] ≡ V2 →
∀I. L1.ⓑ{I}V1 [d + 1, e] ≡ L2.ⓑ{I}V2.
lapply (lift_mono … H2 … HV2) -H2 #H destruct /3 width=5/
qed.
+lemma thin_delift_tpss_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
+ ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+ ∀K. L [dd, ee] ≡ K → d + e ≤ dd →
+ ∃∃T2. K ⊢ T1 [d, e] ▶* T2 &
+ L ⊢ U2 [dd, ee] ≡ T2.
+#L #U1 #U2 #d #e #HU12 #T1 #dd #ee #HUT1 #K * #Y #HLY #HYK #Hdedd
+lapply (delift_ltpss_conf_eq … HUT1 … HLY) -HUT1 #HUT1
+elim (ltpss_tpss_conf … HU12 … HLY) -HU12 #U #HU1 #HU2
+elim (delift_tpss_conf_le … HU1 … HUT1 … HYK ?) -HU1 -HUT1 // -Hdedd #T #HT1 #HUT
+lapply (tpss_delift_trans_eq … HU2 … HUT) -U #HU2T
+lapply (ltpss_delift_trans_eq … HLY … HU2T) -Y /2 width=3/
+qed.
+
+lemma thin_delift_tps_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 →
+ ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+ ∀K. L [dd, ee] ≡ K → d + e ≤ dd →
+ ∃∃T2. K ⊢ T1 [d, e] ▶* T2 &
+ L ⊢ U2 [dd, ee] ≡ T2.
+/3 width=3/ qed.
+
+lemma thin_delift_tpss_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
+ ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+ ∀K. L [dd, ee] ≡ K →
+ d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
+ ∃∃T2. K ⊢ T1 [d, dd - d] ▶* T2 &
+ L ⊢ U2 [dd, ee] ≡ T2.
+#L #U1 #U2 #d #e #HU12 #T1 #dd #ee #HUT1 #K * #Y #HLY #HYK #Hdd #Hdde #Hddee
+lapply (delift_ltpss_conf_eq … HUT1 … HLY) -HUT1 #HUT1
+elim (ltpss_tpss_conf … HU12 … HLY) -HU12 #U #HU1 #HU2
+elim (delift_tpss_conf_le_up … HU1 … HUT1 … HYK ? ? ?) -HU1 -HUT1 // -Hdd -Hdde -Hddee #T #HT1 #HUT
+lapply (tpss_delift_trans_eq … HU2 … HUT) -U #HU2T
+lapply (ltpss_delift_trans_eq … HLY … HU2T) -Y /2 width=3/
+qed.
+
+lemma thin_delift_tps_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 →
+ ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+ ∀K. L [dd, ee] ≡ K →
+ d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
+ ∃∃T2. K ⊢ T1 [d, dd - d] ▶* T2 &
+ L ⊢ U2 [dd, ee] ≡ T2.
+/3 width=6 by thin_delift_tpss_conf_le_up, tpss_strap/ qed. (**) (* too slow without trace *)
+
lemma thin_delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
∀K. L [dd, ee] ≡ K → d ≤ dd → dd + ee ≤ d + e →
include "basic_2/unfold/ltpss_ldrop.ma".
include "basic_2/unfold/thin.ma".
-(* LOCAL ENVIRONMENT THINNING ***********************************************)
+(* BASIC LOCAL ENVIRONMENT THINNING *****************************************)
(* Properties on local environment slicing **********************************)
elim (tps_inv_atom1 … HT2) -HT2 [ /2 width=1/ | * /3 width=10/ ]
| * #K #V1 #V #i #Hdi #Hide #HLK #HV1 #HVT #HI
lapply (ldrop_fwd_ldrop2 … HLK) #H
- elim (tps_inv_lift1_up … HT2 … H … HVT ? ? ?) normalize -HT2 -H -HVT [2,3,4: /2 width=1/ ] #V2 <minus_plus #HV2 #HVT2
+ elim (tps_inv_lift1_ge_up … HT2 … H … HVT ? ? ?) normalize -HT2 -H -HVT [2,3,4: /2 width=1/ ] #V2 <minus_plus #HV2 #HVT2
@or_intror @(ex6_4_intro … Hdi Hide HLK … HVT2 HI) /2 width=3/ (**) (* /4 width=10/ is too slow *)
]
]
<(tps_inv_lift1_eq … HU2 … HTU1) -HU2 -HTU1 //
qed.
+lemma tpss_inv_lift1_ge_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
+ ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+ d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →
+ ∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ▶* T2 &
+ ⇧[d, e] T2 ≡ U2.
+#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet @(tpss_ind … H) -U2
+[ /2 width=3/
+| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
+ elim (tps_inv_lift1_ge_up … HU2 … HLK … HTU ? ? ?) -HU2 -HLK -HTU // /3 width=3/
+]
+qed.
+
lemma tpss_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
dt ≤ d → dt + et ≤ d + e →
elim (tps_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -HU2 -HLK -HTU // /3 width=3/
]
qed.
+
+lemma tpss_inv_lift1_le_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
+ ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+ dt ≤ d → d ≤ dt + et → dt + et ≤ d + e →
+ ∃∃T2. K ⊢ T1 [dt, d - dt] ▶* T2 & ⇧[d, e] T2 ≡ U2.
+#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde @(tpss_ind … H) -U2
+[ /2 width=3/
+| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
+ elim (tps_inv_lift1_le_up … HU2 … HLK … HTU ? ? ?) -HU2 -HLK -HTU // /3 width=3/
+]
+qed.
let rec append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with
[ nil2 ⇒ l2
-| cons2 a1 a2 tl ⇒ {a1, a2} :: append2 A1 A2 tl l2
+| cons2 a1 a2 tl ⇒ {a1, a2} @ append2 A1 A2 tl l2
].
interpretation "append (list of pairs)"
non associative with precedence 90
for @{'Nil}.
-notation "hvbox( hd :: break tl )"
+notation "hvbox( hd @ break tl )"
right associative with precedence 47
for @{'Cons $hd $tl}.
-notation "hvbox( l1 @ break l2 )"
+notation "hvbox( l1 @@ break l2 )"
right associative with precedence 47
for @{'Append $l1 $l2 }.
non associative with precedence 90
for @{'Nil2}.
-notation "hvbox( { hd1 , break hd2 } :: break tl )"
+notation "hvbox( { hd1 , break hd2 } @ break tl )"
non associative with precedence 47
for @{'Cons $hd1 $hd2 $tl}.
#m #n elim (decidable_lt m n) /2 width=1/ /3 width=1/
qed-.
+lemma le_or_ge: ∀m,n. m ≤ n ∨ n ≤ m.
+#m #n elim (decidable_le m n) /2 width=1/ /4 width=2/
+qed-.
+
(* More general conclusion **************************************************)
theorem nat_ind_plus: ∀R:predicate nat.
#A #R #a1 #a2 #Ha12 elim Ha12 -a1 -a2 /2 width=3/
qed.
-fact TC_star_ind_dx_aux: ∀A,R. reflexive A R →
- ∀a2. ∀P:predicate A. P a2 →
- (∀a1,a. R a1 a → TC … R a a2 → P a → P a1) →
- ∀a1,a. TC … R a1 a → a = a2 → P a1.
-#A #R #HR #a2 #P #Ha2 #H #a1 #a #Ha1
+fact TC_ind_dx_aux: ∀A,R,a2. ∀P:predicate A.
+ (∀a1. R a1 a2 → P a1) →
+ (∀a1,a. R a1 a → TC … R a a2 → P a → P a1) →
+ ∀a1,a. TC … R a1 a → a = a2 → P a1.
+#A #R #a2 #P #H1 #H2 #a1 #a #Ha1
elim (TC_to_TC_dx ???? Ha1) -a1 -a
-[ #a #c #Hac #H destruct /3 width=4/
+[ #a #c #Hac #H destruct /2 width=1/
| #a #b #c #Hab #Hbc #IH #H destruct /3 width=4/
]
qed-.
+lemma TC_ind_dx: ∀A,R,a2. ∀P:predicate A.
+ (∀a1. R a1 a2 → P a1) →
+ (∀a1,a. R a1 a → TC … R a a2 → P a → P a1) →
+ ∀a1. TC … R a1 a2 → P a1.
+#A #R #a2 #P #H1 #H2 #a1 #Ha12
+@(TC_ind_dx_aux … H1 H2 … Ha12) //
+qed-.
+
+lemma TC_symmetric: ∀A,R. symmetric A R → symmetric A (TC … R).
+#A #R #HR #x #y #H @(TC_ind_dx ??????? H) -x /3 width=1/ /3 width=3/
+qed.
+
lemma TC_star_ind_dx: ∀A,R. reflexive A R →
∀a2. ∀P:predicate A. P a2 →
(∀a1,a. R a1 a → TC … R a a2 → P a → P a1) →
∀a1. TC … R a1 a2 → P a1.
#A #R #HR #a2 #P #Ha2 #H #a1 #Ha12
-@(TC_star_ind_dx_aux … HR … Ha2 H … Ha12) //
+@(TC_ind_dx … P ? H … Ha12) /3 width=4/
qed-.
definition Conf3: ∀A,B. relation2 A B → relation A → Prop ≝ λA,B,S,R.
projects / helm.git / commitdiff