(* NOTATION FOR THE "functional" COMPONENT ********************************)
-notation "hvbox( ↑ [ d , break e ] break T )"
+notation "hvbox( ↑ [ d , break e ] break term 60 T )"
non associative with precedence 60
for @{ 'Lift $d $e $T }.
-notation "hvbox( [ d ← break V ] break T )"
+notation "hvbox( [ d ← break V ] break term 60 T )"
non associative with precedence 60
for @{ 'Subst $V $d $T }.
-notation "hvbox( T1 ⇨ break T2 )"
+notation "hvbox( T1 ⇨ break term 46 T2 )"
non associative with precedence 45
for @{ 'SRed $T1 $T2 }.
(* Note: it does not hold replacing |L1| with |L2| *)
lemma cprs_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 →
- ∀L2. L1 [0, |L1|] ≼ L2 → L2 ⊢ T1 ➡* T2.
+ ∀L2. L1 ≼ [0, |L1|] L2 → L2 ⊢ T1 ➡* T2.
/3 width=3/
qed.
(* Properties concerning context-sensitive parallel reduction on lenv's *****)
-lemma ltpr_tpss_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2,d,e. L2 ⊢ T1 [d, e] ▶* T2 →
- ∃∃T. L1 ⊢ T1 [d, e] ▶* T & L1 ⊢ T ➡* T2.
+lemma ltpr_tpss_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2,d,e. L2 ⊢ T1 ▶* [d, e] T2 →
+ ∃∃T. L1 ⊢ T1 ▶* [d, e] T & L1 ⊢ T ➡* T2.
#L1 #L2 #HL12 #T1 #T2 #d #e #H @(tpss_ind … H) -T2
[ /2 width=3/
| #T #T2 #_ #HT2 * #T0 #HT10 #HT0
(* Properties concerning parallel unfold on terms ***************************)
(* Basic_1: was only: pr3_subst1 *)
-lemma cprs_tpss_ltpr: ∀L1,T1,U1,d,e. L1 ⊢ T1 [d, e] ▶* U1 →
+lemma cprs_tpss_ltpr: ∀L1,T1,U1,d,e. L1 ⊢ T1 ▶* [d, e] U1 →
∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 →
- ∃∃U2. L2 ⊢ U1 ➡* U2 & L2 ⊢ T2 [d, e] ▶* U2.
+ ∃∃U2. L2 ⊢ U1 ➡* U2 & L2 ⊢ T2 ▶* [d, e] U2.
#L1 #T1 #U1 #d #e #HTU1 #L2 #HL12 #T2 #HT12 elim HT12 -T2
[ #T2 #HT12
elim (cpr_tpss_ltpr … HL12 … HT12 … HTU1) -L1 -T1 /3 width=3/
lemma csn_ind: ∀L. ∀R:predicate term.
(∀T1. L ⊢ ⬇* T1 →
- (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → False) → R T2) →
+ (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → R T2) →
R T1
) →
∀T. L ⊢ ⬇* T → R T.
(* Basic_1: was: sn3_pr2_intro *)
lemma csn_intro: ∀L,T1.
- (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → False) → L ⊢ ⬇* T2) → L ⊢ ⬇* T1.
-#L #T1 #H
-@(SN_intro … H)
-qed.
+ (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬇* T2) → L ⊢ ⬇* T1.
+/4 width=1/ qed.
(* Basic_1: was: sn3_nf2 *)
lemma csn_cnf: ∀L,T. L ⊢ 𝐍[T] → L ⊢ ⬇* T.
(* Basic_1: removed theorems 14:
sn3_cdelta
- sn3_gen_cflat sn3_cflat sn3_cpr3_trans sn3_shift sn3_change
- sn3_appl_cast sn3_appl_beta sn3_appl_lref sn3_appl_abbr
- sn3_appl_appls sn3_bind sn3_appl_bind sn3_appls_bind
+ sn3_gen_cflat sn3_cflat sn3_cpr3_trans sn3_shift sn3_change
+ sn3_appl_cast sn3_appl_beta sn3_appl_lref sn3_appl_abbr
+ sn3_appl_appls sn3_bind sn3_appl_bind sn3_appls_bind
*)
lemma csna_ind: ∀L. ∀R:predicate term.
(∀T1. L ⊢ ⬇⬇* T1 →
- (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → False) → R T2) → R T1
+ (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → R T2) → R T1
) →
∀T. L ⊢ ⬇⬇* T → R T.
#L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1
(* Basic_1: was: sn3_intro *)
lemma csna_intro: ∀L,T1.
- (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → False) → L ⊢ ⬇⬇* T2) → L ⊢ ⬇⬇* T1.
-#L #T1 #H
-@(SN_intro … H)
-qed.
+ (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → L ⊢ ⬇⬇* T2) → L ⊢ ⬇⬇* T1.
+/4 width=1/ qed.
fact csna_intro_aux: ∀L,T1.
- (∀T,T2. L ⊢ T ➡* T2 → T1 = T → (T1 = T2 → False) → L ⊢ ⬇⬇* T2) → L ⊢ ⬇⬇* T1.
+ (∀T,T2. L ⊢ T ➡* T2 → T1 = T → (T1 = T2 → ⊥) → L ⊢ ⬇⬇* T2) → L ⊢ ⬇⬇* T1.
/4 width=3/ qed-.
(* Basic_1: was: sn3_pr3_trans (old version) *)
(* Basic_1: was: sn3_pr2_intro (old version) *)
lemma csna_intro_cpr: ∀L,T1.
- (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → False) → L ⊢ ⬇⬇* T2) →
+ (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬇⬇* T2) →
L ⊢ ⬇⬇* T1.
#L #T1 #H
@csna_intro_aux #T #T2 #H @(cprs_ind_dx … H) -T
lemma csn_ind_alt: ∀L. ∀R:predicate term.
(∀T1. L ⊢ ⬇* T1 →
- (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → False) → R T2) → R T1
+ (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → R T2) → R T1
) →
∀T. L ⊢ ⬇* T → R T.
#L #R #H0 #T1 #H @(csna_ind … (csn_csna … H)) -T1 #T1 #HT1 #IHT1
(* Basic_1: was only: sn3_appl_appl *)
lemma csn_appl_simple_tstc: ∀L,V. L ⊢ ⬇* V → ∀T1.
L ⊢ ⬇* T1 →
- (∀T2. L ⊢ T1 ➡* T2 → (T1 ≃ T2 → False) → L ⊢ ⬇* ⓐV. T2) →
+ (∀T2. L ⊢ T1 ➡* T2 → (T1 ≃ T2 → ⊥) → L ⊢ ⬇* ⓐV. T2) →
𝐒[T1] → L ⊢ ⬇* ⓐV. T1.
#L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1
@csn_intro #X #HL #H
@csn_intro #T #HLT2 #HT2
elim (cpr_inv_lift … HL21 … HT12 … HLT2) -HLT2 #T0 #HT0 #HLT10
@(IHT1 … HLT10) // -L1 -L2 #H destruct
->(lift_mono … HT0 … HT12) in HT2; -T0 /2 width=1/
+>(lift_mono … HT0 … HT12) in HT2; -T1 /2 width=1/
qed.
(* Basic_1: was: sn3_gen_lift *)
elim (lift_total T d e) #T0 #HT0
lapply (cpr_lift … HL12 … HT21 … HT0 HLT2) -HLT2 #HLT10
@(IHT1 … HLT10) // -L1 -L2 #H destruct
->(lift_inj … HT0 … HT21) in HT2; -T0 /2 width=1/
+>(lift_inj … HT0 … HT21) in HT2; -T1 /2 width=1/
qed.
(* Advanced properties ******************************************************)
qed.
lemma csn_appl_simple: ∀L,V. L ⊢ ⬇* V → ∀T1.
- (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → False) → L ⊢ ⬇* ⓐV. T2) →
+ (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬇* ⓐV. T2) →
𝐒[T1] → L ⊢ ⬇* ⓐV. T1.
#L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #IHT1 #HT1
@csn_intro #X #H1 #H2
(* *)
(**************************************************************************)
-include "basic_2/unfold/delift_lift.ma".
-include "basic_2/unfold/thin_ldrop.ma".
+include "basic_2/substitution/lsubs_sfr.ma".
+include "basic_2/unfold/delift.ma".
+include "basic_2/unfold/thin.ma".
+(*
include "basic_2/equivalence/cpcs_delift.ma".
-include "basic_2/dynamic/nta_nta.ma".
+*)
+include "basic_2/dynamic/nta.ma".
(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
(* Properties on reverse basic term relocation ******************************)
(* Basic_1: was only: ty3_gen_cabbr *)
-axiom thin_nta_delift_conf: ∀h,L1,T1,X1. ⦃h, L1⦄ ⊢ T1 : X1 →
- ∀L2,d,e. L1 [d, e] ≡ L2 →
- ∀T2. L1 ⊢ T1 [d, e] ≡ T2 →
- ∃∃U1,U2. ⦃h, L2⦄ ⊢ T2 : U2 & L1 ⊢ U1 [d, e] ≡ U2 &
- L1 ⊢ U1 ⬌* X1.
+axiom thin_nta_delift_conf: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 →
+ ∀L2,d,e. ≼ [d, e] L1 → L1 [d, e] ≡ L2 →
+ ∃∃T2,U2. ⦃h, L2⦄ ⊢ T2 : U2 &
+ L1 ⊢ T1 [d, e] ≡ T2 & L1 ⊢ U1 [d, e] ≡ U2.
(*
#h #L1 #T1 #U1 #H @(nta_ind_alt … H) -L1 -T1 -U1
[ #L1 #k #L2 #d #e #HL12 #X #H
|
|
|
-| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHVW1 #L2 #d #e #HL12 #X #H
+| #L1 #V1 #Y1 #T1 #X1 #_ #_ #IHTX1 #IHXY1 #L2 #d #e #HL12 #X #H
elim (delift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
-(*
- elim (IHTU1 … HL12 … HT12) -T1 #U2 #HTU2 #HU12
- elim (IHVW1 … HL12 (ⓐV2.U2) ?) -IHVW1 -HL12
+ elim (IHTX1 … HL12 … HT12) -T1 #U1 #U2 #HTU2 #HU12 #HUX1
+(*
+ elim (IHXY1 … HL12 (ⓐV2.U2) ?) -IHXY1 -HL12
+*)
+ @(ex3_2_intro … (ⓐV1.U1) (ⓐV2.U2))
+ [2: /2 width=1/ |3: /2 width=1/ ] -HV12 -HU12 -HUX1
+ @(nta_pure … HTU2) -HTU2
+
[ /3 width=5/ | /2 width=1/ ]
*)
+(*
| #L1 #T1 #X1 #Y1 #_ #_ #IHTX1 #IHXY1 #L2 #d #e #HL12 #X #H
elim (delift_inv_flat1 … H) -H #X2 #T2 #HX12 #HT12 #H destruct
elim (IHTX1 … HL12 … HT12) -T1 #U1 #U2 #HTU2 #HU12 #HUX1
lapply (cpcs_trans … HUX211 … HX112) -X11 /2 width=5/
]
*)
-lemma nta_inv_lift1_delift: ∀h,L1,T1,X. ⦃h, L1⦄ ⊢ T1 : X →
- ∀L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀T2. ⇧[d, e] T2 ≡ T1 →
- ∃∃U1,U2. ⦃h, L2⦄ ⊢ T2 : U2 & L1 ⊢ U1 [d, e] ≡ U2 &
- L1 ⊢ U1 ⬌* X.
-/3 width=3/ qed-.
-
-lemma nta_inv_lift1: ∀h,L1,T1,X. ⦃h, L1⦄ ⊢ T1 : X →
+axiom nta_inv_lift1: ∀h,L1,T1,X. ⦃h, L1⦄ ⊢ T1 : X →
∀L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀T2. ⇧[d, e] T2 ≡ T1 →
∃∃U1,U2. ⦃h, L2⦄ ⊢ T2 : U2 & ⇧[d, e] U2 ≡ U1 &
L1 ⊢ U1 ⬌* X.
+(*
#h #L1 #T1 #X #H #L2 #d #e #HL12 #T2 #HT21
elim (nta_inv_lift1_delift … H … HL12 … HT21) -T1 -HL12 #U1 #U2 #HTU2 * #U #HU1 #HU2 #HU1X
lapply (cpcs_cpr_conf … U … HU1X) -HU1X /2 width=3/ -U1 /2 width=5/
qed-.
+*)
\ No newline at end of file
qed-.
(* Basic_1: was: pc3_gen_sort_abst *)
-lemma cpcs_inv_sort_abst: ∀L,W,T,k. L ⊢ ⋆k ⬌* ⓛW.T → False.
+lemma cpcs_inv_sort_abst: ∀L,W,T,k. L ⊢ ⋆k ⬌* ⓛW.T → ⊥.
#L #W #T #k #H
elim (cpcs_inv_cprs … H) -H #X #H1
>(cprs_inv_sort1 … H1) -X #H2
(* Basic inversion lemmas ***************************************************)
-lemma discr_apair_xy_x: ∀A,B. ②B. A = B → False.
+lemma discr_apair_xy_x: ∀A,B. ②B. A = B → ⊥.
#A #B elim B -B
[ #H destruct
| #Y #X #IHY #_ #H destruct
]
qed-.
-lemma discr_tpair_xy_y: ∀B,A. ②B. A = A → False.
+lemma discr_tpair_xy_y: ∀B,A. ②B. A = A → ⊥.
#B #A elim A -A
[ #H destruct
| #Y #X #_ #IHX #H destruct
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/grammar/lenv_length.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
-
-inductive lsubs: nat → nat → relation lenv ≝
-| lsubs_sort: ∀d,e. lsubs d e (⋆) (⋆)
-| lsubs_OO: ∀L1,L2. lsubs 0 0 L1 L2
-| lsubs_abbr: ∀L1,L2,V,e. lsubs 0 e L1 L2 →
- lsubs 0 (e + 1) (L1. ⓓV) (L2.ⓓV)
-| lsubs_abst: ∀L1,L2,I,V1,V2,e. lsubs 0 e L1 L2 →
- lsubs 0 (e + 1) (L1. ⓛV1) (L2.ⓑ{I} V2)
-| lsubs_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
- lsubs d e L1 L2 → lsubs (d + 1) e (L1. ⓑ{I1} V1) (L2. ⓑ{I2} V2)
-.
-
-interpretation
- "local environment refinement (substitution)"
- 'SubEq L1 d e L2 = (lsubs d e L1 L2).
-
-definition lsubs_conf: ∀S. (lenv → relation S) → Prop ≝ λS,R.
- ∀L1,s1,s2. R L1 s1 s2 →
- ∀L2,d,e. L1 [d, e] ≼ L2 → R L2 s1 s2.
-
-(* Basic properties *********************************************************)
-
-lemma TC_lsubs_conf: ∀S,R. lsubs_conf S R → lsubs_conf S (λL. (TC … (R L))).
-#S #R #HR #L1 #s1 #s2 #H elim H -s2
-[ /3 width=5/
-| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12
- lapply (HR … Hs2 … HL12) -HR -Hs2 -HL12 /3 width=3/
-]
-qed.
-
-lemma lsubs_bind_eq: ∀L1,L2,e. L1 [0, e] ≼ L2 → ∀I,V.
- L1. ⓑ{I} V [0, e + 1] ≼ L2.ⓑ{I} V.
-#L1 #L2 #e #HL12 #I #V elim I -I /2 width=1/
-qed.
-
-lemma lsubs_refl: ∀d,e,L. L [d, e] ≼ L.
-#d elim d -d
-[ #e elim e -e // #e #IHe #L elim L -L // /2 width=1/
-| #d #IHd #e #L elim L -L // /2 width=1/
-]
-qed.
-
-lemma lsubs_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≼ L2 → 0 < d →
- ∀I1,I2,V1,V2. L1. ⓑ{I1} V1 [d, e] ≼ L2. ⓑ{I2} V2.
-
-#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) // /2 width=1/
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-(* Basic forward lemmas ***************************************************)
-
-fact lsubs_fwd_length_full1_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 →
- d = 0 → e = |L1| → |L1| ≤ |L2|.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
-[ //
-| /2 width=1/
-| /3 width=1/
-| /3 width=1/
-| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct
-]
-qed.
-
-lemma lsubs_fwd_length_full1: ∀L1,L2. L1 [0, |L1|] ≼ L2 → |L1| ≤ |L2|.
-/2 width=5/ qed-.
-
-fact lsubs_fwd_length_full2_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 →
- d = 0 → e = |L2| → |L2| ≤ |L1|.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
-[ //
-| /2 width=1/
-| /3 width=1/
-| /3 width=1/
-| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct
-]
-qed.
-
-lemma lsubs_fwd_length_full2: ∀L1,L2. L1 [0, |L2|] ≼ L2 → |L2| ≤ |L1|.
-/2 width=5/ qed-.
(* Basic inversion lemmas ***************************************************)
-lemma discr_tpair_xy_x: ∀I,T,V. ②{I} V. T = V → False.
+lemma discr_tpair_xy_x: ∀I,T,V. ②{I} V. T = V → ⊥.
#I #T #V elim V -V
[ #J #H destruct
| #J #W #U #IHW #_ #H destruct
qed-.
(* Basic_1: was: thead_x_y_y *)
-lemma discr_tpair_xy_y: ∀I,V,T. ②{I} V. T = T → False.
+lemma discr_tpair_xy_y: ∀I,V,T. ②{I} V. T = T → ⊥.
#I #V #T elim T -T
[ #J #H destruct
| #J #W #U #_ #IHU #H destruct
qed-.
lemma eq_false_inv_tpair_sn: ∀I,V1,T1,V2,T2.
- (②{I} V1. T1 = ②{I} V2. T2 → False) →
- (V1 = V2 → False) ∨ (V1 = V2 ∧ (T1 = T2 → False)).
+ (②{I} V1. T1 = ②{I} V2. T2 → ⊥) →
+ (V1 = V2 → ⊥) ∨ (V1 = V2 ∧ (T1 = T2 → ⊥)).
#I #V1 #T1 #V2 #T2 #H
elim (term_eq_dec V1 V2) /3 width=1/ #HV12 destruct
@or_intror @conj // #HT12 destruct /2 width=1/
qed-.
lemma eq_false_inv_tpair_dx: ∀I,V1,T1,V2,T2.
- (②{I} V1. T1 = ②{I} V2. T2 → False) →
- (T1 = T2 → False) ∨ (T1 = T2 ∧ (V1 = V2 → False)).
+ (②{I} V1. T1 = ②{I} V2. T2 → ⊥) →
+ (T1 = T2 → ⊥) ∨ (T1 = T2 ∧ (V1 = V2 → ⊥)).
#I #V1 #T1 #V2 #T2 #H
elim (term_eq_dec T1 T2) /3 width=1/ #HT12 destruct
@or_intror @conj // #HT12 destruct /2 width=1/
qed-.
lemma eq_false_inv_beta: ∀V1,V2,W1,W2,T1,T2.
- (ⓐV1. ⓛW1. T1 = ⓐV2. ⓛW2 .T2 →False) →
- (W1 = W2 → False) ∨
- (W1 = W2 ∧ (ⓓV1. T1 = ⓓV2. T2 → False)).
+ (ⓐV1. ⓛW1. T1 = ⓐV2. ⓛW2 .T2 →⊥) →
+ (W1 = W2 → ⊥) ∨
+ (W1 = W2 ∧ (ⓓV1. T1 = ⓓV2. T2 → ⊥)).
#V1 #V2 #W1 #W2 #T1 #T2 #H
elim (eq_false_inv_tpair_sn … H) -H
[ #HV12 elim (term_eq_dec W1 W2) /3 width=1/
(* Basic inversion lemmas ***************************************************)
-fact simple_inv_bind_aux: ∀T. 𝐒[T] → ∀J,W,U. T = ⓑ{J} W. U → False.
+fact simple_inv_bind_aux: ∀T. 𝐒[T] → ∀J,W,U. T = ⓑ{J} W. U → ⊥.
#T * -T
[ #I #J #W #U #H destruct
| #I #V #T #J #W #U #H destruct
]
qed.
-lemma simple_inv_bind: ∀I,V,T. 𝐒[ⓑ{I} V. T] → False.
+lemma simple_inv_bind: ∀I,V,T. 𝐒[ⓑ{I} V. T] → ⊥.
/2 width=6/ qed-.
lemma simple_inv_pair: ∀I,V,T. 𝐒[②{I}V.T] → ∃J. I = Flat2 J.
(* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *)
lemma tstc_inv_bind_appls_simple: ∀I,Vs,V2,T1,T2. ⒶVs.T1 ≃ ⓑ{I} V2. T2 →
- 𝐒[T1] → False.
+ 𝐒[T1] → ⊥.
#I #Vs #V2 #T1 #T2 #H
elim (tstc_inv_pair2 … H) -H #V0 #T0
elim Vs -Vs normalize
(* Grammar ******************************************************************)
-notation "hvbox( ⓪ )"
+notation "⓪"
non associative with precedence 90
for @{ 'Item0 }.
non associative with precedence 90
for @{ 'Item0 $I }.
-notation "hvbox( ⋆ )"
+notation "⋆"
non associative with precedence 90
for @{ 'Star }.
non associative with precedence 90
for @{ 'Weight $x $y }.
-notation "hvbox( 𝐒 [ T ] )"
+notation "hvbox( 𝐒 [ T ] )"
non associative with precedence 45
for @{ 'Simple $T }.
non associative with precedence 45
for @{ 'Iso $T1 $T2 }.
-notation "hvbox( T1 break [ d , break e ] ≼ break term 46 T2 )"
- non associative with precedence 45
- for @{ 'SubEq $T1 $d $e $T2 }.
-
(* Substitution *************************************************************)
-notation "hvbox( L ⊢ break [ d , break e ] break 𝐑 [ T ] )"
+notation "hvbox( L ⊢ break 𝐑 [ d , break e ] break ⦃ T ⦄ )"
non associative with precedence 45
for @{ 'Reducible $L $d $e $T }.
-notation "hvbox( L ⊢ break [ d , break e ] break 𝐈 [ T ] )"
+notation "hvbox( L ⊢ break 𝐈 [ d , break e ] break ⦃ T ⦄ )"
non associative with precedence 45
for @{ 'NotReducible $L $d $e $T }.
-notation "hvbox( L ⊢ break [ d , break e ] break 𝐍 [ T ] )"
+notation "hvbox( L ⊢ break 𝐍 [ d , break e ] break ⦃ T ⦄ )"
non associative with precedence 45
for @{ 'Normal $L $d $e $T }.
non associative with precedence 45
for @{ 'RLift $d $e $T1 $T2 }.
+notation "hvbox( T1 break ≼ [ d , break e ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'SubEq $T1 $d $e $T2 }.
+
+notation "hvbox( ≼ [ d , break e ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'SubEqTop $d $e $T2 }.
+
notation "hvbox( ⇩ [ e ] break term 46 L1 ≡ break term 46 L2 )"
non associative with precedence 45
for @{ 'RDrop $e $L1 $L2 }.
non associative with precedence 45
for @{ 'RDrop $d $e $L1 $L2 }.
-notation "hvbox( L ⊢ break ⌘ [ T ] ≡ break term 46 k )"
+notation "hvbox( L ⊢ break ⌘ ⦃ T ⦄ ≡ break term 46 k )"
non associative with precedence 45
for @{ 'ICM $L $T $k }.
-notation "hvbox( L ⊢ break term 46 T1 break [ d , break e ] ▶ break term 46 T2 )"
+notation "hvbox( L ⊢ break term 46 T1 break ▶ [ d , break e ] break term 46 T2 )"
non associative with precedence 45
for @{ 'PSubst $L $T1 $d $e $T2 }.
non associative with precedence 45
for @{ 'RDropStar $e $L1 $L2 }.
-notation "hvbox( T1 break [ d , break e ] ▶* break term 46 T2 )"
+notation "hvbox( T1 break ▶* [ d , break e ] break term 46 T2 )"
non associative with precedence 45
for @{ 'PSubstStar $T1 $d $e $T2 }.
-notation "hvbox( L ⊢ break term 46 T1 break [ d , break e ] ▶* break term 46 T2 )"
+notation "hvbox( L ⊢ break term 46 T1 break ▶* [ d , break e ] break term 46 T2 )"
non associative with precedence 45
for @{ 'PSubstStar $L $T1 $d $e $T2 }.
-notation "hvbox( L ⊢ break term 46 T1 break [ d , break e ] ▶▶* break term 46 T2 )"
+notation "hvbox( L ⊢ break term 46 T1 break ▶▶* [ d , break e ] break term 46 T2 )"
non associative with precedence 45
for @{ 'PSubstStarAlt $L $T1 $d $e $T2 }.
non associative with precedence 45
for @{ 'TSubst $L $T1 $d $e $T2 }.
-notation "hvbox( T1 break [ d , break e ] ≡≡ break term 46 T2 )"
+notation "hvbox( T1 break [ d , break e ] ≡ ≡ break term 46 T2 )"
non associative with precedence 45
for @{ 'TSubstAlt $T1 $d $e $T2 }.
-notation "hvbox( L ⊢ break term 46 T1 break [ d , break e ] ≡≡ break term 46 T2 )"
+notation "hvbox( L ⊢ break term 46 T1 break [ d , break e ] ≡ ≡ break term 46 T2 )"
non associative with precedence 45
for @{ 'TSubstAlt $L $T1 $d $e $T2 }.
(* Reducibility *************************************************************)
-notation "hvbox( 𝐑 [ T ] )"
+notation "hvbox( 𝐑 [ T ] )"
non associative with precedence 45
for @{ 'Reducible $T }.
non associative with precedence 45
for @{ 'Reducible $L $T }.
-notation "hvbox( 𝐈 [ T ] )"
+notation "hvbox( 𝐈 [ T ] )"
non associative with precedence 45
for @{ 'NotReducible $T }.
non associative with precedence 45
for @{ 'NotReducible $L $T }.
-notation "hvbox( 𝐍 [ T ] )"
+notation "hvbox( 𝐍 [ T ] )"
non associative with precedence 45
for @{ 'Normal $T }.
non associative with precedence 45
for @{ 'WHdReducible $T }.
-notation "hvbox( L ⊢ break 𝐖𝐇𝐑 [ T ] )"
+notation "hvbox( L ⊢ break 𝐖𝐇𝐑 [ T ] )"
non associative with precedence 45
for @{ 'WHdReducible $L $T }.
-notation "hvbox( 𝐖𝐇𝐈 [ T ] )"
+notation "hvbox( 𝐖𝐇𝐈 [ T ] )"
non associative with precedence 45
for @{ 'NotWHdReducible $T }.
(* Basic_1: was: nf2_dec *)
axiom cnf_dec: ∀L,T1. L ⊢ 𝐍[T1] ∨
- ∃∃T2. L ⊢ T1 ➡ T2 & (T1 = T2 → False).
+ ∃∃T2. L ⊢ T1 ➡ T2 & (T1 = T2 → ⊥).
(* Basic_1: removed theorems 1: nf2_abst_shift *)
lemma cnf_abst: ∀I,L,V,W,T. L ⊢ 𝐍[W] → L. ⓑ{I} V ⊢ 𝐍[T] → L ⊢ 𝐍[ⓛW.T].
#I #L #V #W #T #HW #HT #X #H
elim (cpr_inv_abst1 … H I V) -H #W0 #T0 #HW0 #HT0 #H destruct
->(HW … HW0) -W >(HT … HT0) -T //
+>(HW … HW0) -W0 >(HT … HT0) -T0 //
qed.
(* Basic_1: was only: nf2_appl_lref *)
lemma cnf_appl_simple: ∀L,V,T. L ⊢ 𝐍[V] → L ⊢ 𝐍[T] → 𝐒[T] → L ⊢ 𝐍[ⓐV.T].
#L #V #T #HV #HT #HS #X #H
elim (cpr_inv_appl1_simple … H ?) -H // #V0 #T0 #HV0 #HT0 #H destruct
->(HV … HV0) -V >(HT … HT0) -T //
+>(HV … HV0) -V0 >(HT … HT0) -T0 //
qed.
(* Relocation properties ****************************************************)
L ⊢ 𝐍[T] → ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → L0 ⊢ 𝐍[T0].
#L0 #L #T #T0 #d #e #HLT #HL0 #HT0 #X #H
elim (cpr_inv_lift … HL0 … HT0 … H) -L0 #T1 #HT10 #HT1
->(HLT … HT1) in HT0; -L #HT0
+<(HLT … HT1) in HT0; -L #HT0
>(lift_mono … HT10 … HT0) -T1 -X //
qed.
(* Basic_1: includes: pr2_delta1 *)
definition cpr: lenv → relation term ≝
- λL,T1,T2. ∃∃T. T1 ➡ T & L ⊢ T [0, |L|] ▶* T2.
+ λL,T1,T2. ∃∃T. T1 ➡ T & L ⊢ T ▶* [0, |L|] T2.
interpretation
"context-sensitive parallel reduction (term)"
(* Basic properties *********************************************************)
-lemma cpr_intro: ∀L,T1,T,T2,d,e. T1 ➡ T → L ⊢ T [d, e] ▶* T2 → L ⊢ T1 ➡ T2.
+lemma cpr_intro: ∀L,T1,T,T2,d,e. T1 ➡ T → L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ➡ T2.
/4 width=3/ qed-.
(* Basic_1: was by definition: pr2_free *)
lemma cpr_tpr: ∀T1,T2. T1 ➡ T2 → ∀L. L ⊢ T1 ➡ T2.
/2 width=3/ qed.
-lemma cpr_tpss: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ T1 ➡ T2.
+lemma cpr_tpss: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → L ⊢ T1 ➡ T2.
/3 width=5/ qed.
lemma cpr_refl: ∀L,T. L ⊢ T ➡ T.
(* Note: it does not hold replacing |L1| with |L2| *)
(* Basic_1: was only: pr2_change *)
lemma cpr_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 →
- ∀L2. L1 [0, |L1|] ≼ L2 → L2 ⊢ T1 ➡ T2.
+ ∀L2. L1 ≼ [0, |L1|] L2 → L2 ⊢ T1 ➡ T2.
#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12
lapply (tpss_lsubs_conf … HT2 … HL12) -HT2 -HL12 /3 width=4/
qed.
(* Basic_1: was pr2_gen_abbr *)
lemma cpr_inv_abbr1: ∀L,V1,T1,U2. L ⊢ ⓓV1. T1 ➡ U2 →
- (∃∃V,V2,T2. V1 ➡ V & L ⊢ V [O, |L|] ▶* V2 &
+ (∃∃V,V2,T2. V1 ➡ V & L ⊢ V ▶* [O, |L|] V2 &
L. ⓓV ⊢ T1 ➡ T2 &
U2 = ⓓV2. T2
) ∨
(* Advanced properties ******************************************************)
lemma cpr_cdelta: ∀L,K,V1,W1,W2,i.
- ⇩[0, i] L ≡ K. ⓓV1 → K ⊢ V1 [0, |L| - i - 1] ▶* W1 →
+ ⇩[0, i] L ≡ K. ⓓV1 → K ⊢ V1 ▶* [0, |L| - i - 1] W1 →
⇧[0, i + 1] W1 ≡ W2 → L ⊢ #i ➡ W2.
#L #K #V1 #W1 #W2 #i #HLK #HVW1 #HW12
lapply (ldrop_fwd_ldrop2_length … HLK) #Hi
lemma cpr_inv_lref1: ∀L,T2,i. L ⊢ #i ➡ T2 →
T2 = #i ∨
∃∃K,V1,T1. ⇩[0, i] L ≡ K. ⓓV1 &
- K ⊢ V1 [0, |L| - i - 1] ▶* T1 &
+ K ⊢ V1 ▶* [0, |L| - i - 1] T1 &
⇧[0, i + 1] T1 ≡ T2 &
i < |L|.
#L #T2 #i * #X #H
(* Note: we could invoke tpss_weak_all instead of ltpr_fwd_length *)
(* Basic_1: was only: pr2_subst1 *)
lemma cpr_tpss_ltpr: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 →
- ∀d,e,U1. L1 ⊢ T1 [d, e] ▶* U1 →
- ∃∃U2. L2 ⊢ U1 ➡ U2 & L2 ⊢ T2 [d, e] ▶* U2.
+ ∀d,e,U1. L1 ⊢ T1 ▶* [d, e] U1 →
+ ∃∃U2. L2 ⊢ U1 ➡ U2 & L2 ⊢ T2 ▶* [d, e] U2.
#L1 #L2 #HL12 #T1 #T2 * #T #HT1 #HT2 #d #e #U1 #HTU1
elim (tpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 -HT1 #U #HU1 #HTU
elim (tpss_conf_eq … HT2 … HTU) -T /3 width=3/
qed.
lemma cpr_ltpr_conf_tpss: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L1 ⊢ T1 ➡ T2 →
- ∀d,e,U1. L1 ⊢ T1 [d, e] ▶* U1 →
+ ∀d,e,U1. L1 ⊢ T1 ▶* [d, e] U1 →
∃∃U2. L2 ⊢ U1 ➡ U2 & L2 ⊢ T2 ➡ U2.
#L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1
elim (cpr_ltpr_conf_eq … HT12 … HL12) -HT12 #T #HT1 #HT2
(* Properties concerning partial unfold on local environments ***************)
-lemma ltpss_cpr_trans: ∀L1,L2,d,e. L1 [d, e] ▶* L2 →
+lemma ltpss_cpr_trans: ∀L1,L2,d,e. L1 ▶* [d, e] L2 →
∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡ T2.
#L1 #L2 #d #e #HL12 #T1 #T2 *
lapply (ltpss_weak_all … HL12)
(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
definition lcpr: relation lenv ≝
- λL1,L2. ∃∃L. L1 ➡ L & L [0, |L|] ▶* L2
+ λL1,L2. ∃∃L. L1 ➡ L & L ▶* [0, |L|] L2
.
interpretation
(* Properties concerning parallel unfold on local environments **************)
-lemma ltpr_ltpss_conf: ∀L1,K1,d,e. L1 [d, e] ▶* K1 → ∀L2. L1 ➡ L2 →
- ∃∃K2. L2 [d, e] ▶* K2 & K1 ➡ K2.
+lemma ltpr_ltpss_conf: ∀L1,K1,d,e. L1 ▶* [d, e] K1 → ∀L2. L1 ➡ L2 →
+ ∃∃K2. L2 ▶* [d, e] K2 & K1 ➡ K2.
#L1 #K1 #d #e #H elim H -L1 -K1 -d -e
[ /2 width=3/
| #L1 #I #V1 #X #H
(* Properties concerning parallel substitution on terms *********************)
-lemma ltpr_tps_trans: ∀L2,T1,T2,d,e. L2 ⊢ T1 [d, e] ▶ T2 → ∀L1. L1 ➡ L2 →
- ∃∃T. L1 ⊢ T1 [d, e] ▶ T & T ➡ T2.
+lemma ltpr_tps_trans: ∀L2,T1,T2,d,e. L2 ⊢ T1 ▶ [d, e] T2 → ∀L1. L1 ➡ L2 →
+ ∃∃T. L1 ⊢ T1 ▶ [d, e] T & T ➡ T2.
#L2 #T1 #T2 #d #e #H elim H -L2 -T1 -T2 -d -e
[ /2 width=3/
| #L2 #K2 #V2 #W2 #i #d #e #Hdi #Hide #HLK2 #HVW2 #L1 #HL12
]
qed.
-lemma ltpr_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶ T2 → ∀L2. L1 ➡ L2 →
- ∃∃T. L2 ⊢ T1 [d, e] ▶ T & T2 ➡ T.
+lemma ltpr_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶ [d, e] T2 → ∀L2. L1 ➡ L2 →
+ ∃∃T. L2 ⊢ T1 ▶ [d, e] T & T2 ➡ T.
#L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e
[ /2 width=3/
| #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #L2 #HL12
(* CONTEXT-FREE IRREDUCIBLE TERMS *******************************************)
-definition tif: predicate term ≝ λT. 𝐑[T] → False.
+definition tif: predicate term ≝ λT. 𝐑[T] → ⊥.
interpretation "context-free irreducibility (term)"
'NotReducible T = (tif T).
(* Basic inversion lemmas ***************************************************)
-lemma tif_inv_abbr: ∀V,T. 𝐈[ⓓV.T] → False.
+lemma tif_inv_abbr: ∀V,T. 𝐈[ⓓV.T] → ⊥.
/2 width=1/ qed-.
lemma tif_inv_abst: ∀V,T. 𝐈[ⓛV.T] → 𝐈[V] ∧ 𝐈[T].
* // * #U #T #_ #_ #H elim (H ?) -H /2 width=1/
qed-.
-lemma tif_inv_cast: ∀V,T. 𝐈[ⓣV.T] → False.
+lemma tif_inv_cast: ∀V,T. 𝐈[ⓣV.T] → ⊥.
/2 width=1/ qed-.
(* Basic properties *********************************************************)
]
qed-.
-lemma tnf_inv_abbr: ∀V,T. 𝐍[ⓓV.T] → False.
+lemma tnf_inv_abbr: ∀V,T. 𝐍[ⓓV.T] → ⊥.
#V #T #H elim (is_lift_dec T 0 1)
[ * #U #HTU
lapply (H U ?) -H /2 width=3/ #H destruct
]
qed.
-lemma tnf_inv_cast: ∀V,T. 𝐍[ⓣV.T] → False.
+lemma tnf_inv_cast: ∀V,T. 𝐍[ⓣV.T] → ⊥.
#V #T #H lapply (H T ?) -H /2 width=1/ #H
-@(discr_tpair_xy_y … H)
+@discr_tpair_xy_y //
qed-.
qed.
theorem tif_tnf: ∀T1. 𝐈[T1] → 𝐍[T1].
-/2 width=1/ qed.
+/3 width=1/ qed.
(* Note: this property is unusual *)
-lemma tnf_trf_false: ∀T1. 𝐑[T1] → 𝐍[T1] → False.
+lemma tnf_trf_false: ∀T1. 𝐑[T1] → 𝐍[T1] → ⊥.
#T1 #H elim H -T1
[ #V #T #_ #IHV #H elim (tnf_inv_abst … H) -H /2 width=1/
| #V #T #_ #IHT #H elim (tnf_inv_abst … H) -H /2 width=1/
| tpr_beta : ∀V1,V2,W,T1,T2.
tpr V1 V2 → tpr T1 T2 → tpr (ⓐV1. ⓛW. T1) (ⓓV2. T2)
| tpr_delta: ∀I,V1,V2,T1,T2,T.
- tpr V1 V2 → tpr T1 T2 → ⋆. ⓑ{I} V2 ⊢ T2 [0, 1] ▶ T →
+ tpr V1 V2 → tpr T1 T2 → ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] T →
tpr (ⓑ{I} V1. T1) (ⓑ{I} V2. T)
| tpr_theta: ∀V,V1,V2,W1,W2,T1,T2.
tpr V1 V2 → ⇧[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 →
(* Basic properties *********************************************************)
-lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ➡ V2 → T1 ➡ T2 →
- ⓑ{I} V1. T1 ➡ ⓑ{I} V2. T2.
+lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ➡ V2 → T1 ➡ T2 → ⓑ{I} V1. T1 ➡ ⓑ{I} V2. T2.
/2 width=3/ qed.
(* Basic_1: was by definition: pr0_refl *)
fact tpr_inv_bind1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,T1. U1 = ⓑ{I} V1. T1 →
(∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
- ⋆. ⓑ{I} V2 ⊢ T2 [0, 1] ▶ T &
+ ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] T &
U2 = ⓑ{I} V2. T
) ∨
∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2 & I = Abbr.
lemma tpr_inv_bind1: ∀V1,T1,U2,I. ⓑ{I} V1. T1 ➡ U2 →
(∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
- ⋆. ⓑ{I} V2 ⊢ T2 [0, 1] ▶ T &
+ ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] T &
U2 = ⓑ{I} V2. T
) ∨
∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2 & I = Abbr.
(* Basic_1: was pr0_gen_abbr *)
lemma tpr_inv_abbr1: ∀V1,T1,U2. ⓓV1. T1 ➡ U2 →
(∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
- ⋆. ⓓV2 ⊢ T2 [0, 1] ▶ T &
+ ⋆. ⓓV2 ⊢ T2 ▶ [0, 1] T &
U2 = ⓓV2. T
) ∨
∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2.
∃∃X. X1 ➡ X & X2 ➡ X
) →
V0 ➡ V1 → V0 ➡ V2 → T0 ➡ T1 → T0 ➡ T2 →
- ⋆. ⓑ{I1} V1 ⊢ T1 [O, 1] ▶ TT1 →
- ⋆. ⓑ{I1} V2 ⊢ T2 [O, 1] ▶ TT2 →
+ ⋆. ⓑ{I1} V1 ⊢ T1 ▶ [O, 1] TT1 →
+ ⋆. ⓑ{I1} V2 ⊢ T2 ▶ [O, 1] TT2 →
∃∃X. ⓑ{I1} V1. TT1 ➡ X & ⓑ{I1} V2. TT2 ➡ X.
#I1 #V0 #V1 #T0 #T1 #TT1 #V2 #T2 #TT2 #IH #HV01 #HV02 #HT01 #HT02 #HTT1 #HTT2
elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
- V0 ➡ V1 → T0 ➡ T1 → ⋆. ⓓV1 ⊢ T1 [O,1] ▶ TT1 →
+ V0 ➡ V1 → T0 ➡ T1 → ⋆. ⓓV1 ⊢ T1 ▶ [O,1] TT1 →
T2 ➡ X2 → ⇧[O, 1] T2 ≡ T0 →
∃∃X. ⓓV1. TT1 ➡ X & X2 ➡ X.
#X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HTX2 #HTT20
(* Basic_1: was: pr0_subst1 *)
lemma tpr_tps_ltpr: ∀T1,T2. T1 ➡ T2 →
- ∀L1,d,e,U1. L1 ⊢ T1 [d, e] ▶ U1 →
+ ∀L1,d,e,U1. L1 ⊢ T1 ▶ [d, e] U1 →
∀L2. L1 ➡ L2 →
- ∃∃U2. U1 ➡ U2 & L2 ⊢ T2 [d, e] ▶* U2.
+ ∃∃U2. U1 ➡ U2 & L2 ⊢ T2 ▶* [d, e] U2.
#T1 #T2 #H elim H -T1 -T2
[ #I #L1 #d #e #X #H
elim (tps_inv_atom1 … H) -H
qed.
lemma tpr_tps_bind: ∀I,V1,V2,T1,T2,U1. V1 ➡ V2 → T1 ➡ T2 →
- ⋆. ⓑ{I} V1 ⊢ T1 [0, 1] ▶ U1 →
- ∃∃U2. U1 ➡ U2 & ⋆. ⓑ{I} V2 ⊢ T2 [0, 1] ▶ U2.
+ ⋆. ⓑ{I} V1 ⊢ T1 ▶ [0, 1] U1 →
+ ∃∃U2. U1 ➡ U2 & ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] U2.
#I #V1 #V2 #T1 #T2 #U1 #HV12 #HT12 #HTU1
elim (tpr_tps_ltpr … HT12 … HTU1 (⋆. ⓑ{I} V2) ?) -T1 /2 width=1/ /3 width=3/
qed.
lemma tpr_tpss_ltpr: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. T1 ➡ T2 →
- ∀d,e,U1. L1 ⊢ T1 [d, e] ▶* U1 →
- ∃∃U2. U1 ➡ U2 & L2 ⊢ T2 [d, e] ▶* U2.
+ ∀d,e,U1. L1 ⊢ T1 ▶* [d, e] U1 →
+ ∃∃U2. U1 ➡ U2 & L2 ⊢ T2 ▶* [d, e] U2.
#L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1 @(tpss_ind … HTU1) -U1
[ /2 width=3/
| -HT12 #U #U1 #_ #HU1 * #T #HUT #HT2
qed.
lemma tpr_tpss_conf: ∀T1,T2. T1 ➡ T2 →
- ∀L,U1,d,e. L ⊢ T1 [d, e] ▶* U1 →
- ∃∃U2. U1 ➡ U2 & L ⊢ T2 [d, e] ▶* U2.
+ ∀L,U1,d,e. L ⊢ T1 ▶* [d, e] U1 →
+ ∃∃U2. U1 ➡ U2 & L ⊢ T2 ▶* [d, e] U2.
/2 width=5/ qed.
(* Basic inversion lemmas ***************************************************)
-fact trf_inv_atom_aux: ∀I,T. 𝐑[T] → T = ⓪{I} → False.
+fact trf_inv_atom_aux: ∀I,T. 𝐑[T] → T = ⓪{I} → ⊥.
#I #T * -T
[ #V #T #_ #H destruct
| #V #T #_ #H destruct
]
qed.
-lemma trf_inv_atom: ∀I. 𝐑[⓪{I}] → False.
+lemma trf_inv_atom: ∀I. 𝐑[⓪{I}] → ⊥.
/2 width=4/ qed-.
fact trf_inv_abst_aux: ∀W,U,T. 𝐑[T] → T = ⓛW. U → 𝐑[W] ∨ 𝐑[U].
/2 width=3/ qed-.
fact trf_inv_appl_aux: ∀W,U,T. 𝐑[T] → T = ⓐW. U →
- ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → False).
+ ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → ⊥).
#W #U #T * -T
[ #V #T #_ #H destruct
| #V #T #_ #H destruct
]
qed.
-lemma trf_inv_appl: ∀W,U. 𝐑[ⓐW.U] → ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → False).
+lemma trf_inv_appl: ∀W,U. 𝐑[ⓐW.U] → ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → ⊥).
/2 width=3/ qed-.
qed.
lemma twhnf_tshf: ∀T. T ≈ T → 𝐖𝐇𝐍[T].
-/2 width=1/ qed.
+/3 width=1/ qed.
(* Properties about parallel unfold *****************************************)
(* Note: lemma 500 *)
-lemma aaa_ltpss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2,d,e. L1 [d, e] ▶* L2 →
- ∀T2. L2 ⊢ T1 [d, e] ▶* T2 → L2 ⊢ T2 ⁝ A.
+lemma aaa_ltpss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2,d,e. L1 ▶* [d, e] L2 →
+ ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → L2 ⊢ T2 ⁝ A.
#L1 #T1 #A #H elim H -L1 -T1 -A
[ #L1 #k #L2 #d #e #_ #T2 #H
>(tpss_inv_sort1 … H) -H //
]
qed.
-lemma aaa_ltpss_tps_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2,d,e. L1 [d, e] ▶* L2 →
- ∀T2. L2 ⊢ T1 [d, e] ▶ T2 → L2 ⊢ T2 ⁝ A.
+lemma aaa_ltpss_tps_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2,d,e. L1 ▶* [d, e] L2 →
+ ∀T2. L2 ⊢ T1 ▶ [d, e] T2 → L2 ⊢ T2 ⁝ A.
/3 width=7/ qed.
lemma aaa_ltpss_conf: ∀L1,T,A. L1 ⊢ T ⁝ A →
- ∀L2,d,e. L1 [d, e] ▶* L2 → L2 ⊢ T ⁝ A.
+ ∀L2,d,e. L1 ▶* [d, e] L2 → L2 ⊢ T ⁝ A.
/2 width=7/ qed.
lemma aaa_tpss_conf: ∀L,T1,A. L ⊢ T1 ⁝ A →
- ∀T2,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ T2 ⁝ A.
+ ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 → L ⊢ T2 ⁝ A.
/2 width=7/ qed.
lemma aaa_tps_conf: ∀L,T1,A. L ⊢ T1 ⁝ A →
- ∀T2,d,e. L ⊢ T1 [d, e] ▶ T2 → L ⊢ T2 ⁝ A.
+ ∀T2,d,e. L ⊢ T1 ▶ [d, e] T2 → L ⊢ T2 ⁝ A.
/2 width=7/ qed.
(**************************************************************************)
include "basic_2/grammar/cl_weight.ma".
-include "basic_2/grammar/lsubs.ma".
include "basic_2/substitution/lift.ma".
+include "basic_2/substitution/lsubs.ma".
(* LOCAL ENVIRONMENT SLICING ************************************************)
]
qed.
-lemma ldrop_lsubs_ldrop1_abbr: ∀L1,L2,d,e. L1 [d, e] ≼ L2 →
+lemma ldrop_lsubs_ldrop1_abbr: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
∀K1,V,i. ⇩[0, i] L1 ≡ K1. ⓓV →
d ≤ i → i < d + e →
- ∃∃K2. K1 [0, d + e - i - 1] ≼ K2 &
+ ∃∃K2. K1 ≼ [0, d + e - i - 1] K2 &
⇩[0, i] L2 ≡ K2. ⓓV.
#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
[ #d #e #K1 #V #i #H
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/substitution/lsubs_sfr.ma".
+include "basic_2/substitution/ldrop.ma".
+
+(* DROPPING *****************************************************************)
+
+(* Properties about local env. full refinement for substitution *************)
+
+lemma sfr_ldrop: ∀L,d,e.
+ (∀I,K,V,i. d ≤ i → i < d + e → ⇩[0, i] L ≡ K. ⓑ{I}V → I = Abbr) →
+ ≼ [d, e] L.
+#L elim L -L //
+#L #I #V #IHL #d @(nat_ind_plus … d) -d
+[ #e @(nat_ind_plus … e) -e //
+ #e #_ #HH
+ >(HH I L V 0 ? ? ?) // /5 width=6/
+| /5 width=6/
+]
+qed.
+
+(* Inversion lemmas about local env. full refinement for substitution *******)
+
+lemma sfr_inv_ldrop: ∀I,L,K,V,i. ⇩[0, i] L ≡ K. ⓑ{I}V → ∀d,e. ≼ [d, e] L →
+ d ≤ i → i < d + e → I = Abbr.
+#I #L elim L -L
+[ #K #V #i #H
+ lapply (ldrop_inv_atom1 … H) -H #H destruct
+| #L #J #W #IHL #K #V #i #H
+ elim (ldrop_inv_O1 … H) -H *
+ [ -IHL #H1 #H2 #d #e #HL #Hdi #Hide destruct
+ lapply (le_n_O_to_eq … Hdi) -Hdi #H destruct
+ lapply (HL … (L.ⓓW) ?) -HL /2 width=1/ #H
+ elim (lsubs_inv_abbr1 … H ?) -H // -Hide #K #_ #H destruct //
+ | #Hi #HLK #d @(nat_ind_plus … d) -d
+ [ #e #H #_ #Hide
+ elim (sfr_inv_bind … H ?) -H [2: /2 width=2/ ] #HL #H destruct
+ @(IHL … HLK … HL) -IHL -HLK -HL // /2 width=1/
+ | #d #_ #e #H #Hdi #Hide
+ lapply (sfr_inv_skip … H ?) -H // #HL
+ @(IHL … HLK … HL) -IHL -HLK -HL /2 width=1/
+ ]
+ ]
+]
+qed-.
(* Basic_1: was: lift_gen_lref_false *)
lemma lift_inv_lref2_be: ∀d,e,T1,i. ⇧[d,e] T1 ≡ #i →
- d ≤ i → i < d + e → False.
+ d ≤ i → i < d + e → ⊥.
#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
T1 = ⓕ{I} V1. U1.
/2 width=3/ qed-.
-lemma lift_inv_pair_xy_x: ∀d,e,I,V,T. ⇧[d, e] ②{I} V. T ≡ V → False.
+lemma lift_inv_pair_xy_x: ∀d,e,I,V,T. ⇧[d, e] ②{I} V. T ≡ V → ⊥.
#d #e #J #V elim V -V
[ * #i #T #H
[ lapply (lift_inv_sort2 … H) -H #H destruct
]
qed-.
-lemma lift_inv_pair_xy_y: ∀I,T,V,d,e. ⇧[d, e] ②{I} V. T ≡ T → False.
+lemma lift_inv_pair_xy_y: ∀I,T,V,d,e. ⇧[d, e] ②{I} V. T ≡ T → ⊥.
#J #T elim T -T
[ * #i #V #d #e #H
[ lapply (lift_inv_sort2 … H) -H #H destruct
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/grammar/lenv_length.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
+
+inductive lsubs: nat → nat → relation lenv ≝
+| lsubs_sort: ∀d,e. lsubs d e (⋆) (⋆)
+| lsubs_OO: ∀L1,L2. lsubs 0 0 L1 L2
+| lsubs_abbr: ∀L1,L2,V,e. lsubs 0 e L1 L2 →
+ lsubs 0 (e + 1) (L1. ⓓV) (L2.ⓓV)
+| lsubs_abst: ∀L1,L2,I,V1,V2,e. lsubs 0 e L1 L2 →
+ lsubs 0 (e + 1) (L1. ⓛV1) (L2.ⓑ{I} V2)
+| lsubs_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
+ lsubs d e L1 L2 → lsubs (d + 1) e (L1. ⓑ{I1} V1) (L2. ⓑ{I2} V2)
+.
+
+interpretation
+ "local environment refinement (substitution)"
+ 'SubEq L1 d e L2 = (lsubs d e L1 L2).
+
+definition lsubs_conf: ∀S. (lenv → relation S) → Prop ≝ λS,R.
+ ∀L1,s1,s2. R L1 s1 s2 →
+ ∀L2,d,e. L1 ≼ [d, e] L2 → R L2 s1 s2.
+
+(* Basic properties *********************************************************)
+
+lemma lsubs_bind_eq: ∀L1,L2,e. L1 ≼ [0, e] L2 → ∀I,V.
+ L1. ⓑ{I} V ≼ [0, e + 1] L2.ⓑ{I} V.
+#L1 #L2 #e #HL12 #I #V elim I -I /2 width=1/
+qed.
+
+lemma lsubs_abbr_lt: ∀L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e →
+ L1. ⓓV ≼ [0, e] L2.ⓓV.
+#L1 #L2 #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
+qed.
+
+lemma lsubs_abst_lt: ∀L1,L2,I,V1,V2,e. L1 ≼ [0, e - 1] L2 → 0 < e →
+ L1. ⓛV1 ≼ [0, e] L2.ⓑ{I} V2.
+#L1 #L2 #I #V1 #V2 #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
+qed.
+
+lemma lsubs_skip_lt: ∀L1,L2,d,e. L1 ≼ [d - 1, e] L2 → 0 < d →
+ ∀I1,I2,V1,V2. L1. ⓑ{I1} V1 ≼ [d, e] L2. ⓑ{I2} V2.
+#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) // /2 width=1/
+qed.
+
+lemma lsubs_bind_lt: ∀I,L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e →
+ L1. ⓑ{I}V ≼ [0, e] L2.ⓓV.
+* /2 width=1/ qed.
+
+lemma lsubs_refl: ∀d,e,L. L ≼ [d, e] L.
+#d elim d -d
+[ #e elim e -e // #e #IHe #L elim L -L // /2 width=1/
+| #d #IHd #e #L elim L -L // /2 width=1/
+]
+qed.
+
+lemma TC_lsubs_conf: ∀S,R. lsubs_conf S R → lsubs_conf S (λL. (TC … (R L))).
+#S #R #HR #L1 #s1 #s2 #H elim H -s2
+[ /3 width=5/
+| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12
+ lapply (HR … Hs2 … HL12) -HR -Hs2 -HL12 /3 width=3/
+]
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubs_inv_atom1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L1 = ⋆ →
+ L2 = ⋆ ∨ (d = 0 ∧ e = 0).
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ /2 width=1/
+| /3 width=1/
+| #L1 #L2 #W #e #_ #H destruct
+| #L1 #L2 #I #W1 #W2 #e #_ #H destruct
+| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #H destruct
+]
+qed.
+
+lemma lsubs_inv_atom1: ∀L2,d,e. ⋆ ≼ [d, e] L2 →
+ L2 = ⋆ ∨ (d = 0 ∧ e = 0).
+/2 width=3/ qed-.
+
+fact lsubs_inv_abbr1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+ ∀K1,V. L1 = K1.ⓓV → d = 0 → 0 < e →
+ ∃∃K2. K1 ≼ [0, e - 1] K2 & L2 = K2.ⓓV.
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ #d #e #K1 #V #H destruct
+| #L1 #L2 #K1 #V #_ #_ #H
+ elim (lt_zero_false … H)
+| #L1 #L2 #W #e #HL12 #K1 #V #H #_ #_ destruct /2 width=3/
+| #L1 #L2 #I #W1 #W2 #e #_ #K1 #V #H destruct
+| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #K1 #V #_ >commutative_plus normalize #H destruct
+]
+qed.
+
+lemma lsubs_inv_abbr1: ∀K1,L2,V,e. K1.ⓓV ≼ [0, e] L2 → 0 < e →
+ ∃∃K2. K1 ≼ [0, e - 1] K2 & L2 = K2.ⓓV.
+/2 width=5/ qed-.
+
+fact lsubs_inv_skip1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+ ∀I1,K1,V1. L1 = K1.ⓑ{I1}V1 → 0 < d →
+ ∃∃I2,K2,V2. K1 ≼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ #d #e #I1 #K1 #V1 #H destruct
+| #L1 #L2 #I1 #K1 #V1 #_ #H
+ elim (lt_zero_false … H)
+| #L1 #L2 #W #e #_ #I1 #K1 #V1 #_ #H
+ elim (lt_zero_false … H)
+| #L1 #L2 #I #W1 #W2 #e #_ #I1 #K1 #V1 #_ #H
+ elim (lt_zero_false … H)
+| #L1 #L2 #J1 #J2 #W1 #W2 #d #e #HL12 #I1 #K1 #V1 #H #_ destruct /2 width=5/
+]
+qed.
+
+lemma lsubs_inv_skip1: ∀I1,K1,L2,V1,d,e. K1.ⓑ{I1}V1 ≼ [d, e] L2 → 0 < d →
+ ∃∃I2,K2,V2. K1 ≼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
+/2 width=5/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+fact lsubs_fwd_length_full1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+ d = 0 → e = |L1| → |L1| ≤ |L2|.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
+[ //
+| /2 width=1/
+| /3 width=1/
+| /3 width=1/
+| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct
+]
+qed.
+
+lemma lsubs_fwd_length_full1: ∀L1,L2. L1 ≼ [0, |L1|] L2 → |L1| ≤ |L2|.
+/2 width=5/ qed-.
+
+fact lsubs_fwd_length_full2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+ d = 0 → e = |L2| → |L2| ≤ |L1|.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
+[ //
+| /2 width=1/
+| /3 width=1/
+| /3 width=1/
+| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct
+]
+qed.
+
+lemma lsubs_fwd_length_full2: ∀L1,L2. L1 ≼ [0, |L2|] L2 → |L2| ≤ |L1|.
+/2 width=5/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/substitution/lsubs.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
+
+(* top element of the refinement *)
+definition sfr: nat → nat → predicate lenv ≝
+ λd,e. NF … (lsubs d e) (lsubs d e …).
+
+interpretation
+ "local environment full refinement (substitution)"
+ 'SubEqTop d e L = (sfr d e L).
+
+(* Basic properties *********************************************************)
+
+lemma sfr_atom: ∀d,e. ≼ [d, e] ⋆.
+#d #e #L #H
+elim (lsubs_inv_atom1 … H) -H
+[ #H destruct //
+| * #H1 #H2 destruct //
+]
+qed.
+
+lemma sfr_OO: ∀L. ≼ [0, 0] L.
+// qed.
+
+lemma sfr_abbr: ∀L,V,e. ≼ [0, e] L → ≼ [0, e + 1] L.ⓓV.
+#L #V #e #HL #K #H
+elim (lsubs_inv_abbr1 … H ?) -H // <minus_plus_m_m #X #HLX #H destruct
+lapply (HL … HLX) -HL -HLX /2 width=1/
+qed.
+
+lemma sfr_skip: ∀I,L,V,d,e. ≼ [d, e] L → ≼ [d + 1, e] L.ⓑ{I}V.
+#I #L #V #d #e #HL #K #H
+elim (lsubs_inv_skip1 … H ?) -H // <minus_plus_m_m #J #X #W #HLX #H destruct
+lapply (HL … HLX) -HL -HLX /2 width=1/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma sfr_inv_bind: ∀I,L,V,e. ≼ [0, e] L.ⓑ{I}V → 0 < e →
+ ≼ [0, e - 1] L ∧ I = Abbr.
+#I #L #V #e #HL #He
+lapply (HL (L.ⓓV) ?) /2 width=1/ #H
+elim (lsubs_inv_abbr1 … H ?) -H // #K #_ #H destruct
+@conj // #L #HKL
+lapply (HL (L.ⓓV) ?) -HL /2 width=1/ -HKL #H
+elim (lsubs_inv_abbr1 … H ?) -H // -He #X #HLX #H destruct //
+qed-.
+
+lemma sfr_inv_skip: ∀I,L,V,d,e. ≼ [d, e] L.ⓑ{I}V → 0 < d → ≼ [d - 1, e] L.
+#I #L #V #d #e #HL #Hd #K #HLK
+lapply (HL (K.ⓑ{I}V) ?) -HL /2 width=1/ -HLK #H
+elim (lsubs_inv_skip1 … H ?) -H // -Hd #J #X #W #HKX #H destruct //
+qed-.
(* Basic properties *********************************************************)
-lemma tps_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶ T2 →
- ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ▶ T2.
+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 -L1 -T1 -T2 -d -e
[ //
| #L1 #K1 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12
]
qed.
-lemma tps_refl: ∀T,L,d,e. L ⊢ T [d, e] ▶ T.
+lemma tps_refl: ∀T,L,d,e. L ⊢ T ▶ [d, e] T.
#T elim T -T //
#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. ⓓV) →
- ∃∃T2,T. L ⊢ T1 [d, 1] ▶ T2 & ⇧[d, 1] T ≡ T2.
+ ∃∃T2,T. L ⊢ T1 ▶ [d, 1] T2 & ⇧[d, 1] T ≡ T2.
#K #V #T1 elim T1 -T1
[ * #i #L #d #HLK /2 width=4/
elim (lt_or_eq_or_gt i d) #Hid /3 width=4/
]
qed.
-lemma tps_weak: ∀L,T1,T2,d1,e1. L ⊢ T1 [d1, e1] ▶ T2 →
+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 ▶ [d2, e2] T2.
#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
qed.
lemma tps_weak_top: ∀L,T1,T2,d,e.
- L ⊢ T1 [d, e] ▶ T2 → L ⊢ T1 [d, |L| - d] ▶ T2.
+ L ⊢ T1 ▶ [d, e] T2 → L ⊢ T1 ▶ [d, |L| - d] T2.
#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e
[ //
| #L #K #V #W #i #d #e #Hdi #_ #HLK #HVW
qed.
lemma tps_weak_all: ∀L,T1,T2,d,e.
- L ⊢ T1 [d, e] ▶ T2 → L ⊢ T1 [0, |L|] ▶ T2.
+ L ⊢ T1 ▶ [d, e] T2 → L ⊢ T1 ▶ [0, |L|] T2.
#L #T1 #T2 #d #e #HT12
lapply (tps_weak … HT12 0 (d + e) ? ?) -HT12 // #HT12
lapply (tps_weak_top … HT12) //
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.
+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 -L -T1 -T2 -d -e
[ /2 width=3/
| #L #K #V #W #i #d #e #Hdi #Hide #HLK #HVW #j #Hdj #Hjde
(* Basic inversion lemmas ***************************************************)
-fact tps_inv_atom1_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶ T2 → ∀I. T1 = ⓪{I} →
+fact tps_inv_atom1_aux: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → ∀I. T1 = ⓪{I} →
T2 = ⓪{I} ∨
∃∃K,V,i. d ≤ i & i < d + e &
⇩[O, i] L ≡ K. ⓓV &
]
qed.
-lemma tps_inv_atom1: ∀L,T2,I,d,e. L ⊢ ⓪{I} [d, e] ▶ T2 →
+lemma tps_inv_atom1: ∀L,T2,I,d,e. L ⊢ ⓪{I} ▶ [d, e] T2 →
T2 = ⓪{I} ∨
∃∃K,V,i. d ≤ i & i < d + e &
⇩[O, i] L ≡ K. ⓓV &
(* Basic_1: was: subst1_gen_sort *)
-lemma tps_inv_sort1: ∀L,T2,k,d,e. L ⊢ ⋆k [d, e] ▶ T2 → T2 = ⋆k.
+lemma tps_inv_sort1: ∀L,T2,k,d,e. L ⊢ ⋆k ▶ [d, e] T2 → T2 = ⋆k.
#L #T2 #k #d #e #H
elim (tps_inv_atom1 … H) -H //
* #K #V #i #_ #_ #_ #_ #H destruct
qed-.
(* Basic_1: was: subst1_gen_lref *)
-lemma tps_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ▶ T2 →
+lemma tps_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i ▶ [d, e] T2 →
T2 = #i ∨
∃∃K,V. d ≤ i & i < d + e &
⇩[O, i] L ≡ K. ⓓV &
* #K #V #j #Hdj #Hjde #HLK #HVT2 #H destruct /3 width=4/
qed-.
-lemma tps_inv_gref1: ∀L,T2,p,d,e. L ⊢ §p [d, e] ▶ T2 → T2 = §p.
+lemma tps_inv_gref1: ∀L,T2,p,d,e. L ⊢ §p ▶ [d, e] T2 → T2 = §p.
#L #T2 #p #d #e #H
elim (tps_inv_atom1 … H) -H //
* #K #V #i #_ #_ #_ #_ #H destruct
qed-.
-fact tps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ▶ U2 →
+fact tps_inv_bind1_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. ⓑ{I} V2 ⊢ T1 [d + 1, e] ▶ T2 &
+ ∃∃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
[ #L #k #d #e #I #V1 #T1 #H destruct
]
qed.
-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 &
+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 width=3/ qed-.
-fact tps_inv_flat1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ▶ U2 →
+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 &
+ ∃∃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
[ #L #k #d #e #I #V1 #T1 #H destruct
]
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 &
+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 width=3/ qed-.
-fact tps_inv_refl_O2_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶ T2 → e = 0 → T1 = T2.
+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 -L -T1 -T2 -d -e
[ //
| #L #K #V #W #i #d #e #Hdi #Hide #_ #_ #H destruct
]
qed.
-lemma tps_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ▶ T2 → T1 = T2.
+lemma tps_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 ▶ [d, 0] T2 → T1 = T2.
/2 width=6/ qed-.
(* Basic forward lemmas *****************************************************)
-lemma tps_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶ T2 → #[T1] ≤ #[T2].
+lemma tps_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → #[T1] ≤ #[T2].
#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-.
(* Advanced inversion lemmas ************************************************)
-fact tps_inv_S2_aux: ∀L,T1,T2,d,e1. L ⊢ T1 [d, e1] ▶ T2 → ∀e2. e1 = e2 + 1 →
- ∀K,V. ⇩[0, d] L ≡ K. ⓛV → L ⊢ T1 [d + 1, e2] ▶ T2.
+fact tps_inv_S2_aux: ∀L,T1,T2,d,e1. L ⊢ T1 ▶ [d, e1] T2 → ∀e2. e1 = e2 + 1 →
+ ∀K,V. ⇩[0, d] L ≡ K. ⓛV → L ⊢ T1 ▶ [d + 1, e2] T2.
#L #T1 #T2 #d #e1 #H elim H -L -T1 -T2 -d -e1
[ //
| #L #K0 #V0 #W #i #d #e1 #Hdi #Hide1 #HLK0 #HV0 #e2 #He12 #K #V #HLK destruct
]
qed.
-lemma tps_inv_S2: ∀L,T1,T2,d,e. L ⊢ T1 [d, e + 1] ▶ T2 →
- ∀K,V. ⇩[0, d] L ≡ K. ⓛV → L ⊢ T1 [d + 1, e] ▶ T2.
+lemma tps_inv_S2: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e + 1] T2 →
+ ∀K,V. ⇩[0, d] L ≡ K. ⓛV → L ⊢ T1 ▶ [d + 1, e] T2.
/2 width=3/ qed-.
-lemma tps_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ▶ T2 →
+lemma tps_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 ▶ [d, 1] T2 →
∀K,V. ⇩[0, d] L ≡ K. ⓛV → T1 = T2.
#L #T1 #T2 #d #HT12 #K #V #HLK
lapply (tps_inv_S2 … T1 T2 … 0 … HLK) -K // -HT12 #HT12
(* Relocation properties ****************************************************)
(* Basic_1: was: subst1_lift_lt *)
-lemma tps_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶ T2 →
+lemma tps_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 ▶ [dt, et] T2 →
∀L,U1,U2,d,e. ⇩[d, e] L ≡ K →
⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 →
dt + et ≤ d →
- L ⊢ U1 [dt, et] ▶ U2.
+ L ⊢ U1 ▶ [dt, et] U2.
#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 //
]
qed.
-lemma tps_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶ T2 →
+lemma tps_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 ▶ [dt, et] T2 →
∀L,U1,U2,d,e. ⇩[d, e] L ≡ K →
⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 →
dt ≤ d → d ≤ dt + et →
- L ⊢ U1 [dt, et + e] ▶ U2.
+ L ⊢ U1 ▶ [dt, et + e] U2.
#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 //
qed.
(* Basic_1: was: subst1_lift_ge *)
-lemma tps_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶ T2 →
+lemma tps_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 ▶ [dt, et] T2 →
∀L,U1,U2,d,e. ⇩[d, e] L ≡ K →
⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 →
d ≤ dt →
- L ⊢ U1 [dt + e, et] ▶ U2.
+ L ⊢ U1 ▶ [dt + e, et] U2.
#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 //
qed.
(* Basic_1: was: subst1_gen_lift_lt *)
-lemma tps_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶ U2 →
+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.
+ ∃∃T2. K ⊢ T1 ▶ [dt, et] T2 & ⇧[d, e] T2 ≡ U2.
#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 /2 width=3/
]
qed.
-lemma tps_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶ U2 →
+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.
+ ∃∃T2. K ⊢ T1 ▶ [dt, et - e] T2 & ⇧[d, e] T2 ≡ U2.
#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 /2 width=3/
qed.
(* Basic_1: was: subst1_gen_lift_ge *)
-lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶ U2 →
+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.
+ ∃∃T2. K ⊢ T1 ▶ [dt - e, et] T2 & ⇧[d, e] T2 ≡ U2.
#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 /2 width=3/
(* 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 ▶ [d, e] U2 → ∀T1. ⇧[d, e] T1 ≡ U1 → U1 = U2.
#L #U1 #U2 #d #e #H elim H -L -U1 -U2 -d -e
[ //
| #L #K #V #W #i #d #e #Hdi #Hide #_ #_ #T1 #H
(le d i) -> (lt i (plus d h)) ->
(EX u1 | t1 = (lift (minus (plus d h) (S i)) (S i) u1)).
*)
-lemma tps_inv_lift1_ge_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶ U2 →
+lemma tps_inv_lift1_ge_up: ∀L,U1,U2,dt,et. L ⊢ U1 ▶ [dt, et] U2 →
∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →
- ∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ▶ T2 & ⇧[d, e] T2 ≡ U2.
+ ∃∃T2. K ⊢ T1 ▶ [d, dt + et - (d + e)] T2 & ⇧[d, e] T2 ≡ U2.
#L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
elim (tps_split_up … HU12 (d + e) ? ?) -HU12 // -Hdedet #U #HU1 #HU2
lapply (tps_weak … HU1 d e ? ?) -HU1 // [ >commutative_plus /2 width=1/ ] -Hddt -Hdtde #HU1
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 →
+lemma tps_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 ▶ [dt, et] U2 →
∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
dt ≤ d → dt + et ≤ d + e →
- ∃∃T2. K ⊢ T1 [dt, d - dt] ▶ T2 & ⇧[d, e] T2 ≡ U2.
+ ∃∃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 width=3/ -Hdetde #HU12
elim (tps_inv_lift1_be … HU12 … HLK … HTU1 ? ?) -U1 -L // /2 width=3/
qed.
-lemma tps_inv_lift1_le_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶ U2 →
+lemma tps_inv_lift1_le_up: ∀L,U1,U2,dt,et. L ⊢ U1 ▶ [dt, et] U2 →
∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
dt ≤ d → d ≤ dt + et → dt + et ≤ d + e →
- ∃∃T2. K ⊢ T1 [dt, d - dt] ▶ T2 & ⇧[d, e] T2 ≡ U2.
+ ∃∃T2. K ⊢ T1 ▶ [dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2.
#L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde
elim (tps_split_up … HU12 d ? ?) -HU12 // #U #HU1 #HU2
elim (tps_inv_lift1_le … HU1 … HLK … HTU1 ?) -U1 [2: >commutative_plus /2 width=1/ ] -Hdtd #T #HT1 #HTU
(* Main properties **********************************************************)
(* Basic_1: was: subst1_confluence_eq *)
-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.
+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 -L -T0 -T1 -d1 -e1
[ /2 width=3/
| #L #K1 #V1 #T1 #i0 #d1 #e1 #Hd1 #Hde1 #HLK1 #HVT1 #T2 #d2 #e2 #H
qed.
(* Basic_1: was: subst1_confluence_neq *)
-theorem tps_conf_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 [d1, e1] ▶ T1 →
- ∀L2,T2,d2,e2. L2 ⊢ T0 [d2, e2] ▶ T2 →
+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.
+ ∃∃T. L2 ⊢ T1 ▶ [d2, e2] T & L1 ⊢ T2 ▶ [d1, e1] T.
#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
(* Note: the constant 1 comes from tps_subst *)
(* Basic_1: was: subst1_trans *)
-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.
+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 #I #d #e #T2 #H #He
elim (tps_inv_atom1 … H) -H
]
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.
+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 width=3/
| #L #K #V #W #i1 #d1 #e1 #Hdi1 #Hide1 #HLK #HVW #T2 #d2 #e2 #HWT2 #Hde2d1
(* INVERSE BASIC TERM RELOCATION *******************************************)
definition delift: nat → nat → lenv → relation term ≝
- λd,e,L,T1,T2. ∃∃T. L ⊢ T1 [d, e] ▶* T & ⇧[d, e] T2 ≡ T.
+ λd,e,L,T1,T2. ∃∃T. L ⊢ T1 ▶* [d, e] T & ⇧[d, e] T2 ≡ T.
interpretation "inverse basic relocation (term)"
'TSubst L T1 d e T2 = (delift d e L T1 T2).
/2 width=3/ qed.
lemma delift_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≡ T2 →
- ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ≡ T2.
+ ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 [d, e] ≡ T2.
#L1 #T1 #T2 #d #e * /3 width=3/
qed.
(* Basic properties *********************************************************)
lemma delifta_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≡≡ T2 →
- ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ≡≡ T2.
+ ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 [d, e] ≡≡ T2.
#L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e // /2 width=1/
[ #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
elim (ldrop_lsubs_ldrop1_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
(* Properties on partial unfold on local environments ***********************)
lemma delift_ltpss_conf_eq: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≡ T2 →
- ∀K. L [d, e] ▶* K → K ⊢ T1 [d, e] ≡ T2.
+ ∀K. L ▶* [d, e] K → K ⊢ T1 [d, e] ≡ T2.
#L #T1 #T2 #d #e * #T #HT1 #HT2 #K #HLK
elim (ltpss_tpss_conf … HT1 … HLK) -L #T0 #HT10 #HT0
lapply (tpss_inv_lift1_eq … HT0 … HT2) -HT0 #H destruct /2 width=3/
qed.
-lemma ltpss_delift_trans_eq: ∀L,K,d,e. L [d, e] ▶* K →
+lemma ltpss_delift_trans_eq: ∀L,K,d,e. L ▶* [d, e] K →
∀T1,T2. K ⊢ T1 [d, e] ≡ T2 → L ⊢ T1 [d, e] ≡ T2.
#L #K #d #e #HLK #T1 #T2 * #T #HT1 #HT2
lapply (ltpss_tpss_trans_eq … HT1 … HLK) -K /2 width=3/
(* Properties on partial unfold on terms ************************************)
-lemma delift_tpss_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
+lemma delift_tpss_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
∀K. ⇩[dd, ee] L ≡ K → d + e ≤ dd →
- ∃∃T2. K ⊢ T1 [d, e] ▶* T2 & L ⊢ U2 [dd, ee] ≡ T2.
+ ∃∃T2. K ⊢ T1 ▶* [d, e] T2 & L ⊢ U2 [dd, ee] ≡ T2.
#L #U1 #U2 #d #e #HU12 #T1 #dd #ee * #X1 #HUX1 #HTX1 #K #HLK #H1
elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1
elim (tpss_inv_lift1_le … HXU1 … HLK … HTX1 ?) -X1 -HLK // -H1 /3 width=5/
qed.
-lemma delift_tps_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 →
+lemma delift_tps_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
∀K. ⇩[dd, ee] L ≡ K → d + e ≤ dd →
- ∃∃T2. K ⊢ T1 [d, e] ▶* T2 & L ⊢ U2 [dd, ee] ≡ T2.
+ ∃∃T2. K ⊢ T1 ▶* [d, e] T2 & L ⊢ U2 [dd, ee] ≡ T2.
/3 width=3/ qed.
-lemma delift_tpss_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
+lemma delift_tpss_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
∀K. ⇩[dd, ee] L ≡ K →
d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
- ∃∃T2. K ⊢ T1 [d, dd - d] ▶* T2 &
+ ∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 &
L ⊢ U2 [dd, ee] ≡ T2.
#L #U1 #U2 #d #e #HU12 #T1 #dd #ee * #X1 #HUX1 #HTX1 #K #HLK #H1 #H2 #H3
elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1
elim (tpss_inv_lift1_le_up … HXU1 … HLK … HTX1 ? ? ?) -X1 -HLK // -H1 -H2 -H3 /3 width=5/
qed.
-lemma delift_tps_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 →
+lemma delift_tps_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
∀K. ⇩[dd, ee] L ≡ K →
d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
- ∃∃T2. K ⊢ T1 [d, dd - d] ▶* T2 &
+ ∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 &
L ⊢ U2 [dd, ee] ≡ T2.
/3 width=6/ qed.
-lemma delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
+lemma delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
∀K. ⇩[dd, ee] L ≡ K → d ≤ dd → dd + ee ≤ d + e →
- ∃∃T2. K ⊢ T1 [d, e - ee] ▶* T2 &
+ ∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 &
L ⊢ U2 [dd, ee] ≡ T2.
#L #U1 #U2 #d #e #HU12 #T1 #dd #ee * #X1 #HUX1 #HTX1 #K #HLK #H1 #H2
elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1
elim (tpss_inv_lift1_be … HXU1 … HLK … HTX1 ? ?) -X1 -HLK // -H1 -H2 /3 width=5/
qed.
-lemma delift_tps_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 →
+lemma delift_tps_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
∀K. ⇩[dd, ee] L ≡ K → d ≤ dd → dd + ee ≤ d + e →
- ∃∃T2. K ⊢ T1 [d, e - ee] ▶* T2 &
+ ∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 &
L ⊢ U2 [dd, ee] ≡ T2.
/3 width=3/ qed.
-lemma delift_tpss_conf_eq: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
+lemma delift_tpss_conf_eq: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
∀T. L ⊢ U1 [d, e] ≡ T → L ⊢ U2 [d, e] ≡ T.
#L #U1 #U2 #d #e #HU12 #T * #X1 #HUX1 #HTX1
elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1
lapply (tpss_inv_lift1_eq … HXU1 … HTX1) -HXU1 #H destruct /2 width=3/
qed.
-lemma delift_tps_conf_eq: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 →
+lemma delift_tps_conf_eq: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
∀T. L ⊢ U1 [d, e] ≡ T → L ⊢ U2 [d, e] ≡ T.
/3 width=3/ qed.
-lemma tpss_delift_trans_eq: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
+lemma tpss_delift_trans_eq: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
∀T. L ⊢ U2 [d, e] ≡ T → L ⊢ U1 [d, e] ≡ T.
#L #U1 #U2 #d #e #HU12 #T * #X1 #HUX1 #HTX1
lapply (tpss_trans_eq … HU12 … HUX1) -U2 /2 width=3/
qed.
-lemma tps_delift_trans_eq: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 →
+lemma tps_delift_trans_eq: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
∀T. L ⊢ U2 [d, e] ≡ T → L ⊢ U1 [d, e] ≡ T.
/3 width=3/ qed.
| ltpss_atom : ∀d,e. ltpss d e (⋆) (⋆)
| ltpss_pair : ∀L,I,V. ltpss 0 0 (L. ⓑ{I} V) (L. ⓑ{I} V)
| ltpss_tpss2: ∀L1,L2,I,V1,V2,e.
- ltpss 0 e L1 L2 → L2 ⊢ V1 [0, e] ▶* V2 →
+ ltpss 0 e L1 L2 → L2 ⊢ V1 ▶* [0, e] V2 →
ltpss 0 (e + 1) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)
| ltpss_tpss1: ∀L1,L2,I,V1,V2,d,e.
- ltpss d e L1 L2 → L2 ⊢ V1 [d, e] ▶* V2 →
+ ltpss d e L1 L2 → L2 ⊢ V1 ▶* [d, e] V2 →
ltpss (d + 1) e (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)
.
(* Basic properties *********************************************************)
lemma ltpss_tps2: ∀L1,L2,I,V1,V2,e.
- L1 [0, e] ▶* L2 → L2 ⊢ V1 [0, e] ▶ V2 →
- L1. ⓑ{I} V1 [0, e + 1] ▶* L2. ⓑ{I} V2.
+ L1 ▶* [0, e] L2 → L2 ⊢ V1 ▶ [0, e] V2 →
+ L1. ⓑ{I} V1 ▶* [0, e + 1] L2. ⓑ{I} V2.
/3 width=1/ qed.
lemma ltpss_tps1: ∀L1,L2,I,V1,V2,d,e.
- L1 [d, e] ▶* L2 → L2 ⊢ V1 [d, e] ▶ V2 →
- L1. ⓑ{I} V1 [d + 1, e] ▶* L2. ⓑ{I} V2.
+ L1 ▶* [d, e] L2 → L2 ⊢ V1 ▶ [d, e] V2 →
+ L1. ⓑ{I} V1 ▶* [d + 1, e] L2. ⓑ{I} V2.
/3 width=1/ qed.
lemma ltpss_tpss2_lt: ∀L1,L2,I,V1,V2,e.
- L1 [0, e - 1] ▶* L2 → L2 ⊢ V1 [0, e - 1] ▶* V2 →
- 0 < e → L1. ⓑ{I} V1 [0, e] ▶* L2. ⓑ{I} V2.
+ 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 width=1/
qed.
lemma ltpss_tpss1_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 ▶* [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 width=1/
qed.
lemma ltpss_tps2_lt: ∀L1,L2,I,V1,V2,e.
- L1 [0, e - 1] ▶* L2 → L2 ⊢ V1 [0, e - 1] ▶ V2 →
- 0 < e → L1. ⓑ{I} V1 [0, e] ▶* L2. ⓑ{I} V2.
+ L1 ▶* [0, e - 1] L2 → L2 ⊢ V1 ▶ [0, e - 1] V2 →
+ 0 < e → L1. ⓑ{I} V1 ▶* [0, e] L2. ⓑ{I} V2.
/3 width=1/ qed.
lemma ltpss_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 ▶* [d - 1, e] L2 → L2 ⊢ V1 ▶ [d - 1, e] V2 →
+ 0 < d → L1. ⓑ{I} V1 ▶* [d, e] L2. ⓑ{I} V2.
/3 width=1/ qed.
(* Basic_1: was by definition: csubst1_refl *)
-lemma ltpss_refl: ∀L,d,e. L [d, e] ▶* L.
+lemma ltpss_refl: ∀L,d,e. L ▶* [d, e] L.
#L elim L -L //
#L #I #V #IHL * /2 width=1/ * /2 width=1/
qed.
-lemma ltpss_weak: ∀L1,L2,d1,e1. L1 [d1, e1] ▶* L2 →
- ∀d2,e2. d2 ≤ d1 → d1 + e1 ≤ d2 + e2 → L1 [d2, e2] ▶* L2.
+lemma ltpss_weak: ∀L1,L2,d1,e1. L1 ▶* [d1, e1] L2 →
+ ∀d2,e2. d2 ≤ d1 → d1 + e1 ≤ d2 + e2 → L1 ▶* [d2, e2] L2.
#L1 #L2 #d1 #e1 #H elim H -L1 -L2 -d1 -e1 //
[ #L1 #L2 #I #V1 #V2 #e1 #_ #HV12 #IHL12 #d2 #e2 #Hd2 #Hde2
lapply (le_n_O_to_eq … Hd2) #H destruct normalize in Hde2;
]
qed.
-lemma ltpss_weak_all: ∀L1,L2,d,e. L1 [d, e] ▶* L2 → L1 [0, |L2|] ▶* L2.
+lemma ltpss_weak_all: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → L1 ▶* [0, |L2|] L2.
#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
// /3 width=2/ /3 width=3/
qed.
(* Basic forward lemmas *****************************************************)
-lemma ltpss_fwd_length: ∀L1,L2,d,e. L1 [d, e] ▶* L2 → |L1| = |L2|.
+lemma ltpss_fwd_length: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → |L1| = |L2|.
#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
normalize //
qed-.
(* Basic inversion lemmas ***************************************************)
-fact ltpss_inv_refl_O2_aux: ∀d,e,L1,L2. L1 [d, e] ▶* L2 → e = 0 → L1 = L2.
+fact ltpss_inv_refl_O2_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → e = 0 → L1 = L2.
#d #e #L1 #L2 #H elim H -d -e -L1 -L2 //
[ #L1 #L2 #I #V1 #V2 #e #_ #_ #_ >commutative_plus normalize #H destruct
| #L1 #L2 #I #V1 #V2 #d #e #_ #HV12 #IHL12 #He destruct
]
qed.
-lemma ltpss_inv_refl_O2: ∀d,L1,L2. L1 [d, 0] ▶* L2 → L1 = L2.
+lemma ltpss_inv_refl_O2: ∀d,L1,L2. L1 ▶* [d, 0] L2 → L1 = L2.
/2 width=4/ qed-.
fact ltpss_inv_atom1_aux: ∀d,e,L1,L2.
- L1 [d, e] ▶* L2 → L1 = ⋆ → L2 = ⋆.
+ L1 ▶* [d, e] L2 → L1 = ⋆ → L2 = ⋆.
#d #e #L1 #L2 * -d -e -L1 -L2
[ //
| #L #I #V #H destruct
]
qed.
-lemma ltpss_inv_atom1: ∀d,e,L2. ⋆ [d, e] ▶* L2 → L2 = ⋆.
+lemma ltpss_inv_atom1: ∀d,e,L2. ⋆ ▶* [d, e] L2 → L2 = ⋆.
/2 width=5/ qed-.
-fact ltpss_inv_tpss21_aux: ∀d,e,L1,L2. L1 [d, e] ▶* L2 → d = 0 → 0 < e →
+fact ltpss_inv_tpss21_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → d = 0 → 0 < e →
∀K1,I,V1. L1 = K1. ⓑ{I} V1 →
- ∃∃K2,V2. K1 [0, e - 1] ▶* K2 &
- K2 ⊢ V1 [0, e - 1] ▶* V2 &
+ ∃∃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 #_ #_ #K1 #I #V1 #H destruct
]
qed.
-lemma ltpss_inv_tpss21: ∀e,K1,I,V1,L2. K1. ⓑ{I} V1 [0, e] ▶* L2 → 0 < e →
- ∃∃K2,V2. K1 [0, e - 1] ▶* K2 & K2 ⊢ V1 [0, e - 1] ▶* V2 &
+lemma ltpss_inv_tpss21: ∀e,K1,I,V1,L2. K1. ⓑ{I} V1 ▶* [0, e] L2 → 0 < e →
+ ∃∃K2,V2. K1 ▶* [0, e - 1] K2 &
+ K2 ⊢ V1 ▶* [0, e - 1] V2 &
L2 = K2. ⓑ{I} V2.
/2 width=5/ qed-.
-fact ltpss_inv_tpss11_aux: ∀d,e,L1,L2. L1 [d, e] ▶* L2 → 0 < d →
+fact ltpss_inv_tpss11_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → 0 < d →
∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
- ∃∃K2,V2. K1 [d - 1, e] ▶* K2 &
- K2 ⊢ V1 [d - 1, e] ▶* V2 &
+ ∃∃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 #_ #I #K1 #V1 #H destruct
]
qed.
-lemma ltpss_inv_tpss11: ∀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 &
+lemma ltpss_inv_tpss11: ∀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 width=3/ qed-.
fact ltpss_inv_atom2_aux: ∀d,e,L1,L2.
- L1 [d, e] ▶* L2 → L2 = ⋆ → L1 = ⋆.
+ L1 ▶* [d, e] L2 → L2 = ⋆ → L1 = ⋆.
#d #e #L1 #L2 * -d -e -L1 -L2
[ //
| #L #I #V #H destruct
]
qed.
-lemma ltpss_inv_atom2: ∀d,e,L1. L1 [d, e] ▶* ⋆ → L1 = ⋆.
+lemma ltpss_inv_atom2: ∀d,e,L1. L1 ▶* [d, e] ⋆ → L1 = ⋆.
/2 width=5/ qed-.
-fact ltpss_inv_tpss22_aux: ∀d,e,L1,L2. L1 [d, e] ▶* L2 → d = 0 → 0 < e →
+fact ltpss_inv_tpss22_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → d = 0 → 0 < e →
∀K2,I,V2. L2 = K2. ⓑ{I} V2 →
- ∃∃K1,V1. K1 [0, e - 1] ▶* K2 &
- K2 ⊢ V1 [0, e - 1] ▶* V2 &
+ ∃∃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 #_ #_ #K1 #I #V1 #H destruct
]
qed.
-lemma ltpss_inv_tpss22: ∀e,L1,K2,I,V2. L1 [0, e] ▶* K2. ⓑ{I} V2 → 0 < e →
- ∃∃K1,V1. K1 [0, e - 1] ▶* K2 & K2 ⊢ V1 [0, e - 1] ▶* V2 &
+lemma ltpss_inv_tpss22: ∀e,L1,K2,I,V2. L1 ▶* [0, e] K2. ⓑ{I} V2 → 0 < e →
+ ∃∃K1,V1. K1 ▶* [0, e - 1] K2 &
+ K2 ⊢ V1 ▶* [0, e - 1] V2 &
L1 = K1. ⓑ{I} V1.
/2 width=5/ qed-.
-fact ltpss_inv_tpss12_aux: ∀d,e,L1,L2. L1 [d, e] ▶* L2 → 0 < d →
+fact ltpss_inv_tpss12_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → 0 < d →
∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
- ∃∃K1,V1. K1 [d - 1, e] ▶* K2 &
- K2 ⊢ V1 [d - 1, e] ▶* V2 &
- L1 = K1. ⓑ{I} V1.
+ ∃∃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 #_ #I #K2 #V2 #H destruct
| #L #I #V #H elim (lt_refl_false … H)
]
qed.
-lemma ltpss_inv_tpss12: ∀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 &
+lemma ltpss_inv_tpss12: ∀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 width=3/ qed-.
(* PARALLEL UNFOLD ON LOCAL ENVIRONMENTS ************************************)
-lemma ltpss_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 →
+lemma ltpss_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 -L0 -L1 -d1 -e1
]
qed.
-lemma ltpss_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶* L0 →
+lemma ltpss_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 -L1 -L0 -d1 -e1
]
qed.
-lemma ltpss_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 →
+lemma ltpss_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.
+ ∃∃L. L2 ▶* [0, d1 + e1 - e2] L & ⇩[0, e2] L1 ≡ L.
#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
]
qed.
-lemma ltpss_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ▶* L0 →
+lemma ltpss_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.
+ ∃∃L. L ▶* [0, d1 + e1 - e2] L2 & ⇩[0, e2] L1 ≡ L.
#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
]
qed.
-lemma ltpss_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 →
+lemma ltpss_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.
+ ∃∃L. L2 ▶* [d1 - e2, e1] L & ⇩[0, e2] L1 ≡ L.
#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/
]
qed.
-lemma ltpss_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ▶* L0 →
+lemma ltpss_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.
+ ∃∃L. L ▶* [d1 - e2, e1] L2 & ⇩[0, e2] L1 ≡ L.
#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/
(* Advanced properties ******************************************************)
-lemma ltpss_tpss_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶* U2 →
- ∀L1,d1,e1. L0 [d1, e1] ▶* L1 →
- ∃∃T. L1 ⊢ T2 [d2, e2] ▶* T &
- L1 ⊢ U2 [d1, e1] ▶* T.
+lemma ltpss_tpss_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶* [d2, e2] U2 →
+ ∀L1,d1,e1. L0 ▶* [d1, e1] L1 →
+ ∃∃T. L1 ⊢ T2 ▶* [d2, e2] T &
+ L1 ⊢ U2 ▶* [d1, e1] T.
#L0 #T2 #U2 #d2 #e2 #H #L1 #d1 #e1 #HL01 @(tpss_ind … H) -U2 /2 width=3/
#U #U2 #_ #HU2 * #X2 #HTX2 #HUX2
elim (ltpss_tps_conf … HU2 … HL01) -L0 #X1 #HUX1 #HU2X1
qed.
lemma ltpss_tpss_trans_down: ∀L0,L1,T2,U2,d1,e1,d2,e2. d2 + e2 ≤ d1 →
- L1 [d1, e1] ▶* L0 → L0 ⊢ T2 [d2, e2] ▶* U2 →
- ∃∃T. L1 ⊢ T2 [d2, e2] ▶* T & L0 ⊢ T [d1, e1] ▶* U2.
+ L1 ▶* [d1, e1] L0 → L0 ⊢ T2 ▶* [d2, e2] U2 →
+ ∃∃T. L1 ⊢ T2 ▶* [d2, e2] T & L0 ⊢ T ▶* [d1, e1] U2.
#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde2d1 #HL10 #H @(tpss_ind … H) -U2
[ /2 width=3/
| #U #U2 #_ #HU2 * #T #HT2 #HTU
qed.
fact ltpss_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e.
- L1 ⊢ T2 [d, e] ▶* U2 → ∀L0. L0 [d, e] ▶* L1 →
- Y1 = L1 → X2 = T2 → L0 ⊢ T2 [d, e] ▶* U2.
+ L1 ⊢ T2 ▶* [d, e] U2 → ∀L0. L0 ▶* [d, e] L1 →
+ Y1 = L1 → X2 = T2 → L0 ⊢ T2 ▶* [d, e] U2.
#Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH
#L1 #T2 #U2 #d #e #H @(tpss_ind_alt … H) -L1 -T2 -U2 -d -e
[ //
]
qed.
-lemma ltpss_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 [d, e] ▶* U2 →
- ∀L0. L0 [d, e] ▶* L1 → L0 ⊢ T2 [d, e] ▶* U2.
+lemma ltpss_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 →
+ ∀L0. L0 ▶* [d, e] L1 → L0 ⊢ T2 ▶* [d, e] U2.
/2 width=5/ qed.
-lemma ltpss_tps_trans_eq: ∀L0,L1,T2,U2,d,e. L0 [d, e] ▶* L1 →
- L1 ⊢ T2 [d, e] ▶ U2 → L0 ⊢ T2 [d, e] ▶* U2.
+lemma ltpss_tps_trans_eq: ∀L0,L1,T2,U2,d,e. L0 ▶* [d, e] L1 →
+ L1 ⊢ T2 ▶ [d, e] U2 → L0 ⊢ T2 ▶* [d, e] U2.
/3 width=3/ qed.
(* Main properties **********************************************************)
-fact ltpss_conf_aux: ∀K,K1,L1,d1,e1. K1 [d1, e1] ▶* L1 →
- ∀K2,L2,d2,e2. K2 [d2, e2] ▶* L2 → K1 = K → K2 = K →
- ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L.
+fact ltpss_conf_aux: ∀K,K1,L1,d1,e1. K1 ▶* [d1, e1] L1 →
+ ∀K2,L2,d2,e2. K2 ▶* [d2, e2] L2 → K1 = K → K2 = K →
+ ∃∃L. L1 ▶* [d2, e2] L & L2 ▶* [d1, e1] L.
#K @(lw_wf_ind … K) -K #K #IH #K1 #L1 #d1 #e1 * -K1 -L1 -d1 -e1
[ -IH /2 width=3/
| -IH #K1 #I1 #V1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
]
qed.
-lemma ltpss_conf: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 →
- ∀L2,d2,e2. L0 [d2, e2] ▶* L2 →
- ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L.
+lemma ltpss_conf: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 →
+ ∀L2,d2,e2. L0 ▶* [d2, e2] L2 →
+ ∃∃L. L1 ▶* [d2, e2] L & L2 ▶* [d1, e1] L.
/2 width=7/ qed.
(* Properties concerning partial substitution on terms **********************)
-lemma ltpss_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.
+lemma ltpss_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 -L0 -T2 -U2 -d2 -e2
[ //
| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01 #Hde1d2
]
qed.
-lemma ltpss_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.
+lemma ltpss_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 -L0 -T2 -U2 -d2 -e2
[ //
| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 #Hde1d2
(* Properties concerning partial unfold on terms ****************************)
-lemma ltpss_tpss_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.
+lemma ltpss_tpss_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 #L1 #d1 #e1 #HL01 #Hde1d2 @(tpss_ind … H) -U2 //
#U #U2 #_ #HU2 #IHU
lapply (ltpss_tps_conf_ge … HU2 … HL01 ?) -L0 // -Hde1d2 /2 width=3/
qed.
(* Basic_1: was: subst1_subst1_back *)
-lemma ltpss_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
- ∀L1,d1,e1. L0 [d1, e1] ▶* L1 →
- ∃∃T. L1 ⊢ T2 [d2, e2] ▶ T &
- L1 ⊢ U2 [d1, e1] ▶* T.
+lemma ltpss_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
+ ∀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 -L0 -T2 -U2 -d2 -e2
[ /2 width=3/
| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01
]
qed.
-lemma ltpss_tpss_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.
+lemma ltpss_tpss_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 #L1 #d1 #e1 #HL01 #Hde1d2 @(tpss_ind … H) -U2 //
#U #U2 #_ #HU2 #IHU
lapply (ltpss_tps_trans_ge … HU2 … HL01 ?) -L0 // -Hde1d2 /2 width=3/
qed.
(* Basic_1: was: subst1_subst1 *)
-lemma ltpss_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.
+lemma ltpss_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 -L0 -T2 -U2 -d2 -e2
[ /2 width=3/
| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10
(* BASIC LOCAL ENVIRONMENT THINNING *****************************************)
definition thin: nat → nat → relation lenv ≝
- λd,e,L1,L2. ∃∃L. L1 [d, e] ▶* L & ⇩[d, e] L ≡ L2.
+ λd,e,L1,L2. ∃∃L. L1 ▶* [d, e] L & ⇩[d, e] L ≡ L2.
interpretation "basic thinning (local environment)"
'TSubst L1 d e L2 = (thin d e L1 L2).
lapply (lift_mono … H2 … HV2) -H2 #H destruct /3 width=5/
qed.
-lemma thin_delift_tpss_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
+lemma thin_delift_tpss_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
∀K. L [dd, ee] ≡ K → d + e ≤ dd →
- ∃∃T2. K ⊢ T1 [d, e] ▶* T2 &
+ ∃∃T2. K ⊢ T1 ▶* [d, e] T2 &
L ⊢ U2 [dd, ee] ≡ T2.
#L #U1 #U2 #d #e #HU12 #T1 #dd #ee #HUT1 #K * #Y #HLY #HYK #Hdedd
lapply (delift_ltpss_conf_eq … HUT1 … HLY) -HUT1 #HUT1
lapply (ltpss_delift_trans_eq … HLY … HU2T) -Y /2 width=3/
qed.
-lemma thin_delift_tps_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 →
+lemma thin_delift_tps_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
∀K. L [dd, ee] ≡ K → d + e ≤ dd →
- ∃∃T2. K ⊢ T1 [d, e] ▶* T2 &
+ ∃∃T2. K ⊢ T1 ▶* [d, e] T2 &
L ⊢ U2 [dd, ee] ≡ T2.
/3 width=3/ qed.
-lemma thin_delift_tpss_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
+lemma thin_delift_tpss_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
∀K. L [dd, ee] ≡ K →
d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
- ∃∃T2. K ⊢ T1 [d, dd - d] ▶* T2 &
+ ∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 &
L ⊢ U2 [dd, ee] ≡ T2.
#L #U1 #U2 #d #e #HU12 #T1 #dd #ee #HUT1 #K * #Y #HLY #HYK #Hdd #Hdde #Hddee
lapply (delift_ltpss_conf_eq … HUT1 … HLY) -HUT1 #HUT1
lapply (ltpss_delift_trans_eq … HLY … HU2T) -Y /2 width=3/
qed.
-lemma thin_delift_tps_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 →
+lemma thin_delift_tps_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
∀K. L [dd, ee] ≡ K →
d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
- ∃∃T2. K ⊢ T1 [d, dd - d] ▶* T2 &
+ ∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 &
L ⊢ U2 [dd, ee] ≡ T2.
/3 width=6 by thin_delift_tpss_conf_le_up, tpss_strap/ qed. (**) (* too slow without trace *)
-lemma thin_delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
+lemma thin_delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
∀K. L [dd, ee] ≡ K → d ≤ dd → dd + ee ≤ d + e →
- ∃∃T2. K ⊢ T1 [d, e - ee] ▶* T2 &
+ ∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 &
L ⊢ U2 [dd, ee] ≡ T2.
#L #U1 #U2 #d #e #HU12 #T1 #dd #ee #HUT1 #K * #Y #HLY #HYK #Hdd #Hddee
lapply (delift_ltpss_conf_eq … HUT1 … HLY) -HUT1 #HUT1
lapply (ltpss_delift_trans_eq … HLY … HU2T) -Y /2 width=3/
qed.
-lemma thin_delift_tps_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 →
+lemma thin_delift_tps_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
∀K. L [dd, ee] ≡ K → d ≤ dd → dd + ee ≤ d + e →
- ∃∃T2. K ⊢ T1 [d, e - ee] ▶* T2 &
+ ∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 &
L ⊢ U2 [dd, ee] ≡ T2.
/3 width=3/ qed.
(* Basic eliminators ********************************************************)
lemma tpss_ind: ∀d,e,L,T1. ∀R:predicate term. R T1 →
- (∀T,T2. L ⊢ T1 [d, e] ▶* T → L ⊢ T [d, e] ▶ T2 → R T → R T2) →
- ∀T2. L ⊢ T1 [d, e] ▶* T2 → R T2.
+ (∀T,T2. L ⊢ T1 ▶* [d, e] T → L ⊢ T ▶ [d, e] T2 → R T → R T2) →
+ ∀T2. L ⊢ T1 ▶* [d, e] T2 → R T2.
#d #e #L #T1 #R #HT1 #IHT1 #T2 #HT12 @(TC_star_ind … HT1 IHT1 … HT12) //
qed-.
(* Basic properties *********************************************************)
-lemma tpss_strap: ∀L,T1,T,T2,d,e.
- L ⊢ T1 [d, e] ▶ T → L ⊢ T [d, e] ▶* T2 → L ⊢ T1 [d, e] ▶* T2.
+lemma tpss_strap: ∀L,T1,T,T2,d,e.
+ L ⊢ T1 ▶ [d, e] T → L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
/2 width=3/ qed.
-lemma tpss_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶* T2 →
- ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ▶* T2.
+lemma tpss_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶* [d, e] T2 →
+ ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 ▶* [d, e] T2.
/3 width=3/ qed.
-lemma tpss_refl: ∀d,e,L,T. L ⊢ T [d, e] ▶* T.
+lemma tpss_refl: ∀d,e,L,T. L ⊢ T ▶* [d, e] T.
/2 width=1/ qed.
-lemma tpss_bind: ∀L,V1,V2,d,e. L ⊢ V1 [d, e] ▶* V2 →
- ∀I,T1,T2. L. ⓑ{I} V2 ⊢ T1 [d + 1, e] ▶* T2 →
- L ⊢ ⓑ{I} V1. T1 [d, e] ▶* ⓑ{I} V2. T2.
+lemma tpss_bind: ∀L,V1,V2,d,e. L ⊢ V1 ▶* [d, e] V2 →
+ ∀I,T1,T2. L. ⓑ{I} V2 ⊢ T1 ▶* [d + 1, e] T2 →
+ L ⊢ ⓑ{I} V1. T1 ▶* [d, e] ⓑ{I} V2. T2.
#L #V1 #V2 #d #e #HV12 elim HV12 -V2
[ #V2 #HV12 #I #T1 #T2 #HT12 elim HT12 -T2
[ /3 width=5/
qed.
lemma tpss_flat: ∀L,I,V1,V2,T1,T2,d,e.
- L ⊢ V1 [d, e] ▶ * V2 → L ⊢ T1 [d, e] ▶* T2 →
- L ⊢ ⓕ{I} V1. T1 [d, e] ▶* ⓕ{I} V2. T2.
+ L ⊢ V1 ▶* [d, e] V2 → L ⊢ T1 ▶* [d, e] T2 →
+ L ⊢ ⓕ{I} V1. T1 ▶* [d, e] ⓕ{I} V2. T2.
#L #I #V1 #V2 #T1 #T2 #d #e #HV12 elim HV12 -V2
[ #V2 #HV12 #HT12 elim HT12 -T2
[ /3 width=1/
]
qed.
-lemma tpss_weak: ∀L,T1,T2,d1,e1. L ⊢ T1 [d1, e1] ▶* T2 →
+lemma tpss_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 ▶* [d2, e2] T2.
#L #T1 #T2 #d1 #e1 #H #d1 #d2 #Hd21 #Hde12 @(tpss_ind … H) -T2
[ //
| #T #T2 #_ #HT12 #IHT
qed.
lemma tpss_weak_top: ∀L,T1,T2,d,e.
- L ⊢ T1 [d, e] ▶* T2 → L ⊢ T1 [d, |L| - d] ▶* T2.
+ L ⊢ T1 ▶* [d, e] T2 → L ⊢ T1 ▶* [d, |L| - d] T2.
#L #T1 #T2 #d #e #H @(tpss_ind … H) -T2
[ //
| #T #T2 #_ #HT12 #IHT
qed.
lemma tpss_weak_all: ∀L,T1,T2,d,e.
- L ⊢ T1 [d, e] ▶* T2 → L ⊢ T1 [0, |L|] ▶* T2.
+ L ⊢ T1 ▶* [d, e] T2 → L ⊢ T1 ▶* [0, |L|] T2.
#L #T1 #T2 #d #e #HT12
lapply (tpss_weak … HT12 0 (d + e) ? ?) -HT12 // #HT12
lapply (tpss_weak_top … HT12) //
(* Basic inversion lemmas ***************************************************)
(* Note: this can be derived from tpss_inv_atom1 *)
-lemma tpss_inv_sort1: ∀L,T2,k,d,e. L ⊢ ⋆k [d, e] ▶* T2 → T2 = ⋆k.
+lemma tpss_inv_sort1: ∀L,T2,k,d,e. L ⊢ ⋆k ▶* [d, e] T2 → T2 = ⋆k.
#L #T2 #k #d #e #H @(tpss_ind … H) -T2
[ //
| #T #T2 #_ #HT2 #IHT destruct
qed-.
(* Note: this can be derived from tpss_inv_atom1 *)
-lemma tpss_inv_gref1: ∀L,T2,p,d,e. L ⊢ §p [d, e] ▶* T2 → T2 = §p.
+lemma tpss_inv_gref1: ∀L,T2,p,d,e. L ⊢ §p ▶* [d, e] T2 → T2 = §p.
#L #T2 #p #d #e #H @(tpss_ind … H) -T2
[ //
| #T #T2 #_ #HT2 #IHT destruct
]
qed-.
-lemma tpss_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 &
+lemma tpss_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.
#d #e #L #I #V1 #T1 #U2 #H @(tpss_ind … H) -U2
[ /2 width=5/
]
qed-.
-lemma tpss_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 &
+lemma tpss_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.
#d #e #L #I #V1 #T1 #U2 #H @(tpss_ind … H) -U2
[ /2 width=5/
]
qed-.
-lemma tpss_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ▶* T2 → T1 = T2.
+lemma tpss_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 ▶* [d, 0] T2 → T1 = T2.
#L #T1 #T2 #d #H @(tpss_ind … H) -T2
[ //
| #T #T2 #_ #HT2 #IHT <(tps_inv_refl_O2 … HT2) -HT2 //
(* Basic forward lemmas *****************************************************)
-lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶* T2 → #[T1] ≤ #[T2].
+lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → #[T1] ≤ #[T2].
#L #T1 #T2 #d #e #H @(tpss_ind … H) -T2 //
#T #T2 #_ #HT2 #IHT1
lapply (tps_fwd_tw … HT2) -HT2 #HT2
(* Basic properties *********************************************************)
-lemma tpssa_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶▶* T2 →
- ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ▶▶* T2.
+lemma tpssa_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 -L1 -T1 -T2 -d -e
[ //
| #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
]
qed.
-lemma tpssa_refl: ∀T,L,d,e. L ⊢ T [d, e] ▶▶* T.
+lemma tpssa_refl: ∀T,L,d,e. L ⊢ T ▶▶* [d, e] T.
#T elim T -T //
#I elim I -I /2 width=1/
qed.
-lemma tpssa_tps_trans: ∀L,T1,T,d,e. L ⊢ T1 [d, e] ▶▶* T →
- ∀T2. L ⊢ T [d, e] ▶ T2 → L ⊢ T1 [d, e] ▶▶* T2.
+lemma tpssa_tps_trans: ∀L,T1,T,d,e. L ⊢ T1 ▶▶* [d, e] T →
+ ∀T2. L ⊢ T ▶ [d, e] T2 → L ⊢ T1 ▶▶* [d, e] T2.
#L #T1 #T #d #e #H elim H -L -T1 -T -d -e
[ #L #I #d #e #X #H
elim (tps_inv_atom1 … H) -H // * /2 width=6/
]
qed.
-lemma tpss_tpssa: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ T1 [d, e] ▶▶* T2.
+lemma tpss_tpssa: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → L ⊢ T1 ▶▶* [d, e] T2.
#L #T1 #T2 #d #e #H @(tpss_ind … H) -T2 // /2 width=3/
qed.
(* Basic inversion lemmas ***************************************************)
-lemma tpssa_tpss: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶▶* T2 → L ⊢ T1 [d, e] ▶* T2.
+lemma tpssa_tpss: ∀L,T1,T2,d,e. L ⊢ T1 ▶▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e // /2 width=6/
qed-.
lemma tpss_ind_alt: ∀R:ℕ→ℕ→lenv→relation term.
(∀L,I,d,e. R d e L (⓪{I}) (⓪{I})) →
(∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e →
- ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ V1 [O, d + e - i - 1] ▶* V2 →
+ ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ V1 ▶* [O, d + e - i - 1] V2 →
⇧[O, i + 1] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L #i W2
) →
- (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 [d, e] ▶* V2 →
- L.ⓑ{I}V2 ⊢ T1 [d + 1, e] ▶* T2 → R d e L V1 V2 →
+ (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 ▶* [d, e] V2 →
+ L.ⓑ{I}V2 ⊢ T1 ▶* [d + 1, e] T2 → R d e L V1 V2 →
R (d+1) e (L.ⓑ{I}V2) T1 T2 → R d e L (ⓑ{I}V1.T1) (ⓑ{I}V2.T2)
) →
- (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 [d, e] ▶* V2 →
- L⊢ T1 [d, e] ▶* T2 → R d e L V1 V2 →
+ (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 ▶* [d, e] V2 →
+ L ⊢ T1 ▶* [d, e] T2 → R d e L V1 V2 →
R d e L T1 T2 → R d e L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
) →
- ∀d,e,L,T1,T2. L ⊢ T1 [d, e] ▶* T2 → R d e L T1 T2.
+ ∀d,e,L,T1,T2. L ⊢ T1 ▶* [d, e] T2 → R d e L T1 T2.
#R #H1 #H2 #H3 #H4 #d #e #L #T1 #T2 #H elim (tpss_tpssa … H) -L -T1 -T2 -d -e
// /3 width=1 by tpssa_tpss/ /3 width=7 by tpssa_tpss/
qed-.
lemma tpss_subst: ∀L,K,V,U1,i,d,e.
d ≤ i → i < d + e →
- ⇩[0, i] L ≡ K. ⓓV → K ⊢ V [0, d + e - i - 1] ▶* U1 →
- ∀U2. ⇧[0, i + 1] U1 ≡ U2 → L ⊢ #i [d, e] ▶* U2.
+ ⇩[0, i] L ≡ K. ⓓV → K ⊢ V ▶* [0, d + e - i - 1] U1 →
+ ∀U2. ⇧[0, i + 1] U1 ≡ U2 → L ⊢ #i ▶* [d, e] U2.
#L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(tpss_ind … H) -U1
[ /3 width=4/
| #U #U1 #_ #HU1 #IHU #U2 #HU12
(* Advanced inverion lemmas *************************************************)
-lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ ⓪{I} [d, e] ▶* T2 →
+lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ ⓪{I} ▶* [d, e] T2 →
T2 = ⓪{I} ∨
∃∃K,V1,V2,i. d ≤ i & i < d + e &
⇩[O, i] L ≡ K. ⓓV1 &
- K ⊢ V1 [0, d + e - i - 1] ▶* V2 &
+ K ⊢ V1 ▶* [0, d + e - i - 1] V2 &
⇧[O, i + 1] V2 ≡ T2 &
I = LRef i.
#L #T2 #I #d #e #H @(tpss_ind … H) -T2
]
qed-.
-lemma tpss_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ▶* T2 →
+lemma tpss_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i ▶* [d, e] T2 →
T2 = #i ∨
∃∃K,V1,V2. d ≤ i & i < d + e &
⇩[O, i] L ≡ K. ⓓV1 &
- K ⊢ V1 [0, d + e - i - 1] ▶* V2 &
+ K ⊢ V1 ▶* [0, d + e - i - 1] V2 &
⇧[O, i + 1] V2 ≡ T2.
#L #T2 #i #d #e #H
elim (tpss_inv_atom1 … H) -H /2 width=1/
* #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct /3 width=6/
qed-.
-lemma tpss_inv_S2: ∀L,T1,T2,d,e. L ⊢ T1 [d, e + 1] ▶* T2 →
- ∀K,V. ⇩[0, d] L ≡ K. ⓛV → L ⊢ T1 [d + 1, e] ▶* T2.
+lemma tpss_inv_S2: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e + 1] T2 →
+ ∀K,V. ⇩[0, d] L ≡ K. ⓛV → L ⊢ T1 ▶* [d + 1, e] T2.
#L #T1 #T2 #d #e #H #K #V #HLK @(tpss_ind … H) -T2 //
#T #T2 #_ #HT2 #IHT
lapply (tps_inv_S2 … HT2 … HLK) -HT2 -HLK /2 width=3/
qed-.
-lemma tpss_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ▶* T2 →
+lemma tpss_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 ▶* [d, 1] T2 →
∀K,V. ⇩[0, d] L ≡ K. ⓛV → T1 = T2.
#L #T1 #T2 #d #H #K #V #HLK @(tpss_ind … H) -T2 //
#T #T2 #_ #HT2 #IHT <(tps_inv_refl_SO2 … HT2 … HLK) //
(* Relocation properties ****************************************************)
-lemma tpss_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶* T2 →
+lemma tpss_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 ▶* [dt, et] T2 →
∀L,U1,d,e. dt + et ≤ d → ⇩[d, e] L ≡ K →
⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 →
- L ⊢ U1 [dt, et] ▶* U2.
+ L ⊢ U1 ▶* [dt, et] U2.
#K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdetd #HLK #HTU1 @(tpss_ind … H) -T2
[ #U2 #H >(lift_mono … HTU1 … H) -H //
| -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
]
qed.
-lemma tpss_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶* T2 →
+lemma tpss_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 ▶* [dt, et] T2 →
∀L,U1,d,e. dt ≤ d → d ≤ dt + et →
⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 →
- ∀U2. ⇧[d, e] T2 ≡ U2 → L ⊢ U1 [dt, et + e] ▶* U2.
+ ∀U2. ⇧[d, e] T2 ≡ U2 → L ⊢ U1 ▶* [dt, et + e] U2.
#K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1 @(tpss_ind … H) -T2
[ #U2 #H >(lift_mono … HTU1 … H) -H //
| -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
]
qed.
-lemma tpss_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶* T2 →
+lemma tpss_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 ▶* [dt, et] T2 →
∀L,U1,d,e. d ≤ dt → ⇩[d, e] L ≡ K →
⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 →
- L ⊢ U1 [dt + e, et] ▶* U2.
+ L ⊢ U1 ▶* [dt + e, et] U2.
#K #T1 #T2 #dt #et #H #L #U1 #d #e #Hddt #HLK #HTU1 @(tpss_ind … H) -T2
[ #U2 #H >(lift_mono … HTU1 … H) -H //
| -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
]
qed.
-lemma tpss_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
+lemma tpss_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.
+ ∃∃T2. K ⊢ T1 ▶* [dt, et] T2 & ⇧[d, e] T2 ≡ U2.
#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdetd @(tpss_ind … H) -U2
[ /2 width=3/
| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
]
qed.
-lemma tpss_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
+lemma tpss_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.
+ ∃∃T2. K ⊢ T1 ▶* [dt, et - e] T2 & ⇧[d, e] T2 ≡ U2.
#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(tpss_ind … H) -U2
[ /2 width=3/
| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
]
qed.
-lemma tpss_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
+lemma tpss_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.
+ ∃∃T2. K ⊢ T1 ▶* [dt - e, et] T2 & ⇧[d, e] T2 ≡ U2.
#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdedt @(tpss_ind … H) -U2
[ /2 width=3/
| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
qed.
lemma tpss_inv_lift1_eq: ∀L,U1,U2,d,e.
- L ⊢ U1 [d, e] ▶* U2 → ∀T1. ⇧[d, e] T1 ≡ U1 → U1 = U2.
+ L ⊢ U1 ▶* [d, e] U2 → ∀T1. ⇧[d, e] T1 ≡ U1 → U1 = U2.
#L #U1 #U2 #d #e #H #T1 #HTU1 @(tpss_ind … H) -U2 //
#U #U2 #_ #HU2 #IHU destruct
<(tps_inv_lift1_eq … HU2 … HTU1) -HU2 -HTU1 //
qed.
-lemma tpss_inv_lift1_ge_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
+lemma tpss_inv_lift1_ge_up: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 →
∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →
- ∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ▶* T2 &
+ ∃∃T2. K ⊢ T1 ▶* [d, dt + et - (d + e)] T2 &
⇧[d, e] T2 ≡ U2.
#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet @(tpss_ind … H) -U2
[ /2 width=3/
]
qed.
-lemma tpss_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
+lemma tpss_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 →
∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
dt ≤ d → dt + et ≤ d + e →
- ∃∃T2. K ⊢ T1 [dt, d - dt] ▶* T2 & ⇧[d, e] T2 ≡ U2.
+ ∃∃T2. K ⊢ T1 ▶* [dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2.
#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(tpss_ind … H) -U2
[ /2 width=3/
| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
]
qed.
-lemma tpss_inv_lift1_le_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
+lemma tpss_inv_lift1_le_up: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 →
∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
dt ≤ d → d ≤ dt + et → dt + et ≤ d + e →
- ∃∃T2. K ⊢ T1 [dt, d - dt] ▶* T2 & ⇧[d, e] T2 ≡ U2.
+ ∃∃T2. K ⊢ T1 ▶* [dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2.
#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde @(tpss_ind … H) -U2
[ /2 width=3/
| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
(* Advanced properties ******************************************************)
-lemma tpss_tps: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ▶* T2 → L ⊢ T1 [d, 1] ▶ T2.
+lemma tpss_tps: ∀L,T1,T2,d. L ⊢ T1 ▶* [d, 1] T2 → L ⊢ T1 ▶ [d, 1] T2.
#L #T1 #T2 #d #H @(tpss_ind … H) -T2 //
#T #T2 #_ #HT2 #IHT1
lapply (tps_trans_ge … IHT1 … HT2 ?) //
qed.
-lemma tpss_strip_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.
+lemma tpss_strip_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.
/3 width=3/ qed.
-lemma tpss_strip_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 [d1, e1] ▶* T1 →
- ∀L2,T2,d2,e2. L2 ⊢ T0 [d2, e2] ▶ T2 →
+lemma tpss_strip_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.
+ ∃∃T. L2 ⊢ T1 ▶ [d2, e2] T & L1 ⊢ T2 ▶* [d1, e1] T.
/3 width=3/ qed.
-lemma tpss_strap1_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.
+lemma tpss_strap1_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.
/3 width=3/ qed.
-lemma tpss_strap2_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.
+lemma tpss_strap2_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.
/3 width=3/ qed.
-lemma tpss_split_up: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶* T2 →
+lemma tpss_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.
+ ∃∃T. L ⊢ T1 ▶* [d, i - d] T & L ⊢ T ▶* [i, d + e - i] T2.
#L #T1 #T2 #d #e #H #i #Hdi #Hide @(tpss_ind … H) -T2
[ /2 width=3/
| #T #T2 #_ #HT12 * #T3 #HT13 #HT3
]
qed.
-lemma tpss_inv_lift1_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
+lemma tpss_inv_lift1_up: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 →
∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →
- ∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ▶* T2 & ⇧[d, e] T2 ≡ U2.
+ ∃∃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 (tpss_split_up … HU12 (d + e) ? ?) -HU12 // -Hdedet #U #HU1 #HU2
lapply (tpss_weak … HU1 d e ? ?) -HU1 // [ >commutative_plus /2 width=1/ ] -Hddt -Hdtde #HU1
(* Main properties **********************************************************)
-theorem tpss_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.
+theorem tpss_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.
/3 width=3/ qed.
-theorem tpss_conf_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 [d1, e1] ▶* T1 →
- ∀L2,T2,d2,e2. L2 ⊢ T0 [d2, e2] ▶* T2 →
+theorem tpss_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.
+ ∃∃T. L2 ⊢ T1 ▶* [d2, e2] T & L1 ⊢ T2 ▶* [d1, e1] T.
/3 width=3/ qed.
theorem tpss_trans_eq: ∀L,T1,T,T2,d,e.
- L ⊢ T1 [d, e] ▶* T → L ⊢ T [d, e] ▶* T2 →
- L ⊢ T1 [d, e] ▶* T2.
+ L ⊢ T1 ▶* [d, e] T → L ⊢ T ▶* [d, e] T2 →
+ L ⊢ T1 ▶* [d, e] T2.
/2 width=3/ qed.
-theorem tpss_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.
+theorem tpss_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.
/3 width=3/ qed.
#m #Hm * #H /2 width=1/ /3 width=1/
qed-.
-lemma lt_refl_false: ∀n. n < n → False.
+lemma lt_refl_false: ∀n. n < n → ⊥.
#n #H elim (lt_to_not_eq … H) -H /2 width=1/
qed-.
-lemma lt_zero_false: ∀n. n < 0 → False.
+lemma lt_zero_false: ∀n. n < 0 → ⊥.
#n #H elim (lt_to_not_le … H) -H /2 width=1/
qed-.
-lemma false_lt_to_le: ∀x,y. (x < y → False) → y ≤ x.
+lemma false_lt_to_le: ∀x,y. (x < y → ⊥) → y ≤ x.
#x #y #H elim (decidable_lt x y) /2 width=1/
#Hxy elim (H Hxy)
qed-.
let rec all A (R:predicate A) (l:list A) on l ≝
match l with
- [ nil ⇒ True
+ [ nil ⇒ ⊤
| cons hd tl ⇒ R hd ∧ all A R tl
].
(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* Logic ********************************************************************)
+
+notation "⊥"
+ non associative with precedence 90
+ for @{'false}.
+
+notation "⊤"
+ non associative with precedence 90
+ for @{'true}.
+
(* Lists ********************************************************************)
-notation "hvbox( ◊ )"
+notation "◊"
non associative with precedence 90
for @{'Nil}.
right associative with precedence 47
for @{'Append $l1 $l2 }.
-notation "hvbox( ⟠ )"
+notation "⟠"
non associative with precedence 90
for @{'Nil2}.
(* PROPERTIES OF RELATIONS **************************************************)
-definition Decidable: Prop → Prop ≝ λR. R ∨ (R → False).
+definition Decidable: Prop → Prop ≝ λR. R ∨ (R → ⊥).
definition confluent2: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
∀a0,a1. R1 a0 a1 → ∀a2. R2 a0 a2 →
qed.
definition NF: ∀A. relation A → relation A → predicate A ≝
- λA,R,S,a1. ∀a2. R a1 a2 → S a1 a2.
+ λA,R,S,a1. ∀a2. R a1 a2 → S a2 a1.
inductive SN (A) (R,S:relation A): predicate A ≝
-| SN_intro: ∀a1. (∀a2. R a1 a2 → (S a1 a2 → False) → SN A R S a2) → SN A R S a1
+| SN_intro: ∀a1. (∀a2. R a1 a2 → (S a2 a1 → ⊥) → SN A R S a2) → SN A R S a1
.
lemma NF_to_SN: ∀A,R,S,a. NF A R S a → SN A R S a.
(* *)
(**************************************************************************)
+include "basics/logic.ma".
include "ground_2/xoa_notation.ma".
include "ground_2/xoa.ma".
+interpretation "logical false" 'false = False.
+
+interpretation "logical true" 'true = True.
+
lemma ex2_1_comm: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0.
#A0 #P0 #P1 * /2 width=3/
qed.
projects / helm.git / commitdiff