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 ≝
(* 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
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
∀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.
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-.
∃∃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.
∃∃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.
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 *********************************************************)
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 →
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;
- <minus_n_O <minus_plus_m_m /2/
- | -HL12;
- elim (IHL12 … HLK1 ? ?) -IHL12 HLK1 // [2: /2/ ] -Hie >arith_g1 // /3/
+ [ -IHL12 -Hie destruct
+ <minus_n_O <minus_plus_m_m // /2 width=3/
+ | -HL12
+ elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >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.
[ #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-.
[ #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-.
[ #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 //
]
]
(* 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 // <minus_plus_m_m #K2 #V2 #HLK2 #HVT2 #H destruct -X
- >(lift_inj … HVT1 … HVT2) -HVT1 HVT2
- >(IHLK1 … HLK2) -IHLK1 HLK2 //
+ elim (ldrop_inv_skip1 … H ?) -H // <minus_plus_m_m #K2 #V2 #HLK2 #HVT2 #H destruct
+ >(lift_inj … HVT1 … HVT2) -HVT1 -HVT2
+ >(IHLK1 … HLK2) -IHLK1 -HLK2 //
]
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_plus_comm /3/
+ lapply (ldrop_inv_ldrop1 … H ?) -H /2 width=2/ #HL2
+ <minus_plus_comm /3 width=1/
| #L #K #I #V1 #V2 #d #e #_ #_ #IHLK #e2 #L2 #H #Hdee2
lapply (transitive_le 1 … Hdee2) // #He2
lapply (ldrop_inv_ldrop1 … H ?) -H // -He2 #HL2
lapply (transitive_le (1 + e) … Hdee2) // #Hee2
- @ldrop_ldrop_lt >minus_minus_comm /3/ (**) (* explicit constructor *)
+ @ldrop_ldrop_lt >minus_minus_comm /3 width=1/ (**) (* explicit constructor *)
]
qed.
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
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 [ <minus_minus /3 width=5/ | /2/ ] (**) (* a bit slow *)
+ elim (IHL12 … HLK ?) -IHL12 -HLK [ <minus_minus /3 width=5/ | /2 width=1/ ] (**) (* a bit slow *)
]
]
qed.
theorem ldrop_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L →
∀e2,L2. ↓[0, e2] L ≡ L2 → e2 ≤ d1 →
∃∃L0. ↓[0, e2] L1 ≡ L0 & ↓[d1 - e2, e1] L0 ≡ 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 /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.
(* 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.
(* 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
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
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
∀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
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
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
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 <minus_plus_m_m /4/
+| #j #d #e #Hj #i #Hi destruct /3 width=1/
+| #j #d #e #Hj #i #Hi destruct <minus_plus_m_m /4 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
(* Basic_1: was: lift_gen_lref *)
lemma lift_inv_lref2: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i →
(i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)).
-/2/ qed-.
+/2 width=3/ qed-.
(* Basic_1: was: lift_gen_lref_lt *)
lemma lift_inv_lref2_lt: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → i < d → T1 = #i.
#d #e #T1 #i #H elim (lift_inv_lref2 … 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 (plus_lt_false … Hdd)
qed-.
d ≤ i → i < d + e → False.
#d #e #T1 #i #H elim (lift_inv_lref2 … H) -H *
[ #H1 #_ #H2 #_ | #H2 #_ #_ #H1 ]
-lapply (le_to_lt_to_lt … H2 H1) -H2 H1 #H
+lapply (le_to_lt_to_lt … H2 H1) -H2 -H1 #H
elim (lt_refl_false … H)
qed-.
(* Basic_1: was: lift_gen_lref_ge *)
lemma lift_inv_lref2_ge: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → d + e ≤ i → T1 = #(i - e).
#d #e #T1 #i #H elim (lift_inv_lref2 … 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 (plus_lt_false … Hdd)
qed-.
fact lift_inv_gref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀p. T2 = §p → T1 = §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
∀I,V2,U2. T2 = 𝕓{I} V2.U2 →
∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
T1 = 𝕓{I} V1. U1.
-#d #e #T1 #T2 * -d e T1 T2
+#d #e #T1 #T2 * -d -e -T1 -T2
[ #k #d #e #I #V2 #U2 #H destruct
| #i #d #e #_ #I #V2 #U2 #H destruct
| #i #d #e #_ #I #V2 #U2 #H destruct
lemma lift_inv_bind2: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡ 𝕓{I} V2. U2 →
∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
T1 = 𝕓{I} V1. U1.
-/2/ qed-.
+/2 width=3/ qed-.
fact lift_inv_flat2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
∀I,V2,U2. T2 = 𝕗{I} V2.U2 →
∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 &
T1 = 𝕗{I} V1. U1.
-#d #e #T1 #T2 * -d e T1 T2
+#d #e #T1 #T2 * -d -e -T1 -T2
[ #k #d #e #I #V2 #U2 #H destruct
| #i #d #e #_ #I #V2 #U2 #H destruct
| #i #d #e #_ #I #V2 #U2 #H destruct
| #p #d #e #I #V2 #U2 #H destruct
| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V2 #U2 #H destruct
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V2 #U2 #H destruct /2 width = 5/
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V2 #U2 #H destruct /2 width=5/
]
qed.
lemma lift_inv_flat2: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡ 𝕗{I} V2. U2 →
∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 &
T1 = 𝕗{I} V1. U1.
-/2/ qed-.
+/2 width=3/ qed-.
lemma lift_inv_pair_xy_x: ∀d,e,I,V,T. ↑[d, e] 𝕔{I} V. T ≡ V → False.
#d #e #J #V elim V -V
| lapply (lift_inv_gref2 … H) -H #H destruct
]
| * #I #W2 #U2 #IHW2 #_ #T #H
- [ elim (lift_inv_bind2 … H) -H #W1 #U1 #HW12 #_ #H destruct -J T W1 /2/
- | elim (lift_inv_flat2 … H) -H #W1 #U1 #HW12 #_ #H destruct -J T W1 /2/
+ [ elim (lift_inv_bind2 … H) -H #W1 #U1 #HW12 #_ #H destruct /2 width=2/
+ | elim (lift_inv_flat2 … H) -H #W1 #U1 #HW12 #_ #H destruct /2 width=2/
]
]
qed-.
| lapply (lift_inv_gref2 … H) -H #H destruct
]
| * #I #W2 #U2 #_ #IHU2 #V #d #e #H
- [ elim (lift_inv_bind2 … H) -H #W1 #U1 #_ #HU12 #H destruct -J U1 W1 /2/
- | elim (lift_inv_flat2 … H) -H #W1 #U1 #_ #HU12 #H destruct -J U1 W1 /2/
+ [ elim (lift_inv_bind2 … H) -H #W1 #U1 #_ #HU12 #H destruct /2 width=4/
+ | elim (lift_inv_flat2 … H) -H #W1 #U1 #_ #HU12 #H destruct /2 width=4/
]
]
qed-.
(* Basic forward lemmas *****************************************************)
lemma tw_lift: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → #[T1] = #[T2].
-#d #e #T1 #T2 #H elim H -d e T1 T2; normalize //
+#d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize //
qed-.
(* Basic properties *********************************************************)
(* Basic_1: was: lift_lref_gt *)
lemma lift_lref_ge_minus: ∀d,e,i. d + e ≤ i → ↑[d, e] #(i - e) ≡ #i.
-#d #e #i #H >(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.
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.
| 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/
]
(* 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-.
∀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
| #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-.
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.
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.
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 /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/ #T
+ <plus_minus /2 width=2/ /3 width=5/
| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hded
- 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.
L1 [0, e - 1] ≫ L2 → L2 ⊢ V1 [0, e - 1] ≫ V2 →
0 < e → L1. 𝕓{I} V1 [0, e] ≫ L2. 𝕓{I} V2.
#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
->(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
∃∃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.
∃∃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.
∃∃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
∃∃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.
∃∃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.
∃∃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
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 <minus_n_O /3/
- | -HK01 HV01 <minus_le_minus_minus_comm //
- elim (IHK01 … HK0L2 ? ?) -IHK01 HK0L2 /3/
+ [ -IHK01 -He21 destruct <minus_n_O /3 width=3/
+ | -HK01 -HV01 <minus_le_minus_minus_comm //
+ elim (IHK01 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
]
| #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 #He2de1
lapply (plus_le_weak … Hd1e2) #He2
<minus_le_minus_minus_comm //
lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
- elim (IHK01 … HK0L2 ? ?) -IHK01 HK0L2 /3/
+ elim (IHK01 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
]
qed.
lemma ltps_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
∃∃L. L [0, d1 + e1 - e2] ≫ L2 & ↓[0, e2] L1 ≡ L.
-#L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1
-[ #d1 #e1 #L2 #e2 #H >(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 <minus_n_O /3/
- | -HK10 HV10 <minus_le_minus_minus_comm //
- elim (IHK10 … HK0L2 ? ?) -IHK10 HK0L2 /3/
+ [ -IHK10 -He21 destruct <minus_n_O /3 width=3/
+ | -HK10 -HV10 <minus_le_minus_minus_comm //
+ elim (IHK10 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
]
| #K1 #K0 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 #He2de1
lapply (plus_le_weak … Hd1e2) #He2
<minus_le_minus_minus_comm //
lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
- elim (IHK10 … HK0L2 ? ?) -IHK10 HK0L2 /3/
+ elim (IHK10 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
]
qed.
lemma ltps_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →
∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
∃∃L. L2 [d1 - e2, e1] ≫ 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/
-| /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 <minus_n_O /3/
- | -HK01 HV01 <minus_le_minus_minus_comm //
- elim (IHK01 … HK0L2 ?) -IHK01 HK0L2 /3/
+ [ -IHK01 -He2d1 destruct <minus_n_O /3 width=3/
+ | -HK01 -HV01 <minus_le_minus_minus_comm //
+ elim (IHK01 … HK0L2 ?) -K0 /2 width=1/ /3 width=3/
]
]
qed.
lemma ltps_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
∃∃L. L [d1 - e2, e1] ≫ L2 & ↓[0, e2] L1 ≡ L.
-#L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1
-[ #d1 #e1 #L2 #e2 #H >(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 <minus_n_O /3/
- | -HK10 HV10 <minus_le_minus_minus_comm //
- elim (IHK10 … HK0L2 ?) -IHK10 HK0L2 /3/
+ [ -IHK10 -He2d1 destruct <minus_n_O /3 width=3/
+ | -HK10 -HV10 <minus_le_minus_minus_comm //
+ elim (IHK10 … HK0L2 ?) -K0 /2 width=1/ /3 width=3/
]
]
qed.
lemma ltps_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
∀L1,d1,e1. L0 [d1, e1] ≫ L1 → 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 #HL01 #Hde1d2
lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2
- lapply (ltps_ldrop_conf_ge … HL01 … HLK0 ?) -HL01 HLK0 /2/
+ lapply (ltps_ldrop_conf_ge … HL01 … HLK0 ?) -L0 // /2 width=4/
| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 #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.
∀L1,d1,e1. L0 [d1, e1] ≫ L1 →
∃∃T. L1 ⊢ T2 [d2, e2] ≫ T &
L1 ⊢ U2 [d1, e1] ≫ T.
-#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 #HL01
elim (lt_or_ge i2 d1) #Hi2d1
- [ elim (ltps_ldrop_conf_le … HL01 … HLK0 ?) -HL01 HLK0 /2/ #X #H #HLK1
- elim (ltps_inv_tps11 … H ?) -H [2: /2/ ] #K1 #V1 #_ #HV01 #H destruct -X;
+ [ elim (ltps_ldrop_conf_le … HL01 … HLK0 ?) -L0 /2 width=1/ #X #H #HLK1
+ elim (ltps_inv_tps11 … 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 // >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.
∀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.
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 ? ? ?) // <minus_plus_m_m_comm /3/
+ elim (lift_split … HVW i i ? ? ?) // <minus_plus_m_m_comm /3 width=4/
| * #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK
elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
- [ elim (IHU1 (L. 𝕓{I} W2) (d+1) ?) -IHU1 /2/ -HLK /3 width=8/
- | elim (IHU1 … HLK) -IHU1 HLK /3 width=8/
+ [ elim (IHU1 (L. 𝕓{I} W2) (d+1) ?) -IHU1 /2 width=1/ -HLK /3 width=8/
+ | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8/
]
]
qed.
lemma tps_weak: ∀L,T1,T2,d1,e1. L ⊢ T1 [d1, e1] ≫ T2 →
∀d2,e2. d2 ≤ d1 → d1 + e1 ≤ d2 + e2 →
L ⊢ T1 [d2, e2] ≫ T2.
-#L #T1 #T2 #d1 #e1 #H elim H -H L T1 T2 d1 e1
+#L #T1 #T2 #d1 #e1 #H elim H -L -T1 -T2 -d1 -e1
[ //
| #L #K #V #W #i #d1 #e1 #Hid1 #Hide1 #HLK #HVW #d2 #e2 #Hd12 #Hde12
- lapply (transitive_le … Hd12 … Hid1) -Hd12 Hid1 #Hid2
- lapply (lt_to_le_to_lt … Hide1 … Hde12) -Hide1 /2/
-| /4/
-| /4/
+ lapply (transitive_le … Hd12 … Hid1) -Hd12 -Hid1 #Hid2
+ lapply (lt_to_le_to_lt … Hide1 … Hde12) -Hide1 /2 width=4/
+| /4 width=3/
+| /4 width=1/
]
qed.
lemma tps_weak_top: ∀L,T1,T2,d,e.
L ⊢ T1 [d, e] ≫ T2 → L ⊢ T1 [d, |L| - d] ≫ 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 #_ #HLK #HVW
lapply (ldrop_fwd_ldrop2_length … HLK) #Hi
lapply (le_to_lt_to_lt … Hdi Hi) #Hd
- lapply (plus_minus_m_m_comm (|L|) d ?) /2/
-| normalize /2/
-| /2/
+ lapply (plus_minus_m_m_comm (|L|) d ?) /2 width=1/ /2 width=4/
+| normalize /2 width=1/
+| /2 width=1/
]
qed.
lemma tps_split_up: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → ∀i. d ≤ i → i ≤ d + e →
∃∃T. L ⊢ T1 [d, i - d] ≫ T & L ⊢ T [i, d + e - i] ≫ T2.
-#L #T1 #T2 #d #e #H elim H -H L T1 T2 d e
-[ /2/
+#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e
+[ /2 width=3/
| #L #K #V #W #i #d #e #Hdi #Hide #HLK #HVW #j #Hdj #Hjde
elim (lt_or_ge i j)
- [ -Hide Hjde;
- >(plus_minus_m_m_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.
↓[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
]
↓[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 *)
↓[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 →
∃∃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/
∃∃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
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 <plus_n_O #Hdd
+| #L #K #V #W #i #d #e #Hdi #Hide #_ #_ #H destruct
+ lapply (le_to_lt_to_lt … Hdi … Hide) -Hdi
-Hide <plus_n_O #Hdd
elim (lt_refl_false … Hdd)
-| /3/
-| /3/
+| /3 width=1/
+| /3 width=1/
]
qed.
(* Basic forward lemmas *****************************************************)
lemma tps_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → #[T1] ≤ #[T2].
-#L #T1 #T2 #d #e #H elim H normalize -H L T1 T2 d e
-/3 by monotonic_le_plus_l, le_plus/ (**) (* just /3/ is too slow *)
+#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e normalize
+/3 by monotonic_le_plus_l, le_plus/ (**) (* just /3 width=1/ is too slow *)
qed-.
(* Basic_1: removed theorems 25:
fact tps_inv_refl_SO2_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → e = 1 →
∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → 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 #K0 #V0 #W #i #d #e #Hdi #Hide #HLK0 #_ #H destruct -e;
- >(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 //
]
↑[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 // <minus_plus #W #HVW #HWU2
- elim (ldrop_trans_le … HLK … HKV ?) -HLK HKV K [2: /2/] #X #HLK #H
- elim (ldrop_inv_skip2 … H ?) -H [2: /2/] -Hid #K #Y #_ #HVY
- >(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 // <minus_plus #W #HVW #HWU2
+ 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) -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.
↑[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 // <minus_plus #W #HVW #HWU2
- elim (ldrop_trans_le … HLK … HKV ?) -K [2: /2/] #X #HLK #H
- elim (ldrop_inv_skip2 … H ?) -H [2: /2/] -Hid #K #Y #_ #HVY
- >(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.
↑[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.
∀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.
∀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 ?) [ <le_plus_minus /2/ ] -Hdedet #Hidete
+ elim (lift_inv_lref2 … H) -H * #Hid #H destruct
+ [ -Hdtd -Hidet
+ lapply (lt_to_le_to_lt … (dt + (et - e)) Hid ?) [ <le_plus_minus /2 width=1/ ] -Hdedet #Hidete
elim (ldrop_conf_lt … HLK … HLKV ?) -L // #L #U #HKL #_ #HUV
- elim (lift_trans_le … HUV … HVW ?) -V // >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.
∀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/ ]
<plus_minus // /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.
(* Basic_1: was: subst1_gen_lift_eq *)
lemma tps_inv_lift1_eq: ∀L,U1,U2,d,e.
L ⊢ U1 [d, e] ≫ U2 → ∀T1. ↑[d, e] T1 ≡ U1 → U1 = U2.
-#L #U1 #U2 #d #e #H elim H -H L U1 U2 d e
+#L #U1 #U2 #d #e #H elim H -L -U1 -U2 -d -e
[ //
| #L #K #V #W #i #d #e #Hdi #Hide #_ #_ #T1 #H
elim (lift_inv_lref2 … H) -H * #H
- [ lapply (le_to_lt_to_lt … Hdi … H) -Hdi H #H
+ [ lapply (le_to_lt_to_lt … Hdi … H) -Hdi -H #H
elim (lt_refl_false … H)
- | lapply (lt_to_le_to_lt … Hide … H) -Hide H #H
+ | lapply (lt_to_le_to_lt … Hide … H) -Hide -H #H
elim (lt_refl_false … H)
]
| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
- elim (lift_inv_bind2 … HX) -HX #V #T #HV1 #HT1 #H destruct -X
+ elim (lift_inv_bind2 … HX) -HX #V #T #HV1 #HT1 #H destruct
>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) &
).
- 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)).
∃∃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 // <plus_minus_m_m_comm // -Hddt Hdtde #HU1
-lapply (tps_inv_lift1_eq … HU1 … HTU1) -HU1 #HU1 destruct -U1;
-elim (tps_inv_lift1_ge … HU2 … HLK … HTU1 ?) -HU2 HLK HTU1 // <minus_plus_m_m /2/
+lapply (tps_weak … HU1 d e ? ?) -HU1 // <plus_minus_m_m_comm // -Hddt -Hdtde #HU1
+lapply (tps_inv_lift1_eq … HU1 … HTU1) -HU1 #HU1 destruct
+elim (tps_inv_lift1_ge … HU2 … HLK … HTU1 ?) -U -L // <minus_plus_m_m /2 width=3/
qed.
lemma tps_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 →
dt ≤ d → dt + et ≤ d + e →
∃∃T2. K ⊢ T1 [dt, d - dt] ≫ T2 & ↑[d, e] T2 ≡ U2.
#L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde
-lapply (tps_weak … HU12 dt (d + e - dt) ? ?) -HU12 // [ /2/ ] -Hdetde #HU12
-elim (tps_inv_lift1_be … HU12 … HLK … HTU1 ? ?) -U1 L /2/
+lapply (tps_weak … HU12 dt (d + e - dt) ? ?) -HU12 // /2 width=3/ -Hdetde #HU12
+elim (tps_inv_lift1_be … HU12 … HLK … HTU1 ? ?) -U1 -L // /2 width=3/
qed.
theorem tps_conf_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 [d1, e1] ≫ T1 →
∀T2,d2,e2. L ⊢ T0 [d2, e2] ≫ T2 →
∃∃T. L ⊢ T1 [d2, e2] ≫ T & L ⊢ T2 [d1, e1] ≫ T.
-#L #T0 #T1 #d1 #e1 #H elim H -H L T0 T1 d1 e1
-[ /2/
+#L #T0 #T1 #d1 #e1 #H elim H -L -T0 -T1 -d1 -e1
+[ /2 width=3/
| #L #K1 #V1 #T1 #i0 #d1 #e1 #Hd1 #Hde1 #HLK1 #HVT1 #T2 #d2 #e2 #H
elim (tps_inv_lref1 … H) -H
- [ #HX destruct -T2 /4/
- | -Hd1 Hde1 * #K2 #V2 #_ #_ #HLK2 #HVT2
- lapply (ldrop_mono … HLK1 … HLK2) -HLK1 HLK2 #H destruct -V1 K1
- >(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.
∀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.
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.
projects / helm.git / commitdiff