(* Main properties **********************************************************)
theorem fsubst_delift: ∀K,V,T,L,d.
- ⇩[0, d] L ≡ K. ⓓV → L ⊢ T ▼*[d, 1] ≡ [d ← V] T.
+ ⇩[0, d] L ≡ K. ⓓV → L ⊢ ▼*[d, 1] T ≡ [d ← V] T.
#K #V #T elim T -T
[ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/
elim (lt_or_eq_or_gt i d) #Hid
(* Main inversion properties ************************************************)
theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. ⓓV →
- L ⊢ T1 ▼*[d, 1] ≡ T2 → [d ← V] T1 = T2.
+ L ⊢ ▼*[d, 1] T1 ≡ T2 → [d ← V] T1 = T2.
#K #V #T1 elim T1 -T1
[ * #i #L #T2 #d #HLK #H
[ -HLK >(delift_inv_sort1 … H) -H //
(* Basic_properties *********************************************************)
(* Basic_1: was: nf2_sn3 *)
-lemma cpe_csn: â\88\80L,T1. L â\8a¢ â¬\87* T1 → ∃T2. L ⊢ T1 ➡* 𝐍⦃T2⦄.
+lemma cpe_csn: â\88\80L,T1. L â\8a¢ â¬\8a* T1 → ∃T2. L ⊢ T1 ➡* 𝐍⦃T2⦄.
#L #T1 #H @(csn_ind … H) -T1
#T1 #_ #IHT1
elim (cnf_dec L T1) /3 width=3/
(* Properties on inverse basic term relocation ******************************)
(* Note: this should be stated with tprs *)
-lemma cprs_zeta_delift: ∀L,V,T1,T2. L.ⓓV ⊢ T1 ▼*[O, 1] ≡ T2 → L ⊢ ⓓV.T1 ➡* T2.
+lemma cprs_zeta_delift: ∀L,V,T1,T2. L.ⓓV ⊢ ▼*[O, 1] T1 ≡ T2 → L ⊢ ⓓV.T1 ➡* T2.
#L #V #T1 #T2 * #T #HT1 #HT2
@(cprs_strap2 … (ⓓV.T)) [ /3 width=3/ | @inj /3 width=3/ ] (**) (* explicit constructor, /5 width=3/ is too slow *)
qed.
(* Basic_1: was only: pr3_gen_cabbr *)
lemma thin_cprs_delift_conf: ∀L,U1,U2. L ⊢ U1 ➡* U2 →
- ∀K,d,e. L ▼*[d, e] ≡ K → ∀T1. L ⊢ U1 ▼*[d, e] ≡ T1 →
- ∃∃T2. K ⊢ T1 ➡* T2 & L ⊢ U2 ▼*[d, e] ≡ T2.
+ ∀K,d,e. ▼*[d, e] L ≡ K → ∀T1. L ⊢ ▼*[d, e] U1 ≡ T1 →
+ ∃∃T2. K ⊢ T1 ➡* T2 & L ⊢ ▼*[d, e] U2 ≡ T2.
#L #U1 #U2 #H @(cprs_ind … H) -U2 /2 width=3/
#U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1
elim (IHU1 … HLK … HTU1) -U1 #T #HT1 #HUT
@or_intror @(ex4_3_intro … HLK … HT12) // /3 width=3/ (**) (* explicit constructors *)
| * #K #V1 #T1 #HLK #HVT1 #HT1 #Hi
lapply (ldrop_fwd_ldrop2 … HLK) #H0LK
- elim (cpr_inv_lift … H0LK … HT1 … HT2) -H0LK -T /4 width=6/
+ elim (cpr_inv_lift1 … H0LK … HT1 … HT2) -H0LK -T /4 width=6/
]
qed-.
qed.
(* Basic_1: was: pr3_gen_lift *)
-lemma cprs_inv_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K →
- ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀U2. L ⊢ U1 ➡* U2 →
- ∃∃T2. ⇧[d, e] T2 ≡ U2 & K ⊢ T1 ➡* T2.
+lemma cprs_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K →
+ ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀U2. L ⊢ U1 ➡* U2 →
+ ∃∃T2. ⇧[d, e] T2 ≡ U2 & K ⊢ T1 ➡* T2.
#L #K #d #e #HLK #T1 #U1 #HTU1 #U2 #HU12 @(cprs_ind … HU12) -U2 /2 width=3/
-HTU1 #U #U2 #_ #HU2 * #T #HTU #HT1
-elim (cpr_inv_lift … HLK … HTU … HU2) -U -HLK /3 width=5/
+elim (cpr_inv_lift1 … HLK … HTU … HU2) -U -HLK /3 width=5/
qed.
(* Basic eliminators ********************************************************)
lemma csn_ind: ∀L. ∀R:predicate term.
- (â\88\80T1. L â\8a¢ â¬\87* T1 →
+ (â\88\80T1. L â\8a¢ â¬\8a* T1 →
(∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → R T2) →
R T1
) →
- â\88\80T. L â\8a¢ â¬\87* T → R T.
+ â\88\80T. L â\8a¢ â¬\8a* T → R T.
#L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1
@H0 -H0 /3 width=1/ -IHT1 /4 width=1/
qed-.
(* Basic_1: was: sn3_pr2_intro *)
lemma csn_intro: ∀L,T1.
- (â\88\80T2. L â\8a¢ T1 â\9e¡ T2 â\86\92 (T1 = T2 â\86\92 â\8a¥) â\86\92 L â\8a¢ â¬\87* T2) â\86\92 L â\8a¢ â¬\87* T1.
+ (â\88\80T2. L â\8a¢ T1 â\9e¡ T2 â\86\92 (T1 = T2 â\86\92 â\8a¥) â\86\92 L â\8a¢ â¬\8a* T2) â\86\92 L â\8a¢ â¬\8a* T1.
/4 width=1/ qed.
(* Basic_1: was: sn3_nf2 *)
-lemma csn_cnf: â\88\80L,T. L â\8a¢ ð\9d\90\8dâ¦\83Tâ¦\84 â\86\92 L â\8a¢ â¬\87* T.
+lemma csn_cnf: â\88\80L,T. L â\8a¢ ð\9d\90\8dâ¦\83Tâ¦\84 â\86\92 L â\8a¢ â¬\8a* T.
/2 width=1/ qed.
-lemma csn_cpr_trans: â\88\80L,T1. L â\8a¢ â¬\87* T1 â\86\92 â\88\80T2. L â\8a¢ T1 â\9e¡ T2 â\86\92 L â\8a¢ â¬\87* T2.
+lemma csn_cpr_trans: â\88\80L,T1. L â\8a¢ â¬\8a* T1 â\86\92 â\88\80T2. L â\8a¢ T1 â\9e¡ T2 â\86\92 L â\8a¢ â¬\8a* T2.
#L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12
@csn_intro #T #HLT2 #HT2
elim (term_eq_dec T1 T2) #HT12
qed.
(* Basic_1: was: sn3_cast *)
-lemma csn_cast: â\88\80L,W. L â\8a¢ â¬\87* W â\86\92 â\88\80T. L â\8a¢ â¬\87* T â\86\92 L â\8a¢ â¬\87* ⓝW. T.
+lemma csn_cast: â\88\80L,W. L â\8a¢ â¬\8a* W â\86\92 â\88\80T. L â\8a¢ â¬\8a* T â\86\92 L â\8a¢ â¬\8a* ⓝW. T.
#L #W #HW elim HW -W #W #_ #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT
@csn_intro #X #H1 #H2
elim (cpr_inv_cast1 … H1) -H1
(* Basic forward lemmas *****************************************************)
-fact csn_fwd_flat_dx_aux: â\88\80L,U. L â\8a¢ â¬\87* U â\86\92 â\88\80I,V,T. U = â\93\95{I} V. T â\86\92 L â\8a¢ â¬\87* T.
+fact csn_fwd_flat_dx_aux: â\88\80L,U. L â\8a¢ â¬\8a* U â\86\92 â\88\80I,V,T. U = â\93\95{I} V. T â\86\92 L â\8a¢ â¬\8a* T.
#L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
@csn_intro #T2 #HLT2 #HT2
@(IH (ⓕ{I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/
qed.
(* Basic_1: was: sn3_gen_flat *)
-lemma csn_fwd_flat_dx: â\88\80I,L,V,T. L â\8a¢ â¬\87* â\93\95{I} V. T â\86\92 L â\8a¢ â¬\87* T.
+lemma csn_fwd_flat_dx: â\88\80I,L,V,T. L â\8a¢ â¬\8a* â\93\95{I} V. T â\86\92 L â\8a¢ â¬\8a* T.
/2 width=5/ qed-.
(* Basic_1: removed theorems 14:
(* Properties concerning atomic arity assignment ****************************)
-lemma csn_aaa: â\88\80L,T,A. L â\8a¢ T â\81\9d A â\86\92 L â\8a¢ â¬\87* T.
+lemma csn_aaa: â\88\80L,T,A. L â\8a¢ T â\81\9d A â\86\92 L â\8a¢ â¬\8a* T.
#L #T #A #H
@(acp_aaa … csn_acp csn_acr … H)
qed.
(* Basic eliminators ********************************************************)
lemma csna_ind: ∀L. ∀R:predicate term.
- (â\88\80T1. L â\8a¢ â¬\87â¬\87* T1 →
+ (â\88\80T1. L â\8a¢ â¬\8aâ¬\8a* T1 →
(∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → R T2) → R T1
) →
- â\88\80T. L â\8a¢ â¬\87â¬\87* T → R T.
+ â\88\80T. L â\8a¢ â¬\8aâ¬\8a* T → R T.
#L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1
@H0 -H0 /3 width=1/ -IHT1 /4 width=1/
qed-.
(* Basic_1: was: sn3_intro *)
lemma csna_intro: ∀L,T1.
- (â\88\80T2. L â\8a¢ T1 â\9e¡* T2 â\86\92 (T1 = T2 â\86\92 â\8a¥) â\86\92 L â\8a¢ â¬\87â¬\87* T2) â\86\92 L â\8a¢ â¬\87â¬\87* T1.
+ (â\88\80T2. L â\8a¢ T1 â\9e¡* T2 â\86\92 (T1 = T2 â\86\92 â\8a¥) â\86\92 L â\8a¢ â¬\8aâ¬\8a* T2) â\86\92 L â\8a¢ â¬\8aâ¬\8a* T1.
/4 width=1/ qed.
fact csna_intro_aux: ∀L,T1.
- (â\88\80T,T2. L â\8a¢ T â\9e¡* T2 â\86\92 T1 = T â\86\92 (T1 = T2 â\86\92 â\8a¥) â\86\92 L â\8a¢ â¬\87â¬\87* T2) â\86\92 L â\8a¢ â¬\87â¬\87* T1.
+ (â\88\80T,T2. L â\8a¢ T â\9e¡* T2 â\86\92 T1 = T â\86\92 (T1 = T2 â\86\92 â\8a¥) â\86\92 L â\8a¢ â¬\8aâ¬\8a* T2) â\86\92 L â\8a¢ â¬\8aâ¬\8a* T1.
/4 width=3/ qed-.
(* Basic_1: was: sn3_pr3_trans (old version) *)
-lemma csna_cprs_trans: â\88\80L,T1. L â\8a¢ â¬\87â¬\87* T1 â\86\92 â\88\80T2. L â\8a¢ T1 â\9e¡* T2 â\86\92 L â\8a¢ â¬\87â¬\87* T2.
+lemma csna_cprs_trans: â\88\80L,T1. L â\8a¢ â¬\8aâ¬\8a* T1 â\86\92 â\88\80T2. L â\8a¢ T1 â\9e¡* T2 â\86\92 L â\8a¢ â¬\8aâ¬\8a* T2.
#L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12
@csna_intro #T #HLT2 #HT2
elim (term_eq_dec T1 T2) #HT12
(* Basic_1: was: sn3_pr2_intro (old version) *)
lemma csna_intro_cpr: ∀L,T1.
- (â\88\80T2. L â\8a¢ T1 â\9e¡ T2 â\86\92 (T1 = T2 â\86\92 â\8a¥) â\86\92 L â\8a¢ â¬\87â¬\87* T2) →
- L â\8a¢ â¬\87â¬\87* T1.
+ (â\88\80T2. L â\8a¢ T1 â\9e¡ T2 â\86\92 (T1 = T2 â\86\92 â\8a¥) â\86\92 L â\8a¢ â¬\8aâ¬\8a* T2) →
+ L â\8a¢ â¬\8aâ¬\8a* T1.
#L #T1 #H
@csna_intro_aux #T #T2 #H @(cprs_ind_dx … H) -T
[ -H #H destruct #H
(* Main properties **********************************************************)
-theorem csn_csna: â\88\80L,T. L â\8a¢ â¬\87* T â\86\92 L â\8a¢ â¬\87â¬\87* T.
+theorem csn_csna: â\88\80L,T. L â\8a¢ â¬\8a* T â\86\92 L â\8a¢ â¬\8aâ¬\8a* T.
#L #T #H @(csn_ind … H) -T /4 width=1/
qed.
-theorem csna_csn: â\88\80L,T. L â\8a¢ â¬\87â¬\87* T â\86\92 L â\8a¢ â¬\87* T.
+theorem csna_csn: â\88\80L,T. L â\8a¢ â¬\8aâ¬\8a* T â\86\92 L â\8a¢ â¬\8a* T.
#L #T #H @(csna_ind … H) -T /4 width=1/
qed.
(* Basic_1: was: sn3_pr3_trans *)
-lemma csn_cprs_trans: â\88\80L,T1. L â\8a¢ â¬\87* T1 â\86\92 â\88\80T2. L â\8a¢ T1 â\9e¡* T2 â\86\92 L â\8a¢ â¬\87* T2.
+lemma csn_cprs_trans: â\88\80L,T1. L â\8a¢ â¬\8a* T1 â\86\92 â\88\80T2. L â\8a¢ T1 â\9e¡* T2 â\86\92 L â\8a¢ â¬\8a* T2.
/4 width=3/ qed.
(* Main eliminators *********************************************************)
lemma csn_ind_alt: ∀L. ∀R:predicate term.
- (â\88\80T1. L â\8a¢ â¬\87* T1 →
+ (â\88\80T1. L â\8a¢ â¬\8a* T1 →
(∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → R T2) → R T1
) →
- â\88\80T. L â\8a¢ â¬\87* T → R T.
+ â\88\80T. L â\8a¢ â¬\8a* T → R T.
#L #R #H0 #T1 #H @(csna_ind … (csn_csna … H)) -T1 #T1 #HT1 #IHT1
@H0 -H0 /2 width=1/ -HT1 /3 width=1/
qed-.
(* Advanced forvard lemmas **************************************************)
-fact csn_fwd_pair_sn_aux: â\88\80L,U. L â\8a¢ â¬\87* U â\86\92 â\88\80I,V,T. U = â\91¡{I} V. T â\86\92 L â\8a¢ â¬\87* V.
+fact csn_fwd_pair_sn_aux: â\88\80L,U. L â\8a¢ â¬\8a* U â\86\92 â\88\80I,V,T. U = â\91¡{I} V. T â\86\92 L â\8a¢ â¬\8a* V.
#L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
@csn_intro #V2 #HLV2 #HV2
@(IH (②{I} V2. T)) -IH // /2 width=1/ -HLV2 #H destruct /2 width=1/
qed.
(* Basic_1: was: sn3_gen_head *)
-lemma csn_fwd_pair_sn: â\88\80I,L,V,T. L â\8a¢ â¬\87* â\91¡{I} V. T â\86\92 L â\8a¢ â¬\87* V.
+lemma csn_fwd_pair_sn: â\88\80I,L,V,T. L â\8a¢ â¬\8a* â\91¡{I} V. T â\86\92 L â\8a¢ â¬\8a* V.
/2 width=5/ qed.
-fact csn_fwd_bind_dx_aux: â\88\80L,U. L â\8a¢ â¬\87* U →
- â\88\80I,V,T. U = â\93\91{I} V. T â\86\92 L. â\93\91{I} V â\8a¢ â¬\87* T.
+fact csn_fwd_bind_dx_aux: â\88\80L,U. L â\8a¢ â¬\8a* U →
+ â\88\80I,V,T. U = â\93\91{I} V. T â\86\92 L. â\93\91{I} V â\8a¢ â¬\8a* T.
#L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
@csn_intro #T2 #HLT2 #HT2
@(IH (ⓑ{I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/
qed.
(* Basic_1: was: sn3_gen_bind *)
-lemma csn_fwd_bind_dx: â\88\80I,L,V,T. L â\8a¢ â¬\87* â\93\91{I} V. T â\86\92 L. â\93\91{I} V â\8a¢ â¬\87* T.
+lemma csn_fwd_bind_dx: â\88\80I,L,V,T. L â\8a¢ â¬\8a* â\93\91{I} V. T â\86\92 L. â\93\91{I} V â\8a¢ â¬\8a* T.
/2 width=3/ qed.
(* Advanced forward lemmas **************************************************)
-lemma csn_fwd_applv: â\88\80L,T,Vs. L â\8a¢ â¬\87* â\92¶ Vs. T â\86\92 L â\8a¢ â¬\87* Vs â\88§ L â\8a¢ â¬\87* T.
+lemma csn_fwd_applv: â\88\80L,T,Vs. L â\8a¢ â¬\8a* â\92¶ Vs. T â\86\92 L â\8a¢ â¬\8a* Vs â\88§ L â\8a¢ â¬\8a* T.
#L #T #Vs elim Vs -Vs /2 width=1/
#V #Vs #IHVs #HVs
lapply (csn_fwd_pair_sn … HVs) #HV
(* Advanced properties ******************************************************)
-lemma csn_lcpr_conf: â\88\80L1,L2. L1 â\8a¢ â\9e¡ L2 â\86\92 â\88\80T. L1 â\8a¢ â¬\87* T â\86\92 L2 â\8a¢ â¬\87* T.
+lemma csn_lcpr_conf: â\88\80L1,L2. L1 â\8a¢ â\9e¡ L2 â\86\92 â\88\80T. L1 â\8a¢ â¬\8a* T â\86\92 L2 â\8a¢ â¬\8a* T.
#L1 #L2 #HL12 #T #H @(csn_ind_alt … H) -T #T #_ #IHT
@csn_intro #T0 #HLT0 #HT0
@IHT /2 width=2/ -IHT -HT0 /2 width=3/
qed.
-lemma csn_abbr: â\88\80L,V. L â\8a¢ â¬\87* V â\86\92 â\88\80T. L. â\93\93V â\8a¢ â¬\87* T â\86\92 L â\8a¢ â¬\87* ⓓV. T.
+lemma csn_abbr: â\88\80L,V. L â\8a¢ â¬\8a* V â\86\92 â\88\80T. L. â\93\93V â\8a¢ â¬\8a* T â\86\92 L â\8a¢ â¬\8a* ⓓV. T.
#L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_alt … HT) -T #T #HT #IHT
@csn_intro #X #H1 #H2
elim (cpr_inv_abbr1 … H1) -H1 *
]
qed.
-fact csn_appl_beta_aux: â\88\80L,W. L â\8a¢ â¬\87* W â\86\92 â\88\80U. L â\8a¢ â¬\87* U →
- â\88\80V,T. U = â\93\93V. T â\86\92 L â\8a¢ â¬\87* ⓐV. ⓛW. T.
+fact csn_appl_beta_aux: â\88\80L,W. L â\8a¢ â¬\8a* W â\86\92 â\88\80U. L â\8a¢ â¬\8a* U →
+ â\88\80V,T. U = â\93\93V. T â\86\92 L â\8a¢ â¬\8a* ⓐV. ⓛW. T.
#L #W #H elim H -W #W #_ #IHW #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V #T #H destruct
lapply (csn_fwd_pair_sn … HVT) #HV
lapply (csn_fwd_bind_dx … HVT) #HT -HVT
qed.
(* Basic_1: was: sn3_beta *)
-lemma csn_appl_beta: â\88\80L,W. L â\8a¢ â¬\87* W â\86\92 â\88\80V,T. L â\8a¢ â¬\87* ⓓV. T →
- L â\8a¢ â¬\87* ⓐV. ⓛW. T.
+lemma csn_appl_beta: â\88\80L,W. L â\8a¢ â¬\8a* W â\86\92 â\88\80V,T. L â\8a¢ â¬\8a* ⓓV. T →
+ L â\8a¢ â¬\8a* ⓐV. ⓛW. T.
/2 width=3/ qed.
-fact csn_appl_theta_aux: â\88\80L,U. L â\8a¢ â¬\87* U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
- â\88\80V,T. U = â\93\93V. â\93\90V2. T â\86\92 L â\8a¢ â¬\87* ⓐV1. ⓓV. T.
+fact csn_appl_theta_aux: â\88\80L,U. L â\8a¢ â¬\8a* U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
+ â\88\80V,T. U = â\93\93V. â\93\90V2. T â\86\92 L â\8a¢ â¬\8a* ⓐV1. ⓓV. T.
#L #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
lapply (csn_fwd_pair_sn … HVT) #HV
lapply (csn_fwd_bind_dx … HVT) -HVT #HVT
qed.
lemma csn_appl_theta: ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
- â\88\80L,V,T. L â\8a¢ â¬\87* â\93\93V. â\93\90V2. T â\86\92 L â\8a¢ â¬\87* ⓐV1. ⓓV. T.
+ â\88\80L,V,T. L â\8a¢ â¬\8a* â\93\93V. â\93\90V2. T â\86\92 L â\8a¢ â¬\8a* ⓐV1. ⓓV. T.
/2 width=5/ qed.
(* Basic_1: was only: sn3_appl_appl *)
-lemma csn_appl_simple_tstc: â\88\80L,V. L â\8a¢ â¬\87* V → ∀T1.
- L â\8a¢ â¬\87* T1 →
- (â\88\80T2. L â\8a¢ T1 â\9e¡* T2 â\86\92 (T1 â\89\83 T2 â\86\92 â\8a¥) â\86\92 L â\8a¢ â¬\87* ⓐV. T2) →
- ð\9d\90\92â¦\83T1â¦\84 â\86\92 L â\8a¢ â¬\87* ⓐV. T1.
+lemma csn_appl_simple_tstc: â\88\80L,V. L â\8a¢ â¬\8a* V → ∀T1.
+ L â\8a¢ â¬\8a* T1 →
+ (â\88\80T2. L â\8a¢ T1 â\9e¡* T2 â\86\92 (T1 â\89\83 T2 â\86\92 â\8a¥) â\86\92 L â\8a¢ â¬\8a* ⓐV. T2) →
+ ð\9d\90\92â¦\83T1â¦\84 â\86\92 L â\8a¢ â¬\8a* ⓐ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
elim (cpr_inv_appl1_simple … HL ?) -HL //
(* Relocation properties ****************************************************)
(* Basic_1: was: sn3_lift *)
-lemma csn_lift: â\88\80L2,L1,T1,d,e. L1 â\8a¢ â¬\87* T1 →
- â\88\80T2. â\87©[d, e] L2 â\89¡ L1 â\86\92 â\87§[d, e] T1 â\89¡ T2 â\86\92 L2 â\8a¢ â¬\87* T2.
+lemma csn_lift: â\88\80L2,L1,T1,d,e. L1 â\8a¢ â¬\8a* T1 →
+ â\88\80T2. â\87©[d, e] L2 â\89¡ L1 â\86\92 â\87§[d, e] T1 â\89¡ T2 â\86\92 L2 â\8a¢ â¬\8a* T2.
#L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL21 #HT12
@csn_intro #T #HLT2 #HT2
-elim (cpr_inv_lift … HL21 … HT12 … HLT2) -HLT2 #T0 #HT0 #HLT10
+elim (cpr_inv_lift1 … HL21 … HT12 … HLT2) -HLT2 #T0 #HT0 #HLT10
@(IHT1 … HLT10) // -L1 -L2 #H destruct
>(lift_mono … HT0 … HT12) in HT2; -T1 /2 width=1/
qed.
(* Basic_1: was: sn3_gen_lift *)
-lemma csn_inv_lift: â\88\80L2,L1,T1,d,e. L1 â\8a¢ â¬\87* T1 →
- â\88\80T2. â\87©[d, e] L1 â\89¡ L2 â\86\92 â\87§[d, e] T2 â\89¡ T1 â\86\92 L2 â\8a¢ â¬\87* T2.
+lemma csn_inv_lift: â\88\80L2,L1,T1,d,e. L1 â\8a¢ â¬\8a* T1 →
+ â\88\80T2. â\87©[d, e] L1 â\89¡ L2 â\86\92 â\87§[d, e] T2 â\89¡ T1 â\86\92 L2 â\8a¢ â¬\8a* T2.
#L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL12 #HT21
@csn_intro #T #HLT2 #HT2
elim (lift_total T d e) #T0 #HT0
(* Advanced properties ******************************************************)
(* Basic_1: was: sn3_abbr *)
-lemma csn_lref_abbr: â\88\80L,K,V,i. â\87©[0, i] L â\89¡ K. â\93\93V â\86\92 K â\8a¢ â¬\87* V â\86\92 L â\8a¢ â¬\87* #i.
+lemma csn_lref_abbr: â\88\80L,K,V,i. â\87©[0, i] L â\89¡ K. â\93\93V â\86\92 K â\8a¢ â¬\8a* V â\86\92 L â\8a¢ â¬\8a* #i.
#L #K #V #i #HLK #HV
@csn_intro #X #H #Hi
elim (cpr_inv_lref1 … H) -H
]
qed.
-lemma csn_abst: â\88\80L,W. L â\8a¢ â¬\87* W â\86\92 â\88\80I,V,T. L. â\93\91{I} V â\8a¢ â¬\87* T â\86\92 L â\8a¢ â¬\87* ⓛW. T.
+lemma csn_abst: â\88\80L,W. L â\8a¢ â¬\8a* W â\86\92 â\88\80I,V,T. L. â\93\91{I} V â\8a¢ â¬\8a* T â\86\92 L â\8a¢ â¬\8a* ⓛW. T.
#L #W #HW elim HW -W #W #_ #IHW #I #V #T #HT @(csn_ind … HT) -T #T #HT #IHT
@csn_intro #X #H1 #H2
elim (cpr_inv_abst1 … H1 I V) -H1
]
qed.
-lemma csn_appl_simple: â\88\80L,V. L â\8a¢ â¬\87* V → ∀T1.
- (â\88\80T2. L â\8a¢ T1 â\9e¡ T2 â\86\92 (T1 = T2 â\86\92 â\8a¥) â\86\92 L â\8a¢ â¬\87* ⓐV. T2) →
- ð\9d\90\92â¦\83T1â¦\84 â\86\92 L â\8a¢ â¬\87* ⓐV. T1.
+lemma csn_appl_simple: â\88\80L,V. L â\8a¢ â¬\8a* V → ∀T1.
+ (â\88\80T2. L â\8a¢ T1 â\9e¡ T2 â\86\92 (T1 = T2 â\86\92 â\8a¥) â\86\92 L â\8a¢ â¬\8a* ⓐV. T2) →
+ ð\9d\90\92â¦\83T1â¦\84 â\86\92 L â\8a¢ â¬\8a* ⓐV. T1.
#L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #IHT1 #HT1
@csn_intro #X #H1 #H2
elim (cpr_inv_appl1_simple … H1 ?) // -H1
(* Advanced inversion lemmas ************************************************)
(* Basic_1: was: sn3_gen_def *)
-lemma csn_inv_lref_abbr: â\88\80L,K,V,i. â\87©[0, i] L â\89¡ K. â\93\93V â\86\92 L â\8a¢ â¬\87* #i â\86\92 K â\8a¢ â¬\87* V.
+lemma csn_inv_lref_abbr: â\88\80L,K,V,i. â\87©[0, i] L â\89¡ K. â\93\93V â\86\92 L â\8a¢ â¬\8a* #i â\86\92 K â\8a¢ â¬\8a* V.
#L #K #V #i #HLK #Hi
elim (lift_total V 0 (i+1)) #V0 #HV0
lapply (ldrop_fwd_ldrop2 … HLK) #H0LK
(* Basic_1: was only: sn3_appls_lref *)
lemma csn_applv_cnf: ∀L,T. 𝐒⦃T⦄ → L ⊢ 𝐍⦃T⦄ →
- â\88\80Vs. L â\8a¢ â¬\87* Vs â\86\92 L â\8a¢ â¬\87* ⒶVs.T.
+ â\88\80Vs. L â\8a¢ â¬\8a* Vs â\86\92 L â\8a¢ â¬\8a* ⒶVs.T.
#L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(csn_cnf … H2T) ] (**) (* /2 width=1/ does not work *)
#V #Vs #IHV #H
elim (csnv_inv_cons … H) -H #HV #HVs
qed.
(* Basic_1: was: sn3_appls_beta *)
-lemma csn_applv_beta: â\88\80L,W. L â\8a¢ â¬\87* W →
- â\88\80Vs,V,T. L â\8a¢ â¬\87* ⒶVs.ⓓV.T →
- L â\8a¢ â¬\87* ⒶVs. ⓐV.ⓛW. T.
+lemma csn_applv_beta: â\88\80L,W. L â\8a¢ â¬\8a* W →
+ â\88\80Vs,V,T. L â\8a¢ â¬\8a* ⒶVs.ⓓV.T →
+ L â\8a¢ â¬\8a* ⒶVs. ⓐV.ⓛW. T.
#L #W #HW #Vs elim Vs -Vs /2 width=1/ -HW
#V0 #Vs #IHV #V #T #H1T
lapply (csn_fwd_pair_sn … H1T) #HV0
lemma csn_applv_delta: ∀L,K,V1,i. ⇩[0, i] L ≡ K. ⓓV1 →
∀V2. ⇧[0, i + 1] V1 ≡ V2 →
- â\88\80Vs.L â\8a¢ â¬\87* (â\92¶Vs. V2) â\86\92 L â\8a¢ â¬\87* (ⒶVs. #i).
+ â\88\80Vs.L â\8a¢ â¬\8a* (â\92¶Vs. V2) â\86\92 L â\8a¢ â¬\8a* (ⒶVs. #i).
#L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
[ #H
lapply (ldrop_fwd_ldrop2 … HLK) #HLK0
(* Basic_1: was: sn3_appls_abbr *)
lemma csn_applv_theta: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
- â\88\80V,T. L â\8a¢ â¬\87* â\93\93V. â\92¶V2s. T â\86\92 L â\8a¢ â¬\87* V →
- L â\8a¢ â¬\87* ⒶV1s. ⓓV. T.
+ â\88\80V,T. L â\8a¢ â¬\8a* â\93\93V. â\92¶V2s. T â\86\92 L â\8a¢ â¬\8a* V →
+ L â\8a¢ â¬\8a* ⒶV1s. ⓓV. T.
#L #V1s #V2s * -V1s -V2s /2 width=1/
#V1s #V2s #V1 #V2 #HV12 #H
generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1
qed.
(* Basic_1: was: sn3_appls_cast *)
-lemma csn_applv_tau: â\88\80L,W. L â\8a¢ â¬\87* W →
- â\88\80Vs,T. L â\8a¢ â¬\87* ⒶVs. T →
- L â\8a¢ â¬\87* ⒶVs. ⓝW. T.
+lemma csn_applv_tau: â\88\80L,W. L â\8a¢ â¬\8a* W →
+ â\88\80Vs,T. L â\8a¢ â¬\8a* ⒶVs. T →
+ L â\8a¢ â¬\8a* ⒶVs. ⓝW. T.
#L #W #HW #Vs elim Vs -Vs /2 width=1/ -HW
#V #Vs #IHV #T #H1T
lapply (csn_fwd_pair_sn … H1T) #HV
]
qed.
-theorem csn_acr: acr cpr (eq â\80¦) (csn â\80¦) (λL,T. L â\8a¢ â¬\87* T).
+theorem csn_acr: acr cpr (eq â\80¦) (csn â\80¦) (λL,T. L â\8a¢ â¬\8a* T).
@mk_acr //
[ /3 width=1/
| /2 width=1/
(* Basic inversion lemmas ***************************************************)
-lemma csnv_inv_cons: â\88\80L,T,Ts. L â\8a¢ â¬\87* T @ Ts â\86\92 L â\8a¢ â¬\87* T â\88§ L â\8a¢ â¬\87* Ts.
+lemma csnv_inv_cons: â\88\80L,T,Ts. L â\8a¢ â¬\8a* T @ Ts â\86\92 L â\8a¢ â¬\8a* T â\88§ L â\8a¢ â¬\8a* Ts.
normalize // 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/reducibility/xpr.ma".
+(*
+include "basic_2/reducibility/cnf.ma".
+*)
+(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************)
+
+definition xprs: ∀h. sd h → lenv → relation term ≝
+ λh,g,L. TC … (xpr h g L).
+
+interpretation "extended parallel computation (term)"
+ 'XPRedStar h g L T1 T2 = (xprs h g L T1 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma xprs_ind: ∀h,g,L,T1. ∀R:predicate term. R T1 →
+ (∀T,T2. ⦃h, L⦄ ⊢ T1 ➸*[g] T → ⦃h, L⦄ ⊢ T ➸[g] T2 → R T → R T2) →
+ ∀T2. ⦃h, L⦄ ⊢ T1 ➸*[g] T2 → R T2.
+#h #g #L #T1 #R #HT1 #IHT1 #T2 #HT12
+@(TC_star_ind … HT1 IHT1 … HT12) //
+qed-.
+
+lemma xprs_ind_dx: ∀h,g,L,T2. ∀R:predicate term. R T2 →
+ (∀T1,T. ⦃h, L⦄ ⊢ T1 ➸[g] T → ⦃h, L⦄ ⊢ T ➸*[g] T2 → R T → R T1) →
+ ∀T1. ⦃h, L⦄ ⊢ T1 ➸*[g] T2 → R T1.
+#h #g #L #T2 #R #HT2 #IHT2 #T1 #HT12
+@(TC_star_ind_dx … HT2 IHT2 … HT12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma xprs_refl: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ➸*[g] T.
+/2 width=1/ qed.
+
+lemma xprs_strap1: ∀h,g,L,T1,T,T2.
+ ⦃h, L⦄ ⊢ T1 ➸*[g] T → ⦃h, L⦄ ⊢ T ➸[g] T2 → ⦃h, L⦄ ⊢ T1 ➸*[g] T2.
+/2 width=3/ qed.
+
+lemma xprs_strap2: ∀h,g,L,T1,T,T2.
+ ⦃h, L⦄ ⊢ T1 ➸[g] T → ⦃h, L⦄ ⊢ T ➸*[g] T2 → ⦃h, L⦄ ⊢ T1 ➸*[g] T2.
+/2 width=3/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+(*
+axiom xprs_inv_cnf1: ∀L,T,U. L ⊢ T ➡* U → L ⊢ 𝐍⦃T⦄ → T = U.
+(*
+#L #T #U #H @(xprs_ind_dx … H) -T //
+#T0 #T #H1T0 #_ #IHT #H2T0
+lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/
+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/reducibility/xpr_lift.ma".
+include "basic_2/computation/cprs.ma".
+include "basic_2/computation/xprs.ma".
+
+(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************)
+
+(* Advanced forward lemmas **************************************************)
+
+lemma xprs_fwd_abst1: ∀h,g,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛV1. T1 ➸*[g] U2 →
+ ∃∃V2,T2. L ⊢ V1 ➡* V2 & U2 = ⓛV2. T2.
+#h #g #L #V1 #T1 #U2 #H @(xprs_ind … H) -U2 /2 width=4/
+#U #U2 #_ #HU2 * #V #T #HV1 #H destruct
+elim (xpr_inv_abst1 … HU2) -HU2 #V2 #T2 #HV2 #_ #H destruct /3 width=4/
+qed-.
+
+(* Relocation properties ****************************************************)
+
+lemma xprs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → ∀T1,U1. ⇧[d, e] T1 ≡ U1 →
+ ∀h,g,T2. ⦃h, K⦄ ⊢ T1 ➸*[g] T2 → ∀U2. ⇧[d, e] T2 ≡ U2 →
+ ⦃h, L⦄ ⊢ U1 ➸*[g] U2.
+#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #T2 #HT12 @(xprs_ind … HT12) -T2
+[ -HLK #T2 #HT12
+ <(lift_mono … HTU1 … HT12) -T1 //
+| -HTU1 #T #T2 #_ #HT2 #IHT2 #U2 #HTU2
+ elim (lift_total T d e) #U #HTU
+ lapply (xpr_lift … HLK … HTU … HTU2 … HT2) -T2 -HLK (* /3 width=3/ *)
+ #H @(step …H) /2 width=1/ (**) (* NTypeChecker failure *)
+]
+qed.
+
+lemma xprs_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K →
+ ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀h,g,U2. ⦃h, L⦄ ⊢ U1 ➸*[g] U2 →
+ ∃∃T2. ⇧[d, e] T2 ≡ U2 & ⦃h, K⦄ ⊢ T1 ➸*[g] T2.
+#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #U2 #HU12 @(xprs_ind … HU12) -U2 /2 width=3/
+-HTU1 #U #U2 #_ #HU2 * #T #HTU #HT1
+elim (xpr_inv_lift1 … HLK … HTU … HU2) -U -HLK (* /3 width=5/ *)
+#U #HU2 #HTU @(ex2_1_intro … HU2) @(step … HT1 HTU) (**) (* NTypeChecker failure *)
+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/computation/cprs.ma".
+include "basic_2/computation/xprs.ma".
+include "basic_2/equivalence/cpcs.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+inductive snv (h:sh) (g:sd h): lenv → predicate term ≝
+| snv_sort: ∀L,k. snv h g L (⋆k)
+| snv_lref: ∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → snv h g K V → snv h g L (#i)
+| snv_bind: ∀I,L,V,T. snv h g L V → snv h g (L.ⓑ{I}V) T → snv h g L (ⓑ{I}V.T)
+| snv_appl: ∀L,V,W,W0,T,U,l. snv h g L V → snv h g L T →
+ ⦃h, L⦄ ⊢ V •[g, l + 1] W → L ⊢ W ➡* W0 →
+ ⦃h, L⦄ ⊢ T ➸*[g] ⓛW0.U → snv h g L (ⓐV.T)
+| snv_cast: ∀L,W,T,U,l. snv h g L W → snv h g L T →
+ ⦃h, L⦄ ⊢ T •[g, l + 1] U → L ⊢ U ⬌* W → snv h g L (ⓝW.T)
+.
+
+interpretation "stratified native validity (term)"
+ 'NativeValid h g L T = (snv h g L T).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma snv_inv_bind_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀I,V,T. X = ⓑ{I}V.T →
+ ⦃h, L⦄ ⊩ V :[g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊩ T :[g].
+#h #g #L #X * -L -X
+[ #L #k #I #V #T #H destruct
+| #I0 #L #K #V0 #i #_ #_ #I #V #T #H destruct
+| #I0 #L #V0 #T0 #HV0 #HT0 #I #V #T #H destruct /2 width=1/
+| #L #V0 #W0 #W00 #T0 #U0 #l #_ #_ #_ #_ #_ #I #V #T #H destruct
+| #L #W0 #T0 #U0 #l #_ #_ #_ #_ #I #V #T #H destruct
+]
+qed.
+
+lemma snv_inv_bind: ∀h,g,I,L,V,T. ⦃h, L⦄ ⊩ ⓑ{I}V.T :[g] →
+ ⦃h, L⦄ ⊩ V :[g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊩ T :[g].
+/2 width=3/ qed-.
+
+lemma snv_inv_appl_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀V,T. X = ⓐV.T →
+ ∃∃W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] &
+ ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 &
+ ⦃h, L⦄ ⊢ T ➸*[g] ⓛW0.U.
+#h #g #L #X * -L -X
+[ #L #k #V #T #H destruct
+| #I #L #K #V0 #i #_ #_ #V #T #H destruct
+| #I #L #V0 #T0 #_ #_ #V #T #H destruct
+| #L #V0 #W0 #W00 #T0 #U0 #l #HV0 #HT0 #HVW0 #HW00 #HTU0 #V #T #H destruct /2 width=7/
+| #L #W0 #T0 #U0 #l #_ #_ #_ #_ #V #T #H destruct
+]
+qed.
+
+lemma snv_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊩ ⓐV.T :[g] →
+ ∃∃W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] &
+ ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 &
+ ⦃h, L⦄ ⊢ T ➸*[g] ⓛW0.U.
+/2 width=3/ 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/computation/xprs_lift.ma".
+include "basic_2/equivalence/cpcs_cpcs.ma".
+include "basic_2/dynamic/snv.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Relocation properties ****************************************************)
+
+lemma snv_lift: ∀h,g,K,T. ⦃h, K⦄ ⊩ T :[g] → ∀L,d,e. ⇩[d, e] L ≡ K →
+ ∀U. ⇧[d, e] T ≡ U → ⦃h, L⦄ ⊩ U :[g].
+#h #g #K #T #H elim H -K -T
+[ #K #k #L #d #e #_ #X #H
+ >(lift_inv_sort1 … H) -X -K -d -e //
+| #I #K #K0 #V #i #HK0 #_ #IHV #L #d #e #HLK #X #H
+ elim (lift_inv_lref1 … H) * #Hid #H destruct
+ [ elim (ldrop_trans_le … HLK … HK0 ?) -K /2 width=2/ #X #HL0 #H
+ elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #L0 #W #HLK0 #HVW #H destruct
+ /3 width=8/
+ | lapply (ldrop_trans_ge … HLK … HK0 ?) -K // -Hid /3 width=8/
+ ]
+| #I #K #V #T #_ #_ #IHV #IHT #L #d #e #HLK #X #H
+ elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct
+ /4 width=4/
+| #K #V #V0 #V1 #T #T1 #l #_ #_ #HV0 #HV01 #HT1 #IHV #IHT #L #d #e #HLK #X #H
+ elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct
+ elim (lift_total V0 d e) #W0 #HVW0
+ elim (lift_total V1 d e) #W1 #HVW1
+ elim (lift_total T1 (d+1) e) #U1 #HTU1
+ @(snv_appl … W0 … W1 … U1 l)
+ [ /2 width=4/ | /2 width=4/ | /2 width=9/ | /2 width=9/ ]
+ @(xprs_lift … HLK … HTU … HT1) /2 width=1/
+| #K #V0 #T #V #l #_ #_ #HTV #HV0 #IHV0 #IHT #L #d #e #HLK #X #H
+ elim (lift_inv_flat1 … H) -H #W0 #U #HVW0 #HTU #H destruct
+ elim (lift_total V d e) #W #HVW
+ @(snv_cast … W l) [ /2 width=4/ | /2 width=4/ | /2 width=9/ | /2 width=9/ ]
+]
+qed.
+
+lemma snv_inv_lift: ∀h,g,L,U. ⦃h, L⦄ ⊩ U :[g] → ∀K,d,e. ⇩[d, e] L ≡ K →
+ ∀T. ⇧[d, e] T ≡ U → ⦃h, K⦄ ⊩ T :[g].
+#h #g #L #U #H elim H -L -U
+[ #L #k #K #d #e #_ #X #H
+ >(lift_inv_sort2 … H) -X -L -d -e //
+| #I #L #L0 #W #i #HL0 #_ #IHW #K #d #e #HLK #X #H
+ elim (lift_inv_lref2 … H) * #Hid #H destruct
+ [ elim (ldrop_conf_le … HLK … HL0 ?) -L /2 width=2/ #X #HK0 #H
+ elim (ldrop_inv_skip1 … H ?) -H /2 width=1/ -Hid #K0 #V #HLK0 #HVW #H destruct
+ /3 width=8/
+ | lapply (ldrop_conf_ge … HLK … HL0 ?) -L // -Hid /3 width=8/
+ ]
+| #I #L #W #U #_ #_ #IHW #IHU #K #d #e #HLK #X #H
+ elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct /4 width=4/
+| #L #W #W0 #W1 #U #U1 #l #_ #_ #HW0 #HW01 #HU1 #IHW #IHU #K #d #e #HLK #X #H
+ elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct
+ elim (ssta_inv_lift1 … HW0 … HLK … HVW) -HW0 #V0 #HV0 #HVW0
+ elim (cprs_inv_lift1 … HLK … HVW0 … HW01) -W0 #V1 #HVW1 #HV01
+ elim (xprs_inv_lift1 … HLK … HTU … HU1) -HU1 #X #H #HTU
+ elim (lift_inv_bind2 … H) -H #Y #T1 #HY #HTU1 #H destruct
+ lapply (lift_inj … HY … HVW1) -HY #H destruct /3 width=7/
+| #L #W0 #U #W #l #_ #_ #HUW #HW0 #IHW0 #IHU #K #d #e #HLK #X #H
+ elim (lift_inv_flat2 … H) -H #V0 #T #HVW0 #HTU #H destruct
+ elim (ssta_inv_lift1 … HUW … HLK … HTU) -HUW #V #HTV #HVW
+ lapply (cpcs_inv_lift … HLK … HVW … HVW0 ?) // -W /3 width=4/
+]
+qed-.
L ⊢ U1 ⬌* U2 → K ⊢ T1 ⬌* T2.
#L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HU12
elim (cpcs_inv_cprs … HU12) -HU12 #U #HU1 #HU2
-elim (cprs_inv_lift … HLK … HTU1 … HU1) -U1 #T #HTU #HT1
-elim (cprs_inv_lift … HLK … HTU2 … HU2) -L -U2 #X #HXU
+elim (cprs_inv_lift1 … HLK … HTU1 … HU1) -U1 #T #HTU #HT1
+elim (cprs_inv_lift1 … HLK … HTU2 … HU2) -L -U2 #X #HXU
>(lift_inj … HXU … HTU) -X -U -d -e /2 width=3/
qed-.
(* Properties on inverse basic term relocation ******************************)
-lemma cpcs_zeta_delift_comm: ∀L,V,T1,T2. L.ⓓV ⊢ T1 ▼*[O, 1] ≡ T2 →
+lemma cpcs_zeta_delift_comm: ∀L,V,T1,T2. L.ⓓV ⊢ ▼*[O, 1] T1 ≡ T2 →
L ⊢ T2 ⬌* ⓓV.T1.
/3 width=1/ qed.
(* Basic_1: was only: pc3_gen_cabbr *)
lemma thin_cpcs_delift_mono: ∀L,U1,U2. L ⊢ U1 ⬌* U2 →
- ∀K,d,e. L ▼*[d, e] ≡ K → ∀T1. L ⊢ U1 ▼*[d, e] ≡ T1 →
- ∀T2. L ⊢ U2 ▼*[d, e] ≡ T2 → K ⊢ T1 ⬌* T2.
+ ∀K,d,e. ▼*[d, e] L ≡ K → ∀T1. L ⊢ ▼*[d, e] U1 ≡ T1 →
+ ∀T2. L ⊢ ▼*[d, e] U2 ≡ T2 → K ⊢ T1 ⬌* T2.
#L #U1 #U2 #H #K #d #e #HLK #T1 #HTU1 #T2 #HTU2
elim (cpcs_inv_cprs … H) -H #U #HU1 #HU2
elim (thin_cprs_delift_conf … HU1 … HLK … HTU1) -U1 #T #HT1 #HUT
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 }.
-notation "hvbox( T1 break ▼* [ d , break e ] ≡ break term 46 T2 )"
+notation "hvbox( ▼ * [ d , break e ] break term 46 T1 ≡ break term 46 T2 )"
non associative with precedence 45
for @{ 'TSubst $T1 $d $e $T2 }.
-notation "hvbox( L ⊢ break term 46 T1 break ▼* [ d , break e ] ≡ break term 46 T2 )"
+notation "hvbox( L ⊢ break ▼ * [ d , break e ] break term 46 T1 ≡ break term 46 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( ▼ ▼ * [ d , break e ] break term 46 T1 ≡ 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 ▼ ▼ * [ d , break e ] break term 46 T1 ≡ break term 46 T2 )"
non associative with precedence 45
for @{ 'TSubstAlt $L $T1 $d $e $T2 }.
non associative with precedence 45
for @{ 'CrSubEqA $T1 $T2 }.
-notation "hvbox( L ⊢ break term 46 T ÷ break term 46 A )"
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T ÷ break term 46 A )"
non associative with precedence 45
- for @{ 'BinaryArity $L $T $A }.
+ for @{ 'BinaryArity $h $L $T $A }.
-notation "hvbox( T1 ÷ ⊑ break term 46 T2 )"
+notation "hvbox( h ⊢ break term 46 L1 ÷ ⊑ break term 46 L2 )"
non associative with precedence 45
- for @{ 'CrSubEqB $T1 $T2 }.
+ for @{ 'CrSubEqB $h $L1 $L2 }.
notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 • break [ g , break l ] break term 46 T2 )"
non associative with precedence 45
for @{ 'StaticType $h $g $l $L $T1 $T2 }.
+notation "hvbox( h ⊢ break term 46 L1 • ⊑ [ g ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'CrSubEqS $h $g $L1 $L2 }.
+
(* Unwind *******************************************************************)
notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 •* break [ g ] break term 46 T2 )"
notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 ➸ break [ g ] break term 46 T2 )"
non associative with precedence 45
- for @{ 'XRed $h $g $L $T1 $T2 }.
+ for @{ 'XPRed $h $g $L $T1 $T2 }.
(* Computation **************************************************************)
non associative with precedence 45
for @{ 'PEval $L $T1 $T2 }.
-notation "hvbox( â¬\87 * term 46 T )"
+notation "hvbox( â¬\8a * term 46 T )"
non associative with precedence 45
for @{ 'SN $T }.
-notation "hvbox( L â\8a¢ â¬\87 * break term 46 T )"
+notation "hvbox( L â\8a¢ â¬\8a * break term 46 T )"
non associative with precedence 45
for @{ 'SN $L $T }.
-notation "hvbox( L â\8a¢ â¬\87 â¬\87 * break term 46 T )"
+notation "hvbox( L â\8a¢ â¬\8a â¬\8a * break term 46 T )"
non associative with precedence 45
for @{ 'SNAlt $L $T }.
notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 ➸ * break [ g ] break term 46 T2 )"
non associative with precedence 45
- for @{ 'XRedStar $h $g $L $T1 $T2 }.
+ for @{ 'XPRedStar $h $g $L $T1 $T2 }.
notation "hvbox( ⦃ h , break L ⦄ ⊢ ➷ * break [ g ] break term 46 T2 )"
non associative with precedence 45
lemma cnf_lift: ∀L0,L,T,T0,d,e.
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
+elim (cpr_inv_lift1 … HL0 … HT0 … H) -L0 #T1 #HT10 #HT1
<(HLT … HT1) in HT0; -L #HT0
>(lift_mono … HT10 … HT0) -T1 -X //
qed.
(* Basic_1: was only: pr2_gen_cabbr *)
lemma thin_cpr_delift_conf: ∀L,U1,U2. L ⊢ U1 ➡ U2 →
- ∀K,d,e. L ▼*[d, e] ≡ K → ∀T1. L ⊢ U1 ▼*[d, e] ≡ T1 →
- ∃∃T2. K ⊢ T1 ➡ T2 & L ⊢ U2 ▼*[d, e] ≡ T2.
+ ∀K,d,e. ▼*[d, e] L ≡ K → ∀T1. L ⊢ ▼*[d, e] U1 ≡ T1 →
+ ∃∃T2. K ⊢ T1 ➡ T2 & L ⊢ ▼*[d, e] U2 ≡ T2.
#L #U1 #U2 * #U #HU1 #HU2 #K #d #e #HLK #T1 #HTU1
elim (tpr_delift_conf … HU1 … HTU1) -U1 #T #HT1 #HUT
elim (le_or_ge (|L|) d) #Hd
qed.
(* Basic_1: was: pr2_gen_lift *)
-lemma cpr_inv_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K →
- ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀U2. L ⊢ U1 ➡ U2 →
- ∃∃T2. ⇧[d, e] T2 ≡ U2 & K ⊢ T1 ➡ T2.
+lemma cpr_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K →
+ ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀U2. L ⊢ U1 ➡ U2 →
+ ∃∃T2. ⇧[d, e] T2 ≡ U2 & K ⊢ T1 ➡ T2.
#L #K #d #e #HLK #T1 #U1 #HTU1 #U2 * #U #HU1 #HU2
elim (tpr_inv_lift1 … HU1 … HTU1) -U1 #T #HTU #T1
elim (lt_or_ge (|L|) d) #HLd
(* Properties on inverse basic term relocation ******************************)
-lemma tpr_delift_conf: ∀U1,U2. U1 ➡ U2 → ∀L,T1,d,e. L ⊢ U1 ▼*[d, e] ≡ T1 →
- ∃∃T2. T1 ➡ T2 & L ⊢ U2 ▼*[d, e] ≡ T2.
+lemma tpr_delift_conf: ∀U1,U2. U1 ➡ U2 → ∀L,T1,d,e. L ⊢ ▼*[d, e] U1 ≡ T1 →
+ ∃∃T2. T1 ➡ T2 & L ⊢ ▼*[d, e] U2 ≡ T2.
#U1 #U2 #HU12 #L #T1 #d #e * #W1 #HUW1 #HTW1
elim (tpr_tpss_conf … HU12 … HUW1) -U1 #U1 #HWU1 #HU21
elim (tpr_inv_lift1 … HWU1 … HTW1) -W1 /3 width=5/
--- /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/static/ssta.ma".
+include "basic_2/reducibility/cpr.ma".
+
+(* EXTENDED PARALLEL REDUCTION ON TERMS *************************************)
+
+definition xpr: ∀h. sd h → lenv → relation term ≝
+ λh,g,L,T1,T2. L ⊢ T1 ➡ T2 ∨ ∃l. ⦃h, L⦄ ⊢ T1 •[g, l + 1] T2.
+
+interpretation
+ "extended parallel reduction (term)"
+ 'XPRed h g L T1 T2 = (xpr h g L T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma cpr_xpr: ∀h,g,L,T1,T2. L ⊢ T1 ➡ T2 → ⦃h, L⦄ ⊢ T1 ➸[g] T2.
+/2 width=1/ qed.
+
+lemma ssta_xpr: ∀h,g,L,T1,T2,l. ⦃h, L⦄ ⊢ T1 •[g, l + 1] T2 → ⦃h, L⦄ ⊢ T1 ➸[g] T2.
+/3 width=2/ qed.
+
+lemma xpr_refl: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ➸[g] T.
+/2 width=1/ 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/static/ssta_lift.ma".
+include "basic_2/reducibility/cpr_lift.ma".
+include "basic_2/reducibility/xpr.ma".
+
+(* EXTENDED PARALLEL REDUCTION ON TERMS *************************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma xpr_inv_abst1: ∀h,g,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛV1.T1 ➸[g] U2 →
+ ∃∃V2,T2. L ⊢ V1 ➡ V2 & ⦃h, L. ⓛV1⦄ ⊢ T1 ➸[g] T2 &
+ U2 = ⓛV2. T2.
+#h #g #L #V1 #T1 #U2 *
+[ #H elim (cpr_inv_abst1 … H Abst V1) /3 width=5/
+| * #l #H elim (ssta_inv_bind1 … H) /3 width=5/
+]
+qed-.
+
+(* Relocation properties ****************************************************)
+
+lemma xpr_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K →
+ ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 →
+ ∀h,g. ⦃h, K⦄ ⊢ T1 ➸[g] T2 → ⦃h, L⦄ ⊢ U1 ➸[g] U2.
+#L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #h #g * [2: * ]
+/3 width=9/ /3 width=10/
+qed.
+
+lemma xpr_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K →
+ ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀h,g,U2. ⦃h, L⦄ ⊢ U1 ➸[g] U2 →
+ ∃∃T2. ⇧[d, e] T2 ≡ U2 & ⦃h, K⦄ ⊢ T1 ➸[g] T2.
+#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #U2 * [ #HU12 | * #l #HU12 ]
+[ elim (cpr_inv_lift1 … HLK … HTU1 … HU12) -L -U1 /3 width=3/
+| elim (ssta_inv_lift1 … HU12 … HLK … HTU1) -L -U1 /3 width=4/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/static/ssta.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******)
+
+(* Note: may not be transitive *)
+inductive lsubss (h:sh) (g:sd h): relation lenv ≝
+| lsubss_atom: lsubss h g (⋆) (⋆)
+| lsubss_pair: ∀I,L1,L2,W. lsubss h g L1 L2 →
+ lsubss h g (L1. ⓑ{I} W) (L2. ⓑ{I} W)
+| lsubss_abbr: ∀L1,L2,V,W,l. ⦃h, L1⦄ ⊢ V •[g, l+1] W → ⦃h, L2⦄ ⊢ V •[g, l+1] W →
+ lsubss h g L1 L2 → lsubss h g (L1. ⓓV) (L2. ⓛW)
+.
+
+interpretation
+ "local environment refinement (stratified static type assigment)"
+ 'CrSubEqS h g L1 L2 = (lsubss h g L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubss_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 = ⋆ → L2 = ⋆.
+#h #g #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #V #W #l #_ #_ #_ #H destruct
+]
+qed.
+
+lemma lsubss_inv_atom1: ∀h,g,L2. h ⊢ ⋆ •⊑[g] L2 → L2 = ⋆.
+/2 width=5/ qed-.
+
+fact lsubss_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
+ ∀I,K1,V. L1 = K1. ⓑ{I} V →
+ (∃∃K2. h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓑ{I} V) ∨
+ ∃∃K2,W,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W &
+ h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓛW & I = Abbr.
+#h #g #L1 #L2 * -L1 -L2
+[ #I #K1 #V #H destruct
+| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3/
+| #L1 #L2 #V #W #l #H1VW #H2VW #HL12 #I #K1 #V1 #H destruct /3 width=7/
+]
+qed.
+
+lemma lsubss_inv_pair1: ∀h,g,I,K1,L2,V. h ⊢ K1. ⓑ{I} V •⊑[g] L2 →
+ (∃∃K2. h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓑ{I} V) ∨
+ ∃∃K2,W,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W &
+ h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓛW & I = Abbr.
+/2 width=3/ qed-.
+
+fact lsubss_inv_atom2_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L2 = ⋆ → L1 = ⋆.
+#h #g #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #V #W #l #_ #_ #_ #H destruct
+]
+qed.
+
+lemma lsubss_inv_atom2: ∀h,g,L1. h ⊢ L1 •⊑[g] ⋆ → L1 = ⋆.
+/2 width=5/ qed-.
+
+fact lsubss_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
+ ∀I,K2,W. L2 = K2. ⓑ{I} W →
+ (∃∃K1. h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓑ{I} W) ∨
+ ∃∃K1,V,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W &
+ h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓓV & I = Abst.
+#h #g #L1 #L2 * -L1 -L2
+[ #I #K2 #W #H destruct
+| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/
+| #L1 #L2 #V #W #l #H1VW #H2VW #HL12 #I #K2 #W2 #H destruct /3 width=7/
+]
+qed.
+
+lemma lsubss_inv_pair2: ∀h,g,I,L1,K2,W. h ⊢ L1 •⊑[g] K2. ⓑ{I} W →
+ (∃∃K1. h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓑ{I} W) ∨
+ ∃∃K1,V,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W &
+ h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓓV & I = Abst.
+/2 width=3/ qed-.
+
+(* Basic_forward lemmas *****************************************************)
+
+lemma lsubss_fwd_lsubs1: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ≼[0, |L1|] L2.
+#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+qed-.
+
+lemma lsubss_fwd_lsubs2: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ≼[0, |L2|] L2.
+#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lsubss_refl: ∀h,g,L. h ⊢ L •⊑[g] L.
+#h #g #L elim L -L // /2 width=1/
+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/static/lsubss.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******)
+
+(* Properties concerning basic local environment slicing ********************)
+
+(* Note: the constant 0 cannot be generalized *)
+lemma lsubss_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
+ ∀K1,e. ⇩[0, e] L1 ≡ K1 →
+ ∃∃K2. h ⊢ K1 •⊑[g] K2 & ⇩[0, e] L2 ≡ K2.
+#h #g #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3/
+| #I #L1 #L2 #V #_ #IHL12 #K1 #e #H
+ elim (ldrop_inv_O1 … H) -H * #He #HLK1
+ [ destruct
+ elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H
+ <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
+ | elim (IHL12 … HLK1) -L1 /3 width=3/
+ ]
+| #L1 #L2 #V #W #l #H1VW #H2VW #_ #IHL12 #K1 #e #H
+ elim (ldrop_inv_O1 … H) -H * #He #HLK1
+ [ destruct
+ elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H
+ <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
+ | elim (IHL12 … HLK1) -L1 /3 width=3/
+ ]
+]
+qed.
+
+(* Note: the constant 0 cannot be generalized *)
+lemma lsubss_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
+ ∀K2,e. ⇩[0, e] L2 ≡ K2 →
+ ∃∃K1. h ⊢ K1 •⊑[g] K2 & ⇩[0, e] L1 ≡ K1.
+#h #g #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3/
+| #I #L1 #L2 #V #_ #IHL12 #K2 #e #H
+ elim (ldrop_inv_O1 … H) -H * #He #HLK2
+ [ destruct
+ elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H
+ <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
+ | elim (IHL12 … HLK2) -L2 /3 width=3/
+ ]
+| #L1 #L2 #V #W #l #H1VW #H2VW #_ #IHL12 #K2 #e #H
+ elim (ldrop_inv_O1 … H) -H * #He #HLK2
+ [ destruct
+ elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H
+ <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
+ | elim (IHL12 … HLK2) -L2 /3 width=3/
+ ]
+]
+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/static/lsubss_ssta.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STATIC TYPE ASSIGNMENT ******************)
+
+(* Main properties **********************************************************)
+
+theorem lsubss_trans: ∀h,g,L1,L. h ⊢ L1 •⊑[g] L → ∀L2. h ⊢ L •⊑[g] L2 →
+ h ⊢ L1 •⊑[g] L2.
+#h #g #L1 #L #H elim H -L1 -L
+[ #X #H >(lsubss_inv_atom1 … H) -H //
+| #I #L1 #L #W #HL1 #IHL1 #X #H
+ elim (lsubss_inv_pair1 … H) -H * #L2
+ [ #HL2 #H destruct /3 width=1/
+ | #V #l #H1WV #H2WV #HL2 #H1 #H2 destruct /3 width=3/
+ ]
+| #L1 #L #V1 #W1 #l #H1VW1 #H2VW1 #HL1 #IHL1 #X #H
+ elim (lsubss_inv_pair1 … H) -H * #L2
+ [ #HL2 #H destruct /3 width=5/
+ | #V #l0 #_ #_ #_ #_ #H destruct
+ ]
+]
+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/static/ssta_lift.ma".
+include "basic_2/static/ssta_ssta.ma".
+include "basic_2/static/lsubss_ldrop.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******)
+
+(* Properties concerning stratified native type assignment ******************)
+
+lemma lsubss_ssta_trans: ∀h,g,L2,T,U,l. ⦃h, L2⦄ ⊢ T •[g,l] U →
+ ∀L1. h ⊢ L1 •⊑[g] L2 → ⦃h, L1⦄ ⊢ T •[g,l] U.
+#h #g #L2 #T #U #l #H elim H -L2 -T -U -l
+[ /2 width=1/
+| #L2 #K2 #V2 #W2 #U2 #i #l #HLK2 #_ #HWU2 #IHVW2 #L1 #HL12
+ elim (lsubss_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
+ elim (lsubss_inv_pair2 … H) -H * #K1 [ | -HWU2 -IHVW2 -HLK1 ]
+ [ #HK12 #H destruct /3 width=6/
+ | #V1 #l0 #_ #_ #_ #_ #H destruct
+ ]
+| #L2 #K2 #W2 #V2 #U2 #i #l #HLK2 #HWV2 #HWU2 #IHWV2 #L1 #HL12
+ elim (lsubss_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
+ elim (lsubss_inv_pair2 … H) -H * #K1 [ -HWV2 | -IHWV2 ]
+ [ #HK12 #H destruct /3 width=6/
+ | #V1 #l0 #H1 #H2 #_ #H #_ destruct
+ elim (ssta_fwd_correct … H2) -H2 #V #H
+ elim (ssta_mono … HWV2 … H) -HWV2 -H /2 width=6/
+ ]
+| /4 width=1/
+| /3 width=1/
+| /3 width=1/
+]
+qed.
+
+lemma lsubss_ssta_conf: ∀h,g,L1,T,U,l. ⦃h, L1⦄ ⊢ T •[g,l] U →
+ ∀L2. h ⊢ L1 •⊑[g] L2 → ⦃h, L2⦄ ⊢ T •[g,l] U.
+#h #g #L1 #T #U #l #H elim H -L1 -T -U -l
+[ /2 width=1/
+| #L1 #K1 #V1 #W1 #U1 #i #l #HLK1 #HVW1 #HWU1 #IHVW1 #L2 #HL12
+ elim (lsubss_ldrop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2
+ elim (lsubss_inv_pair1 … H) -H * #K2 [ -HVW1 | -IHVW1 ]
+ [ #HK12 #H destruct /3 width=6/
+ | #V2 #l0 #H1 #H2 #_ #H #_ destruct
+ elim (ssta_mono … HVW1 … H1) -HVW1 -H1 #H1 #H2 destruct
+ elim (ssta_fwd_correct … H2) -H2 /2 width=6/
+ ]
+| #L1 #K1 #W1 #V1 #U1 #i #l #HLK1 #_ #HWU1 #IHWV1 #L2 #HL12
+ elim (lsubss_ldrop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2
+ elim (lsubss_inv_pair1 … H) -H * #K2 [ | -HWU1 -IHWV1 -HLK2 ]
+ [ #HK12 #H destruct /3 width=6/
+ | #V2 #l0 #_ #_ #_ #_ #H destruct
+ ]
+| /4 width=1/
+| /3 width=1/
+| /3 width=1/
+]
+qed.
(* Basic properties *********************************************************)
lemma lift_delift: ∀T1,T2,d,e. ⇧[d, e] T1 ≡ T2 →
- ∀L. L ⊢ T2 ▼*[d, e] ≡ T1.
+ ∀L. L ⊢ ▼*[d, e] T2 ≡ T1.
/2 width=3/ qed.
-lemma delift_refl_O2: ∀L,T,d. L ⊢ T ▼*[d, 0] ≡ T.
+lemma delift_refl_O2: ∀L,T,d. L ⊢ ▼*[d, 0] T ≡ T.
/2 width=3/ qed.
-lemma delift_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▼*[d, e] ≡ T2 →
- ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ T1 ▼*[d, e] ≡ T2.
+lemma delift_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼*[d, e] T1 ≡ T2 →
+ ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ ▼*[d, e] T1 ≡ T2.
#L1 #T1 #T2 #d #e * /3 width=3/
qed.
-lemma delift_sort: â\88\80L,d,e,k. L â\8a¢ â\8b\86k â\96¼*[d, e] ≡ ⋆k.
+lemma delift_sort: â\88\80L,d,e,k. L â\8a¢ â\96¼*[d, e] â\8b\86k ≡ ⋆k.
/2 width=3/ qed.
-lemma delift_lref_lt: ∀L,d,e,i. i < d → L ⊢ #i ▼*[d, e] ≡ #i.
+lemma delift_lref_lt: ∀L,d,e,i. i < d → L ⊢ ▼*[d, e] #i ≡ #i.
/3 width=3/ qed.
-lemma delift_lref_ge: ∀L,d,e,i. d + e ≤ i → L ⊢ #i ▼*[d, e] ≡ #(i - e).
+lemma delift_lref_ge: ∀L,d,e,i. d + e ≤ i → L ⊢ ▼*[d, e] #i ≡ #(i - e).
/3 width=3/ qed.
-lemma delift_gref: ∀L,d,e,p. L ⊢ §p ▼*[d, e] ≡ §p.
+lemma delift_gref: ∀L,d,e,p. L ⊢ ▼*[d, e] §p ≡ §p.
/2 width=3/ qed.
lemma delift_bind: ∀I,L,V1,V2,T1,T2,d,e.
- L ⊢ V1 ▼*[d, e] ≡ V2 → L. ⓑ{I} V2 ⊢ T1 ▼*[d+1, e] ≡ T2 →
- L â\8a¢ â\93\91{I} V1. T1 â\96¼*[d, e] ≡ ⓑ{I} V2. T2.
+ L ⊢ ▼*[d, e] V1 ≡ V2 → L. ⓑ{I} V2 ⊢ ▼*[d+1, e] T1 ≡ T2 →
+ L â\8a¢ â\96¼*[d, e] â\93\91{I} V1. T1 ≡ ⓑ{I} V2. T2.
#I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * #T #HT1 #HT2
lapply (tpss_lsubs_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/ /3 width=5/
qed.
lemma delift_flat: ∀I,L,V1,V2,T1,T2,d,e.
- L ⊢ V1 ▼*[d, e] ≡ V2 → L ⊢ T1 ▼*[d, e] ≡ T2 →
- L â\8a¢ â\93\95{I} V1. T1 â\96¼*[d, e] ≡ ⓕ{I} V2. T2.
+ L ⊢ ▼*[d, e] V1 ≡ V2 → L ⊢ ▼*[d, e] T1 ≡ T2 →
+ L â\8a¢ â\96¼*[d, e] â\93\95{I} V1. T1 ≡ ⓕ{I} V2. T2.
#I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * /3 width=5/
qed.
(* Basic inversion lemmas ***************************************************)
-lemma delift_inv_sort1: â\88\80L,U2,d,e,k. L â\8a¢ â\8b\86k â\96¼*[d, e] ≡ U2 → U2 = ⋆k.
+lemma delift_inv_sort1: â\88\80L,U2,d,e,k. L â\8a¢ â\96¼*[d, e] â\8b\86k ≡ U2 → U2 = ⋆k.
#L #U2 #d #e #k * #U #HU
>(tpss_inv_sort1 … HU) -HU #HU2
>(lift_inv_sort2 … HU2) -HU2 //
qed-.
-lemma delift_inv_gref1: ∀L,U2,d,e,p. L ⊢ §p ▼*[d, e] ≡ U2 → U2 = §p.
+lemma delift_inv_gref1: ∀L,U2,d,e,p. L ⊢ ▼*[d, e] §p ≡ U2 → U2 = §p.
#L #U #d #e #p * #U #HU
>(tpss_inv_gref1 … HU) -HU #HU2
>(lift_inv_gref2 … HU2) -HU2 //
qed-.
-lemma delift_inv_bind1: â\88\80I,L,V1,T1,U2,d,e. L â\8a¢ â\93\91{I} V1. T1 â\96¼*[d, e] ≡ U2 →
- ∃∃V2,T2. L ⊢ V1 ▼*[d, e] ≡ V2 &
- L. ⓑ{I} V2 ⊢ T1 ▼*[d+1, e] ≡ T2 &
+lemma delift_inv_bind1: â\88\80I,L,V1,T1,U2,d,e. L â\8a¢ â\96¼*[d, e] â\93\91{I} V1. T1 ≡ U2 →
+ ∃∃V2,T2. L ⊢ ▼*[d, e] V1 ≡ V2 &
+ L. ⓑ{I} V2 ⊢ ▼*[d+1, e] T1 ≡ T2 &
U2 = ⓑ{I} V2. T2.
#I #L #V1 #T1 #U2 #d #e * #U #HU #HU2
elim (tpss_inv_bind1 … HU) -HU #V #T #HV1 #HT1 #X destruct
lapply (tpss_lsubs_trans … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
qed-.
-lemma delift_inv_flat1: â\88\80I,L,V1,T1,U2,d,e. L â\8a¢ â\93\95{I} V1. T1 â\96¼*[d, e] ≡ U2 →
- ∃∃V2,T2. L ⊢ V1 ▼*[d, e] ≡ V2 &
- L ⊢ T1 ▼*[d, e] ≡ T2 &
+lemma delift_inv_flat1: â\88\80I,L,V1,T1,U2,d,e. L â\8a¢ â\96¼*[d, e] â\93\95{I} V1. T1 ≡ U2 →
+ ∃∃V2,T2. L ⊢ ▼*[d, e] V1 ≡ V2 &
+ L ⊢ ▼*[d, e] T1 ≡ T2 &
U2 = ⓕ{I} V2. T2.
#I #L #V1 #T1 #U2 #d #e * #U #HU #HU2
elim (tpss_inv_flat1 … HU) -HU #V #T #HV1 #HT1 #X destruct
elim (lift_inv_flat2 … HU2) -HU2 /3 width=5/
qed-.
-lemma delift_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 ▼*[d, 0] ≡ T2 → T1 = T2.
+lemma delift_inv_refl_O2: ∀L,T1,T2,d. L ⊢ ▼*[d, 0] T1 ≡ T2 → T1 = T2.
#L #T1 #T2 #d * #T #HT1
>(tpss_inv_refl_O2 … HT1) -HT1 #HT2
>(lift_inv_refl_O2 … HT2) -HT2 //
(* Basic forward lemmas *****************************************************)
-lemma delift_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▼*[d, e] ≡ T2 → #[T1] ≤ #[T2].
+lemma delift_fwd_tw: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → #[T1] ≤ #[T2].
#L #T1 #T2 #d #e * #T #HT1 #HT2
>(tw_lift … HT2) -T2 /2 width=4 by tpss_fwd_tw /
qed-.
(* Basic properties *********************************************************)
-lemma delifta_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▼▼*[d, e] ≡ T2 →
- ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ T1 ▼▼*[d, e] ≡ T2.
+lemma delifta_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼▼*[d, e] T1 ≡ T2 →
+ ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ ▼▼*[d, e] T1 ≡ 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_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
]
qed.
-lemma delift_delifta: ∀L,T1,T2,d,e. L ⊢ T1 ▼*[d, e] ≡ T2 → L ⊢ T1 ▼▼*[d, e] ≡ T2.
+lemma delift_delifta: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → L ⊢ ▼▼*[d, e] T1 ≡ T2.
#L #T1 @(cw_wf_ind … L T1) -L -T1 #L #T1 elim T1 -T1
[ * #i #IH #T2 #d #e #H
[ >(delift_inv_sort1 … H) -H //
(* Basic inversion lemmas ***************************************************)
-lemma delifta_delift: ∀L,T1,T2,d,e. L ⊢ T1 ▼▼*[d, e] ≡ T2 → L ⊢ T1 ▼*[d, e] ≡ T2.
+lemma delifta_delift: ∀L,T1,T2,d,e. L ⊢ ▼▼*[d, e] T1 ≡ T2 → L ⊢ ▼*[d, e] T1 ≡ T2.
#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e // /2 width=1/ /2 width=6/
qed-.
(∀L,d,e,k. R d e L (⋆k) (⋆k)) →
(∀L,d,e,i. i < d → 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 ⊢ ▼*[O, d + e - i - 1] V1 ≡ V2 →
⇧[O, d] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L #i W2
) →
(∀L,d,e,i. d + e ≤ i → R d e L (#i) (#(i - e))) →
(∀L,d,e,p. R d e L (§p) (§p)) →
- (∀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 ⊢ ▼*[d, e] V1 ≡ V2 →
+ L.ⓑ{I}V2 ⊢ ▼*[d + 1, e] T1 ≡ 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 ⊢ ▼*[d, e] V1 ≡ V2 →
+ L⊢ ▼*[d, e] T1 ≡ 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 ⊢ ▼*[d, e] T1 ≡ T2 → R d e L T1 T2.
#R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #d #e #L #T1 #T2 #H elim (delift_delifta … H) -L -T1 -T2 -d -e
// /2 width=1 by delifta_delift/ /3 width=1 by delifta_delift/ /3 width=7 by delifta_delift/
qed-.
(* Main properties **********************************************************)
theorem delift_mono: ∀L,T,T1,T2,d,e.
- L ⊢ T ▼*[d, e] ≡ T1 → L ⊢ T ▼*[d, e] ≡ T2 → T1 = T2.
+ L ⊢ ▼*[d, e] T ≡ T1 → L ⊢ ▼*[d, e] T ≡ T2 → T1 = T2.
#L #T #T1 #T2 #d #e * #U1 #H1TU1 #H2TU1 * #U2 #H1TU2 #H2TU2
elim (tpss_conf_eq … H1TU1 … H1TU2) -T #U #HU1 #HU2
lapply (tpss_inv_lift1_eq … HU1 … H2TU1) -HU1 #H destruct
(* Advanced properties ******************************************************)
lemma delift_lref_be: ∀L,K,V1,V2,U2,i,d,e. d ≤ i → i < d + e →
- ⇩[0, i] L ≡ K. ⓓV1 → K ⊢ V1 ▼*[0, d + e - i - 1] ≡ V2 →
- ⇧[0, d] V2 ≡ U2 → L ⊢ #i ▼*[d, e] ≡ U2.
+ ⇩[0, i] L ≡ K. ⓓV1 → K ⊢ ▼*[0, d + e - i - 1] V1 ≡ V2 →
+ ⇧[0, d] V2 ≡ U2 → L ⊢ ▼*[d, e] #i ≡ U2.
#L #K #V1 #V2 #U2 #i #d #e #Hdi #Hide #HLK * #V #HV1 #HV2 #HVU2
elim (lift_total V 0 (i+1)) #U #HVU
lapply (lift_trans_be … HV2 … HVU ? ?) -HV2 // >minus_plus <plus_minus_m_m /2 width=1/ #HV2U
qed.
fact sfr_delift_aux: ∀L,T,T1,d,e. d + e ≤ |L| → ≽ [d, e] L → T = T1 →
- ∃T2. L ⊢ T1 ▼*[d, e] ≡ T2.
+ ∃T2. L ⊢ ▼*[d, e] T1 ≡ T2.
#L #T @(cw_wf_ind … L T) -L -T #L #T #IH * * /2 width=2/
[ #i #d #e #Hde #HL #H destruct
elim (lt_or_ge i d) #Hdi [ /3 width=2/ ]
qed.
lemma sfr_delift: ∀L,T1,d,e. d + e ≤ |L| → ≽ [d, e] L →
- ∃T2. L ⊢ T1 ▼*[d, e] ≡ T2.
+ ∃T2. L ⊢ ▼*[d, e] T1 ≡ T2.
/2 width=2/ qed-.
(* Advanced inversion lemmas ************************************************)
-lemma delift_inv_lref1_lt: ∀L,U2,i,d,e. L ⊢ #i ▼*[d, e] ≡ U2 → i < d → U2 = #i.
+lemma delift_inv_lref1_lt: ∀L,U2,i,d,e. L ⊢ ▼*[d, e] #i ≡ U2 → i < d → U2 = #i.
#L #U2 #i #d #e * #U #HU #HU2 #Hid
elim (tpss_inv_lref1 … HU) -HU
[ #H destruct >(lift_inv_lref2_lt … HU2) //
]
qed-.
-lemma delift_inv_lref1_be: ∀L,U2,d,e,i. L ⊢ #i ▼*[d, e] ≡ U2 →
+lemma delift_inv_lref1_be: ∀L,U2,d,e,i. L ⊢ ▼*[d, e] #i ≡ U2 →
d ≤ i → i < d + e →
∃∃K,V1,V2. ⇩[0, i] L ≡ K. ⓓV1 &
- K ⊢ V1 ▼*[0, d + e - i - 1] ≡ V2 &
+ K ⊢ ▼*[0, d + e - i - 1] V1 ≡ V2 &
⇧[0, d] V2 ≡ U2.
#L #U2 #d #e #i * #U #HU #HU2 #Hdi #Hide
elim (tpss_inv_lref1 … HU) -HU
]
qed-.
-lemma delift_inv_lref1_ge: ∀L,U2,i,d,e. L ⊢ #i ▼*[d, e] ≡ U2 →
+lemma delift_inv_lref1_ge: ∀L,U2,i,d,e. L ⊢ ▼*[d, e] #i ≡ U2 →
d + e ≤ i → U2 = #(i - e).
#L #U2 #i #d #e * #U #HU #HU2 #Hdei
elim (tpss_inv_lref1 … HU) -HU
]
qed-.
-lemma delift_inv_lref1: ∀L,U2,i,d,e. L ⊢ #i ▼*[d, e] ≡ U2 →
+lemma delift_inv_lref1: ∀L,U2,i,d,e. L ⊢ ▼*[d, e] #i ≡ U2 →
∨∨ (i < d ∧ U2 = #i)
| (∃∃K,V1,V2. d ≤ i & i < d + e &
⇩[0, i] L ≡ K. ⓓV1 &
- K ⊢ V1 ▼*[0, d + e - i - 1] ≡ V2 &
+ K ⊢ ▼*[0, d + e - i - 1] V1 ≡ V2 &
⇧[0, d] V2 ≡ U2
)
| (d + e ≤ i ∧ U2 = #(i - e)).
(* Properties on basic term relocation **************************************)
-lemma delift_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 ▼*[dt, et] ≡ T2 →
+lemma delift_lift_le: ∀K,T1,T2,dt,et. K ⊢ ▼*[dt, et] T1 ≡ T2 →
∀L,U1,d,e. dt + et ≤ d → ⇩[d, e] L ≡ K →
⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d - et, e] T2 ≡ U2 →
- L ⊢ U1 ▼*[dt, et] ≡ U2.
+ L ⊢ ▼*[dt, et] U1 ≡ U2.
#K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hdetd #HLK #HTU1 #U2 #HTU2
elim (lift_total T d e) #U #HTU
lapply (tpss_lift_le … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1
>(lift_mono … HTU2 … HT2) -T2 /2 width=3/
qed.
-lemma delift_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 ▼*[dt, et] ≡ T2 →
+lemma delift_lift_be: ∀K,T1,T2,dt,et. K ⊢ ▼*[dt, et] T1 ≡ T2 →
∀L,U1,d,e. dt ≤ d → d ≤ dt + et →
⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 →
- L ⊢ U1 ▼*[dt, et + e] ≡ T2.
+ L ⊢ ▼*[dt, et + e] U1 ≡ T2.
#K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1
elim (lift_total T d e) #U #HTU
lapply (tpss_lift_be … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1
lapply (lift_trans_be … HT2 … HTU ? ?) -T // -Hdtd -Hddet /2 width=3/
qed.
-lemma delift_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 ▼*[dt, et] ≡ T2 →
+lemma delift_lift_ge: ∀K,T1,T2,dt,et. K ⊢ ▼*[dt, et] T1 ≡ 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 ⊢ ▼*[dt + e, et] U1 ≡ U2.
#K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hddt #HLK #HTU1 #U2 #HTU2
elim (lift_total T d e) #U #HTU
lapply (tpss_lift_ge … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1
>(lift_mono … HTU2 … HT2) -T2 /2 width=3/
qed.
-lemma delift_inv_lift1_eq: ∀L,U1,T2,d,e. L ⊢ U1 ▼*[d, e] ≡ T2 →
+lemma delift_inv_lift1_eq: ∀L,U1,T2,d,e. L ⊢ ▼*[d, e] U1 ≡ T2 →
∀K. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → T1 = T2.
#L #U1 #T2 #d #e * #U2 #HU12 #HTU2 #K #HLK #T1 #HTU1
lapply (tpss_inv_lift1_eq … HU12 … HTU1) -L -K #H destruct
lapply (lift_inj … HTU1 … HTU2) -U2 //
qed-.
-lemma delift_lift_div_be: ∀L,T1,T,d,e,i. L ⊢ T1 ▼*[i, d + e - i] ≡ T →
+lemma delift_lift_div_be: ∀L,T1,T,d,e,i. L ⊢ ▼*[i, d + e - i] T1 ≡ T →
∀T2. ⇧[d, i - d] T2 ≡ T → d ≤ i → i ≤ d + e →
- L ⊢ T1 ▼*[d, e] ≡ T2.
+ L ⊢ ▼*[d, e] T1 ≡ T2.
#L #T1 #T #d #e #i * #T0 #HT10 #HT0 #T2 #HT2 #Hdi #Hide
lapply (tpss_weak … HT10 d e ? ?) -HT10 // [ >commutative_plus /2 width=1/ ] #HT10
lapply (lift_trans_be … HT2 … HT0 ? ?) -T //
(* 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.
+lemma delift_ltpss_conf_eq: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 →
+ ∀K. L ▶* [d, e] K → K ⊢ ▼*[d, e] T1 ≡ 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 →
- ∀T1,T2. K ⊢ T1 ▼*[d, e] ≡ T2 → L ⊢ T1 ▼*[d, e] ≡ T2.
+ ∀T1,T2. K ⊢ ▼*[d, e] T1 ≡ T2 → L ⊢ ▼*[d, e] T1 ≡ T2.
#L #K #d #e #HLK #T1 #T2 * #T #HT1 #HT2
lapply (ltpss_tpss_trans_eq … HT1 … HLK) -K /2 width=3/
qed.
(* Properties on partial unfold on terms ************************************)
lemma delift_tpss_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
- ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 →
+ ∀T1,dd,ee. L ⊢ ▼*[dd, ee] U1 ≡ 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 ⊢ ▼*[dd, ee] U2 ≡ 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 →
- ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 →
+ ∀T1,dd,ee. L ⊢ ▼*[dd, ee] U1 ≡ 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 ⊢ ▼*[dd, ee] U2 ≡ T2.
/3 width=3/ qed.
lemma delift_tpss_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
- ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 →
+ ∀T1,dd,ee. L ⊢ ▼*[dd, ee] U1 ≡ T1 →
∀K. ⇩[dd, ee] L ≡ K →
d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 &
- L ⊢ U2 ▼*[dd, ee] ≡ T2.
+ L ⊢ ▼*[dd, ee] U2 ≡ 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 →
- ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 →
+ ∀T1,dd,ee. L ⊢ ▼*[dd, ee] U1 ≡ T1 →
∀K. ⇩[dd, ee] L ≡ K →
d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 &
- L ⊢ U2 ▼*[dd, ee] ≡ T2.
+ L ⊢ ▼*[dd, ee] U2 ≡ T2.
/3 width=6/ qed.
lemma delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
- ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 →
+ ∀T1,dd,ee. L ⊢ ▼*[dd, ee] U1 ≡ T1 →
∀K. ⇩[dd, ee] L ≡ K → d ≤ dd → dd + ee ≤ d + e →
∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 &
- L ⊢ U2 ▼*[dd, ee] ≡ T2.
+ L ⊢ ▼*[dd, ee] U2 ≡ 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 →
- ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 →
+ ∀T1,dd,ee. L ⊢ ▼*[dd, ee] U1 ≡ T1 →
∀K. ⇩[dd, ee] L ≡ K → d ≤ dd → dd + ee ≤ d + e →
∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 &
- L ⊢ U2 ▼*[dd, ee] ≡ T2.
+ L ⊢ ▼*[dd, ee] U2 ≡ T2.
/3 width=3/ qed.
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.
+ ∀T. L ⊢ ▼*[d, e] U1 ≡ T → L ⊢ ▼*[d, e] U2 ≡ 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 →
- ∀T. L ⊢ U1 ▼*[d, e] ≡ T → L ⊢ U2 ▼*[d, e] ≡ T.
+ ∀T. L ⊢ ▼*[d, e] U1 ≡ T → L ⊢ ▼*[d, e] U2 ≡ T.
/3 width=3/ qed.
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.
+ ∀T. L ⊢ ▼*[d, e] U2 ≡ T → L ⊢ ▼*[d, e] U1 ≡ 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 →
- ∀T. L ⊢ U2 ▼*[d, e] ≡ T → L ⊢ U1 ▼*[d, e] ≡ T.
+ ∀T. L ⊢ ▼*[d, e] U2 ≡ T → L ⊢ ▼*[d, e] U1 ≡ T.
/3 width=3/ qed.
(* Basic properties *********************************************************)
-lemma ldrop_thin: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → L1 ▼*[d, e] ≡ L2.
+lemma ldrop_thin: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ▼*[d, e] L1 ≡ L2.
/2 width=3/ qed.
(* Basic inversion lemmas ***************************************************)
-lemma thin_inv_thin1: ∀I,K1,V1,L2,e. K1. ⓑ{I} V1 ▼*[0, e] ≡ L2 → 0 < e →
- K1 ▼*[0, e - 1] ≡ L2.
+lemma thin_inv_thin1: ∀I,K1,V1,L2,e. ▼*[0, e] K1.ⓑ{I} V1 ≡ L2 → 0 < e →
+ ▼*[0, e - 1] K1 ≡ L2.
#I #K1 #V1 #L2 #e * #X #HK1 #HL2 #e
elim (ltpss_inv_tpss21 … HK1 ?) -HK1 // #K #V #HK1 #_ #H destruct
lapply (ldrop_inv_ldrop1 … HL2 ?) -HL2 // /2 width=3/
(* Inversion lemmas on inverse basic term relocation ************************)
-lemma thin_inv_delift1: ∀I,K1,V1,L2,d,e. K1. ⓑ{I} V1 ▼*[d, e] ≡ L2 → 0 < d →
- ∃∃K2,V2. K1 ▼*[d - 1, e] ≡ K2 &
- K1 ⊢ V1 ▼*[d - 1, e] ≡ V2 &
+lemma thin_inv_delift1: ∀I,K1,V1,L2,d,e. ▼*[d, e] K1. ⓑ{I} V1 ≡ L2 → 0 < d →
+ ∃∃K2,V2. ▼*[d - 1, e] K1 ≡ K2 &
+ K1 ⊢ ▼*[d - 1, e] V1 ≡ V2 &
L2 = K2. ⓑ{I} V2.
#I #K1 #V1 #L2 #d #e * #X #HK1 #HL2 #e
elim (ltpss_inv_tpss11 … HK1 ?) -HK1 // #K #V #HK1 #HV1 #H destruct
(* Properties on inverse basic term relocation ******************************)
-lemma thin_delift1: ∀L1,L2,d,e. L1 ▼*[d, e] ≡ L2 → ∀V1,V2. L1 ⊢ V1 ▼*[d, e] ≡ V2 →
- ∀I. L1.ⓑ{I}V1 ▼*[d + 1, e] ≡ L2.ⓑ{I}V2.
+lemma thin_delift1: ∀L1,L2,d,e. ▼*[d, e] L1 ≡ L2 → ∀V1,V2. L1 ⊢ ▼*[d, e] V1 ≡ V2 →
+ ∀I. ▼*[d + 1, e] L1.ⓑ{I}V1 ≡ L2.ⓑ{I}V2.
#L1 #L2 #d #e * #L #HL1 #HL2 #V1 #V2 * #V #HV1 #HV2 #I
elim (ltpss_tpss_conf … HV1 … HL1) -HV1 #V0 #HV10 #HV0
elim (tpss_inv_lift1_be … HV0 … HL2 … HV2 ? ?) -HV0 // <minus_n_n #X #H1 #H2
qed.
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 →
+ ∀T1,dd,ee. L ⊢ ▼*[dd, ee] U1 ≡ T1 →
+ ∀K. ▼*[dd, ee] L ≡ K → d + e ≤ dd →
∃∃T2. K ⊢ T1 ▶* [d, e] T2 &
- L ⊢ U2 ▼*[dd, ee] ≡ T2.
+ L ⊢ ▼*[dd, ee] U2 ≡ 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
elim (ltpss_tpss_conf … HU12 … HLY) -HU12 #U #HU1 #HU2
qed.
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 →
+ ∀T1,dd,ee. L ⊢ ▼*[dd, ee] U1 ≡ T1 →
+ ∀K. ▼*[dd, ee] L ≡ K → d + e ≤ dd →
∃∃T2. K ⊢ T1 ▶* [d, e] T2 &
- L ⊢ U2 ▼*[dd, ee] ≡ T2.
+ L ⊢ ▼*[dd, ee] U2 ≡ T2.
/3 width=3/ qed.
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 →
+ ∀T1,dd,ee. L ⊢ ▼*[dd, ee] U1 ≡ T1 →
+ ∀K. ▼*[dd, ee] L ≡ K →
d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 &
- L ⊢ U2 ▼*[dd, ee] ≡ T2.
+ L ⊢ ▼*[dd, ee] U2 ≡ 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
elim (ltpss_tpss_conf … HU12 … HLY) -HU12 #U #HU1 #HU2
qed.
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 →
+ ∀T1,dd,ee. L ⊢ ▼*[dd, ee] U1 ≡ T1 →
+ ∀K. ▼*[dd, ee] L ≡ K →
d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 &
- L ⊢ U2 ▼*[dd, ee] ≡ T2.
+ L ⊢ ▼*[dd, ee] U2 ≡ T2.
/3 width=6 by thin_delift_tpss_conf_le_up, tpss_strap2/ qed. (**) (* too slow without trace *)
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 →
+ ∀T1,dd,ee. L ⊢ ▼*[dd, ee] U1 ≡ T1 →
+ ∀K. ▼*[dd, ee] L ≡ K → d ≤ dd → dd + ee ≤ d + e →
∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 &
- L ⊢ U2 ▼*[dd, ee] ≡ T2.
+ L ⊢ ▼*[dd, ee] U2 ≡ 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
elim (ltpss_tpss_conf … HU12 … HLY) -HU12 #U #HU1 #HU2
qed.
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 →
+ ∀T1,dd,ee. L ⊢ ▼*[dd, ee] U1 ≡ T1 →
+ ∀K. ▼*[dd, ee] L ≡ K → d ≤ dd → dd + ee ≤ d + e →
∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 &
- L ⊢ U2 ▼*[dd, ee] ≡ T2.
+ L ⊢ ▼*[dd, ee] U2 ≡ T2.
/3 width=3/ qed.
(* Properties on local environment slicing **********************************)
-lemma thin_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 ▼*[d1, e1] ≡ L1 →
+lemma thin_ldrop_conf_ge: ∀L0,L1,d1,e1. ▼*[d1, e1] L0 ≡ L1 →
∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
d1 + e1 ≤ e2 → ⇩[0, e2 - e1] L1 ≡ L2.
#L0 #L1 #d1 #e1 * /3 width=8 by ltpss_ldrop_conf_ge, ldrop_conf_ge/
qed.
-lemma thin_ldrop_conf_be: ∀L0,L1,d1,e1. L0 ▼*[d1, e1] ≡ L1 →
+lemma thin_ldrop_conf_be: ∀L0,L1,d1,e1. ▼*[d1, e1] L0 ≡ L1 →
∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
- ∃∃L. L2 ▼*[0, d1 + e1 - e2] ≡ L & ⇩[0, d1] L1 ≡ L.
+ ∃∃L. ▼*[0, d1 + e1 - e2] L2 ≡ L & ⇩[0, d1] L1 ≡ L.
#L0 #L1 #d1 #e1 * #L #HL0 #HL1 #L2 #e2 #HL02 #Hd1e2 #He2de1
elim (ltpss_ldrop_conf_be … HL0 … HL02 ? ?) -L0 // #L0 #HL20 #HL0
elim (ldrop_conf_be … HL1 … HL0 ? ?) -L // -Hd1e2 -He2de1 /3 width=3/
qed.
-lemma thin_ldrop_conf_le: ∀L0,L1,d1,e1. L0 ▼*[d1, e1] ≡ L1 →
+lemma thin_ldrop_conf_le: ∀L0,L1,d1,e1. ▼*[d1, e1] L0 ≡ L1 →
∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
- ∃∃L. L2 ▼*[d1 - e2, e1] ≡ L & ⇩[0, e2] L1 ≡ L.
+ ∃∃L. ▼*[d1 - e2, e1] L2 ≡ L & ⇩[0, e2] L1 ≡ L.
#L0 #L1 #d1 #e1 * #L #HL0 #HL1 #L2 #e2 #HL02 #He2d1
elim (ltpss_ldrop_conf_le … HL0 … HL02 ?) -L0 // #L0 #HL20 #HL0
elim (ldrop_conf_le … HL1 … HL0 ?) -L // -He2d1 /3 width=3/
qed.
-lemma thin_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 ▼*[d1, e1] ≡ L0 →
+lemma thin_ldrop_trans_ge: ∀L1,L0,d1,e1. ▼*[d1, e1] L1 ≡ L0 →
∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
d1 ≤ e2 → ⇩[0, e1 + e2] L1 ≡ L2.
#L1 #L0 #d1 #e1 * #L #HL1 #HL0 #L2 #e2 #HL02 #Hd1e2
lapply (ltpss_ldrop_trans_ge … HL1 … HL2 ?) -L // /2 width=1/
qed.
-lemma thin_ldrop_trans_le: ∀L1,L0,d1,e1. L1 ▼*[d1, e1] ≡ L0 →
+lemma thin_ldrop_trans_le: ∀L1,L0,d1,e1. ▼*[d1, e1] L1 ≡ L0 →
∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
- ∃∃L. L ▼*[d1 - e2, e1] ≡ L2 & ⇩[0, e2] L1 ≡ L.
+ ∃∃L. ▼*[d1 - e2, e1] L ≡ L2 & ⇩[0, e2] L1 ≡ L.
#L1 #L0 #d1 #e1 * #L #HL1 #HL0 #L2 #e2 #HL02 #He2d1
elim (ldrop_trans_le … HL0 … HL02 He2d1) -L0 #L0 #HL0 #HL02
elim (ltpss_ldrop_trans_le … HL1 … HL0 He2d1) -L -He2d1 /3 width=3/
fact sstas_inv_lref1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → ∀j. T = #j →
∃∃I,K,V,W. ⇩[0, j] L ≡ K. ⓑ{I}V & ⦃h, K⦄ ⊢ V •*[g] W &
- L ⊢ U ▼*[0, j + 1] ≡ W.
+ L ⊢ ▼*[0, j + 1] U ≡ W.
#h #g #L #T #U #H @(sstas_ind_alt … H) -T
[ #T #HUT #j #H destruct
elim (ssta_inv_lref1 … HUT) -HUT * #K #V #W [2: #l] #HLK #HVW #HVT
projects / helm.git / commitdiff