From: Ferruccio Guidi Date: Sat, 26 Nov 2011 16:42:19 +0000 (+0000) Subject: component "substitution" updated to new syntax ... X-Git-Tag: make_still_working~2058 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=48e1e9851375f52d26ccba5bf4babd0b3474d869;hp=18ac3a120a3887b144c1d0e13d64d6e1c2d10d93;p=helm.git component "substitution" updated to new syntax ... --- diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma index ffd44c5aa..db31dfaab 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma @@ -16,7 +16,7 @@ include "Basic_2/grammar/lenv_weight.ma". include "Basic_2/grammar/lsubs.ma". include "Basic_2/substitution/lift.ma". -(* DROPPING *****************************************************************) +(* LOCAL ENVIRONMENT SLICING ************************************************) (* Basic_1: includes: ldrop_skip_bind *) inductive ldrop: nat → nat → relation lenv ≝ @@ -33,7 +33,7 @@ interpretation "ldropping" 'RDrop d e L1 L2 = (ldrop d e L1 L2). (* Basic inversion lemmas ***************************************************) fact ldrop_inv_refl_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → e = 0 → L1 = L2. -#d #e #L1 #L2 * -d e L1 L2 +#d #e #L1 #L2 * -d -e -L1 -L2 [ // | // | #L1 #L2 #I #V #e #_ #_ #H @@ -49,7 +49,7 @@ lemma ldrop_inv_refl: ∀L1,L2. ↓[0, 0] L1 ≡ L2 → L1 = L2. fact ldrop_inv_atom1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → L1 = ⋆ → L2 = ⋆. -#d #e #L1 #L2 * -d e L1 L2 +#d #e #L1 #L2 * -d -e -L1 -L2 [ // | #L #I #V #H destruct | #L1 #L2 #I #V #e #_ #H destruct @@ -65,10 +65,10 @@ fact ldrop_inv_O1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → ∀K,I,V. L1 = K. 𝕓{I} V → (e = 0 ∧ L2 = K. 𝕓{I} V) ∨ (0 < e ∧ ↓[d, e - 1] K ≡ L2). -#d #e #L1 #L2 * -d e L1 L2 +#d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #K #I #V #H destruct -| #L #I #V #_ #K #J #W #HX destruct -L I V /3/ -| #L1 #L2 #I #V #e #HL12 #_ #K #J #W #H destruct -L1 I V /3/ +| #L #I #V #_ #K #J #W #HX destruct /3 width=1/ +| #L1 #L2 #I #V #e #HL12 #_ #K #J #W #H destruct /3 width=1/ | #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false … H) ] qed. @@ -76,13 +76,13 @@ qed. lemma ldrop_inv_O1: ∀e,K,I,V,L2. ↓[0, e] K. 𝕓{I} V ≡ L2 → (e = 0 ∧ L2 = K. 𝕓{I} V) ∨ (0 < e ∧ ↓[0, e - 1] K ≡ L2). -/2/ qed-. +/2 width=3/ qed-. (* Basic_1: was: ldrop_gen_ldrop *) lemma ldrop_inv_ldrop1: ∀e,K,I,V,L2. ↓[0, e] K. 𝕓{I} V ≡ L2 → 0 < e → ↓[0, e - 1] K ≡ L2. #e #K #I #V #L2 #H #He -elim (ldrop_inv_O1 … H) -H * // #H destruct -e; +elim (ldrop_inv_O1 … H) -H * // #H destruct elim (lt_refl_false … He) qed-. @@ -91,12 +91,11 @@ fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → ∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 & ↑[d - 1, e] V2 ≡ V1 & L2 = K2. 𝕓{I} V2. -#d #e #L1 #L2 * -d e L1 L2 +#d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #I #K #V #H destruct | #L #I #V #H elim (lt_refl_false … H) | #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H) -| #X #L2 #Y #Z #V2 #d #e #HL12 #HV12 #_ #I #L1 #V1 #H destruct -X Y Z - /2 width=5/ +| #X #L2 #Y #Z #V2 #d #e #HL12 #HV12 #_ #I #L1 #V1 #H destruct /2 width=5/ ] qed. @@ -105,19 +104,18 @@ lemma ldrop_inv_skip1: ∀d,e,I,K1,V1,L2. ↓[d, e] K1. 𝕓{I} V1 ≡ L2 → 0 ∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 & ↑[d - 1, e] V2 ≡ V1 & L2 = K2. 𝕓{I} V2. -/2/ qed-. +/2 width=3/ qed-. fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → ∀I,K2,V2. L2 = K2. 𝕓{I} V2 → ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & ↑[d - 1, e] V2 ≡ V1 & L1 = K1. 𝕓{I} V1. -#d #e #L1 #L2 * -d e L1 L2 +#d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #I #K #V #H destruct | #L #I #V #H elim (lt_refl_false … H) | #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H) -| #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #I #L2 #V2 #H destruct -X Y Z - /2 width=5/ +| #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #I #L2 #V2 #H destruct /2 width=5/ ] qed. @@ -125,7 +123,7 @@ qed. lemma ldrop_inv_skip2: ∀d,e,I,L1,K2,V2. ↓[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < d → ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & ↑[d - 1, e] V2 ≡ V1 & L1 = K1. 𝕓{I} V1. -/2/ qed-. +/2 width=3/ qed-. (* Basic properties *********************************************************) @@ -136,7 +134,7 @@ qed. lemma ldrop_ldrop_lt: ∀L1,L2,I,V,e. ↓[0, e - 1] L1 ≡ L2 → 0 < e → ↓[0, e] L1. 𝕓{I} V ≡ L2. -#L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) /2/ +#L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/ qed. lemma ldrop_lsubs_ldrop1_abbr: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → @@ -144,27 +142,27 @@ lemma ldrop_lsubs_ldrop1_abbr: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → d ≤ i → i < d + e → ∃∃K2. K1 [0, d + e - i - 1] ≼ K2 & ↓[0, i] L2 ≡ K2. 𝕓{Abbr} V. -#L1 #L2 #d #e #H elim H -H L1 L2 d e +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e [ #d #e #K1 #V #i #H lapply (ldrop_inv_atom1 … H) -H #H destruct | #L1 #L2 #K1 #V #i #_ #_ #H elim (lt_zero_false … H) | #L1 #L2 #V #e #HL12 #IHL12 #K1 #W #i #H #_ #Hie elim (ldrop_inv_O1 … H) -H * #Hi #HLK1 - [ -IHL12 Hie; destruct -i K1 W; - arith_g1 // /3/ + [ -IHL12 -Hie destruct + arith_g1 // /3 width=3/ ] | #L1 #L2 #I #V1 #V2 #e #_ #IHL12 #K1 #W #i #H #_ #Hie elim (ldrop_inv_O1 … H) -H * #Hi #HLK1 - [ -IHL12 Hie Hi; destruct - | elim (IHL12 … HLK1 ? ?) -IHL12 HLK1 // [2: /2/ ] -Hie >arith_g1 // /3/ + [ -IHL12 -Hie -Hi destruct + | elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >arith_g1 // /3 width=3/ ] | #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #IHL12 #K1 #V #i #H #Hdi >plus_plus_comm_23 #Hide lapply (plus_S_le_to_pos … Hdi) #Hi lapply (ldrop_inv_ldrop1 … H ?) -H // #HLK1 - elim (IHL12 … HLK1 ? ?) -IHL12 HLK1 [2: /2/ |3: /2/ ] -Hdi Hide >arith_g1 // /3/ + elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 /2 width=1/ -Hdi -Hide >arith_g1 // /3 width=3/ ] qed. @@ -177,17 +175,17 @@ lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ↓[O, e] L1 ≡ K2. 𝕓{I2} V2 → [ #I2 #K2 #V2 #e #H lapply (ldrop_inv_atom1 … H) -H #H destruct | #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H elim (ldrop_inv_O1 … H) -H * #He #H - [ -IHL1; destruct -e K2 I2 V2 /2/ - | @ldrop_ldrop >(plus_minus_m_m e 1) /2/ + [ -IHL1 destruct /2 width=1/ + | @ldrop_ldrop >(plus_minus_m_m e 1) // /2 width=3/ ] ] qed-. lemma ldrop_fwd_lw: ∀L1,L2,d,e. ↓[d, e] L1 ≡ L2 → #[L2] ≤ #[L1]. -#L1 #L2 #d #e #H elim H -H L1 L2 d e // normalize -[ /2/ +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize +[ /2 width=1/ | #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 - >(tw_lift … HV21) -HV21 /2/ + >(tw_lift … HV21) -HV21 /2 width=1/ ] qed-. @@ -197,8 +195,8 @@ lemma ldrop_fwd_ldrop2_length: ∀L1,I2,K2,V2,e. [ #I2 #K2 #V2 #e #H lapply (ldrop_inv_atom1 … H) -H #H destruct | #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H elim (ldrop_inv_O1 … H) -H * #He #H - [ -IHL1; destruct -e K2 I2 V2 // - | lapply (IHL1 … H) -IHL1 H #HeK1 whd in ⊢ (? ? %) /2/ + [ -IHL1 destruct // + | lapply (IHL1 … H) -IHL1 -H #HeK1 whd in ⊢ (? ? %); /2 width=1/ ] ] qed-. @@ -208,8 +206,8 @@ lemma ldrop_fwd_O1_length: ∀L1,L2,e. ↓[0, e] L1 ≡ L2 → |L2| = |L1| - e. [ #L2 #e #H >(ldrop_inv_atom1 … H) -H // | #K1 #I1 #V1 #IHL1 #L2 #e #H elim (ldrop_inv_O1 … H) -H * #He #H - [ -IHL1; destruct -e L2 // - | lapply (IHL1 … H) -IHL1 H #H >H -H; normalize + [ -IHL1 destruct // + | lapply (IHL1 … H) -IHL1 -H #H >H -H normalize >minus_le_minus_minus_comm // ] ] diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma index a495bbdcb..f4b20bcb5 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma @@ -22,17 +22,17 @@ include "Basic_2/substitution/ldrop.ma". (* Basic_1: was: ldrop_mono *) theorem ldrop_mono: ∀d,e,L,L1. ↓[d, e] L ≡ L1 → ∀L2. ↓[d, e] L ≡ L2 → L1 = L2. -#d #e #L #L1 #H elim H -H d e L L1 +#d #e #L #L1 #H elim H -d -e -L -L1 [ #d #e #L2 #H - >(ldrop_inv_atom1 … H) -H L2 // + >(ldrop_inv_atom1 … H) -L2 // | #K #I #V #L2 #HL12 - <(ldrop_inv_refl … HL12) -HL12 L2 // + <(ldrop_inv_refl … HL12) -L2 // | #L #K #I #V #e #_ #IHLK #L2 #H - lapply (ldrop_inv_ldrop1 … H ?) -H /2/ + lapply (ldrop_inv_ldrop1 … H ?) -H // /2 width=1/ | #L #K1 #I #T #V1 #d #e #_ #HVT1 #IHLK1 #X #H - elim (ldrop_inv_skip1 … H ?) -H // (lift_inj … HVT1 … HVT2) -HVT1 HVT2 - >(IHLK1 … HLK2) -IHLK1 HLK2 // + elim (ldrop_inv_skip1 … H ?) -H // (lift_inj … HVT1 … HVT2) -HVT1 -HVT2 + >(IHLK1 … HLK2) -IHLK1 -HLK2 // ] qed-. @@ -40,18 +40,18 @@ qed-. theorem ldrop_conf_ge: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 → ∀e2,L2. ↓[0, e2] L ≡ L2 → d1 + e1 ≤ e2 → ↓[0, e2 - e1] L1 ≡ L2. -#d1 #e1 #L #L1 #H elim H -H d1 e1 L L1 +#d1 #e1 #L #L1 #H elim H -d1 -e1 -L -L1 [ #d #e #e2 #L2 #H - >(ldrop_inv_atom1 … H) -H L2 // + >(ldrop_inv_atom1 … H) -L2 // | // | #L #K #I #V #e #_ #IHLK #e2 #L2 #H #He2 - lapply (ldrop_inv_ldrop1 … H ?) -H /2/ #HL2 - minus_minus_comm /3/ (**) (* explicit constructor *) + @ldrop_ldrop_lt >minus_minus_comm /3 width=1/ (**) (* explicit constructor *) ] qed. @@ -61,7 +61,7 @@ theorem ldrop_conf_lt: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 → e2 < d1 → let d ≝ d1 - e2 - 1 in ∃∃K1,V1. ↓[0, e2] L1 ≡ K1. 𝕓{I} V1 & ↓[d, e1] K2 ≡ K1 & ↑[d, e1] V1 ≡ V2. -#d1 #e1 #L #L1 #H elim H -H d1 e1 L L1 +#d1 #e1 #L #L1 #H elim H -d1 -e1 -L -L1 [ #d #e #e2 #K2 #I #V2 #H lapply (ldrop_inv_atom1 … H) -H #H destruct | #L #I #V #e2 #K2 #J #V2 #_ #H @@ -70,9 +70,9 @@ theorem ldrop_conf_lt: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 → elim (lt_zero_false … H) | #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #IHL12 #e2 #K2 #J #V #H #He2d elim (ldrop_inv_O1 … H) -H * - [ -IHL12 He2d #H1 #H2 destruct -e2 K2 J V /2 width=5/ + [ -IHL12 -He2d #H1 #H2 destruct /2 width=5/ | -HL12 -HV12 #He #HLK - elim (IHL12 … HLK ?) -IHL12 HLK [ (ldrop_inv_atom1 … H) -H L2 /2/ + >(ldrop_inv_atom1 … H) -L2 /2 width=3/ | #K #I #V #e2 #L2 #HL2 #H - lapply (le_O_to_eq_O … H) -H #H destruct -e2 /2/ + lapply (le_O_to_eq_O … H) -H #H destruct /2 width=3/ | #L1 #L2 #I #V #e #_ #IHL12 #e2 #L #HL2 #H - lapply (le_O_to_eq_O … H) -H #H destruct -e2; - elim (IHL12 … HL2 ?) -IHL12 HL2 // #L0 #H #HL0 - lapply (ldrop_inv_refl … H) -H #H destruct -L1 /3 width=5/ + lapply (le_O_to_eq_O … H) -H #H destruct + elim (IHL12 … HL2 ?) -IHL12 -HL2 // #L0 #H #HL0 + lapply (ldrop_inv_refl … H) -H #H destruct /3 width=5/ | #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #IHL12 #e2 #L #H #He2d elim (ldrop_inv_O1 … H) -H * - [ -He2d IHL12 #H1 #H2 destruct -e2 L /3 width=5/ - | -HL12 HV12 #He2 #HL2 - elim (IHL12 … HL2 ?) -IHL12 HL2 L2 - [ >minus_le_minus_minus_comm // /3/ | /2/ ] + [ -He2d -IHL12 #H1 #H2 destruct /3 width=5/ + | -HL12 -HV12 #He2 #HL2 + elim (IHL12 … HL2 ?) -L2 [ >minus_le_minus_minus_comm // /3 width=3/ | /2 width=1/ ] ] ] qed. @@ -103,16 +102,16 @@ qed. (* Basic_1: was: ldrop_trans_ge *) theorem ldrop_trans_ge: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L → ∀e2,L2. ↓[0, e2] L ≡ L2 → d1 ≤ e2 → ↓[0, e1 + e2] L1 ≡ L2. -#d1 #e1 #L1 #L #H elim H -H d1 e1 L1 L +#d1 #e1 #L1 #L #H elim H -d1 -e1 -L1 -L [ #d #e #e2 #L2 #H - >(ldrop_inv_atom1 … H) -H L2 // + >(ldrop_inv_atom1 … H) -H -L2 // | // -| /3/ +| /3 width=1/ | #L1 #L2 #I #V1 #V2 #d #e #H_ #_ #IHL12 #e2 #L #H #Hde2 lapply (lt_to_le_to_lt 0 … Hde2) // #He2 lapply (lt_to_le_to_lt … (e + e2) He2 ?) // #Hee2 lapply (ldrop_inv_ldrop1 … H ?) -H // #HL2 - @ldrop_ldrop_lt // >le_plus_minus // @IHL12 /2/ (**) (* explicit constructor *) + @ldrop_ldrop_lt // >le_plus_minus // @IHL12 /2 width=1/ (**) (* explicit constructor *) ] qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma index 7d0f43c81..f58c1906e 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma @@ -37,14 +37,14 @@ interpretation "relocation" 'RLift d e T1 T2 = (lift d e T1 T2). (* Basic inversion lemmas ***************************************************) fact lift_inv_refl_aux: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → e = 0 → T1 = T2. -#d #e #T1 #T2 #H elim H -H d e T1 T2 /3/ +#d #e #T1 #T2 #H elim H -d -e -T1 -T2 // /3 width=1/ qed. lemma lift_inv_refl: ∀d,T1,T2. ↑[d, 0] T1 ≡ T2 → T1 = T2. -/2/ qed-. +/2 width=4/ qed-. fact lift_inv_sort1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T1 = ⋆k → T2 = ⋆k. -#d #e #T1 #T2 * -d e T1 T2 // +#d #e #T1 #T2 * -d -e -T1 -T2 // [ #i #d #e #_ #k #H destruct | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct @@ -56,10 +56,10 @@ lemma lift_inv_sort1: ∀d,e,T2,k. ↑[d,e] ⋆k ≡ T2 → T2 = ⋆k. fact lift_inv_lref1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T1 = #i → (i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)). -#d #e #T1 #T2 * -d e T1 T2 +#d #e #T1 #T2 * -d -e -T1 -T2 [ #k #d #e #i #H destruct -| #j #d #e #Hj #i #Hi destruct /3/ -| #j #d #e #Hj #i #Hi destruct /3/ +| #j #d #e #Hj #i #Hi destruct /3 width=1/ +| #j #d #e #Hj #i #Hi destruct /3 width=1/ | #p #d #e #i #H destruct | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct @@ -68,22 +68,22 @@ qed. lemma lift_inv_lref1: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 → (i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)). -/2/ qed-. +/2 width=3/ qed-. lemma lift_inv_lref1_lt: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 → i < d → T2 = #i. #d #e #T2 #i #H elim (lift_inv_lref1 … H) -H * // -#Hdi #_ #Hid lapply (le_to_lt_to_lt … Hdi Hid) -Hdi Hid #Hdd +#Hdi #_ #Hid lapply (le_to_lt_to_lt … Hdi Hid) -Hdi -Hid #Hdd elim (lt_refl_false … Hdd) qed-. lemma lift_inv_lref1_ge: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 → d ≤ i → T2 = #(i + e). #d #e #T2 #i #H elim (lift_inv_lref1 … H) -H * // -#Hid #_ #Hdi lapply (le_to_lt_to_lt … Hdi Hid) -Hdi Hid #Hdd +#Hid #_ #Hdi lapply (le_to_lt_to_lt … Hdi Hid) -Hdi -Hid #Hdd elim (lt_refl_false … Hdd) qed-. fact lift_inv_gref1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀p. T1 = §p → T2 = §p. -#d #e #T1 #T2 * -d e T1 T2 // +#d #e #T1 #T2 * -d -e -T1 -T2 // [ #i #d #e #_ #k #H destruct | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct @@ -97,7 +97,7 @@ fact lift_inv_bind1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀I,V1,U1. T1 = 𝕓{I} V1.U1 → ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 & T2 = 𝕓{I} V2. U2. -#d #e #T1 #T2 * -d e T1 T2 +#d #e #T1 #T2 * -d -e -T1 -T2 [ #k #d #e #I #V1 #U1 #H destruct | #i #d #e #_ #I #V1 #U1 #H destruct | #i #d #e #_ #I #V1 #U1 #H destruct @@ -110,13 +110,13 @@ qed. lemma lift_inv_bind1: ∀d,e,T2,I,V1,U1. ↑[d,e] 𝕓{I} V1. U1 ≡ T2 → ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 & T2 = 𝕓{I} V2. U2. -/2/ qed-. +/2 width=3/ qed-. fact lift_inv_flat1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀I,V1,U1. T1 = 𝕗{I} V1.U1 → ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 & T2 = 𝕗{I} V2. U2. -#d #e #T1 #T2 * -d e T1 T2 +#d #e #T1 #T2 * -d -e -T1 -T2 [ #k #d #e #I #V1 #U1 #H destruct | #i #d #e #_ #I #V1 #U1 #H destruct | #i #d #e #_ #I #V1 #U1 #H destruct @@ -129,10 +129,10 @@ qed. lemma lift_inv_flat1: ∀d,e,T2,I,V1,U1. ↑[d,e] 𝕗{I} V1. U1 ≡ T2 → ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 & T2 = 𝕗{I} V2. U2. -/2/ qed-. +/2 width=3/ qed-. fact lift_inv_sort2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k → T1 = ⋆k. -#d #e #T1 #T2 * -d e T1 T2 // +#d #e #T1 #T2 * -d -e -T1 -T2 // [ #i #d #e #_ #k #H destruct | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct @@ -145,10 +145,10 @@ lemma lift_inv_sort2: ∀d,e,T1,k. ↑[d,e] T1 ≡ ⋆k → T1 = ⋆k. fact lift_inv_lref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T2 = #i → (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)). -#d #e #T1 #T2 * -d e T1 T2 +#d #e #T1 #T2 * -d -e -T1 -T2 [ #k #d #e #i #H destruct -| #j #d #e #Hj #i #Hi destruct /3/ -| #j #d #e #Hj #i #Hi destruct (plus_minus_m_m i e) in ⊢ (? ? ? ? %) /3 width=2/ +#d #e #i #H >(plus_minus_m_m i e) in ⊢ (? ? ? ? %); /2 width=2/ /3 width=2/ qed. (* Basic_1: was: lift_r *) lemma lift_refl: ∀T,d. ↑[d, 0] T ≡ T. #T elim T -T -[ * #i // #d elim (lt_or_ge i d) /2/ -| * /2/ +[ * #i // #d elim (lt_or_ge i d) /2 width=1/ +| * /2 width=1/ ] qed. lemma lift_total: ∀T1,d,e. ∃T2. ↑[d,e] T1 ≡ T2. #T1 elim T1 -T1 -[ * #i /2/ #d #e elim (lt_or_ge i d) /3/ +[ * #i /2 width=2/ #d #e elim (lt_or_ge i d) /3 width=2/ | * #I #V1 #T1 #IHV1 #IHT1 #d #e elim (IHV1 d e) -IHV1 #V2 #HV12 - [ elim (IHT1 (d+1) e) -IHT1 /3/ - | elim (IHT1 d e) -IHT1 /3/ + [ elim (IHT1 (d+1) e) -IHT1 /3 width=2/ + | elim (IHT1 d e) -IHT1 /3 width=2/ ] ] qed. @@ -298,20 +298,20 @@ qed. lemma lift_split: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 → ∀d2,e1. d1 ≤ d2 → d2 ≤ d1 + e1 → e1 ≤ e2 → ∃∃T. ↑[d1, e1] T1 ≡ T & ↑[d2, e2 - e1] T ≡ T2. -#d1 #e2 #T1 #T2 #H elim H -H d1 e2 T1 T2 -[ /3/ +#d1 #e2 #T1 #T2 #H elim H -d1 -e2 -T1 -T2 +[ /3 width=3/ | #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_ - lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4/ + lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4 width=3/ | #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12 - lapply (transitive_le …(i+e1) Hd21 ?) /2/ -Hd21 #Hd21 - <(arith_d1 i e2 e1) // /3/ -| /3/ + lapply (transitive_le …(i+e1) Hd21 ?) /2 width=1/ -Hd21 #Hd21 + <(arith_d1 i e2 e1) // /3 width=3/ +| /3 width=3/ | #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b - elim (IHT (d2+1) … ? ? He12) /3 width=5/ + elim (IHT (d2+1) … ? ? He12) /2 width=1/ /3 width=5/ | #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b - elim (IHT d2 … ? ? He12) /3 width=5/ + elim (IHT d2 … ? ? He12) // /3 width=5/ ] qed. @@ -324,14 +324,14 @@ lemma is_lift_dec: ∀T2,d,e. Decidable (∃T1. ↑[d,e] T1 ≡ T2). | lapply (false_lt_to_le … Hid) -Hid #Hid elim (lt_dec i (d + e)) #Hide [ @or_intror * #T1 #H - elim (lift_inv_lref2_be … H Hid Hide) + elim (lift_inv_lref2_be … H Hid Hide) | lapply (false_lt_to_le … Hide) -Hide /4 width=2/ ] ] | * #I #V2 #T2 #IHV2 #IHT2 #d #e [ elim (IHV2 d e) -IHV2 [ * #V1 #HV12 elim (IHT2 (d+1) e) -IHT2 - [ * #T1 #HT12 @or_introl /3/ + [ * #T1 #HT12 @or_introl /3 width=2/ | -V1 #HT2 @or_intror * #X #H elim (lift_inv_bind2 … H) -H /3 width=2/ ] diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma index 5bc36f943..2f92251bd 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma @@ -20,19 +20,19 @@ include "Basic_2/substitution/lift.ma". (* Basic_1: was: lift_inj *) theorem lift_inj: ∀d,e,T1,U. ↑[d,e] T1 ≡ U → ∀T2. ↑[d,e] T2 ≡ U → T1 = T2. -#d #e #T1 #U #H elim H -H d e T1 U +#d #e #T1 #U #H elim H -d -e -T1 -U [ #k #d #e #X #HX lapply (lift_inv_sort2 … HX) -HX // -| #i #d #e #Hid #X #HX +| #i #d #e #Hid #X #HX lapply (lift_inv_lref2_lt … HX ?) -HX // -| #i #d #e #Hdi #X #HX - lapply (lift_inv_lref2_ge … HX ?) -HX /2/ +| #i #d #e #Hdi #X #HX + lapply (lift_inv_lref2_ge … HX ?) -HX // /2 width=1/ | #p #d #e #X #HX lapply (lift_inv_gref2 … HX) -HX // | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX - elim (lift_inv_bind2 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/ + elim (lift_inv_bind2 … HX) -HX #V #T #HV1 #HT1 #HX destruct /3 width=1/ | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX - elim (lift_inv_flat2 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/ + elim (lift_inv_flat2 … HX) -HX #V #T #HV1 #HT1 #HX destruct /3 width=1/ ] qed-. @@ -41,36 +41,36 @@ theorem lift_div_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → ∀d2,e2,T2. ↑[d2 + e1, e2] T2 ≡ T → d1 ≤ d2 → ∃∃T0. ↑[d1, e1] T0 ≡ T2 & ↑[d2, e2] T0 ≡ T1. -#d1 #e1 #T1 #T #H elim H -H d1 e1 T1 T +#d1 #e1 #T1 #T #H elim H -d1 -e1 -T1 -T [ #k #d1 #e1 #d2 #e2 #T2 #Hk #Hd12 - lapply (lift_inv_sort2 … Hk) -Hk #Hk destruct -T2 /3/ + lapply (lift_inv_sort2 … Hk) -Hk #Hk destruct /3 width=3/ | #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12 lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 - lapply (lift_inv_lref2_lt … Hi ?) -Hi /2/ /3/ + lapply (lift_inv_lref2_lt … Hi ?) -Hi /2 width=3/ /3 width=3/ | #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12 - elim (lift_inv_lref2 … Hi) -Hi * #Hid2 #H destruct -T2 - [ -Hd12; lapply (lt_plus_to_lt_l … Hid2) -Hid2 #Hid2 /3/ - | -Hid1; lapply (arith1 … Hid2) -Hid2 #Hid2 + elim (lift_inv_lref2 … Hi) -Hi * #Hid2 #H destruct + [ -Hd12 lapply (lt_plus_to_lt_l … Hid2) -Hid2 #Hid2 /3 width=3/ + | -Hid1 lapply (arith1 … Hid2) -Hid2 #Hid2 @(ex2_1_intro … #(i - e2)) - [ >le_plus_minus_comm [ @lift_lref_ge @(transitive_le … Hd12) -Hd12 /2/ | -Hd12 /2/ ] - | -Hd12 >(plus_minus_m_m i e2) in ⊢ (? ? ? ? %) /2/ /3/ + [ >le_plus_minus_comm [ @lift_lref_ge @(transitive_le … Hd12) -Hd12 /2 width=1/ | -Hd12 /2 width=2/ ] + | -Hd12 >(plus_minus_m_m i e2) in ⊢ (? ? ? ? %); /2 width=2/ /3 width=1/ ] ] | #p #d1 #e1 #d2 #e2 #T2 #Hk #Hd12 - lapply (lift_inv_gref2 … Hk) -Hk #Hk destruct -T2 /3/ + lapply (lift_inv_gref2 … Hk) -Hk #Hk destruct /3 width=3/ | #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12 - lapply (lift_inv_bind2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct -T2; - elim (IHW … HW2 ?) // -IHW HW2 #W0 #HW2 #HW1 - >plus_plus_comm_23 in HU2 #HU2 elim (IHU … HU2 ?) /2/ /3 width = 5/ + lapply (lift_inv_bind2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct + elim (IHW … HW2 ?) // -IHW -HW2 #W0 #HW2 #HW1 + >plus_plus_comm_23 in HU2; #HU2 elim (IHU … HU2 ?) /2 width=1/ /3 width=5/ | #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12 - lapply (lift_inv_flat2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct -T2; - elim (IHW … HW2 ?) // -IHW HW2 #W0 #HW2 #HW1 - elim (IHU … HU2 ?) // /3 width = 5/ + lapply (lift_inv_flat2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct + elim (IHW … HW2 ?) // -IHW -HW2 #W0 #HW2 #HW1 + elim (IHU … HU2 ?) // /3 width=5/ ] qed. theorem lift_mono: ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 → U1 = U2. -#d #e #T #U1 #H elim H -H d e T U1 +#d #e #T #U1 #H elim H -d -e -T -U1 [ #k #d #e #X #HX lapply (lift_inv_sort1 … HX) -HX // | #i #d #e #Hid #X #HX @@ -80,9 +80,9 @@ theorem lift_mono: ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 | #p #d #e #X #HX lapply (lift_inv_gref1 … HX) -HX // | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX - elim (lift_inv_bind1 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/ + elim (lift_inv_bind1 … HX) -HX #V #T #HV1 #HT1 #HX destruct /3 width=1/ | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX - elim (lift_inv_flat1 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/ + elim (lift_inv_flat1 … HX) -HX #V #T #HV1 #HT1 #HX destruct /3 width=1/ ] qed-. @@ -90,27 +90,27 @@ qed-. theorem lift_trans_be: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → d1 ≤ d2 → d2 ≤ d1 + e1 → ↑[d1, e1 + e2] T1 ≡ T2. -#d1 #e1 #T1 #T #H elim H -H d1 e1 T1 T +#d1 #e1 #T1 #T #H elim H -d1 -e1 -T1 -T [ #k #d1 #e1 #d2 #e2 #T2 #HT2 #_ #_ >(lift_inv_sort1 … HT2) -HT2 // | #i #d1 #e1 #Hid1 #d2 #e2 #T2 #HT2 #Hd12 #_ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 - lapply (lift_inv_lref1_lt … HT2 Hid2) /2/ + lapply (lift_inv_lref1_lt … HT2 Hid2) /2 width=1/ | #i #d1 #e1 #Hid1 #d2 #e2 #T2 #HT2 #_ #Hd21 lapply (lift_inv_lref1_ge … HT2 ?) -HT2 - [ @(transitive_le … Hd21 ?) -Hd21 /2/ - | -Hd21 /2/ + [ @(transitive_le … Hd21 ?) -Hd21 /2 width=1/ + | -Hd21 /2 width=1/ ] | #p #d1 #e1 #d2 #e2 #T2 #HT2 #_ #_ >(lift_inv_gref1 … HT2) -HT2 // | #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd12 #Hd21 - elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X; - lapply (IHV12 … HV20 ? ?) // -IHV12 HV20 #HV10 - lapply (IHT12 … HT20 ? ?) /2/ + elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct + lapply (IHV12 … HV20 ? ?) // -IHV12 -HV20 #HV10 + lapply (IHT12 … HT20 ? ?) /2 width=1/ | #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd12 #Hd21 - elim (lift_inv_flat1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X; - lapply (IHV12 … HV20 ? ?) // -IHV12 HV20 #HV10 - lapply (IHT12 … HT20 ? ?) // /2/ + elim (lift_inv_flat1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct + lapply (IHV12 … HV20 ? ?) // -IHV12 -HV20 #HV10 + lapply (IHT12 … HT20 ? ?) // /2 width=1/ ] qed. @@ -118,26 +118,26 @@ qed. theorem lift_trans_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → d2 ≤ d1 → ∃∃T0. ↑[d2, e2] T1 ≡ T0 & ↑[d1 + e2, e1] T0 ≡ T2. -#d1 #e1 #T1 #T #H elim H -H d1 e1 T1 T +#d1 #e1 #T1 #T #H elim H -d1 -e1 -T1 -T [ #k #d1 #e1 #d2 #e2 #X #HX #_ - >(lift_inv_sort1 … HX) -HX /2/ + >(lift_inv_sort1 … HX) -HX /2 width=3/ | #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #_ lapply (lt_to_le_to_lt … (d1+e2) Hid1 ?) // #Hie2 - elim (lift_inv_lref1 … HX) -HX * #Hid2 #HX destruct -X /3/ /4/ + elim (lift_inv_lref1 … HX) -HX * #Hid2 #HX destruct /3 width=3/ /4 width=3/ | #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #Hd21 lapply (transitive_le … Hd21 Hid1) -Hd21 #Hid2 - lapply (lift_inv_lref1_ge … HX ?) -HX /2/ #HX destruct -X; - >plus_plus_comm_23 /4/ + lapply (lift_inv_lref1_ge … HX ?) -HX /2 width=1/ #HX destruct + >plus_plus_comm_23 /4 width=3/ | #p #d1 #e1 #d2 #e2 #X #HX #_ - >(lift_inv_gref1 … HX) -HX /2/ + >(lift_inv_gref1 … HX) -HX /2 width=3/ | #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd21 - elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X; - elim (IHV12 … HV20 ?) -IHV12 HV20 // - elim (IHT12 … HT20 ?) -IHT12 HT20 /2/ /3 width=5/ + elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct + elim (IHV12 … HV20 ?) -IHV12 -HV20 // + elim (IHT12 … HT20 ?) -IHT12 -HT20 /2 width=1/ /3 width=5/ | #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd21 - elim (lift_inv_flat1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X; - elim (IHV12 … HV20 ?) -IHV12 HV20 // - elim (IHT12 … HT20 ?) -IHT12 HT20 // /3 width=5/ + elim (lift_inv_flat1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct + elim (IHV12 … HV20 ?) -IHV12 -HV20 // + elim (IHT12 … HT20 ?) -IHT12 -HT20 // /3 width=5/ ] qed. @@ -145,27 +145,27 @@ qed. theorem lift_trans_ge: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → d1 + e1 ≤ d2 → ∃∃T0. ↑[d2 - e1, e2] T1 ≡ T0 & ↑[d1, e1] T0 ≡ T2. -#d1 #e1 #T1 #T #H elim H -H d1 e1 T1 T +#d1 #e1 #T1 #T #H elim H -d1 -e1 -T1 -T [ #k #d1 #e1 #d2 #e2 #X #HX #_ - >(lift_inv_sort1 … HX) -HX /2/ + >(lift_inv_sort1 … HX) -HX /2 width=3/ | #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #Hded lapply (lt_to_le_to_lt … (d1+e1) Hid1 ?) // #Hid1e - lapply (lt_to_le_to_lt … (d2-e1) Hid1 ?) /2/ #Hid2e - lapply (lt_to_le_to_lt … Hid1e Hded) -Hid1e Hded #Hid2 - lapply (lift_inv_lref1_lt … HX ?) -HX // #HX destruct -X /3/ + lapply (lt_to_le_to_lt … (d2-e1) Hid1 ?) /2 width=1/ #Hid2e + lapply (lt_to_le_to_lt … Hid1e Hded) -Hid1e -Hded #Hid2 + lapply (lift_inv_lref1_lt … HX ?) -HX // #HX destruct /3 width=3/ | #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #_ - elim (lift_inv_lref1 … HX) -HX * #Hied #HX destruct -X; - [ /4/ | >plus_plus_comm_23 /4/ ] + elim (lift_inv_lref1 … HX) -HX * #Hied #HX destruct + [ /4 width=3/ | >plus_plus_comm_23 /4 width=3/ ] | #p #d1 #e1 #d2 #e2 #X #HX #_ - >(lift_inv_gref1 … HX) -HX /2/ + >(lift_inv_gref1 … HX) -HX /2 width=3/ | #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hded - elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X; - elim (IHV12 … HV20 ?) -IHV12 HV20 // - elim (IHT12 … HT20 ?) -IHT12 HT20 /2/ #T - (plus_minus_m_m e 1) /2/ +>(plus_minus_m_m e 1) /2 width=1/ qed. lemma ltps_tps1_lt: ∀L1,L2,I,V1,V2,d,e. L1 [d - 1, e] ≫ L2 → L2 ⊢ V1 [d - 1, e] ≫ V2 → 0 < d → L1. 𝕓{I} V1 [d, e] ≫ L2. 𝕓{I} V2. #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd ->(plus_minus_m_m d 1) /2/ +>(plus_minus_m_m d 1) /2 width=1/ qed. (* Basic_1: was by definition: csubst1_refl *) lemma ltps_refl: ∀L,d,e. L [d, e] ≫ L. #L elim L -L // -#L #I #V #IHL * /2/ * /2/ +#L #I #V #IHL * /2 width=1/ * /2 width=1/ qed. (* Basic inversion lemmas ***************************************************) fact ltps_inv_refl_O2_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → e = 0 → L1 = L2. -#d #e #L1 #L2 #H elim H -H d e L1 L2 // +#d #e #L1 #L2 #H elim H -d -e -L1 -L2 // [ #L1 #L2 #I #V1 #V2 #e #_ #_ #_ #H elim (plus_S_eq_O_false … H) -| #L1 #L2 #I #V1 #V2 #d #e #_ #HV12 #IHL12 #He destruct -e +| #L1 #L2 #I #V1 #V2 #d #e #_ #HV12 #IHL12 #He destruct >(IHL12 ?) -IHL12 // >(tps_inv_refl_O2 … HV12) // ] qed. lemma ltps_inv_refl_O2: ∀d,L1,L2. L1 [d, 0] ≫ L2 → L1 = L2. -/2/ qed-. +/2 width=4/ qed-. fact ltps_inv_atom1_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → L1 = ⋆ → L2 = ⋆. -#d #e #L1 #L2 * -d e L1 L2 +#d #e #L1 #L2 * -d -e -L1 -L2 [ // | #L #I #V #H destruct | #L1 #L2 #I #V1 #V2 #e #_ #_ #H destruct @@ -85,10 +85,10 @@ fact ltps_inv_tps21_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → d = 0 → 0 < e → ∃∃K2,V2. K1 [0, e - 1] ≫ K2 & K2 ⊢ V1 [0, e - 1] ≫ V2 & L2 = K2. 𝕓{I} V2. -#d #e #L1 #L2 * -d e L1 L2 +#d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #_ #K1 #I #V1 #H destruct | #L1 #I #V #_ #H elim (lt_refl_false … H) -| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K1 #J #W1 #H destruct -L1 I V1 /2 width=5/ +| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K1 #J #W1 #H destruct /2 width=5/ | #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false … H) ] qed. @@ -103,12 +103,11 @@ fact ltps_inv_tps11_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → 0 < d → ∃∃K2,V2. K1 [d - 1, e] ≫ K2 & K2 ⊢ V1 [d - 1, e] ≫ V2 & L2 = K2. 𝕓{I} V2. -#d #e #L1 #L2 * -d e L1 L2 +#d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #I #K1 #V1 #H destruct | #L #I #V #H elim (lt_refl_false … H) | #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false … H) -| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K1 #W1 #H destruct -L1 I V1 - /2 width=5/ +| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K1 #W1 #H destruct /2 width=5/ ] qed. @@ -116,11 +115,11 @@ lemma ltps_inv_tps11: ∀d,e,I,K1,V1,L2. K1. 𝕓{I} V1 [d, e] ≫ L2 → 0 < d ∃∃K2,V2. K1 [d - 1, e] ≫ K2 & K2 ⊢ V1 [d - 1, e] ≫ V2 & L2 = K2. 𝕓{I} V2. -/2/ qed-. +/2 width=3/ qed-. fact ltps_inv_atom2_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → L2 = ⋆ → L1 = ⋆. -#d #e #L1 #L2 * -d e L1 L2 +#d #e #L1 #L2 * -d -e -L1 -L2 [ // | #L #I #V #H destruct | #L1 #L2 #I #V1 #V2 #e #_ #_ #H destruct @@ -136,10 +135,10 @@ fact ltps_inv_tps22_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → d = 0 → 0 < e → ∃∃K1,V1. K1 [0, e - 1] ≫ K2 & K2 ⊢ V1 [0, e - 1] ≫ V2 & L1 = K1. 𝕓{I} V1. -#d #e #L1 #L2 * -d e L1 L2 +#d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #_ #K1 #I #V1 #H destruct | #L1 #I #V #_ #H elim (lt_refl_false … H) -| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K2 #J #W2 #H destruct -L2 I V2 /2 width=5/ +| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K2 #J #W2 #H destruct /2 width=5/ | #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false … H) ] qed. @@ -154,12 +153,11 @@ fact ltps_inv_tps12_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → 0 < d → ∃∃K1,V1. K1 [d - 1, e] ≫ K2 & K2 ⊢ V1 [d - 1, e] ≫ V2 & L1 = K1. 𝕓{I} V1. -#d #e #L1 #L2 * -d e L1 L2 +#d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #I #K2 #V2 #H destruct | #L #I #V #H elim (lt_refl_false … H) | #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false … H) -| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K2 #W2 #H destruct -L2 I V2 - /2 width=5/ +| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K2 #W2 #H destruct /2 width=5/ ] qed. @@ -167,7 +165,7 @@ lemma ltps_inv_tps12: ∀L1,K2,I,V2,d,e. L1 [d, e] ≫ K2. 𝕓{I} V2 → 0 < d ∃∃K1,V1. K1 [d - 1, e] ≫ K2 & K2 ⊢ V1 [d - 1, e] ≫ V2 & L1 = K1. 𝕓{I} V1. -/2/ qed-. +/2 width=3/ qed-. (* Basic_1: removed theorems 27: csubst0_clear_O csubst0_ldrop_lt csubst0_ldrop_gt csubst0_ldrop_eq diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma index 5482e2407..7996f53a6 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma @@ -19,95 +19,95 @@ include "Basic_2/substitution/ltps.ma". lemma ltps_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2. -#L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1 +#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H // | // | normalize #K0 #K1 #I #V0 #V1 #e1 #_ #_ #IHK01 #L2 #e2 #H #He12 lapply (plus_le_weak … He12) #He2 lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2 - lapply (IHK01 … HK0L2 ?) -IHK01 HK0L2 /2/ + lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/ | #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 lapply (plus_le_weak … Hd1e2) #He2 lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2 - lapply (IHK01 … HK0L2 ?) -IHK01 HK0L2 /2/ + lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/ ] qed. lemma ltps_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 → ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2. -#L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1 +#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H // | // | normalize #K1 #K0 #I #V1 #V0 #e1 #_ #_ #IHK10 #L2 #e2 #H #He12 lapply (plus_le_weak … He12) #He2 lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2 - lapply (IHK10 … HK0L2 ?) -IHK10 HK0L2 /2/ + lapply (IHK10 … HK0L2 ?) -K0 /2 width=1/ | #K0 #K1 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 lapply (plus_le_weak … Hd1e2) #He2 lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2 - lapply (IHK10 … HK0L2 ?) -IHK10 HK0L2 /2/ + lapply (IHK10 … HK0L2 ?) -IHK10 -HK0L2 /2 width=1/ ] qed. lemma ltps_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → ∃∃L. L2 [0, d1 + e1 - e2] ≫ L & ↓[0, e2] L1 ≡ L. -#L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1 -[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2/ +#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1 +[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/ | normalize #L #I #V #L2 #e2 #HL2 #_ #He2 - lapply (le_n_O_to_eq … He2) -He2 #H destruct -e2; - lapply (ldrop_inv_refl … HL2) -HL2 #H destruct -L2 /2/ + lapply (le_n_O_to_eq … He2) -He2 #H destruct + lapply (ldrop_inv_refl … HL2) -HL2 #H destruct /2 width=3/ | normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #_ #He21 lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2 - [ destruct -IHK01 He21 e2 L2 plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 #He2de1 lapply (plus_le_weak … Hd1e2) #He2 (ldrop_inv_atom1 … H) -H /2/ +#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1 +[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/ | normalize #L #I #V #L2 #e2 #HL2 #_ #He2 - lapply (le_n_O_to_eq … He2) -He2 #H destruct -e2; - lapply (ldrop_inv_refl … HL2) -HL2 #H destruct -L2 /2/ + lapply (le_n_O_to_eq … He2) -He2 #H destruct + lapply (ldrop_inv_refl … HL2) -HL2 #H destruct /2 width=3/ | normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #_ #He21 lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2 - [ destruct -IHK10 He21 e2 L2 plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 #He2de1 lapply (plus_le_weak … Hd1e2) #He2 (ldrop_inv_atom1 … H) -H /2/ -| /2/ +#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1 +[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/ +| /2 width=3/ | normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #_ #L2 #e2 #H #He2 - lapply (le_n_O_to_eq … He2) -He2 #He2 destruct -e2; - lapply (ldrop_inv_refl … H) -H #H destruct -L2 /3/ + lapply (le_n_O_to_eq … He2) -He2 #He2 destruct + lapply (ldrop_inv_refl … H) -H #H destruct /3 width=3/ | #K0 #K1 #I #V0 #V1 #d1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #He2d1 lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2 - [ destruct -IHK01 He2d1 e2 L2 (ldrop_inv_atom1 … H) -H /2/ -| /2/ +#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1 +[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/ +| /2 width=3/ | normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #_ #L2 #e2 #H #He2 - lapply (le_n_O_to_eq … He2) -He2 #He2 destruct -e2; - lapply (ldrop_inv_refl … H) -H #H destruct -L2 /3/ + lapply (le_n_O_to_eq … He2) -He2 #He2 destruct + lapply (ldrop_inv_refl … H) -H #H destruct /3 width=3/ | #K1 #K0 #I #V1 #V0 #d1 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #He2d1 lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2 - [ destruct -IHK10 He2d1 e2 L2 arith_a2 /3/ + lapply (tps_lift_ge … HV01 … H HVW0 HVW1 ?) -V0 -H // >arith_a2 // /3 width=4/ | elim (lt_or_ge i2 (d1 + e1)) #Hde1i2 - [ elim (ltps_ldrop_conf_be … HL01 … HLK0 ? ?) -HL01 HLK0 [2,3: /2/ ] #X #H #HLK1 - elim (ltps_inv_tps21 … H ?) -H [2: /2/ ] #K1 #V1 #_ #HV01 #H destruct -X; + [ elim (ltps_ldrop_conf_be … HL01 … HLK0 ? ?) -L0 /2 width=1/ #X #H #HLK1 + elim (ltps_inv_tps21 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct lapply (ldrop_fwd_ldrop2 … HLK1) #H elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1 - lapply (tps_lift_ge … HV01 … H HVW0 HVW1 ?) -H HV01 HVW0 // normalize #HW01 - lapply (tps_weak … HW01 d1 e1 ? ?) [2,3: /3/ ] >arith_i2 // - | lapply (ltps_ldrop_conf_ge … HL01 … HLK0 ?) -HL01 HLK0 /3/ + lapply (tps_lift_ge … HV01 … H HVW0 HVW1 ?) -V0 -H // normalize #HW01 + lapply (tps_weak … HW01 d1 e1 ? ?) [2: /2 width=1/ |3: /3 width=4/ ] >arith_i2 // + | lapply (ltps_ldrop_conf_ge … HL01 … HLK0 ?) -L0 // /3 width=4/ ] ] | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 elim (IHVW2 … HL01) -IHVW2 #V #HV2 #HVW2 - elim (IHTU2 (L1. 𝕓{I} V) (d1 + 1) e1 ?) -IHTU2 [2: /2/ ] -HL01 /3 width=5/ + elim (IHTU2 (L1. 𝕓{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL01 /3 width=5/ | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 - elim (IHVW2 … HL01) -IHVW2; - elim (IHTU2 … HL01) -IHTU2 HL01 /3 width=5/ + elim (IHVW2 … HL01) -IHVW2 + elim (IHTU2 … HL01) -IHTU2 -HL01 /3 width=5/ ] qed. lemma ltps_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 → ∀L1,d1,e1. L1 [d1, e1] ≫ L0 → d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ≫ U2. -#L0 #T2 #U2 #d2 #e2 #H elim H -H L0 T2 U2 d2 e2 +#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2 [ // | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 #Hde1d2 lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2 - lapply (ltps_ldrop_trans_ge … HL10 … HLK0 ?) -HL10 HLK0 /2/ + lapply (ltps_ldrop_trans_ge … HL10 … HLK0 ?) -L0 // /2 width=4/ | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 #Hde1d2 - @tps_bind [ /2/ | @IHTU2 [3: /2/ |1,2: skip | /2/ ] ] (**) (* /3/ is too slow *) -| /3/ + @tps_bind [ /2 width=4/ | @IHTU2 /2 width=4/ ] (**) (* explicit constructor *) +| /3 width=4/ ] qed. @@ -83,30 +83,30 @@ lemma ltps_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 → ∀L1,d1,e1. L1 [d1, e1] ≫ L0 → ∃∃T. L1 ⊢ T2 [d2, e2] ≫ T & L0 ⊢ T [d1, e1] ≫ U2. -#L0 #T2 #U2 #d2 #e2 #H elim H -H L0 T2 U2 d2 e2 -[ /2/ +#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2 +[ /2 width=3/ | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 elim (lt_or_ge i2 d1) #Hi2d1 - [ elim (ltps_ldrop_trans_le … HL10 … HLK0 ?) -HL10 /2/ #X #H #HLK1 - elim (ltps_inv_tps12 … H ?) -H [2: /2/ ] #K1 #V1 #_ #HV01 #H destruct -X; + [ elim (ltps_ldrop_trans_le … HL10 … HLK0 ?) -HL10 /2 width=1/ #X #H #HLK1 + elim (ltps_inv_tps12 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #H elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1 - lapply (tps_lift_ge … HV01 … H HVW1 HVW0 ?) -H HV01 HVW0 // >arith_a2 /3/ + lapply (tps_lift_ge … HV01 … H HVW1 HVW0 ?) -V0 -H // >arith_a2 // /3 width=4/ | elim (lt_or_ge i2 (d1 + e1)) #Hde1i2 - [ elim (ltps_ldrop_trans_be … HL10 … HLK0 ? ?) -HL10 [2,3: /2/ ] #X #H #HLK1 - elim (ltps_inv_tps22 … H ?) -H [2: /2/ ] #K1 #V1 #_ #HV01 #H destruct -X; + [ elim (ltps_ldrop_trans_be … HL10 … HLK0 ? ?) -HL10 // /2 width=1/ #X #H #HLK1 + elim (ltps_inv_tps22 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #H elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1 - lapply (tps_lift_ge … HV01 … H HVW1 HVW0 ?) -H HV01 HVW0 // normalize #HW01 - lapply (tps_weak … HW01 d1 e1 ? ?) [2,3: /3/ ] >arith_i2 // - | lapply (ltps_ldrop_trans_ge … HL10 … HLK0 ?) -HL10 HLK0 /3/ + lapply (tps_lift_ge … HV01 … H HVW1 HVW0 ?) -V0 -H // normalize #HW01 + lapply (tps_weak … HW01 d1 e1 ? ?) [2: /3 width=1/ |3: /3 width=4/ ] >arith_i2 // + | lapply (ltps_ldrop_trans_ge … HL10 … HLK0 ?) -HL10 -HLK0 // /3 width=4/ ] ] | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 elim (IHVW2 … HL10) -IHVW2 #V #HV2 #HVW2 - elim (IHTU2 (L1. 𝕓{I} V) (d1 + 1) e1 ?) -IHTU2 [2: /2/ ] -HL10 /3 width=5/ + elim (IHTU2 (L1. 𝕓{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL10 /3 width=5/ | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 - elim (IHVW2 … HL10) -IHVW2; - elim (IHTU2 … HL10) -IHTU2 HL10 /3 width=5/ + elim (IHVW2 … HL10) -IHVW2 + elim (IHTU2 … HL10) -IHTU2 -HL10 /3 width=5/ ] qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma index 9f10dcc2a..762e2a9a0 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma @@ -36,33 +36,33 @@ interpretation "parallel substritution (term)" lemma tps_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫ T2 → ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ≫ T2. -#L1 #T1 #T2 #d #e #H elim H -H L1 T1 T2 d e +#L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e [ // | #L1 #K1 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12 - elim (ldrop_lsubs_ldrop1_abbr … HL12 … HLK1 ? ?) -HL12 HLK1 // /2/ -| /4/ -| /3/ + elim (ldrop_lsubs_ldrop1_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /2 width=4/ +| /4 width=1/ +| /3 width=1/ ] qed. lemma tps_refl: ∀T,L,d,e. L ⊢ T [d, e] ≫ T. #T elim T -T // -#I elim I -I /2/ +#I elim I -I /2 width=1/ qed. (* Basic_1: was: subst1_ex *) lemma tps_full: ∀K,V,T1,L,d. ↓[0, d] L ≡ (K. 𝕓{Abbr} V) → ∃∃T2,T. L ⊢ T1 [d, 1] ≫ T2 & ↑[d, 1] T ≡ T2. #K #V #T1 elim T1 -T1 -[ * #i #L #d #HLK /2/ - elim (lt_or_eq_or_gt i d) #Hid [ /3/ |3: /3/ ] - destruct -d; +[ * #i #L #d #HLK /2 width=4/ + elim (lt_or_eq_or_gt i d) #Hid /3 width=4/ + destruct elim (lift_total V 0 (i+1)) #W #HVW - elim (lift_split … HVW i i ? ? ?) // (plus_minus_m_m_comm j d) in ⊢ (% → ?) // -Hdj /3/ - | -Hdi Hdj; #Hid - generalize in match Hide -Hide (**) (* rewriting in the premises, rewrites in the goal too *) - >(plus_minus_m_m_comm … Hjde) in ⊢ (% → ?) -Hjde /4/ + [ -Hide -Hjde + >(plus_minus_m_m_comm j d) in ⊢ (% → ?); // -Hdj /3 width=4/ + | -Hdi -Hdj #Hid + generalize in match Hide; -Hide (**) (* rewriting in the premises, rewrites in the goal too *) + >(plus_minus_m_m_comm … Hjde) in ⊢ (% → ?); -Hjde /4 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: /2 by arith4/ |3: /2/ ] (* just /2/ is too slow *) - -Hdi Hide >arith_c1 >arith_c1x #T #HT1 #HT2 + elim (IHT12 (i + 1) ? ?) -IHT12 /2 width=1/ + -Hdi -Hide >arith_c1 >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/ + -Hdi -Hide /3 width=5/ ] qed. @@ -131,9 +131,9 @@ fact tps_inv_atom1_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → ∀I. T1 = ↓[O, i] L ≡ K. 𝕓{Abbr} V & ↑[O, i + 1] V ≡ T2 & I = LRef i. -#L #T1 #T2 #d #e * -L T1 T2 d e -[ #L #I #d #e #J #H destruct -I /2/ -| #L #K #V #T2 #i #d #e #Hdi #Hide #HLK #HVT2 #I #H destruct -I /3 width=8/ +#L #T1 #T2 #d #e * -L -T1 -T2 -d -e +[ #L #I #d #e #J #H destruct /2 width=1/ +| #L #K #V #T2 #i #d #e #Hdi #Hide #HLK #HVT2 #I #H destruct /3 width=8/ | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #J #H destruct | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #J #H destruct ] @@ -145,7 +145,7 @@ lemma tps_inv_atom1: ∀L,T2,I,d,e. L ⊢ 𝕒{I} [d, e] ≫ T2 → ↓[O, i] L ≡ K. 𝕓{Abbr} V & ↑[O, i + 1] V ≡ T2 & I = LRef i. -/2/ qed-. +/2 width=3/ qed-. (* Basic_1: was: subst1_gen_sort *) @@ -162,8 +162,8 @@ lemma tps_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ≫ T2 → ↓[O, i] L ≡ K. 𝕓{Abbr} V & ↑[O, i + 1] V ≡ T2. #L #T2 #i #d #e #H -elim (tps_inv_atom1 … H) -H /2/ -* #K #V #j #Hdj #Hjde #HLK #HVT2 #H destruct -i /3/ +elim (tps_inv_atom1 … H) -H /2 width=1/ +* #K #V #j #Hdj #Hjde #HLK #HVT2 #H destruct /3 width=4/ qed-. fact tps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 → @@ -171,7 +171,7 @@ fact tps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 → ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ≫ T2 & U2 = 𝕓{I} V2. T2. -#d #e #L #U1 #U2 * -d e L U1 U2 +#d #e #L #U1 #U2 * -d -e -L -U1 -U2 [ #L #k #d #e #I #V1 #T1 #H destruct | #L #K #V #W #i #d #e #_ #_ #_ #_ #I #V1 #T1 #H destruct | #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #I #V #T #H destruct /2 width=5/ @@ -183,13 +183,13 @@ lemma tps_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ≫ U2 → ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ≫ T2 & U2 = 𝕓{I} V2. T2. -/2/ qed-. +/2 width=3/ qed-. fact tps_inv_flat1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 → ∀I,V1,T1. U1 = 𝕗{I} V1. T1 → ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & L ⊢ T1 [d, e] ≫ T2 & U2 = 𝕗{I} V2. T2. -#d #e #L #U1 #U2 * -d e L U1 U2 +#d #e #L #U1 #U2 * -d -e -L -U1 -U2 [ #L #k #d #e #I #V1 #T1 #H destruct | #L #K #V #W #i #d #e #_ #_ #_ #_ #I #V1 #T1 #H destruct | #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #I #V #T #H destruct @@ -200,16 +200,16 @@ qed. lemma tps_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕗{I} V1. T1 [d, e] ≫ U2 → ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & L ⊢ T1 [d, e] ≫ T2 & U2 = 𝕗{I} V2. T2. -/2/ qed-. +/2 width=3/ qed-. fact tps_inv_refl_O2_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → e = 0 → T1 = T2. -#L #T1 #T2 #d #e #H elim H -H L T1 T2 d e +#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e [ // -| #L #K #V #W #i #d #e #Hdi #Hide #_ #_ #H destruct -e; - lapply (le_to_lt_to_lt … Hdi … Hide) -Hdi Hide (le_to_le_to_eq … Hdi ?) /2/ -d #K #V #HLK +| #L #K0 #V0 #W #i #d #e #Hdi #Hide #HLK0 #_ #H destruct + >(le_to_le_to_eq … Hdi ?) /2 width=1/ -d #K #V #HLK lapply (ldrop_mono … HLK0 … HLK) #H destruct | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #H1 #K #V #HLK - >(IHV12 H1 … HLK) -IHV12 >(IHT12 H1 K V) -IHT12 // /2/ + >(IHV12 H1 … HLK) -IHV12 >(IHT12 H1 K V) -IHT12 // /2 width=1/ | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #H1 #K #V #HLK >(IHV12 H1 … HLK) -IHV12 >(IHT12 H1 … HLK) -IHT12 // ] @@ -45,24 +45,23 @@ lemma tps_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 → ↑[d, e] T1 ≡ U1 → ↑[d, e] T2 ≡ U2 → dt + et ≤ d → L ⊢ U1 [dt, et] ≫ U2. -#K #T1 #T2 #dt #et #H elim H -H K T1 T2 dt et +#K #T1 #T2 #dt #et #H elim H -K -T1 -T2 -dt -et [ #K #I #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_ - >(lift_mono … H1 … H2) -H1 H2 // + >(lift_mono … H1 … H2) -H1 -H2 // | #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #d #e #HLK #H #HWU2 #Hdetd lapply (lt_to_le_to_lt … Hidet … Hdetd) -Hdetd #Hid - lapply (lift_inv_lref1_lt … H … Hid) -H #H destruct -U1; - elim (lift_trans_ge … HVW … HWU2 ?) -HVW HWU2 W // (lift_mono … HVY … HVW) -HVY HVW Y #H destruct -X /2/ + lapply (lift_inv_lref1_lt … H … Hid) -H #H destruct + elim (lift_trans_ge … HVW … HWU2 ?) -W // (lift_mono … HVY … HVW) -Y -HVW #H destruct /2 width=4/ | #K #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 - elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct -U1 U2; - @tps_bind [ /2 width=6/ | @IHT12 [4,5: // |1,2: skip | /2/ | /2/ ] ] (**) (* /3 width=6/ is too slow, arith3 needed to avoid crash *) + elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct + @tps_bind [ /2 width=6/ | @IHT12 /2 width=6/ ] (**) (* /3 width=6/ is too slow, arith3 needed to avoid crash *) | #K #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 - elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct -U1 U2; - /3 width=6/ + elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6/ ] qed. @@ -71,30 +70,30 @@ lemma tps_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 → ↑[d, e] T1 ≡ U1 → ↑[d, e] T2 ≡ U2 → dt ≤ d → d ≤ dt + et → L ⊢ U1 [dt, et + e] ≫ U2. -#K #T1 #T2 #dt #et #H elim H -H K T1 T2 dt et +#K #T1 #T2 #dt #et #H elim H -K -T1 -T2 -dt -et [ #K #I #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_ #_ - >(lift_mono … H1 … H2) -H1 H2 // + >(lift_mono … H1 … H2) -H1 -H2 // | #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #d #e #HLK #H #HWU2 #Hdtd #_ - elim (lift_inv_lref1 … H) -H * #Hid #H destruct -U1; - [ -Hdtd; + elim (lift_inv_lref1 … H) -H * #Hid #H destruct + [ -Hdtd lapply (lt_to_le_to_lt … (dt+et+e) Hidet ?) // -Hidet #Hidete elim (lift_trans_ge … HVW … HWU2 ?) -W // (lift_mono … HVY … HVW) -V #H destruct -X /2/ - | -Hdti; + elim (ldrop_trans_le … HLK … HKV ?) -K /2 width=1/ #X #HLK #H + elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K #Y #_ #HVY + >(lift_mono … HVY … HVW) -V #H destruct /2 width=4/ + | -Hdti lapply (transitive_le … Hdtd Hid) -Hdtd #Hdti - lapply (lift_trans_be … HVW … HWU2 ? ?) -W // [ /2/ ] >plus_plus_comm_23 #HVU2 - lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid /3/ + lapply (lift_trans_be … HVW … HWU2 ? ?) -W // /2 width=1/ >plus_plus_comm_23 #HVU2 + lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid /3 width=4/ ] | #K #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdtd #Hddet elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 - elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct -U1 U2; - @tps_bind [ /2 width=6/ | @IHT12 [3,4: // | skip |5,6: /2/ | /2/ ] ] (**) (* /3 width=6/ is too slow, arith3 needed to avoid crash *) + elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct + @tps_bind [ /2 width=6/ | @IHT12 [3,4: // | skip |5,6: /2 width=1/ | /2 width=1/ ] + ] (**) (* /3 width=6/ is too slow, arith3 needed to avoid crash, simplification like tps_lift_le is too slow *) | #K #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 - elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct -U1 U2; - /3 width=6/ + elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6/ ] qed. @@ -104,22 +103,21 @@ lemma tps_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 → ↑[d, e] T1 ≡ U1 → ↑[d, e] T2 ≡ U2 → d ≤ dt → L ⊢ U1 [dt + e, et] ≫ U2. -#K #T1 #T2 #dt #et #H elim H -H K T1 T2 dt et +#K #T1 #T2 #dt #et #H elim H -K -T1 -T2 -dt -et [ #K #I #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_ - >(lift_mono … H1 … H2) -H1 H2 // + >(lift_mono … H1 … H2) -H1 -H2 // | #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #d #e #HLK #H #HWU2 #Hddt lapply (transitive_le … Hddt … Hdti) -Hddt #Hid - lapply (lift_inv_lref1_ge … H … Hid) -H #H destruct -U1; - lapply (lift_trans_be … HVW … HWU2 ? ?) -HVW HWU2 W // [ /2/ ] >plus_plus_comm_23 #HVU2 - lapply (ldrop_trans_ge_comm … HLK … HKV ?) -HLK HKV K // -Hid /3/ + lapply (lift_inv_lref1_ge … H … Hid) -H #H destruct + lapply (lift_trans_be … HVW … HWU2 ? ?) -W // /2 width=1/ >plus_plus_comm_23 #HVU2 + lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid /3 width=4/ | #K #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hddt elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 - elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct -U1 U2; + elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct @tps_bind [ /2 width=5/ | /3 width=5/ ] (**) (* explicit constructor *) | #K #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hddt elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 - elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct -U1 U2; - /3 width=5/ + elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=5/ ] qed. @@ -128,26 +126,26 @@ lemma tps_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 → dt + et ≤ d → ∃∃T2. K ⊢ T1 [dt, et] ≫ T2 & ↑[d, e] T2 ≡ U2. -#L #U1 #U2 #dt #et #H elim H -H L U1 U2 dt et +#L #U1 #U2 #dt #et #H elim H -L -U1 -U2 -dt -et [ #L * #i #dt #et #K #d #e #_ #T1 #H #_ - [ lapply (lift_inv_sort2 … H) -H #H destruct -T1 /2/ - | elim (lift_inv_lref2 … H) -H * #Hid #H destruct -T1 /3/ - | lapply (lift_inv_gref2 … H) -H #H destruct -T1 /2/ + [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/ + | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3/ + | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3/ ] | #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdetd lapply (lt_to_le_to_lt … Hidet … Hdetd) -Hdetd #Hid - lapply (lift_inv_lref2_lt … H … Hid) -H #H destruct -T1; - elim (ldrop_conf_lt … HLK … HLKV ?) -HLK HLKV L // #L #U #HKL #_ #HUV - elim (lift_trans_le … HUV … HVW ?) -HUV HVW V // >arith_a2 // -Hid /3/ + lapply (lift_inv_lref2_lt … H … Hid) -H #H destruct + elim (ldrop_conf_lt … HLK … HLKV ?) -L // #L #U #HKL #_ #HUV + elim (lift_trans_le … HUV … HVW ?) -V // >arith_a2 // -Hid /3 width=4/ | #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd - elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct -X; - elim (IHV12 … HLK … HWV1 ?) -IHV12 HWV1 // #W2 #HW12 #HWV2 - elim (IHU12 … HTU1 ?) -IHU12 HTU1 [3: /2/ |4: @ldrop_skip // |2: skip ] -HLK Hdetd (**) (* /3 width=5/ is too slow *) + elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct + elim (IHV12 … HLK … HWV1 ?) -V1 // #W2 #HW12 #HWV2 + elim (IHU12 … HTU1 ?) -IHU12 -HTU1 [3: /2 width=1/ |4: @ldrop_skip // |2: skip ] -HLK -Hdetd (**) (* /3 width=5/ is too slow *) /3 width=5/ | #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd - elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct -X; - elim (IHV12 … HLK … HWV1 ?) -IHV12 HWV1 // - elim (IHU12 … HLK … HTU1 ?) -IHU12 HLK HTU1 // /3 width=5/ + elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct + elim (IHV12 … HLK … HWV1 ?) -V1 // + elim (IHU12 … HLK … HTU1 ?) -U1 -HLK // /3 width=5/ ] qed. @@ -155,34 +153,34 @@ lemma tps_inv_lift1_be: ∀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 + e ≤ dt + et → ∃∃T2. K ⊢ T1 [dt, et - e] ≫ T2 & ↑[d, e] T2 ≡ U2. -#L #U1 #U2 #dt #et #H elim H -H L U1 U2 dt et +#L #U1 #U2 #dt #et #H elim H -L -U1 -U2 -dt -et [ #L * #i #dt #et #K #d #e #_ #T1 #H #_ - [ lapply (lift_inv_sort2 … H) -H #H destruct -T1 /2/ - | elim (lift_inv_lref2 … H) -H * #Hid #H destruct -T1 /3/ - | lapply (lift_inv_gref2 … H) -H #H destruct -T1 /2/ + [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/ + | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3/ + | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3/ ] | #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdtd #Hdedet lapply (le_fwd_plus_plus_ge … Hdtd … Hdedet) #Heet - elim (lift_inv_lref2 … H) -H * #Hid #H destruct -T1 - [ -Hdtd Hidet; - lapply (lt_to_le_to_lt … (dt + (et - e)) Hid ?) [ arith_a2 // -Hid /3/ - | -Hdti Hdedet; - lapply (transitive_le … (i - e) Hdtd ?) [ /2/ ] -Hdtd #Hdtie + elim (lift_trans_le … HUV … HVW ?) -V // >arith_a2 // -Hid /3 width=4/ + | -Hdti -Hdedet + lapply (transitive_le … (i - e) Hdtd ?) /2 width=1/ -Hdtd #Hdtie lapply (plus_le_weak … Hid) #Hei lapply (ldrop_conf_ge … HLK … HLKV ?) -L // #HKV - elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW; [4: // |2,3: /2/ ] -Hid >arith_e2 // /4/ + elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |2,3: /2 width=1/ ] -Hid >arith_e2 // /4 width=4/ ] | #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet - elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct -X; - elim (IHV12 … HLK … HWV1 ? ?) -IHV12 HWV1 // #W2 #HW12 #HWV2 - elim (IHU12 … HTU1 ? ?) -IHU12 HTU1 [5: @ldrop_skip // |2: skip |3: >plus_plus_comm_23 >(plus_plus_comm_23 dt) /2/ ] + elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct + elim (IHV12 … HLK … HWV1 ? ?) -V1 // #W2 #HW12 #HWV2 + elim (IHU12 … HTU1 ? ?) -U1 [5: @ldrop_skip // |2: skip |3: >plus_plus_comm_23 >(plus_plus_comm_23 dt) /2 width=1/ |4: /2 width=1/ ] /3 width=5/ | #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet - elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct -X; - elim (IHV12 … HLK … HWV1 ? ?) -IHV12 HWV1 // - elim (IHU12 … HLK … HTU1 ? ?) -IHU12 HLK HTU1 // /3 width=5/ + elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct + elim (IHV12 … HLK … HWV1 ? ?) -V1 // + elim (IHU12 … HLK … HTU1 ? ?) -U1 -HLK // /3 width=5/ ] qed. @@ -191,59 +189,55 @@ lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 → d + e ≤ dt → ∃∃T2. K ⊢ T1 [dt - e, et] ≫ T2 & ↑[d, e] T2 ≡ U2. -#L #U1 #U2 #dt #et #H elim H -H L U1 U2 dt et +#L #U1 #U2 #dt #et #H elim H -L -U1 -U2 -dt -et [ #L * #i #dt #et #K #d #e #_ #T1 #H #_ - [ lapply (lift_inv_sort2 … H) -H #H destruct -T1 /2/ - | elim (lift_inv_lref2 … H) -H * #Hid #H destruct -T1 /3/ - | lapply (lift_inv_gref2 … H) -H #H destruct -T1 /2/ + [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/ + | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3/ + | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3/ ] -| #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdedt +| #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdedt lapply (transitive_le … Hdedt … Hdti) #Hdei lapply (plus_le_weak … Hdedt) -Hdedt #Hedt lapply (plus_le_weak … Hdei) #Hei - lapply (lift_inv_lref2_ge … H … Hdei) -H #H destruct -T1; - lapply (ldrop_conf_ge … HLK … HLKV ?) -HLK HLKV L // #HKV - elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW; [4: // | 2,3: normalize /2/ ] -Hdei >arith_e2 // #V0 #HV10 #HV02 - @ex2_1_intro - [2: @tps_subst [3: /2/ |5,6: // |1,2: skip |4: @arith5 // ] - |1: skip - | // - ] (**) (* explicitc constructors *) + lapply (lift_inv_lref2_ge … H … Hdei) -H #H destruct + lapply (ldrop_conf_ge … HLK … HLKV ?) -L // #HKV + elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |2,3: normalize /2 width=1/ ] -Hdei >arith_e2 // #V0 #HV10 #HV02 + @ex2_1_intro /3 width=4/ (**) (* explicitc constructors *) | #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd - elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct -X; + elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct lapply (plus_le_weak … Hdetd) #Hedt - elim (IHV12 … HLK … HWV1 ?) -IHV12 HWV1 // #W2 #HW12 #HWV2 - elim (IHU12 … HTU1 ?) -IHU12 HTU1 [4: @ldrop_skip // |2: skip |3: /2/ ] + elim (IHV12 … HLK … HWV1 ?) -V1 // #W2 #HW12 #HWV2 + elim (IHU12 … HTU1 ?) -U1 [4: @ldrop_skip // |2: skip |3: /2 width=1/ ] IHV12 // >IHT12 // | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX - elim (lift_inv_flat2 … HX) -HX #V #T #HV1 #HT1 #H destruct -X + elim (lift_inv_flat2 … HX) -HX #V #T #HV1 #HT1 #H destruct >IHV12 // >IHT12 // ] qed. (* - Theorem subst0_gen_lift_rev_ge: (t1,v,u2:?; i,h,d:?) + Theorem subst0_gen_lift_rev_ge: (t1,v,u2,i,h,d:?) (subst0 i v t1 (lift h d u2)) -> (le (plus d h) i) -> (EX u1 | (subst0 (minus i h) v u1 u2) & @@ -251,7 +245,7 @@ qed. ). - Theorem subst0_gen_lift_rev_lelt: (t1,v,u2:?; i,h,d:?) + Theorem subst0_gen_lift_rev_lelt: (t1,v,u2,i,h,d:?) (subst0 i v t1 (lift h d u2)) -> (le d i) -> (lt i (plus d h)) -> (EX u1 | t1 = (lift (minus (plus d h) (S i)) (S i) u1)). @@ -262,9 +256,9 @@ lemma tps_inv_lift1_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → ∃∃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 // (lift_mono … HVT1 … HVT2) -HVT1 HVT2 /2/ + [ #HX destruct /4 width=4/ + | -Hd1 -Hde1 * #K2 #V2 #_ #_ #HLK2 #HVT2 + lapply (ldrop_mono … HLK1 … HLK2) -HLK1 -HLK2 #H destruct + >(lift_mono … HVT1 … HVT2) -HVT1 -HVT2 /2 width=3/ ] | #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX - elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X; - lapply (tps_lsubs_conf … HT02 (L. 𝕓{I} V1) ?) -HT02 /2/ #HT02 - elim (IHV01 … HV02) -IHV01 HV02 #V #HV1 #HV2 - elim (IHT01 … HT02) -IHT01 HT02 #T #HT1 #HT2 - lapply (tps_lsubs_conf … HT1 (L. 𝕓{I} V) ?) -HT1 /2/ + elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct + lapply (tps_lsubs_conf … HT02 (L. 𝕓{I} V1) ?) -HT02 /2 width=1/ #HT02 + elim (IHV01 … HV02) -V0 #V #HV1 #HV2 + elim (IHT01 … HT02) -T0 #T #HT1 #HT2 + lapply (tps_lsubs_conf … HT1 (L. 𝕓{I} V) ?) -HT1 /2 width=1/ lapply (tps_lsubs_conf … HT2 (L. 𝕓{I} V) ?) -HT2 /3 width=5/ | #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX - elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X; - elim (IHV01 … HV02) -IHV01 HV02; - elim (IHT01 … HT02) -IHT01 HT02 /3 width=5/ + elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct + elim (IHV01 … HV02) -V0 + elim (IHT01 … HT02) -T0 /3 width=5/ ] qed. @@ -50,36 +50,36 @@ theorem tps_conf_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 [d1, e1] ≫ T1 → ∀L2,T2,d2,e2. L2 ⊢ T0 [d2, e2] ≫ T2 → (d1 + e1 ≤ d2 ∨ d2 + e2 ≤ d1) → ∃∃T. L2 ⊢ T1 [d2, e2] ≫ T & L1 ⊢ T2 [d1, e1] ≫ T. -#L1 #T0 #T1 #d1 #e1 #H elim H -H L1 T0 T1 d1 e1 -[ /2/ -| #L1 #K1 #V1 #T1 #i0 #d1 #e1 #Hd1 #Hde1 #HLK1 #HVT1 #L2 #T2 #d2 #e2 #H1 #H2 +#L1 #T0 #T1 #d1 #e1 #H elim H -L1 -T0 -T1 -d1 -e1 +[ /2 width=3/ +| #L1 #K1 #V1 #T1 #i0 #d1 #e1 #Hd1 #Hde1 #HLK1 #HVT1 #L2 #T2 #d2 #e2 #H1 #H2 elim (tps_inv_lref1 … H1) -H1 - [ #H destruct -T2 /4/ - | -HLK1 HVT1 * #K2 #V2 #Hd2 #Hde2 #_ #_ elim H2 -H2 #Hded - [ -Hd1 Hde2; - lapply (transitive_le … Hded Hd2) -Hded Hd2 #H - lapply (lt_to_le_to_lt … Hde1 H) -Hde1 H #H + [ #H destruct /4 width=4/ + | -HLK1 -HVT1 * #K2 #V2 #Hd2 #Hde2 #_ #_ elim H2 -H2 #Hded + [ -Hd1 -Hde2 + lapply (transitive_le … Hded Hd2) -Hded -Hd2 #H + lapply (lt_to_le_to_lt … Hde1 H) -Hde1 -H #H elim (lt_refl_false … H) - | -Hd2 Hde1; - lapply (transitive_le … Hded Hd1) -Hded Hd1 #H - lapply (lt_to_le_to_lt … Hde2 H) -Hde2 H #H + | -Hd2 -Hde1 + lapply (transitive_le … Hded Hd1) -Hded -Hd1 #H + lapply (lt_to_le_to_lt … Hde2 H) -Hde2 -H #H elim (lt_refl_false … H) ] ] | #L1 #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #L2 #X #d2 #e2 #HX #H - elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X; - elim (IHV01 … HV02 H) -IHV01 HV02 #V #HV1 #HV2 - elim (IHT01 … HT02 ?) -IHT01 HT02 + elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct + elim (IHV01 … HV02 H) -V0 #V #HV1 #HV2 + elim (IHT01 … HT02 ?) -T0 [ -H #T #HT1 #HT2 - lapply (tps_lsubs_conf … HT1 (L2. 𝕓{I} V) ?) -HT1 /2/ - lapply (tps_lsubs_conf … HT2 (L1. 𝕓{I} V) ?) -HT2 /3 width=5/ - | -HV1 HV2 >plus_plus_comm_23 >plus_plus_comm_23 in ⊢ (? ? %) elim H -H #H - [ @or_introl | @or_intror ] /2 by monotonic_le_plus_l/ (**) (* /3/ is too slow *) + lapply (tps_lsubs_conf … HT1 (L2. 𝕓{I} V) ?) -HT1 /2 width=1/ + lapply (tps_lsubs_conf … HT2 (L1. 𝕓{I} V) ?) -HT2 /2 width=1/ /3 width=5/ + | -HV1 -HV2 >plus_plus_comm_23 >plus_plus_comm_23 in ⊢ (? ? %); elim H -H #H + [ @or_introl | @or_intror ] /2 by monotonic_le_plus_l/ (**) (* /3 / is too slow *) ] | #L1 #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #L2 #X #d2 #e2 #HX #H - elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X; - elim (IHV01 … HV02 H) -IHV01 HV02; - elim (IHT01 … HT02 H) -IHT01 HT02 H /3 width=5/ + elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct + elim (IHV01 … HV02 H) -V0 + elim (IHT01 … HT02 H) -T0 -H /3 width=5/ ] qed. @@ -88,45 +88,45 @@ qed. theorem tps_trans_ge: ∀L,T1,T0,d,e. L ⊢ T1 [d, e] ≫ T0 → ∀T2. L ⊢ T0 [d, 1] ≫ T2 → 1 ≤ e → L ⊢ T1 [d, e] ≫ T2. -#L #T1 #T0 #d #e #H elim H -L T1 T0 d e +#L #T1 #T0 #d #e #H elim H -L -T1 -T0 -d -e [ #L #I #d #e #T2 #H #He elim (tps_inv_atom1 … H) -H - [ #H destruct -T2 // - | * #K #V #i #Hd2i #Hide2 #HLK #HVT2 #H destruct -I; - lapply (lt_to_le_to_lt … (d + e) Hide2 ?) /2/ + [ #H destruct // + | * #K #V #i #Hd2i #Hide2 #HLK #HVT2 #H destruct + lapply (lt_to_le_to_lt … (d + e) Hide2 ?) /2 width=4/ ] | #L #K #V #V2 #i #d #e #Hdi #Hide #HLK #HVW #T2 #HVT2 #He - lapply (tps_weak … HVT2 0 (i +1) ? ?) -HVT2 /2/ #HVT2 - <(tps_inv_lift1_eq … HVT2 … HVW) -HVT2 /2/ + lapply (tps_weak … HVT2 0 (i +1) ? ?) -HVT2 /2 width=1/ #HVT2 + <(tps_inv_lift1_eq … HVT2 … HVW) -HVT2 /2 width=4/ | #L #I #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He - elim (tps_inv_bind1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct -X; - lapply (tps_lsubs_conf … HT02 (L. 𝕓{I} V0) ?) -HT02 /2/ #HT02 - lapply (IHT10 … HT02 He) -IHT10 HT02 #HT12 - lapply (tps_lsubs_conf … HT12 (L. 𝕓{I} V2) ?) -HT12 /3/ + elim (tps_inv_bind1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct + lapply (tps_lsubs_conf … HT02 (L. 𝕓{I} V0) ?) -HT02 /2 width=1/ #HT02 + lapply (IHT10 … HT02 He) -T0 #HT12 + lapply (tps_lsubs_conf … HT12 (L. 𝕓{I} V2) ?) -HT12 /2 width=1/ /3 width=1/ | #L #I #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He - elim (tps_inv_flat1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct -X /3/ + elim (tps_inv_flat1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct /3 width=1/ ] qed. theorem tps_trans_down: ∀L,T1,T0,d1,e1. L ⊢ T1 [d1, e1] ≫ T0 → ∀T2,d2,e2. L ⊢ T0 [d2, e2] ≫ T2 → d2 + e2 ≤ d1 → ∃∃T. L ⊢ T1 [d2, e2] ≫ T & L ⊢ T [d1, e1] ≫ T2. -#L #T1 #T0 #d1 #e1 #H elim H -L T1 T0 d1 e1 -[ /2/ +#L #T1 #T0 #d1 #e1 #H elim H -L -T1 -T0 -d1 -e1 +[ /2 width=3/ | #L #K #V #W #i1 #d1 #e1 #Hdi1 #Hide1 #HLK #HVW #T2 #d2 #e2 #HWT2 #Hde2d1 lapply (transitive_le … Hde2d1 Hdi1) -Hde2d1 #Hde2i1 - lapply (tps_weak … HWT2 0 (i1 + 1) ? ?) -HWT2; normalize /2/ -Hde2i1 #HWT2 - <(tps_inv_lift1_eq … HWT2 … HVW) -HWT2 /4/ + lapply (tps_weak … HWT2 0 (i1 + 1) ? ?) -HWT2 normalize /2 width=1/ -Hde2i1 #HWT2 + <(tps_inv_lift1_eq … HWT2 … HVW) -HWT2 /4 width=4/ | #L #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1 - elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X; - lapply (tps_lsubs_conf … HT02 (L. 𝕓{I} V0) ?) -HT02 /2/ #HT02 - elim (IHV10 … HV02 ?) -IHV10 HV02 // #V - elim (IHT10 … HT02 ?) -IHT10 HT02 [2: /2/ ] #T #HT1 #HT2 - lapply (tps_lsubs_conf … HT1 (L. 𝕓{I} V) ?) -HT1; - lapply (tps_lsubs_conf … HT2 (L. 𝕓{I} V2) ?) -HT2 /3 width=6/ + elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct + lapply (tps_lsubs_conf … HT02 (L. 𝕓{I} V0) ?) -HT02 /2 width=1/ #HT02 + elim (IHV10 … HV02 ?) -IHV10 -HV02 // #V + elim (IHT10 … HT02 ?) -T0 /2 width=1/ #T #HT1 #HT2 + lapply (tps_lsubs_conf … HT1 (L. 𝕓{I} V) ?) -HT1 /2 width=1/ + lapply (tps_lsubs_conf … HT2 (L. 𝕓{I} V2) ?) -HT2 /2 width=1/ /3 width=6/ | #L #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1 - elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X; - elim (IHV10 … HV02 ?) -IHV10 HV02 // - elim (IHT10 … HT02 ?) -IHT10 HT02 // /3 width=6/ + elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct + elim (IHV10 … HV02 ?) -V0 // + elim (IHT10 … HT02 ?) -T0 // /3 width=6/ ] qed.