(* Properties on inverse basic term relocation ******************************)
+(* Note: this should be stated with tprs *)
lemma cprs_zeta_delift: ∀L,V,T1,T2. L.ⓓV ⊢ T1 ▼*[O, 1] ≡ T2 → L ⊢ ⓓV.T1 ➡* T2.
#L #V #T1 #T2 * #T #HT1 #HT2
@(cprs_strap2 … (ⓓV.T)) [ /3 width=3/ | @inj /3 width=3/ ] (**) (* explicit constructor, /5 width=3/ is too slow *)
#L1 #L2 #HL12 @(lcprs_ind … HL12) -L2 // /3 width=3/
qed.
+lemma lcprs_cpr_trans: ∀L1,L2. L1 ⊢ ➡* L2 →
+ ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2.
+/3 width=3 by lcprs_cprs_trans, inj/ qed.
+
(* Advanced inversion lemmas ************************************************)
(* Basic_1: was pr3_gen_abbr *)
(∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓓV1 ⊢ T1 ➡* T2 &
U2 = ⓓV2. T2
) ∨
- ∃∃U. ⇧[0, 1] U2 ≡ U & L. ⓓV1 ⊢ T1 ➡* U.
+ ∃∃T2. L. ⓓV1 ⊢ T1 ➡* T2 & ⇧[0, 1] U2 ≡ T2.
#L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
#U0 #U2 #_ #HU02 * *
[ #V0 #T0 #HV10 #HT10 #H destruct
lapply (cpr_intro … HV0 … HV2) -HV2 #HV02
lapply (ltpr_cpr_trans (L.ⓓV0) … HT02) /2 width=1/ -V #HT02
lapply (lcprs_cprs_trans (L. ⓓV1) … HT02) -HT02 /2 width=1/ /4 width=5/
- | -V0 #T2 #HT20 #HTU2
- elim (lift_total U2 0 1) #U0 #HU20
- lapply (cpr_lift (L.ⓓV1) … HT20 … HU20 HTU2) -T2 /2 width=1/ /4 width=5/
+ | #T2 #HT02 #HUT2
+ lapply (lcprs_cpr_trans (L.ⓓV1) … HT02) -HT02 /2 width=1/ -V0 #HT02
+ lapply (cprs_trans … HT10 … HT02) -T0 /3 width=3/
]
-| #U1 #HU01 #HTU1
+| #U1 #HTU1 #HU01
elim (lift_total U2 0 1) #U #HU2
- lapply (cpr_lift (L.ⓓV1) … HU01 … HU2 HU02) -U0 /2 width=1/ /4 width=5/
+ lapply (cpr_lift (L.ⓓV1) … HU01 … HU2 HU02) -U0 /2 width=1/ /4 width=3/
]
qed-.
| #V0 #W #T0 #HV10 #HT0 #HU
elim (cprs_inv_abbr1 … HT0) -HT0 *
[ #V3 #T3 #_ #_ #H destruct
- | #X #H #HT2
+ | #X #HT2 #H
elim (lift_inv_bind1 … H) -H #W2 #T2 #HW2 #HT02 #H destruct
@or_intror @(cprs_trans … HU) -U (**) (* explicit constructor *)
@(cprs_trans … (ⓓV.ⓐV2.ⓛW2.T2)) [ /3 width=1/ ] -T
- @(cprs_strap2 … (ⓐV1.ⓛW.T0)) [ /5 width=3/ ] -V -V2 -W2 -T2
+ @(cprs_strap2 … (ⓐV1.ⓛW.T0)) [ /5 width=7/ ] -V -V2 -W2 -T2
@(cprs_strap2 … (ⓓV1.T0)) [ /3 width=1/ ] -W /2 width=1/
]
| #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU
[ #V5 #T5 #HV5 #HT5 #H destruct
lapply (cprs_lift (L.ⓓV) … HV12 … HV13 … HV34) -V1 -V3 /2 width=1/
/3 width=1/
- | #X #H #HT1
+ | #X #HT1 #H
elim (lift_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct
lapply (cprs_lift (L.ⓓV0) … HV12 … HV13 … HV34) -V3 /2 width=1/ #HV24
@(cprs_trans … (ⓓV.ⓐV2.ⓓV5.T5)) [ /3 width=1/ ] -T
- @(cprs_strap2 … (ⓐV1.ⓓV0.T0)) [ /5 width=3/ ] -V -V5 -T5
- @(cprs_strap2 … (ⓓV0.ⓐV2.T0)) [ /3 width=3/ ] -V1 /3 width=9/
+ @(cprs_strap2 … (ⓐV1.ⓓV0.T0)) [ /5 width=7/ ] -V -V5 -T5
+ @(cprs_strap2 … (ⓓV0.ⓐV2.T0)) [ /3 width=3/ ] -V1 /3 width=1/
]
]
qed-.
@(cprs_trans … HU) -U
elim (cprs_inv_abbr1 … HT0) -HT0 *
[ -HV12a -HV12b -HV10a #V1 #T1 #_ #_ #H destruct
- | -V1b #X #H #HT1
+ | -V1b #X #HT1 #H
elim (lift_inv_bind1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct
@(cprs_trans … (ⓓV.ⓐV2a.ⓛW1.T1)) [ /3 width=1/ ] -T -V2b -V2s
- @(cprs_strap2 … (ⓐV1a.ⓛW0.T0)) [ /5 width=3/ ] -V -V2a -W1 -T1
+ @(cprs_strap2 … (ⓐV1a.ⓛW0.T0)) [ /5 width=7/ ] -V -V2a -W1 -T1
@(cprs_strap2 … (ⓓV1a.T0)) [ /3 width=1/ ] -W0 /2 width=1/
]
]
[ #V1 #T1 #HV1 #HT1 #H destruct
lapply (cprs_lift (L.ⓓV) … HV12a … HV10a … HV0a) -V1a -V0a [ /2 width=1/ ] #HV2a
@(cprs_trans … (ⓓV.ⓐV2a.T1)) [ /3 width=1/ ] -T -V2b -V2s /3 width=1/
- | #X #H #HT1
+ | #X #HT1 #H
elim (lift_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct
lapply (cprs_lift (L.ⓓV0) … HV12a … HV10a … HV0a) -V0a [ /2 width=1/ ] #HV2a
@(cprs_trans … (ⓓV.ⓐV2a.ⓓV1.T1)) [ /3 width=1/ ] -T -V2b -V2s
- @(cprs_strap2 … (ⓐV1a.ⓓV0.T0)) [ /5 width=3/ ] -V -V1 -T1
+ @(cprs_strap2 … (ⓐV1a.ⓓV0.T0)) [ /5 width=7/ ] -V -V1 -T1
@(cprs_strap2 … (ⓓV0.ⓐV2a.T0)) [ /3 width=3/ ] -V1a /3 width=1/
]
]
@(csn_lcpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3/
| -IHV -HLV1 * #H destruct /3 width=1/
]
-| -IHV -IHT -H2 #T0 #HT0 #HLT0
- lapply (csn_inv_lift … HT … HT0) -HT /2 width=3/
+| -IHV -IHT -H2 #T0 #HLT0 #HT0
+ lapply (csn_cpr_trans … HT … HLT0) -T #HLT0
+ lapply (csn_inv_lift … HLT0 … HT0) -T0 /2 width=3/
]
qed.
lapply (ltpr_cpr_trans (L. ⓓV) … HLT3) /2 width=1/ -HLT3 #HLT3
@(IHVT … H … HV05) -IHVT // -H -HV05 /3 width=1/
]
- | -H -IHVT #T0 #HT0 #HLT0
- @(csn_cpr_trans … (ⓐV1.T0)) /2 width=1/ -V0 -Y
- @(csn_inv_lift … 0 1 HVT) /2 width=1/
+ | -H -IHVT #T0 #HLT0 #HT0
+ lapply (csn_cpr_trans … HVT (ⓐV2.T0) ?) /2 width=1/ -T #HVT0
+ lapply (csn_inv_lift L … 1 HVT0 ? ? ?) -HVT0 [ /2 width=4/ |2,3: skip | /2 width=1/ ] -V2 -T0 #HVY
+ @(csn_cpr_trans … HVY) /2 width=1/
]
| -HV -HV12 -HVT -IHVT -H #V0 #W0 #T0 #T1 #_ #_ #H destruct
| -IHVT -H #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HLW01 #HLT01 #HV03 #H1 #H2 destruct
(* *)
(**************************************************************************)
-(* FRAGMENT 0
-include "basic_2/unfold/delift_lift.ma".
-
-
-include "basic_2/equivalence/cpcs_cpcs.ma".
-include "basic_2/unfold/delift_delift.ma".
-
-
-
-axiom pippo1: ∀T1,V. ∃∃T2. ⓓV.T1 ➡ T2 & ⋆.ⓓV ⊢ T1 ▼*[0, 1] ≡ T2.
-(*
-#T1 #V elim (pippo0 (⋆.ⓓV) 0 1 ? T1)
-[ #T2 #HT12 @(ex2_1_intro … HT12)
- @tpr
-*)
-
-axiom pippo: ∀L,V,T1. ∃∃T2. L ⊢ ⓓV.T1 ➡ T2 & L.ⓓV ⊢ T1 ▼*[0, 1] ≡ T2.
-
-axiom cprs_inv_appl1_cpcs: ∀L,V1,T1,U2. L ⊢ ⓐV1. T1 ➡* U2 → (
- ∃∃V2,T2. L ⊢ V1 ➡* V2 & L ⊢ T1 ➡* T2 &
- L ⊢ U2 ➡* ⓐV2. T2
- ) ∨
- ∃∃V2,W,T. L ⊢ V1 ➡* V2 &
- L ⊢ T1 ➡* ⓛW. T & L ⊢ ⓓV2. T ⬌* U2.
-#L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
-#U #U2 #_ #HU2 * *
-[ #V0 #T0 #HV10 #HT10 #HUT0
- elim (cprs_strip … HUT0 … HU2) -U #U #H #HU2
- elim (cpr_inv_appl1 … H) -H *
- [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/
- | #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct
- lapply (cprs_strap1 … HV10 HV02) -V0 #HV12
- lapply (cprs_div ? (ⓓV2.T) ? ? ? HU2) -HU2 /2 width=1/ /3 width=6/
- | #V #V2 #W0 #W2 #T #T2 #HV0 #HW02 #HT2 #HV2 #H1 #H2 destruct
- lapply (cprs_strap1 … HV10 HV0) -V0 #HV1
- lapply (cprs_trans … HT10 (ⓓW2.T2) ?) -HT10 /2 width=1/ -W0 -T #HT1
- elim (pippo L W2 T2) #T3 #H1T3 #H2T3
- elim (pippo L W2 (ⓐV2.T2)) #X #H1X #H
- elim (delift_inv_flat1 … H) -H #V3 #Y #HV23 #HY #H destruct
-
-
- @or_introl @(ex3_2_intro … HV1 HT1) -HV1 -HT1
-
- ]
-| /4 width=8/
-]
-qed-.
-
-
-include "basic_2/computation/cprs_lcprs.ma".
+include "basic_2/equivalence/cpcs_delift.ma".
include "basic_2/dynamic/nta.ma".
-
-axiom cprs_inv_appl_abst: ∀L,V,T,W,U. L ⊢ ⓐV.T ➡* ⓛW.U →
- ∃∃V0,W0,T0,W1,U1. ⇧[O, 1] W ≡ W1 &
- ⇧[O + 1, 1] U ≡ U1 &
- L ⊢ V ➡* V0 & L ⊢ T ➡* ⓛW0.T0 &
- L.ⓓV0 ⊢ T0 ➡* ⓛW1.U1.
-#L #V #T #W #U #H
-elim (cprs_inv_appl1 … H) -H *
-[ #V0 #T0 #_ #_ #H destruct
-| #V0 #W0 #T0 #HV0 #HT0 #H
- elim (cprs_inv_abbr1 … H) -H *
- [ #V1 #T1 #_ #_ #H destruct
- | #X #H #HT01
- elim (lift_inv_bind1 … H) -H #W1 #U1 #HW1 #HU1 #H destruct /2 width=10/
- ]
-| #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #H
- elim (cprs_inv_abbr1 … H) -H *
- [ #V3 #T3 #_ #_ #H destruct
- | #X #H #HT3
- elim (lift_inv_bind1 … H) -H #W3 #U3 #HW3 #HU3 #H destruct /2 width=10/
-
-axiom pippo: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. L ⊢ T ➡* ⓛX.Y →
+(*
+lemma pippo: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. L ⊢ T ➡* ⓛX.Y →
∃Z. L ⊢ U ➡* ⓛX.Z.
#h #L #T #U #H elim H -L -T -U
[
|
|
|
-|
-| #L #V #W #T #U #HTU #HUW #IHTU #IHUW #X #Y #HTY
- elim (cprs_inv_appl1 … HTY) -HTY *
+| #L #V #W #T #U #_ #_ #IHVW #IHTU #X #Y #H
+| #L #V #W #T #U #_ #HUW #IHTU #IHUW #X #Y #HTY
+ elim (cprs_inv_appl_abst … HTY) -HTY #W1 #T1 #W2 #T2 #HT1 #HT12 #HYT2
+ elim (IHTU … HT1) -IHTU -HT1 #U1 #HU1
+
+
+
+ *
[ #V0 #T0 #_ #_ #H destruct
| #V0 #W0 #T0 #HV0 #HT0 #HTY
elim (IHTU … HT0) -IHTU -HT0 #Z #HUZ
elim (cprs_inv_abbr1 … HTY) -HTY *
[ #V1 #T1 #_ #_ #H destruct #X0
+*)
+
+(*
+
+include "basic_2/computation/cprs_lcprs.ma".
+
+
+
include "basic_2/dynamic/nta_ltpss.ma".
include "basic_2/dynamic/nta_thin.ma".
(**************************************************************************)
include "basic_2/static/sta.ma".
-include "basic_2/dynamic/nta_lift.ma".
+include "basic_2/equivalence/cpcs_cpcs.ma".
+include "basic_2/dynamic/nta.ma".
(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
-axiom pippo: ∀h,L,X,Y1,U. ⦃h, L⦄ ⊢ ⓐX.Y1 : U → ∀Y2. L ⊢ Y1 ⬌* Y2 →
- ∀U2. ⦃h, L⦄ ⊢ Y2 : U2 → ⦃h, L⦄ ⊢ ⓐX.Y2 : U.
-
(* Properties on static type assignment *************************************)
lemma nta_fwd_sta: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U →
- ∃∃U0. ⦃h, L⦄ ⊢ T • U0 & L ⊢ U0 ⬌* U & ⦃h, L⦄ ⊢ T : U0.
+ ∃∃U0. ⦃h, L⦄ ⊢ T • U0 & L ⊢ U0 ⬌* U.
#h #L #T #U #H elim H -L -T -U
-[ /2 width=4/
-| #L #K #V #W1 #V1 #i #HLK #_ #HWV1 * #W0 #H1VW0 #HW01 #H2VW0
+[ /2 width=3/
+| #L #K #V #W1 #V1 #i #HLK #_ #HWV1 * #W0 #HVW0 #HW01
elim (lift_total W0 0 (i+1)) #V0 #HWV0
lapply (ldrop_fwd_ldrop2 … HLK) #HLK0
- lapply (cpcs_lift … HLK0 … HWV0 … HWV1 HW01) -HLK0 -HWV1 -HW01 /3 width=9/
-| #L #K #W #V1 #W1 #i #HLK #HWV1 #HW1 * /3 width=9/
-| #I #L #V #W #T #U #_ #_ * #W0 #_ #_ #H2VW0 * /3 width=4/
-| #L #V #W #T #U #_ #_ * #W0 #_ #HW0 #H2VW0 * #X #H1 #HX #H2
- elim (sta_inv_bind1 … H1) -H1 #U0 #HTU0 #H destruct
- elim (nta_inv_bind1 … H2) /4 width=4/
-| #L #V #W #T #U #_ #_ * #U0 #H1TU0 #HU0 #H2TU0 * #W0 #_ #_ #H2UW0 -W
- elim (nta_fwd_correct … H2TU0) #T0 #HUT0
- @(ex3_1_intro … (ⓐV.U0)) /2 width=1/ -H1TU0
- @(nta_pure … W0 … H2TU0) -T /3 width=3/
-| #L #T #U #HTU * #U0 #H1TU0 #HU0 #H2TU0
- elim (nta_fwd_correct … H2TU0) -H2TU0 /4 width=8/
-| #L #T #U1 #U2 #V2 #_ #HU12 #_ * #U0 #H1TU0 #HU01 #H2TU0 #_
- lapply (cpcs_trans … HU01 … HU12) -U1 /2 width=4/
+ lapply (cpcs_lift … HLK0 … HWV0 … HWV1 HW01) -HLK0 -HWV1 -HW01 /3 width=6/
+| #L #K #W #V1 #W1 #i #HLK #HWV1 #HW1 * /3 width=6/
+| #I #L #V #W #T #U #_ #_ * #W0 #_ #_ * /3 width=3/
+| #L #V #W #T #U #_ #_ * #W0 #_ #HW0 * #X #H #HX
+ elim (sta_inv_bind1 … H) -H #U0 #HTU0 #H destruct
+ @(ex2_1_intro … (ⓐV.ⓛW.U0)) /2 width=1/ /3 width=1/
+| #L #V #W #T #U #_ #_ * #U0 #HTU0 #HU0 #_ -W
+ @(ex2_1_intro … (ⓐV.U0)) /2 width=1/
+| #L #T #U #HTU * #U0 #HTU0 #HU0 /3 width=3/
+| #L #T #U1 #U2 #V2 #_ #HU12 #_ * #U0 #HTU0 #HU01 #_
+ lapply (cpcs_trans … HU01 … HU12) -U1 /2 width=3/
]
qed-.
(* *)
(**************************************************************************)
-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 ***************************)
+(* Properties on basic local environment thinning ***************************)
(* Note: this is known as the substitution lemma *)
(* Basic_1: was only: ty3_gen_cabbr *)
@(ex2_2_intro … H2) -H2 /2 width=2/ (**) (* explicit constructor, /3 width=6/ is slow *)
qed-.
+lemma cpcs_inv_abst2: ∀L,W1,T1,T. L ⊢ T ⬌* ⓛW1.T1 →
+ ∃∃W2,T2. L ⊢ T ➡* ⓛW2.T2 & L ⊢ ⓛW1.T1 ➡* ⓛW2.T2.
+/3 width=1 by cpcs_inv_abst1, cpcs_sym/ qed-.
+
(* Basic_1: was: pc3_gen_lift *)
lemma cpcs_inv_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K →
∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 →
(* *)
(**************************************************************************)
+include "basic_2/unfold/delift_lift.ma".
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 **************************)
+(* Advanced inversion lemmas ************************************************)
+
+lemma cprs_inv_appl1_cpcs: ∀L,V1,T1,U2. L ⊢ ⓐV1. T1 ➡* U2 → (
+ ∃∃V2,T2. L ⊢ V1 ➡* V2 & L ⊢ T1 ➡* T2 &
+ L ⊢ U2 ➡* ⓐV2. T2
+ ) ∨
+ ∃∃V2,W,T. L ⊢ V1 ➡* V2 &
+ L ⊢ T1 ➡* ⓛW. T & L ⊢ ⓓV2. T ⬌* U2.
+#L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
+#U #U2 #_ #HU2 * *
+[ #V0 #T0 #HV10 #HT10 #HUT0
+ elim (cprs_strip … HUT0 … HU2) -U #U #H #HU2
+ elim (cpr_inv_appl1 … H) -H *
+ [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/
+ | #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct
+ lapply (cprs_strap1 … HV10 HV02) -V0 #HV12
+ lapply (cprs_div ? (ⓓV2.T) ? ? ? HU2) -HU2 /2 width=1/ /3 width=6/
+ | #V #V2 #W0 #W2 #T #T2 #HV0 #HW02 #HT2 #HV2 #H1 #H2 destruct
+ lapply (cprs_strap1 … HV10 HV0) -V0 #HV1
+ lapply (cprs_trans … HT10 (ⓓW2.T2) ?) -HT10 /2 width=1/ -W0 -T #HT1
+ elim (sfr_delift (L.ⓓW2) (ⓐV2.T2) 0 1 ? ?) // #X #H1
+ lapply (cprs_zeta_delift … H1) #H2
+ lapply (cprs_trans … HU2 … H2) -HU2 -H2 #HU2T3
+ elim (delift_inv_flat1 … H1) -H1 #V3 #T3 #HV23 #HT23 #H destruct
+ lapply (delift_inv_lift1_eq … HV23 … HV2) -V2 [ /2 width=1/ | skip ] #H destruct
+ lapply (cprs_zeta_delift … HT23) -HT23 #H
+ lapply (cprs_trans … HT1 … H) -W2 -T2 /3 width=5/
+ ]
+| /4 width=8/
+]
+qed-.
+
+lemma cprs_inv_appl_abst: ∀L,V,T,W,U. L ⊢ ⓐV.T ➡* ⓛW.U →
+ ∃∃W0,T0,V1,T1. L ⊢ T ➡* ⓛW0.T0 &
+ L ⊢ ⓓV.T0 ➡* ⓛV1.T1 &
+ L ⊢ ⓛW.U ➡* ⓛV1.T1.
+#L #V #T #W #U #H
+elim (cprs_inv_appl1_cpcs … H) -H *
+[ #V0 #T0 #HV0 #HT0 #H
+ elim (cprs_inv_abst1 Abst W … H) -H #W0 #U0 #_ #_ #H destruct
+| #V0 #W0 #T0 #HV0 #HT0 #H
+ elim (cpcs_inv_abst2 … H) -H #V1 #T1 #H1 #H2
+ lapply (cprs_trans … (ⓓV.T0) … H1) -H1 /2 width=1/ -V0 /2 width=7/
+]
+qed-.
+
(* Properties on inverse basic term relocation ******************************)
lemma cpcs_zeta_delift_comm: ∀L,V,T1,T2. L.ⓓV ⊢ T1 ▼*[O, 1] ≡ T2 →
>(tpss_inv_sort1 … H) -H //
qed-.
-(* Basic_1: was pr2_gen_abbr *)
-lemma cpr_inv_abbr1: ∀L,V1,T1,U2. L ⊢ ⓓV1. T1 ➡ U2 →
- (∃∃V,V2,T2. V1 ➡ V & L ⊢ V ▶* [O, |L|] V2 &
- L. ⓓV ⊢ T1 ➡ T2 &
- U2 = ⓓV2. T2
- ) ∨
- ∃∃T. ⇧[0,1] T ≡ T1 & L ⊢ T ➡ U2.
-#L #V1 #T1 #Y * #X #H1 #H2
-elim (tpr_inv_abbr1 … H1) -H1 *
-[ #V #T0 #T #HV1 #HT10 #HT0 #H destruct
- elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct
- lapply (tps_lsubs_trans … HT0 (L. ⓓV) ?) -HT0 /2 width=1/ #HT0
- lapply (tps_weak_all … HT0) -HT0 #HT0
- lapply (tpss_lsubs_trans … HT2 (L. ⓓV) ?) -HT2 /2 width=1/ #HT2
- lapply (tpss_weak_all … HT2) -HT2 #HT2
- lapply (tpss_strap … HT0 HT2) -T /4 width=7/
-| /4 width=5/
-]
-qed-.
-
(* Basic_1: was: pr2_gen_cast *)
lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ ⓝV1. T1 ➡ U2 → (
∃∃V2,T2. L ⊢ V1 ➡ V2 & L ⊢ T1 ➡ T2 &
#I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2
elim (tpss_split_up … HT2 1 ? ?) -HT2 // #T0 <minus_n_O #HT0 normalize <minus_plus_m_m #HT02
lapply (tpss_lsubs_trans … HT0 (⋆. ⓑ{I} V2) ?) -HT0 /2 width=1/ #HT0
-lapply (tpss_tps … HT0) -HT0 #HT0
+lapply (tpss_inv_SO2 … HT0) -HT0 #HT0
@ex2_1_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2 width=1/ ] (**) (* /3 width=5/ is too slow *)
qed.
* /3 width=6/
qed-.
+(* Basic_1: was pr2_gen_abbr *)
+lemma cpr_inv_abbr1: ∀L,V1,T1,U2. L ⊢ ⓓV1. T1 ➡ U2 →
+ (∃∃V,V2,T2. V1 ➡ V & L ⊢ V ▶* [O, |L|] V2 &
+ L. ⓓV ⊢ T1 ➡ T2 &
+ U2 = ⓓV2. T2
+ ) ∨
+ ∃∃T2. L.ⓓV1 ⊢ T1 ➡ T2 & ⇧[0,1] U2 ≡ T2.
+#L #V1 #T1 #Y * #X #H1 #H2
+elim (tpr_inv_abbr1 … H1) -H1 *
+[ #V #T #T0 #HV1 #HT1 #HT0 #H destruct
+ elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT02 #H destruct
+ lapply (tps_lsubs_trans … HT0 (L. ⓓV) ?) -HT0 /2 width=1/ #HT0
+ lapply (tps_weak_all … HT0) -HT0 #HT0
+ lapply (tpss_lsubs_trans … HT02 (L. ⓓV) ?) -HT02 /2 width=1/ #HT02
+ lapply (tpss_weak_all … HT02) -HT02 #HT02
+ lapply (tpss_strap … HT0 HT02) -T0 /4 width=7/
+| #T2 #HT12 #HXT2
+ elim (lift_total Y 0 1) #Z #HYZ
+ lapply (tpss_lift_ge … H2 (L.ⓓV1) … HXT2 … HYZ) -X // /2 width=1/ #H
+ lapply (cpr_intro … HT12 … H) -T2 /3 width=3/
+]
+qed-.
+
(* Basic_1: was: pr2_gen_abst *)
lemma cpr_inv_abst1: ∀L,V1,T1,U2. L ⊢ ⓛV1. T1 ➡ U2 → ∀I,W.
∃∃V2,T2. L ⊢ V1 ➡ V2 & L. ⓑ{I} W ⊢ T1 ➡ T2 & U2 = ⓛV2. T2.
∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀U2. L ⊢ U1 ➡ U2 →
∃∃T2. ⇧[d, e] T2 ≡ U2 & K ⊢ T1 ➡ T2.
#L #K #d #e #HLK #T1 #U1 #HTU1 #U2 * #U #HU1 #HU2
-elim (tpr_inv_lift … HU1 … HTU1) -U1 #T #HTU #T1
+elim (tpr_inv_lift1 … HU1 … HTU1) -U1 #T #HTU #T1
elim (lt_or_ge (|L|) d) #HLd
[ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U -HLK [ /5 width=4/ | /2 width=2/ ]
| elim (lt_or_ge (|L|) (d + e)) #HLde
lapply (IH … HKV1 … HK1 … HK12 … HV12) // -L1 -K1 -V1 /2 width=5/
| #L1 #V1 #T1 #B #A #HB #HA #H1 #H2 #L2 #HL12 #X #H destruct
elim (tpr_inv_abbr1 … H) -H *
- [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
- lapply (tps_lsubs_trans … HT02 (L2.ⓓV2) ?) -HT02 /2 width=1/ #HT02
+ [ #V2 #T #T2 #HV12 #HT1 #HT2 #H destruct
+ lapply (tps_lsubs_trans … HT2 (L2.ⓓV2) ?) -HT2 /2 width=1/ #HT2
lapply (IH … HB … HL12 … HV12) -HB /width=5/ #HB
- lapply (IH … HA … (L2.ⓓV2) … HT10) -IH -HA -HT10 /width=5/ -T1 /2 width=1/ -L1 -V1 /3 width=5/
- | -B #T #HT1 #HTX
- elim (lift_total X 0 1) #X1 #HX1
- lapply (tpr_lift … HTX … HT1 … HX1) -T #HTX1
- lapply (IH … HA … (L2.ⓓV1) … HTX1) /width=5/ -T1 /2 width=1/ -L1 #HA
- @(aaa_inv_lift … HA … HX1) /2 width=1/
+ lapply (IH … HA … (L2.ⓓV2) … HT1) -IH -HA -HT1 /width=5/ -T1 /2 width=1/ -L1 -V1 /3 width=5/
+ | -B #T #HT1 #HXT
+ lapply (IH … HA … (L2.ⓓV1) … HT1) /width=5/ -T1 /2 width=1/ -L1 #HA
+ @(aaa_inv_lift … HA … HXT) /2 width=1/
]
| #L1 #V1 #T1 #B #A #HB #HA #H1 #H2 #L2 #HL12 #X #H destruct
elim (tpr_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
elim (IHLK1 … HL12) -L1 /3 width=3/
| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H
elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
- elim (tpr_inv_lift … HV12 … HWV1) -V1
+ elim (tpr_inv_lift1 … HV12 … HWV1) -V1
elim (IHLK1 … HL12) -L1 /3 width=5/
]
qed.
| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
elim (tif_inv_appl … H) -H #_ #_ #H
elim (simple_inv_bind … H)
-| #V1 #T1 #T2 #T #_ #_ #_ #H
+| #V1 #T1 #T #T2 #_ #_ #_ #H
elim (tif_inv_abbr … H)
-| #V1 #T1 #T #_ #_ #H
+| #V1 #T1 #T2 #_ #_ #H
elim (tif_inv_cast … H)
]
qed.
tpr (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
| tpr_beta : ∀V1,V2,W,T1,T2.
tpr V1 V2 → tpr T1 T2 → tpr (ⓐV1. ⓛW. T1) (ⓓV2. T2)
-| tpr_delta: ∀I,V1,V2,T1,T2,T.
- tpr V1 V2 → tpr T1 T2 → ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] T →
- tpr (ⓑ{I} V1. T1) (ⓑ{I} V2. T)
+| tpr_delta: ∀I,V1,V2,T1,T,T2.
+ tpr V1 V2 → tpr T1 T → ⋆. ⓑ{I} V2 ⊢ T ▶ [0, 1] T2 →
+ tpr (ⓑ{I} V1. T1) (ⓑ{I} V2. T2)
| tpr_theta: ∀V,V1,V2,W1,W2,T1,T2.
tpr V1 V2 → ⇧[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 →
tpr (ⓐV1. ⓓW1. T1) (ⓓW2. ⓐV. T2)
-| tpr_zeta : ∀V,T,T1,T2. ⇧[0,1] T1 ≡ T → tpr T1 T2 → tpr (ⓓV. T) T2
+| tpr_zeta : ∀V,T1,T,T2. tpr T1 T → ⇧[0, 1] T2 ≡ T → tpr (ⓓV. T1) T2
| tpr_tau : ∀V,T1,T2. tpr T1 T2 → tpr (ⓝV. T1) T2
.
[ //
| #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
| #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct
-| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #k #H destruct
+| #I #V1 #V2 #T1 #T #T2 #_ #_ #_ #k #H destruct
| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #k #H destruct
-| #V #T #T1 #T2 #_ #_ #k #H destruct
+| #V #T1 #T #T2 #_ #_ #k #H destruct
| #V #T1 #T2 #_ #k #H destruct
]
qed.
/2 width=3/ qed-.
fact tpr_inv_bind1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,T1. U1 = ⓑ{I} V1. T1 →
- (∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
- ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] T &
- U2 = ⓑ{I} V2. T
+ (∃∃V2,T,T2. V1 ➡ V2 & T1 ➡ T &
+ ⋆. ⓑ{I} V2 ⊢ T ▶ [0, 1] T2 &
+ U2 = ⓑ{I} V2. T2
) ∨
- ∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2 & I = Abbr.
+ ∃∃T. T1 ➡ T & ⇧[0, 1] U2 ≡ T & I = Abbr.
#U1 #U2 * -U1 -U2
[ #J #I #V #T #H destruct
| #I1 #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct
| #V1 #V2 #W #T1 #T2 #_ #_ #I #V #T #H destruct
-| #I1 #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #I0 #V0 #T0 #H destruct /3 width=7/
+| #I1 #V1 #V2 #T1 #T #T2 #HV12 #HT1 #HT2 #I0 #V0 #T0 #H destruct /3 width=7/
| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #I0 #V0 #T0 #H destruct
-| #V #T #T1 #T2 #HT1 #HT12 #I0 #V0 #T0 #H destruct /3 width=3/
+| #V #T1 #T #T2 #HT1 #HT2 #I0 #V0 #T0 #H destruct /3 width=3/
| #V #T1 #T2 #_ #I0 #V0 #T0 #H destruct
]
qed.
lemma tpr_inv_bind1: ∀V1,T1,U2,I. ⓑ{I} V1. T1 ➡ U2 →
- (∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
- ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] T &
- U2 = ⓑ{I} V2. T
+ (∃∃V2,T,T2. V1 ➡ V2 & T1 ➡ T &
+ ⋆. ⓑ{I} V2 ⊢ T ▶ [0, 1] T2 &
+ U2 = ⓑ{I} V2. T2
) ∨
- ∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2 & I = Abbr.
+ ∃∃T. T1 ➡ T & ⇧[0,1] U2 ≡ T & I = Abbr.
/2 width=3/ qed-.
(* Basic_1: was pr0_gen_abbr *)
lemma tpr_inv_abbr1: ∀V1,T1,U2. ⓓV1. T1 ➡ U2 →
- (∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
- ⋆. ⓓV2 ⊢ T2 ▶ [0, 1] T &
- U2 = ⓓV2. T
+ (∃∃V2,T,T2. V1 ➡ V2 & T1 ➡ T &
+ ⋆. ⓓV2 ⊢ T ▶ [0, 1] T2 &
+ U2 = ⓓV2. T2
) ∨
- ∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2.
+ ∃∃T. T1 ➡ T & ⇧[0, 1] U2 ≡ T.
#V1 #T1 #U2 #H
elim (tpr_inv_bind1 … H) -H * /3 width=7/
qed-.
[ #I #J #V #T #H destruct
| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=5/
| #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=8/
-| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #J #V0 #T0 #H destruct
+| #I #V1 #V2 #T1 #T #T2 #_ #_ #_ #J #V0 #T0 #H destruct
| #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H destruct /3 width=12/
-| #V #T #T1 #T2 #_ #_ #J #V0 #T0 #H destruct
+| #V #T1 #T #T2 #_ #_ #J #V0 #T0 #H destruct
| #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct /3 width=1/
]
qed.
qed-.
fact tpr_inv_lref2_aux: ∀T1,T2. T1 ➡ T2 → ∀i. T2 = #i →
- ∨∨ T1 = #i
- | ∃∃V,T,T0. ⇧[O,1] T0 ≡ T & T0 ➡ #i &
- T1 = ⓓV. T
- | ∃∃V,T. T ➡ #i & T1 = ⓝV. T.
+ ∨∨ T1 = #i
+ | ∃∃V,T. T ➡ #(i+1) & T1 = ⓓV. T
+ | ∃∃V,T. T ➡ #i & T1 = ⓝV. T.
#T1 #T2 * -T1 -T2
[ #I #i #H destruct /2 width=1/
| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
| #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
-| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
+| #I #V1 #V2 #T1 #T #T2 #_ #_ #_ #i #H destruct
| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
-| #V #T #T1 #T2 #HT1 #HT12 #i #H destruct /3 width=6/
+| #V #T1 #T #T2 #HT1 #HT2 #i #H destruct
+ lapply (lift_inv_lref1_ge … HT2 ?) -HT2 // #H destruct /3 width=4/
| #V #T1 #T2 #HT12 #i #H destruct /3 width=4/
]
qed.
lemma tpr_inv_lref2: ∀T1,i. T1 ➡ #i →
- ∨∨ T1 = #i
- | ∃∃V,T,T0. ⇧[O,1] T0 ≡ T & T0 ➡ #i &
- T1 = ⓓV. T
- | ∃∃V,T. T ➡ #i & T1 = ⓝV. T.
+ ∨∨ T1 = #i
+ | ∃∃V,T. T ➡ #(i+1) & T1 = ⓓV. T
+ | ∃∃V,T. T ➡ #i & T1 = ⓝV. T.
/2 width=3/ qed-.
(* Basic_1: removed theorems 3:
∃∃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/
+elim (tpr_inv_lift1 … HWU1 … HTW1) -W1 /3 width=5/
qed.
elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct /3 width=4/
-| #I #V1 #V2 #T1 #T2 #T0 #HV12 #HT12 #HT2 #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
+| #I #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV12 #IHT1 #d #e #X1 #HX1 #X2 #HX2
elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct
elim (lift_inv_bind1 … HX2) -HX2 #W2 #U0 #HVW2 #HTU0 #HX2 destruct
- elim (lift_total T2 (d + 1) e) #U2 #HTU2
+ elim (lift_total T (d + 1) e) #U #HTU
@tpr_delta
- [4: @(tps_lift_le … HT2 … HTU2 HTU0 ?) /2 width=1/ |1: skip |2: /2 width=4/ |3: /2 width=4/ ] (**) (*/3. is too slow *)
+ [4: @(tps_lift_le … HT2 … HTU HTU0 ?) /2 width=1/ |1: skip |2: /2 width=4/ |3: /2 width=4/ ] (**) (*/3. is too slow *)
| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct
elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct
elim (lift_trans_ge … HV2 … HV3 ?) -V // /3 width=4/
-| #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #X #HX #T0 #HT20
- elim (lift_inv_bind1 … HX) -HX #V3 #T3 #_ #HT3 #HX destruct
- elim (lift_trans_ge … HT1 … HT3 ?) -T // /3 width=6/
+| #V #T1 #T #T2 #_ #HT2 #IHT1 #d #e #X #H #U2 #HTU2
+ elim (lift_inv_bind1 … H) -H #V3 #T3 #_ #HT13 #H destruct -V
+ elim (lift_conf_O1 … HTU2 … HT2) -T2 /3 width=4/
| #V #T1 #T2 #_ #IHT12 #d #e #X #HX #T #HT2
elim (lift_inv_flat1 … HX) -HX #V0 #T0 #_ #HT0 #HX destruct /3 width=4/
]
qed.
(* Basic_1: was: pr0_gen_lift *)
-lemma tpr_inv_lift: ∀T1,T2. T1 ➡ T2 →
- ∀d,e,U1. ⇧[d, e] U1 ≡ T1 →
- ∃∃U2. ⇧[d, e] U2 ≡ T2 & U1 ➡ U2.
+lemma tpr_inv_lift1: ∀T1,T2. T1 ➡ T2 →
+ ∀d,e,U1. ⇧[d, e] U1 ≡ T1 →
+ ∃∃U2. ⇧[d, e] U2 ≡ T2 & U1 ➡ U2.
#T1 #T2 #H elim H -T1 -T2
[ * #i #d #e #U1 #HU1
[ lapply (lift_inv_sort2 … HU1) -HU1 #H destruct /2 width=3/
elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
elim (IHV12 … HV01) -V1
elim (IHT12 … HT01) -T1 /3 width=5/
-| #I #V1 #V2 #T1 #T2 #T0 #_ #_ #HT20 #IHV12 #IHT12 #d #e #X #HX
+| #I #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV12 #IHT1 #d #e #X #HX
elim (lift_inv_bind2 … HX) -HX #W1 #U1 #HWV1 #HUT1 #HX destruct
elim (IHV12 … HWV1) -V1 #W2 #HWV2 #HW12
- elim (IHT12 … HUT1) -T1 #U2 #HUT2 #HU12
- elim (tps_inv_lift1_le … HT20 … HUT2 ?) -T2 // [3: /2 width=5/ |2: skip ] #U0 #HU20 #HUT0
+ elim (IHT1 … HUT1) -T1 #U #HUT #HU1
+ elim (tps_inv_lift1_le … HT2 … HUT ?) -T // [3: /2 width=5/ |2: skip ] #U2 #HU2 #HUT2
@ex2_1_intro [2: /2 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /3 width=5/ is slow *)
| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X #HX
elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
elim (IHT12 … HT01) -T1 #T3 #HT32 #HT03
elim (lift_trans_le … HV32 … HV2 ?) -V2 // #V2 #HV32 #HV2
@ex2_1_intro [2: /3 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /4 width=5/ is slow *)
-| #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #X #HX
- elim (lift_inv_bind2 … HX) -HX #V0 #T0 #_ #HT0 #H destruct
- elim (lift_div_le … HT1 … HT0 ?) -T // #T #HT0 #HT1
- elim (IHT12 … HT1) -T1 /3 width=5/
+| #V #T1 #T #T2 #_ #HT2 #IHT1 #d #e #X #HX
+ elim (lift_inv_bind2 … HX) -HX #V3 #T3 #_ #HT31 #H destruct
+ elim (IHT1 … HT31) -T1 #T1 #HT1 #HT31
+ elim (lift_div_le … HT2 … HT1 ?) -T // /3 width=5/
| #V #T1 #T2 #_ #IHT12 #d #e #X #HX
elim (lift_inv_flat2 … HX) -HX #V0 #T0 #_ #HT01 #H destruct
elim (IHT12 … HT01) -T1 /3 width=3/
]
-qed.
+qed-.
(* Advanced inversion lemmas ************************************************)
[ #I #V #T #H destruct
| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct
- <(tps_inv_refl_SO2 … HT2 ? ? ?) -T /2 width=5/
+| #I #V1 #V2 #T1 #T #T2 #HV12 #HT1 #HT2 #V0 #T0 #H destruct
+ <(tps_inv_refl_SO2 … HT2 ? ? ?) -T2 /2 width=5/
| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
-| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
+| #V #T1 #T #T2 #_ #_ #V0 #T0 #H destruct
| #V #T1 #T2 #_ #V0 #T0 #H destruct
]
qed.
elim (IH … HT02 … HU01) -HT02 -HU01 -IH /2 width=1/ /3 width=5/
qed.
-(* basic-1: was:
+(* Basic-1: was:
pr0_cong_upsilon_refl pr0_cong_upsilon_zeta
pr0_cong_upsilon_cong pr0_cong_upsilon_delta
*)
|3: @tpr_delta [3: @tpr_flat |1: skip ] /2 width=5/
] (**) (* /5 width=14/ is too slow *)
(* case 3: zeta *)
-| -HW02 -HVV -HVVV #UU1 #HUU10 #HUUT1
- elim (tpr_inv_lift … HU02 … HUU10) -HU02 #UU #HUU2 #HUU1
- lapply (tw_lift … HUU10) -HUU10 #HUU10
- elim (IH … HUUT1 … HUU1) -HUUT1 -HUU1 -IH /2 width=1/ -HUU10 #U #HU2 #HUUU2
- @ex2_1_intro
- [2: @tpr_flat
- |1: skip
- |3: @tpr_zeta [2: @lift_flat |1: skip |3: @tpr_flat ]
- ] /2 width=5/ (**) (* /5 width=5/ is too slow *)
+| -HV2 -HW02 -HVV2 #U1 #HU01 #HTU1
+ elim (IH … HU01 … HU02) -HU01 -HU02 -IH // -U0 #U #HU1 #HU2
+ elim (tpr_inv_lift1 … HU1 … HTU1) -U1 #UU #HUU #HT1UU
+ @(ex2_1_intro … (ⓐVV.UU)) /2 width=1/ /3 width=5/ (**) (* /4 width=9/ is too slow *)
]
qed.
∃∃X. X1 ➡ X & X2 ➡ X
) →
V0 ➡ V1 → T0 ➡ T1 → ⋆. ⓓV1 ⊢ T1 ▶ [O,1] TT1 →
- T2 ➡ X2 → ⇧[O, 1] T2 ≡ T0 →
+ T0 ➡ T2 → ⇧[O, 1] X2 ≡ T2 →
∃∃X. ⓓV1. TT1 ➡ X & X2 ➡ X.
-#X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HTX2 #HTT20
-elim (tpr_inv_lift … HT01 … HTT20) -HT01 #TT2 #HTT21 #HTT2
-lapply (tps_inv_lift1_eq … HTT1 … HTT21) -HTT1 #HTT1 destruct
-lapply (tw_lift … HTT20) -HTT20 #HTT20
-elim (IH … HTX2 … HTT2) -HTX2 -HTT2 -IH // /3 width=3/
+#X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HT02 #HXT2
+elim (IH … HT01 … HT02) -IH -HT01 -HT02 // -V0 -T0 #T #HT1 #HT2
+elim (tpr_tps_bind ? ? V1 … HT1 HTT1) -T1 // #TT #HTT1 #HTT
+elim (tpr_inv_lift1 … HT2 … HXT2) -T2 #X #HXT #HX2
+lapply (tps_inv_lift1_eq … HTT … HXT) -HTT #H destruct /3 width=3/
qed.
(* Basic_1: was: pr0_upsilon_upsilon *)
qed.
fact tpr_conf_zeta_zeta:
- ∀V0:term. ∀X2,TT0,T0,T1,T2. (
+ ∀V0:term. ∀X2,TT0,T0,T1,TT2. (
∀X0:term. #[X0] < #[V0] + #[TT0] + 1 →
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
- T0 ➡ T1 → T2 ➡ X2 →
- ⇧[O, 1] T0 ≡ TT0 → ⇧[O, 1] T2 ≡ TT0 →
+ TT0 ➡ T0 → ⇧[O, 1] T1 ≡ T0 →
+ TT0 ➡ TT2 → ⇧[O, 1] X2 ≡ TT2 →
∃∃X. T1 ➡ X & X2 ➡ X.
-#V0 #X2 #TT0 #T0 #T1 #T2 #IH #HT01 #HTX2 #HTT0 #HTT20
-lapply (lift_inj … HTT0 … HTT20) -HTT0 #H destruct
-lapply (tw_lift … HTT20) -HTT20 #HTT20
-elim (IH … HT01 … HTX2) -HT01 -HTX2 -IH // /2 width=3/
+#V0 #X2 #TT0 #T0 #T1 #TT2 #IH #HTT0 #HT10 #HTT02 #HXTT2
+elim (IH … HTT0 … HTT02) -IH -HTT0 -HTT02 // -V0 -TT0 #T #HT0 #HTT2
+elim (tpr_inv_lift1 … HT0 … HT10) -T0 #T0 #HT0 #HT10
+elim (tpr_inv_lift1 … HTT2 … HXTT2) -TT2 #TT2 #HTT2 #HXTT2
+lapply (lift_inj … HTT2 … HT0) -HTT2 #H destruct /2 width=3/
qed.
fact tpr_conf_tau_tau:
(* case 9: delta, delta *)
[ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct
/3 width=11 by tpr_conf_delta_delta/ (**) (* /3 width=11/ is too slow *)
-(* case 10: delta, zata *)
+(* case 10: delta, zeta *)
| #T2 #HT20 #HTX2 #H destruct
/3 width=10 by tpr_conf_delta_zeta/ (**) (* /3 width=10/ is too slow *)
]
| #V0 #TT0 #T0 #T1 #HTT0 #HT01 #H1 #H2 destruct
elim (tpr_inv_abbr1 … H1) -H1 *
(* case 14: zeta, delta (repeated) *)
- [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct
+ [ #V2 #TT2 #T2 #HV02 #HTT02 #HTT2 #H destruct
@ex2_1_comm /3 width=10 by tpr_conf_delta_zeta/
(* case 15: zeta, zeta *)
- | #T2 #HTT20 #HTX2
+ | #TT2 #HTT02 #HXTT2
/3 width=9 by tpr_conf_zeta_zeta/ (**) (* /3 width=9/ is too slow *)
]
| #V0 #T0 #T1 #HT01 #H1 #H2 destruct
elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
elim (IHT12 … HTT1 (L2. ⓛWW) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
lapply (tpss_lsubs_trans … HTT2 (L2. ⓓVV2) ?) -HTT2 /3 width=5/
-| #I #V1 #V2 #T1 #T2 #U2 #HV12 #_ #HTU2 #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
- elim (tps_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
- elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
- elim (IHT12 … HTT1 (L2. ⓑ{I} VV2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
- elim (tpss_strip_neq … HTT2 … HTU2 ?) -T2 /2 width=1/ #T2 #HTT2 #HUT2
- lapply (tps_lsubs_trans … HTT2 (L2. ⓑ{I} V2) ?) -HTT2 /2 width=1/ #HTT2
- elim (ltpss_tps_conf … HTT2 (L2. ⓑ{I} VV2) (d + 1) e ?) -HTT2 /2 width=1/ #W2 #HTTW2 #HTW2
- lapply (tps_lsubs_trans … HTTW2 (⋆. ⓑ{I} VV2) ?) -HTTW2 /2 width=1/ #HTTW2
- lapply (tpss_lsubs_trans … HTW2 (L2. ⓑ{I} VV2) ?) -HTW2 /2 width=1/ #HTW2
- lapply (tpss_trans_eq … HUT2 … HTW2) -T2 /3 width=5/
+| #I #V1 #V2 #T1 #T #T2 #HV12 #_ #HT2 #IHV12 #IHT1 #L1 #d #e #X #H #L2 #HL12
+ elim (tps_inv_bind1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct
+ elim (IHV12 … HVW1 … HL12) -V1 #W2 #HW12 #HVW2
+ elim (IHT1 … HTU1 (L2. ⓑ{I} W2) ?) -T1 /2 width=1/ -HL12 #U #HU1 #HTU
+ elim (tpss_strip_neq … HTU … HT2 ?) -T /2 width=1/ #U2 #HU2 #HTU2
+ lapply (tps_lsubs_trans … HU2 (L2. ⓑ{I} V2) ?) -HU2 /2 width=1/ #HU2
+ elim (ltpss_tps_conf … HU2 (L2. ⓑ{I} W2) (d + 1) e ?) -HU2 /2 width=1/ #U3 #HU3 #HU23
+ lapply (tps_lsubs_trans … HU3 (⋆. ⓑ{I} W2) ?) -HU3 /2 width=1/ #HU3
+ lapply (tpss_lsubs_trans … HU23 (L2. ⓑ{I} W2) ?) -HU23 /2 width=1/ #HU23
+ lapply (tpss_trans_eq … HTU2 … HU23) -U2 /3 width=5/
| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #e #X #H #L2 #HL12
elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct
elim (tps_inv_bind1 … HY) -HY #WW1 #TT1 #HWW1 #HTT1 #H destruct
elim (lift_total VV2 0 1) #VV #H2VV
lapply (tpss_lift_ge … HVV2 (L2. ⓓWW2) … HV2 … H2VV) -V2 /2 width=1/ #HVV
@ex2_1_intro [2: @tpr_theta |1: skip |3: @tpss_bind [2: @tpss_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *)
-| #V1 #TT1 #T1 #T2 #HTT1 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
- elim (tps_inv_bind1 … H) -H #V2 #TT2 #HV12 #HTT12 #H destruct
- elim (tps_inv_lift1_ge … HTT12 L1 … HTT1 ?) -TT1 /2 width=1/ #T2 #HT12 #HTT2
- elim (IHT12 … HT12 … HL12) -T1 -HL12 <minus_plus_m_m /3 width=3/
+| #V #T1 #T #T2 #_ #HT2 #IHT1 #L1 #d #e #X #H #L2 #HL12
+ elim (tps_inv_bind1 … H) -H #W #U1 #_ #HTU1 #H destruct -V
+ elim (IHT1 … HTU1 (L2.ⓓW) ?) -T1 /2 width=1/ -HL12 #U #HU1 #HTU
+ elim (tpss_inv_lift1_ge … HTU L2 … HT2 ?) -T <minus_plus_m_m /3 width=3/
| #V1 #T1 #T2 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
elim (tps_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
elim (IHT12 … HTT1 … HL12) -T1 -HL12 /3 width=3/
⋆. ⓑ{I} V1 ⊢ T1 ▶ [0, 1] U1 →
∃∃U2. U1 ➡ U2 & ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] U2.
#I #V1 #V2 #T1 #T2 #U1 #HV12 #HT12 #HTU1
-elim (tpr_tps_ltpr … HT12 … HTU1 (⋆. ⓑ{I} V2) ?) -T1 /2 width=1/ /3 width=3/
+elim (tpr_tps_ltpr … HT12 … HTU1 (⋆. ⓑ{I} V2) ?) -T1 /2 width=1/ -V1 #U2 #HU12 #HTU2
+lapply (tpss_inv_SO2 … HTU2) -HTU2 /2 width=3/
qed.
lemma tpr_tpss_ltpr: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. T1 ➡ T2 →
qed.
(* Note: apparently this was missing in basic_1 *)
-lemma sta_inv_lift: ∀h,L2,T2,U2. ⦃h, L2⦄ ⊢ T2 • U2 → ∀L1,d,e. ⇩[d, e] L2 ≡ L1 →
- ∀T1. ⇧[d, e] T1 ≡ T2 →
- ∃∃U1. ⦃h, L1⦄ ⊢ T1 • U1 & ⇧[d, e] U1 ≡ U2.
+lemma sta_inv_lift1: ∀h,L2,T2,U2. ⦃h, L2⦄ ⊢ T2 • U2 → ∀L1,d,e. ⇩[d, e] L2 ≡ L1 →
+ ∀T1. ⇧[d, e] T1 ≡ T2 →
+ ∃∃U1. ⦃h, L1⦄ ⊢ T1 • U1 & ⇧[d, e] U1 ≡ U2.
#h #L2 #T2 #U2 #H elim H -L2 -T2 -U2
[ #L2 #k #L1 #d #e #_ #X #H
>(lift_inv_sort2 … H) -X /2 width=3/
--- /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/tpss_tpss.ma".
+include "basic_2/unfold/ltpss_tpss.ma".
+include "basic_2/static/sta_lift.ma".
+
+(* STATIC TYPE ASSIGNMENT ON TERMS ******************************************)
+
+(* Properties about parallel unfold *****************************************)
+
+lemma sta_ltpss_tpss_conf: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 • U1 →
+ ∀L2,d,e. L1 ▶* [d, e] L2 →
+ ∀T2. L2 ⊢ T1 ▶* [d, e] T2 →
+ ∃∃U2. ⦃h, L2⦄ ⊢ T2 • U2 & L2 ⊢ U1 ▶* [d, e] U2.
+#h #L1 #T1 #U #H elim H -L1 -T1 -U
+[ #L1 #k1 #L2 #d #e #_ #T2 #H
+ >(tpss_inv_sort1 … H) -H /2 width=3/
+| #L1 #K1 #V1 #W1 #U1 #i #HLK1 #HVW1 #HWU1 #IHVW1 #L2 #d #e #HL12 #T2 #H
+ elim (tpss_inv_lref1 … H) -H [ | -HVW1 ]
+ [ #H destruct
+ elim (lt_or_ge i d) #Hdi [ -HVW1 | ]
+ [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2
+ elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ #K2 #V2 #HK12 #HV12 #H destruct
+ elim (IHVW1 … HK12 … HV12) -IHVW1 -HK12 -HV12 #W2 #HVW2 #HW12
+ lapply (ldrop_fwd_ldrop2 … HLK2) #H
+ elim (lift_total W2 0 (i+1)) #U2 #HWU2
+ lapply (tpss_lift_ge … HW12 … H … HWU1 … HWU2) // -HW12 -H -HWU1
+ >minus_plus <plus_minus_m_m // -Hdi /3 width=6/
+ | elim (lt_or_ge i (d + e)) #Hide [ -HVW1 | -Hdi -IHVW1 ]
+ [ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2
+ elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ #K2 #V2 #HK12 #HV12 #H destruct
+ elim (IHVW1 … HK12 … HV12) -IHVW1 -HK12 -HV12 #W2 #HVW2 #HW12
+ lapply (ldrop_fwd_ldrop2 … HLK2) #H
+ elim (lift_total W2 0 (i+1)) #U2 #HWU2
+ lapply (tpss_lift_ge … HW12 … H … HWU1 … HWU2) // -HW12 -H -HWU1 >minus_plus #H
+ lapply (tpss_weak … H d e ? ?) [1,2: normalize [ >commutative_plus <plus_minus_m_m // | /2 width=1/ ]] -Hdi -Hide /3 width=6/
+ | lapply (ltpss_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide /3 width=6/
+ ]
+ ]
+ | * #K2 #V2 #W2 #Hdi #Hide #HLK2 #HVW2 #HWT2
+ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0
+ elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ #K0 #V0 #HK12 #HV12 #H destruct
+ lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2
+ lapply (tpss_trans_eq … HV12 HVW2) -V2 #HV1W2
+ elim (IHVW1 … HK12 … HV1W2) -IHVW1 -HK12 -HV1W2 #V2 #HWV2 #HW1V2
+ elim (lift_total V2 0 (i+1)) #U2 #HVU2
+ lapply (sta_lift … HWV2 … HLK2 … HWT2 … HVU2) -HWV2 -HWT2 #HTU2
+ lapply (tpss_lift_ge … HW1V2 … HLK2 … HWU1 … HVU2) // -HW1V2 -HLK2 -HWU1 -HVU2 >minus_plus #H
+ lapply (tpss_weak … H d e ? ?) [1,2: normalize [ >commutative_plus <plus_minus_m_m // | /2 width=1/ ]] -Hdi -Hide /2 width=3/
+ ]
+| #L1 #K1 #W1 #V1 #U1 #i #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #d #e #HL12 #T2 #H
+ elim (tpss_inv_lref1 … H) -H [ | -HWV1 -HWU1 -IHWV1 ]
+ [ #H destruct
+ elim (lt_or_ge i d) #Hdi [ -HWV1 ]
+ [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2
+ elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ #K2 #W2 #HK12 #HW12 #H destruct
+ elim (IHWV1 … HK12 … HW12) -IHWV1 -HK12 #V2 #HWV2 #_
+ lapply (ldrop_fwd_ldrop2 … HLK2) #HLK
+ elim (lift_total W2 0 (i+1)) #U2 #HWU2
+ lapply (tpss_lift_ge … HW12 … HLK … HWU1 … HWU2) // -HW12 -HLK -HWU1
+ >minus_plus <plus_minus_m_m // -Hdi /3 width=6/
+ | elim (lt_or_ge i (d + e)) #Hide [ -HWV1 | -IHWV1 -Hdi ]
+ [ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2
+ elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ #K2 #W2 #HK12 #HW12 #H destruct
+ elim (IHWV1 … HK12 … HW12) -IHWV1 -HK12 #V2 #HWV2 #_
+ lapply (ldrop_fwd_ldrop2 … HLK2) #HLK
+ elim (lift_total W2 0 (i+1)) #U2 #HWU2
+ lapply (tpss_lift_ge … HW12 … HLK … HWU1 … HWU2) // -HW12 -HLK -HWU1 >minus_plus #H
+ lapply (tpss_weak … H d e ? ?) [1,2: normalize [ >commutative_plus <plus_minus_m_m // | /2 width=1/ ]] -Hdi -Hide /3 width=6/
+ | lapply (ltpss_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide /3 width=6/
+ ]
+ ]
+ | * #K2 #V2 #W2 #Hdi #Hide #HLK2 #_ #_
+ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0
+ elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #_ #_ #H destruct
+ lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 -HLK2 #H destruct
+ ]
+| #I #L1 #V1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL12 #X #H
+ elim (tpss_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ elim (IHTU1 … HT12) -IHTU1 -HT12 /2 width=1/ -HL12 /3 width=5/
+| #L1 #V1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL12 #X #H
+ elim (tpss_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ elim (IHTU1 … HT12) -IHTU1 -HT12 // -HL12 /3 width=5/
+| #L1 #W1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL12 #X #H
+ elim (tpss_inv_flat1 … H) -H #W2 #T2 #HW12 #HT12 #H destruct
+ elim (IHTU1 … HT12) -IHTU1 -HT12 // -HL12 /3 width=3/
+]
+qed.
+
+lemma sta_ltpss_tps_conf: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 • U1 →
+ ∀L2,d,e. L1 ▶* [d, e] L2 →
+ ∀T2. L2 ⊢ T1 ▶ [d, e] T2 →
+ ∃∃U2. ⦃h, L2⦄ ⊢ T2 • U2 & L2 ⊢ U1 ▶* [d, e] U2.
+/3 width=5/ qed.
+
+lemma sta_ltpss_conf: ∀h,L1,T,U1. ⦃h, L1⦄ ⊢ T • U1 →
+ ∀L2,d,e. L1 ▶* [d, e] L2 →
+ ∃∃U2. ⦃h, L2⦄ ⊢ T • U2 & L2 ⊢ U1 ▶* [d, e] U2.
+/2 width=5/ qed.
+
+lemma sta_tpss_conf: ∀h,L,T1,U1. ⦃h, L⦄ ⊢ T1 • U1 →
+ ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 →
+ ∃∃U2. ⦃h, L⦄ ⊢ T2 • U2 & L ⊢ U1 ▶* [d, e] U2.
+/2 width=5/ qed.
+
+lemma sta_tps_conf: ∀h,L,T1,U1. ⦃h, L⦄ ⊢ T1 • U1 →
+ ∀T2,d,e. L ⊢ T1 ▶ [d, e] T2 →
+ ∃∃U2. ⦃h, L⦄ ⊢ T2 • U2 & L ⊢ U1 ▶* [d, e] U2.
+/2 width=5/ qed.
(* Advanced properties ******************************************************)
+lemma lift_conf_O1: ∀T,T1,d1,e1. ⇧[d1, e1] T ≡ T1 → ∀T2,e2. ⇧[0, e2] T ≡ T2 →
+ ∃∃T0. ⇧[0, e2] T1 ≡ T0 & ⇧[d1 + e2, e1] T2 ≡ T0.
+#T #T1 #d1 #e1 #HT1 #T2 #e2 #HT2
+elim (lift_total T1 0 e2) #T0 #HT10
+elim (lift_trans_le … HT1 … HT10 ?) -HT1 // #X #HTX #HT20
+lapply (lift_mono … HTX … HT2) -T #H destruct /2 width=3/
+qed.
+
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
lapply (HL … HLX) -HL -HLX /2 width=1/
qed.
+lemma sfr_abbr_O: ∀L,V. ≽[0,1] L.ⓓV.
+#L #V
+@(sfr_abbr … 0) //
+qed.
+
lemma sfr_skip: ∀I,L,V,d,e. ≽ [d, e] L → ≽ [d + 1, e] L.ⓑ{I}V.
#I #L #V #d #e #HL #K #H
elim (lsubs_inv_skip2 … H ?) -H // <minus_plus_m_m #J #X #W #HLX #H destruct
(* PARTIAL UNFOLD ON TERMS **************************************************)
-(* Advanced properties ******************************************************)
+(* Advanced inversion lemmas ************************************************)
-lemma tpss_tps: ∀L,T1,T2,d. L ⊢ T1 ▶* [d, 1] T2 → L ⊢ T1 ▶ [d, 1] T2.
+lemma tpss_inv_SO2: ∀L,T1,T2,d. L ⊢ T1 ▶* [d, 1] T2 → L ⊢ T1 ▶ [d, 1] T2.
#L #T1 #T2 #d #H @(tpss_ind … H) -T2 //
#T #T2 #_ #HT2 #IHT1
lapply (tps_trans_ge … IHT1 … HT2 ?) //
-qed.
+qed-.
+
+(* Advanced properties ******************************************************)
lemma tpss_strip_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 ▶* [d1, e1] T1 →
∀T2,d2,e2. L ⊢ T0 ▶ [d2, e2] T2 →
<key name="ex">3 1</key>
<key name="ex">3 2</key>
<key name="ex">3 3</key>
+ <key name="ex">3 4</key>
<key name="ex">4 2</key>
<key name="ex">4 3</key>
<key name="ex">4 4</key>
<key name="ex">5 2</key>
<key name="ex">5 3</key>
<key name="ex">5 4</key>
- <key name="ex">5 5</key>
<key name="ex">6 4</key>
<key name="ex">6 6</key>
<key name="ex">7 6</key>
interpretation "multiple existental quantifier (3, 3)" 'Ex P0 P1 P2 = (ex3_3 ? ? ? P0 P1 P2).
+(* multiple existental quantifier (3, 4) *)
+
+inductive ex3_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2:A0→A1→A2→A3→Prop) : Prop ≝
+ | ex3_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → ex3_4 ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (3, 4)" 'Ex P0 P1 P2 = (ex3_4 ? ? ? ? P0 P1 P2).
+
(* multiple existental quantifier (4, 2) *)
inductive ex4_2 (A0,A1:Type[0]) (P0,P1,P2,P3:A0→A1→Prop) : Prop ≝
interpretation "multiple existental quantifier (5, 4)" 'Ex P0 P1 P2 P3 P4 = (ex5_4 ? ? ? ? P0 P1 P2 P3 P4).
-(* multiple existental quantifier (5, 5) *)
-
-inductive ex5_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→A4→Prop) : Prop ≝
- | ex5_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → ex5_5 ? ? ? ? ? ? ? ? ? ?
-.
-
-interpretation "multiple existental quantifier (5, 5)" 'Ex P0 P1 P2 P3 P4 = (ex5_5 ? ? ? ? ? P0 P1 P2 P3 P4).
-
(* multiple existental quantifier (6, 4) *)
inductive ex6_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→Prop) : Prop ≝
non associative with precedence 20
for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) }.
+(* multiple existental quantifier (3, 4) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) }.
+
(* multiple existental quantifier (4, 2) *)
notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)"
non associative with precedence 20
for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) }.
-(* multiple existental quantifier (5, 5) *)
-
-notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)"
- non associative with precedence 20
- for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P4) }.
-
-notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)"
- non associative with precedence 20
- for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) }.
-
(* multiple existental quantifier (6, 4) *)
notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)"
(* star *)
inductive star (A:Type[0]) (R:relation A) (a:A): A → Prop ≝
- |inj: ∀b,c.star A R a b → R b c → star A R a c
+ |sstep: ∀b,c.star A R a b → R b c → star A R a c
|refl: star A R a a.
lemma R_to_star: ∀A,R,a,b. R a b → star A R a b.
(* right associative version of star *)
inductive starl (A:Type[0]) (R:relation A) : A → A → Prop ≝
- |injl: ∀a,b,c.R a b → starl A R b c → starl A R a c
+ |sstepl: ∀a,b,c.R a b → starl A R b c → starl A R a c
|refll: ∀a.starl A R a a.
lemma starl_comp : ∀A,R,a,b,c.
starl A R a b → R b c → starl A R a c.
#A #R #a #b #c #Hstar elim Hstar
- [#a1 #b1 #c1 #Rab #sbc #Hind #a1 @(injl … Rab) @Hind //
- |#a1 #Rac @(injl … Rac) //
+ [#a1 #b1 #c1 #Rab #sbc #Hind #a1 @(sstepl … Rab) @Hind //
+ |#a1 #Rac @(sstepl … Rac) //
]
qed.
lemma star_compl : ∀A,R,a,b,c.
R a b → star A R b c → star A R a c.
#A #R #a #b #c #Rab #Hstar elim Hstar
- [#b1 #c1 #sbb1 #Rb1c1 #Hind @(inj … Rb1c1) @Hind
- |@(inj … Rab) //
+ [#b1 #c1 #sbb1 #Rb1c1 #Hind @(sstep … Rb1c1) @Hind
+ |@(sstep … Rab) //
]
qed.
projects / helm.git / commitdiff