theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP.
acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
∀L1,T,A. L1 ⊢ T ⁝ A → ∀L0,des. ⇩*[des] L0 ≡ L1 →
- ∀T0. ⇧*[des] T ≡ T0 → ∀L2. L2 [RP] ⊑ L0 →
- ⦃L2, T0⦄ [RP] ϵ 〚A〛.
+ ∀T0. ⇧*[des] T ≡ T0 → ∀L2. L2 ⊑[RP] L0 →
+ ⦃L2, T0⦄ ϵ[RP] 〚A〛.
#RR #RS #RP #H1RP #H2RP #L1 #T #A #H elim H -L1 -T -A
[ #L #k #L0 #des #HL0 #X #H #L2 #HL20
>(lifts_inv_sort1 … H) -H
(* Basic_1: was: sc3_arity *)
lemma aacr_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
- ∀L,T,A. L ⊢ T ⁝ A → ⦃L, T⦄ [RP] ϵ 〚A〛.
+ ∀L,T,A. L ⊢ T ⁝ A → ⦃L, T⦄ ϵ[RP] 〚A〛.
/2 width=8/ qed.
lemma acp_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
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 → ⇧*[des + 1] T ≡ T0 →
- ⦃L0, V0⦄ [RP] ϵ 〚B〛 → ⦃L0. ⓓV0, T0⦄ [RP] ϵ 〚A〛
+ ⦃L0, V0⦄ ϵ[RP] 〚B〛 → ⦃L0. ⓓV0, T0⦄ ϵ[RP] 〚A〛
) →
- ⦃L, ⓛW. T⦄ [RP] ϵ 〚②B. A〛.
+ ⦃L, ⓛ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
inductive lsubc (RP:lenv→predicate term): relation lenv ≝
| lsubc_atom: lsubc RP (⋆) (⋆)
| lsubc_pair: ∀I,L1,L2,V. lsubc RP L1 L2 → lsubc RP (L1. ⓑ{I} V) (L2. ⓑ{I} V)
-| lsubc_abbr: ∀L1,L2,V,W,A. ⦃L1, V⦄ [RP] ϵ 〚A〛 → L2 ⊢ W ⁝ A →
+| lsubc_abbr: ∀L1,L2,V,W,A. ⦃L1, V⦄ ϵ[RP] 〚A〛 → L2 ⊢ W ⁝ A →
lsubc RP L1 L2 → lsubc RP (L1. ⓓV) (L2. ⓛW)
.
(* Basic inversion lemmas ***************************************************)
-fact lsubc_inv_atom1_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → L1 = ⋆ → L2 = ⋆.
+fact lsubc_inv_atom1_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → L1 = ⋆ → L2 = ⋆.
#RP #L1 #L2 * -L1 -L2
[ //
| #I #L1 #L2 #V #_ #H destruct
qed.
(* Basic_1: was: csubc_gen_sort_r *)
-lemma lsubc_inv_atom1: ∀RP,L2. ⋆ [RP] ⊑ L2 → L2 = ⋆.
+lemma lsubc_inv_atom1: ∀RP,L2. ⋆ ⊑[RP] L2 → L2 = ⋆.
/2 width=4/ qed-.
-fact lsubc_inv_pair1_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀I,K1,V. L1 = K1. ⓑ{I} V →
- (∃∃K2. K1 [RP] ⊑ K2 & L2 = K2. ⓑ{I} V) ∨
- ∃∃K2,W,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ⁝ A &
- K1 [RP] ⊑ K2 &
+fact lsubc_inv_pair1_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀I,K1,V. L1 = K1. ⓑ{I} V →
+ (∃∃K2. K1 ⊑[RP] K2 & L2 = K2. ⓑ{I} V) ∨
+ ∃∃K2,W,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
+ K1 ⊑[RP] K2 &
L2 = K2. ⓛW & I = Abbr.
#RP #L1 #L2 * -L1 -L2
[ #I #K1 #V #H destruct
qed.
(* Basic_1: was: csubc_gen_head_r *)
-lemma lsubc_inv_pair1: ∀RP,I,K1,L2,V. K1. ⓑ{I} V [RP] ⊑ L2 →
- (∃∃K2. K1 [RP] ⊑ K2 & L2 = K2. ⓑ{I} V) ∨
- ∃∃K2,W,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ⁝ A &
- K1 [RP] ⊑ K2 &
+lemma lsubc_inv_pair1: ∀RP,I,K1,L2,V. K1. ⓑ{I} V ⊑[RP] L2 →
+ (∃∃K2. K1 ⊑[RP] K2 & L2 = K2. ⓑ{I} V) ∨
+ ∃∃K2,W,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
+ K1 ⊑[RP] K2 &
L2 = K2. ⓛW & I = Abbr.
/2 width=3/ qed-.
-fact lsubc_inv_atom2_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → L2 = ⋆ → L1 = ⋆.
+fact lsubc_inv_atom2_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → L2 = ⋆ → L1 = ⋆.
#RP #L1 #L2 * -L1 -L2
[ //
| #I #L1 #L2 #V #_ #H destruct
qed.
(* Basic_1: was: csubc_gen_sort_l *)
-lemma lsubc_inv_atom2: ∀RP,L1. L1 [RP] ⊑ ⋆ → L1 = ⋆.
+lemma lsubc_inv_atom2: ∀RP,L1. L1 ⊑[RP] ⋆ → L1 = ⋆.
/2 width=4/ qed-.
-fact lsubc_inv_pair2_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀I,K2,W. L2 = K2. ⓑ{I} W →
- (∃∃K1. K1 [RP] ⊑ K2 & L1 = K1. ⓑ{I} W) ∨
- ∃∃K1,V,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ⁝ A &
- K1 [RP] ⊑ K2 &
+fact lsubc_inv_pair2_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀I,K2,W. L2 = K2. ⓑ{I} W →
+ (∃∃K1. K1 ⊑[RP] K2 & L1 = K1. ⓑ{I} W) ∨
+ ∃∃K1,V,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
+ K1 ⊑[RP] K2 &
L1 = K1. ⓓV & I = Abst.
#RP #L1 #L2 * -L1 -L2
[ #I #K2 #W #H destruct
qed.
(* Basic_1: was: csubc_gen_head_l *)
-lemma lsubc_inv_pair2: ∀RP,I,L1,K2,W. L1 [RP] ⊑ K2. ⓑ{I} W →
- (∃∃K1. K1 [RP] ⊑ K2 & L1 = K1. ⓑ{I} W) ∨
- ∃∃K1,V,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ⁝ A &
- K1 [RP] ⊑ K2 &
+lemma lsubc_inv_pair2: ∀RP,I,L1,K2,W. L1 ⊑[RP] K2. ⓑ{I} W →
+ (∃∃K1. K1 ⊑[RP] K2 & L1 = K1. ⓑ{I} W) ∨
+ ∃∃K1,V,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
+ K1 ⊑[RP] K2 &
L1 = K1. ⓓV & I = Abst.
/2 width=3/ qed-.
(* Basic properties *********************************************************)
(* Basic_1: was: csubc_refl *)
-lemma lsubc_refl: ∀RP,L. L [RP] ⊑ L.
+lemma lsubc_refl: ∀RP,L. L ⊑[RP] L.
#RP #L elim L -L // /2 width=1/
qed.
(* Basic_1: was: csubc_drop_conf_O *)
(* Note: the constant 0 can not be generalized *)
-lemma lsubc_ldrop_O1_trans: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
- ∃∃K1. ⇩[0, e] L1 ≡ K1 & K1 [RP] ⊑ K2.
+lemma lsubc_ldrop_O1_trans: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
+ ∃∃K1. ⇩[0, e] L1 ≡ K1 & K1 ⊑[RP] K2.
#RP #L1 #L2 #H elim H -L1 -L2
[ #X #e #H
>(ldrop_inv_atom1 … H) -H /2 width=3/
(* Basic_1: was: csubc_drop_conf_rev *)
lemma ldrop_lsubc_trans: ∀RR,RS,RP.
acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
- ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. K1 [RP] ⊑ K2 →
- ∃∃L2. L1 [RP] ⊑ L2 & ⇩[d, e] L2 ≡ K2.
+ ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. K1 ⊑[RP] K2 →
+ ∃∃L2. L1 ⊑[RP] L2 & ⇩[d, e] L2 ≡ K2.
#RR #RS #RP #Hacp #Hacr #L1 #K1 #d #e #H elim H -L1 -K1 -d -e
[ #d #e #X #H
>(lsubc_inv_atom1 … H) -H /2 width=3/
(* Basic_1: was: csubc_drop1_conf_rev *)
lemma ldrops_lsubc_trans: ∀RR,RS,RP.
acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
- ∀L1,K1,des. ⇩*[des] L1 ≡ K1 → ∀K2. K1 [RP] ⊑ K2 →
- ∃∃L2. L1 [RP] ⊑ L2 & ⇩*[des] L2 ≡ K2.
+ ∀L1,K1,des. ⇩*[des] L1 ≡ K1 → ∀K2. K1 ⊑[RP] K2 →
+ ∃∃L2. L1 ⊑[RP] L2 & ⇩*[des] L2 ≡ K2.
#RR #RS #RP #Hacp #Hacr #L1 #K1 #des #H elim H -L1 -K1 -des
[ /2 width=3/
| #L1 #L #K1 #des #d #e #_ #HLK1 #IHL #K2 #HK12
(* properties concerning lenv refinement for atomic arity assignment ********)
lemma lsubc_lsuba: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
- ∀L1,L2. L1 ⁝⊑ L2 → L1 [RP] ⊑ L2.
+ ∀L1,L2. L1 ⁝⊑ L2 → L1 ⊑[RP] L2.
#RR #RS #RP #H1RP #H2RP #L1 #L2 #H elim H -L1 -L2
// /2 width=1/ /3 width=4/
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/lsubs_sfr.ma".
-include "basic_2/unfold/delift.ma".
-include "basic_2/unfold/thin.ma".
-(*
-include "basic_2/equivalence/cpcs_delift.ma".
-*)
-include "basic_2/dynamic/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,U1. ⦃h, L1⦄ ⊢ T1 : U1 →
- ∀L2,d,e. ≼ [d, e] L1 → L1 [d, e] ≡ L2 →
- ∃∃T2,U2. ⦃h, L2⦄ ⊢ T2 : U2 &
- L1 ⊢ T1 [d, e] ≡ T2 & L1 ⊢ U1 [d, e] ≡ U2.
-(*
-#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 #Y1 #T1 #X1 #_ #_ #IHTX1 #IHXY1 #L2 #d #e #HL12 #X #H
- elim (delift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
- elim (IHTX1 … HL12 … HT12) -T1 #U1 #U2 #HTU2 #HU12 #HUX1
-(*
- elim (IHXY1 … HL12 (ⓐV2.U2) ?) -IHXY1 -HL12
-*)
- @(ex3_2_intro … (ⓐV1.U1) (ⓐV2.U2))
- [2: /2 width=1/ |3: /2 width=1/ ] -HV12 -HU12 -HUX1
- @(nta_pure … HTU2) -HTU2
-
- [ /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/
-]
-*)
-axiom 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-.
-*)
\ No newline at end of file
--- /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/ldrop_sfr.ma".
+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_lift.ma".
+
+(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
+
+(* Properties on basic local environment thibbing ***************************)
+
+(* Note: this is known as the substitution lemma *)
+(* Basic_1: was only: ty3_gen_cabbr *)
+lemma nta_thin_conf: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 →
+ ∀L2,d,e. ≼ [d, e] L1 → L1 [d, e] ≡ L2 →
+ ∃∃T2,U2. ⦃h, L2⦄ ⊢ T2 : U2 &
+ L1 ⊢ T1 [d, e] ≡ T2 & L1 ⊢ U1 [d, e] ≡ U2.
+#h #L1 #T1 #U1 #H elim H -L1 -T1 -U1
+[ /2 width=5/
+| #L1 #K1 #V1 #W1 #U1 #i #HLK1 #HVW1 #HWU1 #IHVW1 #L2 #d #e #HL1 #HL12
+ elim (lt_or_ge i d) #Hdi [ -HVW1 ]
+ [ lapply (sfr_ldrop_trans_ge … HLK1 … HL1 ?) -HL1 /2 width=2/ #H
+ lapply (sfr_inv_skip … H ?) -H /2 width=1/ #HK1
+ elim (thin_ldrop_conf_le … HL12 … HLK1 ?) -HL12 /2 width=2/ #X #H #HLK2
+ elim (thin_inv_delift1 … H ?) -H /2 width=1/ #K2 #V2 #HK12 #HV12 #H destruct
+ elim (IHVW1 … HK1 HK12) -IHVW1 -HK1 -HK12 #X2 #W2 #HVW2 #H #HW12
+ lapply (delift_mono … H … HV12) -H -HV12 #H destruct
+ elim (lift_total W2 0 (i+1)) #U2 #HWU2
+ lapply (ldrop_fwd_ldrop2 … HLK1) -V1 #HLK1
+ lapply (delift_lift_ge … HW12 … HLK1 HWU1 … HWU2) -HW12 -HLK1 -HWU1 //
+ >minus_plus <plus_minus_m_m // /3 width=6/
+ | elim (lt_or_ge i (d+e)) #Hide [ -HVW1 | -Hdi -IHVW1 -HL1 ]
+ [ lapply (sfr_ldrop_trans_be_up … HLK1 … HL1 ? ?) -HL1 // /2 width=2/ <minus_n_O #H
+ elim (sfr_inv_bind … H ?) -H /2 width=1/ #HK1 #_
+ elim (thin_ldrop_conf_be … HL12 … HLK1 ? ?) -HL12 /2 width=2/ #K2 #H #HLK2
+ lapply (thin_inv_thin1 … H ?) -H /2 width=1/ #HK12
+ elim (IHVW1 … HK1 HK12) -IHVW1 -HK1 -HK12 #V2 #W2 #HVW2 #HV12 #HW12
+ elim (lift_total V2 0 d) #T2 #HVT2
+ elim (lift_total W2 0 d) #U2 #HWU2
+ elim (lift_total W2 0 (i+1)) #U #HW2U
+ lapply (nta_lift … HVW2 … HLK2 … HVT2 … HWU2) -HVW2 -HLK2 #HTU2
+ lapply (ldrop_fwd_ldrop2 … HLK1) #HLK0
+ lapply (delift_lift_ge … HW12 … HLK0 HWU1 … HW2U) -HW12 -HLK0 -HWU1 // >minus_plus #HU1
+ lapply (lift_conf_be … HWU2 … HW2U ?) -W2 /2 width=1/ #HU2
+ lapply (delift_lift_div_be … HU1 … HU2 ? ?) -U // /2 width=1/ /3 width=8/
+ | lapply (transitive_le … (i+1) Hide ?) /2 width=1/ #Hdei
+ lapply (thin_ldrop_conf_ge … HL12 … HLK1 ?) -HL12 -HLK1 // #HL2K1
+ elim (lift_split … HWU1 d (i+1-e) ? ? ?) -HWU1 // /2 width=1/ #W
+ <plus_minus in ⊢ (??%??→?); /2 width=2/ #HW1
+ <minus_minus // /2 width=2/ -Hdei >commutative_plus <minus_n_n /3 width=6/
+ ]
+ ]
+| #L1 #K1 #W1 #V1 #U1 #i #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #d #e #HL1 #HL12
+ elim (lt_or_ge i d) #Hdi [ -HWV1 | -IHWV1 ]
+ [ lapply (sfr_ldrop_trans_ge … HLK1 … HL1 ?) -HL1 /2 width=2/ #H
+ lapply (sfr_inv_skip … H ?) -H /2 width=1/ #HK1
+ elim (thin_ldrop_conf_le … HL12 … HLK1 ?) -HL12 /2 width=2/ #X #H #HLK2
+ elim (thin_inv_delift1 … H ?) -H /2 width=1/ #K2 #W2 #HK12 #HW12 #H destruct
+ elim (IHWV1 … HK1 HK12) -IHWV1 -HK1 -HK12 #X2 #V2 #HWV2 #H #_
+ lapply (delift_mono … H … HW12) -H #H destruct
+ elim (lift_total W2 0 (i+1)) #U2 #HWU2
+ lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 #HLK1
+ lapply (delift_lift_ge … HW12 … HLK1 HWU1 … HWU2) -HW12 -HLK1 -HWU1 //
+ >minus_plus <plus_minus_m_m // /3 width=6/
+ | elim (lt_or_ge i (d+e)) #Hide [ -HWV1 -HWU1 -HL12 | -Hdi -HL1 ]
+ [ lapply (sfr_inv_ldrop … HLK1 … HL1 ? ?) -HLK1 -HL1 // -Hdi -Hide #H destruct
+ | lapply (transitive_le … (i+1) Hide ?) /2 width=1/ #Hdei
+ lapply (thin_ldrop_conf_ge … HL12 … HLK1 ?) -HL12 -HLK1 // #HL2K1
+ elim (lift_split … HWU1 d (i+1-e) ? ? ?) -HWU1 // /2 width=1/ #W
+ <plus_minus in ⊢ (??%??→?); /2 width=2/ #HW1
+ <minus_minus // /2 width=2/ -Hdei >commutative_plus <minus_n_n /3 width=6/
+ ]
+ ]
+| #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL1 #HL12
+ elim (IHVW1 … HL1 HL12) -IHVW1 #V2 #W2 #HVW2 #HV12 #_
+ elim (IHTU1 (L2.ⓑ{I}V2) (d+1) e ? ?) -IHTU1 /2 width=1/ -HL1 -HL12 #T2 #U2 #HTU2 #HT12 #HU12
+ lapply (delift_lsubs_conf … HT12 (L1.ⓑ{I}V2) ?) -HT12 /2 width=1/
+ lapply (delift_lsubs_conf … HU12 (L1.ⓑ{I}V2) ?) -HU12 /2 width=1/ /3 width=7/
+| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL1 #HL12
+ elim (IHVW1 … HL1 HL12) -IHVW1 #V2 #W2 #HVW2 #HV12 #HW12
+ elim (IHTU1 … HL1 HL12) -IHTU1 -HL1 -HL12 #X2 #Y2 #HXY2 #HX2 #HY2
+ elim (delift_inv_bind1 … HX2) -HX2 #Z21 #T2 #HZ21 #HT12 #H destruct
+ elim (delift_inv_bind1 … HY2) -HY2 #Z22 #U2 #HZ22 #HU12 #H destruct
+ lapply (delift_mono … HZ21 … HW12) -HZ21 #H destruct
+ lapply (delift_mono … HZ22 … HW12) -HZ22 #H destruct
+ @(ex3_2_intro … (ⓐV2.ⓛW2.T2) (ⓐV2.ⓛW2.U2)) /3 width=1/ (**) (* explict constructor, /4 depth=?/ is too slow *)
+| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL1 #HL12
+ elim (IHTU1 … HL1 HL12) -IHTU1 #T2 #U2 #HTU2 #HT12 #HU12
+ elim (IHUW1 … HL1 HL12) -IHUW1 -HL1 -HL12 #X2 #W2 #HXW2 #H #HW12
+ elim (delift_inv_flat1 … H) -H #V2 #Y2 #HV12 #HY2 #H destruct
+ lapply (delift_mono … HY2 … HU12) -HY2 #H destruct /3 width=7/
+| #L1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL1 #HL12
+ elim (IHTU1 … HL1 HL12) -IHTU1 -HL1 -HL12 /3 width=5/
+| #L1 #T1 #U11 #U12 #V1 #_ #HU112 #_ #IHT1 #IHU12 #L2 #d #e #HL1 #HL12
+ elim (IHT1 … HL1 HL12) -IHT1 #T2 #U21 #HT2 #HT12 #HU121
+ elim (IHU12 … HL1 HL12) -IHU12 -HL1 #U22 #V2 #HU22 #HU122 #_
+ lapply (thin_cpcs_delift_mono … HU112 … HL12 … HU121 … HU122) -HU112 -HL12 -HU121 /3 width=5/
+]
+qed.
+
+lemma nta_ldrop_conf: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 →
+ ∀L2,d,e. ≼ [d, e] L1 → ⇩[d, e] L1 ≡ L2 →
+ ∃∃T2,U2. ⦃h, L2⦄ ⊢ T2 : U2 &
+ L1 ⊢ T1 [d, e] ≡ T2 & L1 ⊢ U1 [d, e] ≡ U2.
+/3 width=1/ qed.
(**************************************************************************)
(* THE FORMAL SYSTEM λδ: MATITA SOURCE FILES
- * - Patience on me to gain peace and perfection! -
- * [ suggested invocation to start formal specifications with ]
- * Context-sensitive subject equivalence for atomic arity assignment: 2012 April 16
- * Context-sensitive strong normalization for simply typed terms: 2012 March 15
- * Support for abstract candidates of reducibility closed: 2012 January 27
- * Confluence for context-sensitive parallel reduction: 2011 September 21
- * Confluence for context-free parallel reduction: 2011 September 6
- * Specification starts: 2011 April 17
+ * Suggested invocation to start formal specifications with:
+ * - Patience on me to gain peace and perfection! -
+ * 2012 April 16 (anniversary milestone):
+ * context-sensitive subject equivalence for atomic arity assignment.
+ * 2012 March 15:
+ * context-sensitive strong normalization for simply typed terms.
+ * 2012 January 27:
+ * support for abstract candidates of reducibility.
+ * 2011 September 21:
+ * confluence for context-sensitive parallel reduction.
+ * 2011 September 6:
+ * confluence for context-free parallel reduction.
+ * 2011 April 17:
+ * specification starts.
*)
include "ground_2/star.ma".
non associative with precedence 45
for @{ 'SN $T }.
-notation "hvbox( L ⊢ ⬇ * term 46 T )"
+notation "hvbox( L ⊢ break ⬇ * term 46 T )"
non associative with precedence 45
for @{ 'SN $L $T }.
-notation "hvbox( L ⊢ ⬇ ⬇ * term 46 T )"
+notation "hvbox( L ⊢ break ⬇ ⬇ * term 46 T )"
non associative with precedence 45
for @{ 'SNAlt $L $T }.
-notation "hvbox( ⦃ L, break T ⦄ break [ R ] ϵ break 〚 A 〛 )"
+notation "hvbox( ⦃ L, break T ⦄ ϵ break [ R ] break 〚 A 〛 )"
non associative with precedence 45
for @{ 'InEInt $R $L $T $A }.
-notation "hvbox( T1 break [ R ] ⊑ break term 46 T2 )"
+notation "hvbox( T1 ⊑ break [ R ] break term 46 T2 )"
non associative with precedence 45
for @{ 'CrSubEq $T1 $R $T2 }.
(**************************************************************************)
include "basic_2/substitution/lsubs_sfr.ma".
-include "basic_2/substitution/ldrop.ma".
+include "basic_2/substitution/ldrop_ldrop.ma".
(* DROPPING *****************************************************************)
-(* Properties about local env. full refinement for substitution *************)
-
-lemma sfr_ldrop: ∀L,d,e.
- (∀I,K,V,i. d ≤ i → i < d + e → ⇩[0, i] L ≡ K. ⓑ{I}V → I = Abbr) →
- ≼ [d, e] L.
-#L elim L -L //
-#L #I #V #IHL #d @(nat_ind_plus … d) -d
-[ #e @(nat_ind_plus … e) -e //
- #e #_ #HH
- >(HH I L V 0 ? ? ?) // /5 width=6/
-| /5 width=6/
-]
-qed.
-
(* Inversion lemmas about local env. full refinement for substitution *******)
+(* Note: ldrop_ldrop not needed *)
lemma sfr_inv_ldrop: ∀I,L,K,V,i. ⇩[0, i] L ≡ K. ⓑ{I}V → ∀d,e. ≼ [d, e] L →
d ≤ i → i < d + e → I = Abbr.
#I #L elim L -L
]
]
qed-.
+
+(* Properties about local env. full refinement for substitution *************)
+
+(* Note: ldrop_ldrop not needed *)
+lemma sfr_ldrop: ∀L,d,e.
+ (∀I,K,V,i. d ≤ i → i < d + e → ⇩[0, i] L ≡ K. ⓑ{I}V → I = Abbr) →
+ ≼ [d, e] L.
+#L elim L -L //
+#L #I #V #IHL #d @(nat_ind_plus … d) -d
+[ #e @(nat_ind_plus … e) -e //
+ #e #_ #HH
+ >(HH I L V 0 ? ? ?) // /5 width=6/
+| /5 width=6/
+]
+qed.
+
+lemma sfr_ldrop_trans_le: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ≼ [dd, ee] L1 →
+ dd + ee ≤ d → ≼ [dd, ee] L2.
+#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hddee
+@sfr_ldrop #I #K2 #V2 #i #Hddi #Hiddee #HLK2
+lapply (lt_to_le_to_lt … Hiddee Hddee) -Hddee #Hid
+elim (ldrop_trans_le … HL12 … HLK2 ?) -L2 /2 width=2/ #X #HLK1 #H
+elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K1 #V1 #HK12 #HV21 #H destruct
+@(sfr_inv_ldrop … HLK1 … HL1) -L1 -K1 -V1 //
+qed.
+
+lemma sfr_ldrop_trans_be_up: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 →
+ ∀dd,ee. ≼ [dd, ee] L1 →
+ dd ≤ d + e → d + e ≤ dd + ee →
+ ≼ [d, dd + ee - d - e] L2.
+#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hdde #Hddee
+@sfr_ldrop #I #K2 #V2 #i #Hdi #Hiddee #HLK2
+lapply (transitive_le ? ? (i+e)… Hdde ?) -Hdde /2 width=1/ #Hddie
+>commutative_plus in Hiddee; >minus_minus_comm <plus_minus_m_m /2 width=1/ -Hddee #Hiddee
+lapply (ldrop_trans_ge … HL12 … HLK2 ?) -L2 // -Hdi #HL1K2
+@(sfr_inv_ldrop … HL1K2 … HL1) -L1 >commutative_plus // -Hddie /2 width=1/
+qed.
+
+lemma sfr_ldrop_trans_ge: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ≼ [dd, ee] L1 →
+ d + e ≤ dd → ≼ [dd - e, ee] L2.
+#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hddee
+@sfr_ldrop #I #K2 #V2 #i #Hddi #Hiddee #HLK2
+elim (le_inv_plus_l … Hddee) -Hddee #Hdde #Hedd
+>plus_minus in Hiddee; // #Hiddee
+lapply (transitive_le … Hdde Hddi) -Hdde #Hid
+lapply (ldrop_trans_ge … HL12 … HLK2 ?) -L2 // -Hid #HL1K2
+@(sfr_inv_ldrop … HL1K2 … HL1) -L1 >commutative_plus /2 width=1/
+qed.
(* Advanced properties ******************************************************)
-lemma lift_conf_le: ∀T,T1,d. ⇧[O, d] T ≡ T1 → ∀T2,e. ⇧[O, d + e] T ≡ T2 →
- ⇧[d, e] T1 ≡ T2.
-#T #T1 #d #HT1 #T2 #e #HT2
-elim (lift_split … HT2 d d ? ? ?) -HT2 // #X #H
+lemma lift_conf_be: ∀T,T1,d,e1. ⇧[d, e1] T ≡ T1 → ∀T2,e2. ⇧[d, e2] T ≡ T2 →
+ e1 ≤ e2 → ⇧[d + e1, e2 - e1] T1 ≡ T2.
+#T #T1 #d #e1 #HT1 #T2 #e2 #HT2 #He12
+elim (lift_split … HT2 (d+e1) e1 ? ? ?) -HT2 // #X #H
>(lift_mono … H … HT1) -T //
qed.
]
qed.
+lemma tps_split_down: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 →
+ ∀i. d ≤ i → i ≤ d + e →
+ ∃∃T. L ⊢ T1 ▶ [i, d + e - i] T &
+ L ⊢ T ▶ [d, i - d] T2.
+#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e
+[ /2 width=3/
+| #L #K #V #W #i #d #e #Hdi #Hide #HLK #HVW #j #Hdj #Hjde
+ elim (lt_or_ge i j)
+ [ -Hide -Hjde >(plus_minus_m_m j d) in ⊢ (% → ?); // -Hdj /4 width=4/
+ | -Hdi -Hdj
+ >(plus_minus_m_m (d+e) j) in Hide; // -Hjde /3 width=4/
+ ]
+| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide
+ elim (IHV12 i ? ?) -IHV12 // #V #HV1 #HV2
+ elim (IHT12 (i + 1) ? ?) -IHT12 /2 width=1/
+ -Hdi -Hide >arith_c1x #T #HT1 #HT2
+ lapply (tps_lsubs_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /3 width=5/
+| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide
+ elim (IHV12 i ? ?) -IHV12 // elim (IHT12 i ? ?) -IHT12 //
+ -Hdi -Hide /3 width=5/
+]
+qed.
+
(* Basic inversion lemmas ***************************************************)
fact tps_inv_atom1_aux: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → ∀I. T1 = ⓪{I} →
(* *)
(**************************************************************************)
+include "basic_2/substitution/lift_lift.ma".
include "basic_2/unfold/tpss_tpss.ma".
include "basic_2/unfold/delift.ma".
⇧[0, d] V2 ≡ U2 → L ⊢ #i [d, e] ≡ U2.
#L #K #V1 #V2 #U2 #i #d #e #Hdi #Hide #HLK * #V #HV1 #HV2 #HVU2
elim (lift_total V 0 (i+1)) #U #HVU
-lapply (lift_trans_be … HV2 … HVU ? ?) -HV2 // >minus_plus <plus_minus_m_m
-/2 width=1/ /3 width=6/
+lapply (lift_trans_be … HV2 … HVU ? ?) -HV2 // >minus_plus <plus_minus_m_m /2 width=1/ #HV2U
+lapply (lift_conf_be … HVU2 … HV2U ?) //
+>commutative_plus in ⊢ (??%??→?); <minus_plus_m_m /3 width=6/
qed.
(* Advanced inversion lemmas ************************************************)
elim (lift_trans_le … HT2 … HTU ?) -T // -Hddt #T #HT2 #HTU
>(lift_mono … HTU2 … HT2) -T2 /2 width=3/
qed.
+
+lemma delift_lift_div_be: ∀L,T1,T,d,e,i. L ⊢ T1 [i, d + e - i] ≡ T →
+ ∀T2. ⇧[d, i - d] T2 ≡ T → d ≤ i → i ≤ d + e →
+ L ⊢ T1 [d, e] ≡ T2.
+#L #T1 #T #d #e #i * #T0 #HT10 #HT0 #T2 #HT2 #Hdi #Hide
+lapply (tpss_weak … HT10 d e ? ?) -HT10 // [ >commutative_plus /2 width=1/ ] #HT10
+lapply (lift_trans_be … HT2 … HT0 ? ?) -T //
+>commutative_plus >commutative_plus in ⊢ (? ? (? % ?) ? ? → ?);
+<minus_le_minus_minus_comm // <plus_minus_m_m [ /2 width=3/ | /2 width=1/ ]
+qed.
lemma tpss_ind: ∀d,e,L,T1. ∀R:predicate term. R T1 →
(∀T,T2. L ⊢ T1 ▶* [d, e] T → L ⊢ T ▶ [d, e] T2 → R T → R T2) →
∀T2. L ⊢ T1 ▶* [d, e] T2 → R T2.
-#d #e #L #T1 #R #HT1 #IHT1 #T2 #HT12 @(TC_star_ind … HT1 IHT1 … HT12) //
+#d #e #L #T1 #R #HT1 #IHT1 #T2 #HT12
+@(TC_star_ind … HT1 IHT1 … HT12) //
+qed-.
+
+lemma tpss_ind_dx: ∀d,e,L,T2. ∀R:predicate term. R T2 →
+ (∀T1,T. L ⊢ T1 ▶ [d, e] T → L ⊢ T ▶* [d, e] T2 → R T → R T1) →
+ ∀T1. L ⊢ T1 ▶* [d, e] T2 → R T1.
+#d #e #L #T2 #R #HT2 #IHT2 #T1 #HT12
+@(TC_star_ind_dx … HT2 IHT2 … HT12) //
qed-.
(* Basic properties *********************************************************)
projects / helm.git / commitdiff