csubt/csuba csubt_csuba
csubt/fwd csubt_gen_abbr
csubt/fwd csubt_gen_abst
-csubt/pc3 csubt_pr2
-csubt/pc3 csubt_pc3
csubv/clear csubv_clear_conf
csubv/clear csubv_clear_conf_void
/2 width=3/ qed.
(* 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.
+lemma cprs_lsubs_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 →
+ ∀L2. L2 ≼ [0, |L1|] L1 → L2 ⊢ T1 ➡* T2.
/3 width=3/
qed.
lemma cprs_abst: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀V,T1,T2.
L.ⓛV ⊢ T1 ➡* T2 → L ⊢ ⓛV1. T1 ➡* ⓛV2. T2.
#L #V1 #V2 #HV12 #V #T1 #T2 #HT12 @(cprs_ind … HV12) -V2
-[ lapply (cprs_lsubs_conf … HT12 (L.ⓛV1) ?) -HT12 /2 width=2/
+[ lapply (cprs_lsubs_trans … HT12 (L.ⓛV1) ?) -HT12 /2 width=2/
| #V0 #V2 #_ #HV02 #IHV01
@(cprs_trans … IHV01) -V1 /2 width=2/
]
h ⊢ K1 :⊑ K2 & L1 = K1. ⓓV & I = Abst.
/2 width=3/ qed-.
+(* Basic_forward lemmas *****************************************************)
+
+lemma lsubn_fwd_lsubs1: ∀h,L1,L2. h ⊢ L1 :⊑ L2 → L1 ≼[0, |L1|] L2.
+#h #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+qed-.
+
+lemma lsubn_fwd_lsubs2: ∀h,L1,L2. h ⊢ L1 :⊑ L2 → L1 ≼[0, |L2|] L2.
+#h #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+qed-.
+
(* Basic properties *********************************************************)
(* Basic_1: was: csubt_refl *)
--- /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/equivalence/cpcs_cpcs.ma".
+include "basic_2/dynamic/lsubn.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE TYPE ASSIGNMENT ******************)
+
+(* Properties on context-sensitive parallel equivalence for terms ***********)
+
+(* Basic_1: was: csubt_pr2 *)
+lemma cpr_lsubn_trans: ∀h,L1,L2. h ⊢ L1 :⊑ L2 →
+ ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡ T2.
+/3 width=4 by lsubn_fwd_lsubs2, cpr_lsubs_trans/ qed.
+
+lemma cprs_lsubn_trans: ∀h,L1,L2. h ⊢ L1 :⊑ L2 →
+ ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
+/3 width=4 by lsubn_fwd_lsubs2, cprs_lsubs_trans/ qed.
+
+(* Basic_1: was: csubt_pc3 *)
+lemma cpcs_lsubn_trans: ∀h,L1,L2. h ⊢ L1 :⊑ L2 →
+ ∀T1,T2. L2 ⊢ T1 ⬌* T2 → L1 ⊢ T1 ⬌* T2.
+/3 width=4 by lsubn_fwd_lsubs2, cpcs_lsubs_trans/ qed.
include "basic_2/dynamic/nta_nta.ma".
include "basic_2/dynamic/lsubn_ldrop.ma".
+include "basic_2/dynamic/lsubn_cpcs.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE TYPE ASSIGNMENT ******************)
(* Note: the corresponding confluence property does not hold *)
(* Basic_1: was: csubt_ty3 *)
-axiom lsubn_nta_trans: ∀h,L2,T,U. ⦃h, L2⦄ ⊢ T : U → ∀L1. h ⊢ L1 :⊑ L2 →
+lemma lsubn_nta_trans: ∀h,L2,T,U. ⦃h, L2⦄ ⊢ T : U → ∀L1. h ⊢ L1 :⊑ L2 →
⦃h, L1⦄ ⊢ T : U.
-(*
#h #L2 #T #U #H elim H -L2 -T -U
[ //
| #L2 #K2 #V2 #W2 #U2 #i #HLK2 #_ #WU2 #IHVW2 #L1 #HL12
| /3 width=1/
| /3 width=2/
| /3 width=1/
+| /4 width=6/
]
qed.
-*)
(* Note: this is known as the substitution lemma *)
(* Basic_1: was only: ty3_gen_cabbr *)
lemma nta_thin_conf: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 →
- â\88\80L2,d,e. â\89¼ [d, e] L1 → L1 ▼*[d, e] ≡ L2 →
+ â\88\80L2,d,e. â\89½ [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 elim H -L1 -T1 -U1
| #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL1 #HL12
elim (IHVW1 … HL1 HL12) -IHVW1 #V2 #W2 #HVW2 #HV12 #_
elim (IHTU1 (L2.ⓑ{I}V2) (d+1) e ? ?) -IHTU1 /2 width=1/ -HL1 -HL12 #T2 #U2 #HTU2 #HT12 #HU12
- lapply (delift_lsubs_conf … HT12 (L1.ⓑ{I}V2) ?) -HT12 /2 width=1/
- lapply (delift_lsubs_conf … HU12 (L1.ⓑ{I}V2) ?) -HU12 /2 width=1/ /3 width=7/
+ lapply (delift_lsubs_trans … HT12 (L1.ⓑ{I}V2) ?) -HT12 /2 width=1/
+ lapply (delift_lsubs_trans … HU12 (L1.ⓑ{I}V2) ?) -HU12 /2 width=1/ /3 width=7/
| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL1 #HL12
elim (IHVW1 … HL1 HL12) -IHVW1 #V2 #W2 #HVW2 #HV12 #HW12
elim (IHTU1 … HL1 HL12) -IHTU1 -HL1 -HL12 #X2 #Y2 #HXY2 #HX2 #HY2
qed.
lemma nta_ldrop_conf: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 →
- â\88\80L2,d,e. â\89¼ [d, e] L1 → ⇩[d, e] L1 ≡ L2 →
+ â\88\80L2,d,e. â\89½ [d, e] L1 → ⇩[d, e] L1 ≡ L2 →
∃∃T2,U2. ⦃h, L2⦄ ⊢ T2 : U2 &
L1 ⊢ T1 ▼*[d, e] ≡ T2 & L1 ⊢ U1 ▼*[d, e] ≡ U2.
/3 width=1/ qed.
lemma cpcs_bind_sn: ∀I,L,V1,V2,T. L ⊢ V1 ⬌* V2 → L ⊢ ⓑ{I}V1. T ⬌* ⓑ{I}V2. T.
* /2 width=1/ /2 width=2/ qed.
+(* Note: it does not hold replacing |L1| with |L2| *)
+lemma cpcs_lsubs_trans: ∀L1,T1,T2. L1 ⊢ T1 ⬌* T2 →
+ ∀L2. L2 ≼ [0, |L1|] L1 → L2 ⊢ T1 ⬌* T2.
+#L1 #T1 #T2 #HT12
+elim (cpcs_inv_cprs … HT12) -HT12
+/3 width=5 by cprs_div, cprs_lsubs_trans/ (**) (* /3 width=5/ is a bit slow *)
+qed.
+
+
(* Basic_1: was: pc3_lift *)
lemma cpcs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K →
∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 →
non associative with precedence 45
for @{ 'SubEq $T1 $d $e $T2 }.
-notation "hvbox( â\89¼ [ d , break e ] break term 46 T2 )"
+notation "hvbox( â\89½ [ d , break e ] break term 46 T2 )"
non associative with precedence 45
- for @{ 'SubEqTop $d $e $T2 }.
+ for @{ 'SubEqBottom $d $e $T2 }.
notation "hvbox( ⇩ [ e ] break term 46 L1 ≡ break term 46 L2 )"
non associative with precedence 45
(* 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.
+lemma cpr_lsubs_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 →
+ ∀L2. L2 ≼ [0, |L1|] L1 → L2 ⊢ T1 ➡ T2.
#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12
-lapply (tpss_lsubs_conf … HT2 … HL12) -HT2 -HL12 /3 width=4/
+lapply (tpss_lsubs_trans … HT2 … HL12) -HT2 -HL12 /3 width=4/
qed.
(* Basic inversion lemmas ***************************************************)
elim (tpr_inv_abbr1 … H1) -H1 *
[ #V #T0 #T #HV1 #HT10 #HT0 #H destruct
elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct
- lapply (tps_lsubs_conf … HT0 (L. ⓓV) ?) -HT0 /2 width=1/ #HT0
+ lapply (tps_lsubs_trans … HT0 (L. ⓓV) ?) -HT0 /2 width=1/ #HT0
lapply (tps_weak_all … HT0) -HT0 #HT0
- lapply (tpss_lsubs_conf … HT2 (L. ⓓV) ?) -HT2 /2 width=1/ #HT2
+ lapply (tpss_lsubs_trans … HT2 (L. ⓓV) ?) -HT2 /2 width=1/ #HT2
lapply (tpss_weak_all … HT2) -HT2 #HT2
lapply (tpss_strap … HT0 HT2) -T /4 width=7/
| /4 width=5/
L ⊢ ⓑ{I} V1. T1 ➡ ⓑ{I} V2. T2.
#I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2
elim (tpss_split_up … HT2 1 ? ?) -HT2 // #T0 <minus_n_O #HT0 normalize <minus_plus_m_m #HT02
-lapply (tpss_lsubs_conf … HT0 (⋆. ⓑ{I} V2) ?) -HT0 /2 width=1/ #HT0
+lapply (tpss_lsubs_trans … HT0 (⋆. ⓑ{I} V2) ?) -HT0 /2 width=1/ #HT0
lapply (tpss_tps … HT0) -HT0 #HT0
@ex2_1_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2 width=1/ ] (**) (* /3 width=5/ is too slow *)
qed.
lapply (tpss_inv_S2 … HT02 L V ?) -HT02 // #HT02
@(ex2_1_intro … (ⓛV0.T0)) /2 width=1/ -V1 -T1 (**) (* explicit constructors *)
@tpss_bind // -V0
-@(tpss_lsubs_conf (L.ⓛV)) // -T0 -T2 /2 width=1/
+@(tpss_lsubs_trans (L.ⓛV)) // -T0 -T2 /2 width=1/
qed.
(* Advanced inversion lemmas ************************************************)
#L #V1 #T1 #Y * #X #H1 #H2 #I #W
elim (tpr_inv_abst1 … H1) -H1 #V #T #HV1 #HT1 #H destruct
elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct
-lapply (tpss_lsubs_conf … HT2 (L. ⓑ{I} W) ?) -HT2 /2 width=1/ /4 width=5/
+lapply (tpss_lsubs_trans … HT2 (L. ⓑ{I} W) ?) -HT2 /2 width=1/ /4 width=5/
qed-.
(* Basic_1: was pr2_gen_appl *)
| #L1 #V1 #T1 #B #A #HB #HA #H1 #H2 #L2 #HL12 #X #H destruct
elim (tpr_inv_abbr1 … H) -H *
[ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
- lapply (tps_lsubs_conf … HT02 (L2.ⓓV2) ?) -HT02 /2 width=1/ #HT02
+ lapply (tps_lsubs_trans … HT02 (L2.ⓓV2) ?) -HT02 /2 width=1/ #HT02
lapply (IH … HB … HL12 … HV12) -HB /width=5/ #HB
lapply (IH … HA … (L2.ⓓV2) … HT10) -IH -HA -HT10 /width=5/ -T1 /2 width=1/ -L1 -V1 /3 width=5/
| -B #T #HT1 #HTX
elim (tps_inv_bind1 … HY) -HY #WW #TT1 #_ #HTT1 #H destruct
elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
elim (IHT12 … HTT1 (L2. ⓛWW) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
- lapply (tpss_lsubs_conf … HTT2 (L2. ⓓVV2) ?) -HTT2 /3 width=5/
+ lapply (tpss_lsubs_trans … HTT2 (L2. ⓓVV2) ?) -HTT2 /3 width=5/
| #I #V1 #V2 #T1 #T2 #U2 #HV12 #_ #HTU2 #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
elim (tps_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
elim (IHT12 … HTT1 (L2. ⓑ{I} VV2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
elim (tpss_strip_neq … HTT2 … HTU2 ?) -T2 /2 width=1/ #T2 #HTT2 #HUT2
- lapply (tps_lsubs_conf … HTT2 (L2. ⓑ{I} V2) ?) -HTT2 /2 width=1/ #HTT2
+ lapply (tps_lsubs_trans … HTT2 (L2. ⓑ{I} V2) ?) -HTT2 /2 width=1/ #HTT2
elim (ltpss_tps_conf … HTT2 (L2. ⓑ{I} VV2) (d + 1) e ?) -HTT2 /2 width=1/ #W2 #HTTW2 #HTW2
- lapply (tps_lsubs_conf … HTTW2 (⋆. ⓑ{I} VV2) ?) -HTTW2 /2 width=1/ #HTTW2
- lapply (tpss_lsubs_conf … HTW2 (L2. ⓑ{I} VV2) ?) -HTW2 /2 width=1/ #HTW2
+ lapply (tps_lsubs_trans … HTTW2 (⋆. ⓑ{I} VV2) ?) -HTTW2 /2 width=1/ #HTTW2
+ lapply (tpss_lsubs_trans … HTW2 (L2. ⓑ{I} VV2) ?) -HTW2 /2 width=1/ #HTW2
lapply (tpss_trans_eq … HUT2 … HTW2) -T2 /3 width=5/
| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #e #X #H #L2 #HL12
elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct
inductive lsuba: relation lenv ≝
| lsuba_atom: lsuba (⋆) (⋆)
| lsuba_pair: ∀I,L1,L2,V. lsuba L1 L2 → lsuba (L1. ⓑ{I} V) (L2. ⓑ{I} V)
-| lsuba_abbr: ∀L1,L2,V,W,A. L1 ⊢ V ⁝ A → L2 ⊢ W ⁝ A →
+| lsuba_abbr: ∀L1,L2,V,W,A. L1 ⊢ V ⁝ A → L2 ⊢ W ⁝ A →
lsuba L1 L2 → lsuba (L1. ⓓV) (L2. ⓛW)
.
(* Properties concerning basic local environment slicing ********************)
(* Note: the constant 0 cannot be generalized *)
-
lemma lsuba_ldrop_O1_conf: ∀L1,L2. L1 ⁝⊑ L2 → ∀K1,e. ⇩[0, e] L1 ≡ K1 →
∃∃K2. K1 ⁝⊑ K2 & ⇩[0, e] L2 ≡ K2.
#L1 #L2 #H elim H -L1 -L2
]
qed-.
+(* Note: the constant 0 cannot be generalized *)
lemma lsuba_ldrop_O1_trans: ∀L1,L2. L1 ⁝⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
∃∃K1. K1 ⁝⊑ K2 & ⇩[0, e] L1 ≡ K1.
#L1 #L2 #H elim H -L1 -L2
lapply (lt_plus_to_lt_l … H) -H #Hi
elim (IHL i ?) // /3 width=4/
]
-qed.
+qed.
-lemma ldrop_lsubs_ldrop1_abbr: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
- ∀K1,V,i. ⇩[0, i] L1 ≡ K1. ⓓV →
+lemma ldrop_lsubs_ldrop2_abbr: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+ ∀K2,V,i. ⇩[0, i] L2 ≡ K2. ⓓV →
d ≤ i → i < d + e →
- ∃∃K2. K1 ≼ [0, d + e - i - 1] K2 &
- ⇩[0, i] L2 ≡ K2. ⓓV.
+ ∃∃K1. K1 ≼ [0, d + e - i - 1] K2 &
+ ⇩[0, i] L1 ≡ K1. ⓓV.
#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
[ #d #e #K1 #V #i #H
lapply (ldrop_inv_atom1 … H) -H #H destruct
(* Inversion lemmas about local env. full refinement for substitution *******)
(* Note: ldrop_ldrop not needed *)
-lemma sfr_inv_ldrop: â\88\80I,L,K,V,i. â\87©[0, i] L â\89¡ K. â\93\91{I}V â\86\92 â\88\80d,e. â\89¼ [d, e] L →
+lemma sfr_inv_ldrop: â\88\80I,L,K,V,i. â\87©[0, i] L â\89¡ K. â\93\91{I}V â\86\92 â\88\80d,e. â\89½ [d, e] L →
d ≤ i → i < d + e → I = Abbr.
#I #L elim L -L
[ #K #V #i #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 //
+ elim (lsubs_inv_abbr2 … 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
(* Note: ldrop_ldrop not needed *)
lemma sfr_ldrop: ∀L,d,e.
(∀I,K,V,i. d ≤ i → i < d + e → ⇩[0, i] L ≡ K. ⓑ{I}V → I = Abbr) →
- â\89¼ [d, e] L.
+ â\89½ [d, e] L.
#L elim L -L //
#L #I #V #IHL #d @(nat_ind_plus … d) -d
[ #e @(nat_ind_plus … e) -e //
]
qed.
-lemma sfr_ldrop_trans_le: â\88\80L1,L2,d,e. â\87©[d, e] L1 â\89¡ L2 â\86\92 â\88\80dd,ee. â\89¼ [dd, ee] L1 →
- dd + ee â\89¤ d â\86\92 â\89¼ [dd, ee] L2.
+lemma sfr_ldrop_trans_le: â\88\80L1,L2,d,e. â\87©[d, e] L1 â\89¡ L2 â\86\92 â\88\80dd,ee. â\89½ [dd, ee] L1 →
+ dd + ee â\89¤ d â\86\92 â\89½ [dd, ee] L2.
#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hddee
@sfr_ldrop #I #K2 #V2 #i #Hddi #Hiddee #HLK2
lapply (lt_to_le_to_lt … Hiddee Hddee) -Hddee #Hid
qed.
lemma sfr_ldrop_trans_be_up: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 →
- â\88\80dd,ee. â\89¼ [dd, ee] L1 →
+ â\88\80dd,ee. â\89½ [dd, ee] L1 →
dd ≤ d + e → d + e ≤ dd + ee →
- â\89¼ [d, dd + ee - d - e] L2.
+ â\89½ [d, dd + ee - d - e] L2.
#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hdde #Hddee
@sfr_ldrop #I #K2 #V2 #i #Hdi #Hiddee #HLK2
lapply (transitive_le ? ? (i+e)… Hdde ?) -Hdde /2 width=1/ #Hddie
@(sfr_inv_ldrop … HL1K2 … HL1) -L1 >commutative_plus // -Hddie /2 width=1/
qed.
-lemma sfr_ldrop_trans_ge: â\88\80L1,L2,d,e. â\87©[d, e] L1 â\89¡ L2 â\86\92 â\88\80dd,ee. â\89¼ [dd, ee] L1 →
- d + e â\89¤ dd â\86\92 â\89¼ [dd - e, ee] L2.
+lemma sfr_ldrop_trans_ge: â\88\80L1,L2,d,e. â\87©[d, e] L1 â\89¡ L2 â\86\92 â\88\80dd,ee. â\89½ [dd, ee] L1 →
+ d + e â\89¤ dd â\86\92 â\89½ [dd - e, ee] L2.
#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hddee
@sfr_ldrop #I #K2 #V2 #i #Hddi #Hiddee #HLK2
elim (le_inv_plus_l … Hddee) -Hddee #Hdde #Hedd
| 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. â\93\9bV1) (L2.â\93\91{I} V2)
+ lsubs 0 (e + 1) (L1. â\93\91{I}V1) (L2. â\93\9bV2)
| 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)
.
"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.
+definition lsubs_trans: ∀S. (lenv → relation S) → Prop ≝ λS,R.
+ ∀L2,s1,s2. R L2 s1 s2 →
+ ∀L1,d,e. L1 ≼ [d, e] L2 → R L1 s1 s2.
(* Basic properties *********************************************************)
qed.
lemma lsubs_abst_lt: ∀L1,L2,I,V1,V2,e. L1 ≼ [0, e - 1] L2 → 0 < e →
- L1. â\93\9bV1 â\89¼ [0, e] L2.â\93\91{I} V2.
+ L1. â\93\91{I}V1 â\89¼ [0, e] L2. â\93\9bV2.
#L1 #L2 #I #V1 #V2 #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
qed.
qed.
lemma lsubs_bind_lt: ∀I,L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e →
- L1. â\93\91{I}V â\89¼ [0, e] L2.â\93\93V.
+ L1. â\93\93V â\89¼ [0, e] L2. â\93\91{I}V.
* /2 width=1/ qed.
lemma lsubs_refl: ∀d,e,L. L ≼ [d, e] L.
]
qed.
-lemma TC_lsubs_conf: ∀S,R. lsubs_conf S R → lsubs_conf S (λL. (TC … (R L))).
+lemma TC_lsubs_trans: ∀S,R. lsubs_trans S R → lsubs_trans 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
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.
+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-.
+
+fact lsubs_inv_atom2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L2 = ⋆ →
+ L1 = ⋆ ∨ (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_atom2: ∀L1,d,e. L1 ≼ [d, e] ⋆ →
+ L1 = ⋆ ∨ (d = 0 ∧ e = 0).
+/2 width=3/ qed-.
+
+fact lsubs_inv_abbr2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+ ∀K2,V. L2 = K2.ⓓV → d = 0 → 0 < e →
+ ∃∃K1. K1 ≼ [0, e - 1] K2 & L1 = K1.ⓓV.
#L1 #L2 #d #e * -L1 -L2 -d -e
[ #d #e #K1 #V #H destruct
| #L1 #L2 #K1 #V #_ #_ #H
]
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.
+lemma lsubs_inv_abbr2: ∀L1,K2,V,e. L1 ≼ [0, e] K2.ⓓV → 0 < e →
+ ∃∃K1. K1 ≼ [0, e - 1] K2 & L1 = K1.ⓓ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.
+fact lsubs_inv_skip2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+ ∀I2,K2,V2. L2 = K2.ⓑ{I2}V2 → 0 < d →
+ ∃∃I1,K1,V1. K1 ≼ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
#L1 #L2 #d #e * -L1 -L2 -d -e
[ #d #e #I1 #K1 #V1 #H destruct
| #L1 #L2 #I1 #K1 #V1 #_ #H
]
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.
+lemma lsubs_inv_skip2: ∀I2,L1,K2,V2,d,e. L1 ≼ [d, e] K2.ⓑ{I2}V2 → 0 < d →
+ ∃∃I1,K1,V1. K1 ≼ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
/2 width=5/ qed-.
(* Basic forward lemmas *****************************************************)
(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
-(* top element of the refinement *)
+(* bottom element of the refinement *)
definition sfr: nat → nat → predicate lenv ≝
- λd,e. NF … (lsubs d e) (lsubs d e …).
+ λd,e. NF_sn … (lsubs d e) (lsubs d e …).
interpretation
"local environment full refinement (substitution)"
- 'SubEqTop d e L = (sfr d e L).
+ 'SubEqBottom d e L = (sfr d e L).
(* Basic properties *********************************************************)
-lemma sfr_atom: â\88\80d,e. â\89¼ [d, e] ⋆.
+lemma sfr_atom: â\88\80d,e. â\89½ [d, e] ⋆.
#d #e #L #H
-elim (lsubs_inv_atom1 … H) -H
+elim (lsubs_inv_atom2 … H) -H
[ #H destruct //
| * #H1 #H2 destruct //
]
qed.
-lemma sfr_OO: â\88\80L. â\89¼ [0, 0] L.
+lemma sfr_OO: â\88\80L. â\89½ [0, 0] L.
// qed.
-lemma sfr_abbr: â\88\80L,V,e. â\89¼ [0, e] L â\86\92 â\89¼ [0, e + 1] L.ⓓV.
+lemma sfr_abbr: â\88\80L,V,e. â\89½ [0, e] L â\86\92 â\89½ [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
+elim (lsubs_inv_abbr2 … H ?) -H // <minus_plus_m_m #X #HLX #H destruct
lapply (HL … HLX) -HL -HLX /2 width=1/
qed.
-lemma sfr_skip: â\88\80I,L,V,d,e. â\89¼ [d, e] L â\86\92 â\89¼ [d + 1, e] L.ⓑ{I}V.
+lemma sfr_skip: â\88\80I,L,V,d,e. â\89½ [d, e] L â\86\92 â\89½ [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
+elim (lsubs_inv_skip2 … 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: â\88\80I,L,V,e. â\89¼ [0, e] L.ⓑ{I}V → 0 < e →
- â\89¼ [0, e - 1] L ∧ I = Abbr.
+lemma sfr_inv_bind: â\88\80I,L,V,e. â\89½ [0, e] L.ⓑ{I}V → 0 < e →
+ â\89½ [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
+elim (lsubs_inv_abbr2 … 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 //
+elim (lsubs_inv_abbr2 … H ?) -H // -He #X #HLX #H destruct //
qed-.
-lemma sfr_inv_skip: â\88\80I,L,V,d,e. â\89¼ [d, e] L.â\93\91{I}V â\86\92 0 < d â\86\92 â\89¼ [d - 1, e] L.
+lemma sfr_inv_skip: â\88\80I,L,V,d,e. â\89½ [d, e] L.â\93\91{I}V â\86\92 0 < d â\86\92 â\89½ [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 //
+elim (lsubs_inv_skip2 … 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_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶ [d, e] T2 →
+ ∀L2. L2 ≼ [d, e] L1 → 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
- elim (ldrop_lsubs_ldrop1_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /2 width=4/
+ elim (ldrop_lsubs_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /2 width=4/
| /4 width=1/
| /3 width=1/
]
elim (IHV12 i ? ?) -IHV12 // #V #HV1 #HV2
elim (IHT12 (i + 1) ? ?) -IHT12 /2 width=1/
-Hdi -Hide >arith_c1x #T #HT1 #HT2
- lapply (tps_lsubs_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /3 width=5/
+ lapply (tps_lsubs_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /3 width=5/
| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide
elim (IHV12 i ? ?) -IHV12 // elim (IHT12 i ? ?) -IHT12 //
-Hdi -Hide /3 width=5/
elim (IHV12 i ? ?) -IHV12 // #V #HV1 #HV2
elim (IHT12 (i + 1) ? ?) -IHT12 /2 width=1/
-Hdi -Hide >arith_c1x #T #HT1 #HT2
- lapply (tps_lsubs_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /3 width=5/
+ lapply (tps_lsubs_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /3 width=5/
| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide
elim (IHV12 i ? ?) -IHV12 // elim (IHT12 i ? ?) -IHT12 //
-Hdi -Hide /3 width=5/
]
| #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX
elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
- lapply (tps_lsubs_conf … HT02 (L. ⓑ{I} V1) ?) -HT02 /2 width=1/ #HT02
+ lapply (tps_lsubs_trans … HT02 (L. ⓑ{I} V1) ?) -HT02 /2 width=1/ #HT02
elim (IHV01 … HV02) -V0 #V #HV1 #HV2
elim (IHT01 … HT02) -T0 #T #HT1 #HT2
- lapply (tps_lsubs_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/
- lapply (tps_lsubs_conf … HT2 (L. ⓑ{I} V) ?) -HT2 /3 width=5/
+ lapply (tps_lsubs_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/
+ lapply (tps_lsubs_trans … HT2 (L. ⓑ{I} V) ?) -HT2 /3 width=5/
| #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX
elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
elim (IHV01 … HV02) -V0
elim (IHV01 … HV02 H) -V0 #V #HV1 #HV2
elim (IHT01 … HT02 ?) -T0
[ -H #T #HT1 #HT2
- lapply (tps_lsubs_conf … HT1 (L2. ⓑ{I} V) ?) -HT1 /2 width=1/
- lapply (tps_lsubs_conf … HT2 (L1. ⓑ{I} V) ?) -HT2 /2 width=1/ /3 width=5/
+ lapply (tps_lsubs_trans … HT1 (L2. ⓑ{I} V) ?) -HT1 /2 width=1/
+ lapply (tps_lsubs_trans … HT2 (L1. ⓑ{I} V) ?) -HT2 /2 width=1/ /3 width=5/
| -HV1 -HV2 >plus_plus_comm_23 >plus_plus_comm_23 in ⊢ (? ? %); elim H -H #H
[ @or_introl | @or_intror ] /2 by monotonic_le_plus_l/ (**) (* /3 / is too slow *)
]
<(tps_inv_lift1_eq … HVT2 … HVW) -HVT2 /2 width=4/
| #L #I #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He
elim (tps_inv_bind1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct
- lapply (tps_lsubs_conf … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02
+ lapply (tps_lsubs_trans … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02
lapply (IHT10 … HT02 He) -T0 #HT12
- lapply (tps_lsubs_conf … HT12 (L. ⓑ{I} V2) ?) -HT12 /2 width=1/ /3 width=1/
+ lapply (tps_lsubs_trans … HT12 (L. ⓑ{I} V2) ?) -HT12 /2 width=1/ /3 width=1/
| #L #I #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He
elim (tps_inv_flat1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct /3 width=1/
]
<(tps_inv_lift1_eq … HWT2 … HVW) -HWT2 /4 width=4/
| #L #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
- lapply (tps_lsubs_conf … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02
+ lapply (tps_lsubs_trans … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02
elim (IHV10 … HV02 ?) -IHV10 -HV02 // #V
elim (IHT10 … HT02 ?) -T0 /2 width=1/ #T #HT1 #HT2
- lapply (tps_lsubs_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/
- lapply (tps_lsubs_conf … HT2 (L. ⓑ{I} V2) ?) -HT2 /2 width=1/ /3 width=6/
+ lapply (tps_lsubs_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/
+ lapply (tps_lsubs_trans … HT2 (L. ⓑ{I} V2) ?) -HT2 /2 width=1/ /3 width=6/
| #L #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
elim (IHV10 … HV02 ?) -V0 //
lemma delift_refl_O2: ∀L,T,d. L ⊢ T ▼*[d, 0] ≡ T.
/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.
+lemma delift_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▼*[d, e] ≡ T2 →
+ ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ T1 ▼*[d, e] ≡ T2.
#L1 #T1 #T2 #d #e * /3 width=3/
qed.
L ⊢ V1 ▼*[d, e] ≡ V2 → L. ⓑ{I} V2 ⊢ T1 ▼*[d+1, e] ≡ T2 →
L ⊢ ⓑ{I} V1. T1 ▼*[d, e] ≡ ⓑ{I} V2. T2.
#I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * #T #HT1 #HT2
-lapply (tpss_lsubs_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/ /3 width=5/
+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.
#I #L #V1 #T1 #U2 #d #e * #U #HU #HU2
elim (tpss_inv_bind1 … HU) -HU #V #T #HV1 #HT1 #X destruct
elim (lift_inv_bind2 … HU2) -HU2 #V2 #T2 #HV2 #HT2
-lapply (tpss_lsubs_conf … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
+lapply (tpss_lsubs_trans … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
qed-.
lemma delift_inv_flat1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓕ{I} V1. T1 ▼*[d, e] ≡ U2 →
(* 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.
+lemma delifta_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▼▼*[d, e] ≡ T2 →
+ ∀L2. L2 ≼ [d, e] L1 → 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/
+ elim (ldrop_lsubs_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
| /4 width=1/
| /3 width=1/
]
]
| * #I #V1 #T1 #_ #_ #IH #X #d #e #H
[ elim (delift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
- lapply (delift_lsubs_conf … HT12 (L.ⓑ{I}V1) ?) -HT12 /2 width=1/ #HT12
+ lapply (delift_lsubs_trans … HT12 (L.ⓑ{I}V1) ?) -HT12 /2 width=1/ #HT12
lapply (IH … HV12) -HV12 // #HV12
lapply (IH … HT12) -IH -HT12 /2 width=1/ #HT12
- lapply (delifta_lsubs_conf … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
+ lapply (delifta_lsubs_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
| elim (delift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
lapply (IH … HV12) -HV12 //
lapply (IH … HT12) -IH -HT12 // /2 width=1/
lapply (IH … HV02 … HK01 ? ?) -IH -HV02 -HK01
[1,3: // |2,4: skip | normalize /2 width=1/ | /2 width=6/ ]
| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct
- lapply (tpss_lsubs_conf … HT12 (L. ⓑ{I} V1) ?) -HT12 /2 width=1/ #HT12
+ lapply (tpss_lsubs_trans … HT12 (L. ⓑ{I} V1) ?) -HT12 /2 width=1/ #HT12
lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=2/ ] #HV12
lapply (IH … HT12 (L0. ⓑ{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12
- lapply (tpss_lsubs_conf … HT12 (L0. ⓑ{I} V2) ?) -HT12 /2 width=1/
+ lapply (tpss_lsubs_trans … HT12 (L0. ⓑ{I} V2) ?) -HT12 /2 width=1/
| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct
lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=3/ ]
lapply (IH … HT12 … HL0 ? ?) -IH -HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2 width=1/
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_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶* [d, e] T2 →
+ ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ T1 ▶* [d, e] T2.
/3 width=3/ qed.
lemma tpss_refl: ∀d,e,L,T. L ⊢ T ▶* [d, e] T.
| #T #T2 #_ #HT2 #IHT @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
]
| #V #V2 #_ #HV12 #IHV #I #T1 #T2 #HT12
- lapply (tpss_lsubs_conf … HT12 (L. ⓑ{I} V) ?) -HT12 /2 width=1/ #HT12
+ lapply (tpss_lsubs_trans … HT12 (L. ⓑ{I} V) ?) -HT12 /2 width=1/ #HT12
lapply (IHV … HT12) -IHV -HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
]
qed.
[ /2 width=5/
| #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct
elim (tps_inv_bind1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H
- lapply (tpss_lsubs_conf … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
+ lapply (tpss_lsubs_trans … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
]
qed-.
(* 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_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶▶* [d, e] T2 →
+ ∀L2. L2 ≼ [d, e] L1 → 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
- elim (ldrop_lsubs_ldrop1_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
+ elim (ldrop_lsubs_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
| /4 width=1/
| /3 width=1/
]
elim (tps_inv_lift1_be … H … H0LK … HVW2 ? ?) -H -H0LK -HVW2 // /3 width=6/
| #L #I #V1 #V #T1 #T #d #e #_ #_ #IHV1 #IHT1 #X #H
elim (tps_inv_bind1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct
- lapply (tps_lsubs_conf … HT2 (L.ⓑ{I}V) ?) -HT2 /2 width=1/ #HT2
+ lapply (tps_lsubs_trans … HT2 (L.ⓑ{I}V) ?) -HT2 /2 width=1/ #HT2
lapply (IHV1 … HV2) -IHV1 -HV2 #HV12
lapply (IHT1 … HT2) -IHT1 -HT2 #HT12
- lapply (tpssa_lsubs_conf … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
+ lapply (tpssa_lsubs_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
| #L #I #V1 #V #T1 #T #d #e #_ #_ #IHV1 #IHT1 #X #H
elim (tps_inv_flat1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct /3 width=1/
]
@SN_intro #a2 #HRa12 #HSa12
elim (HSa12 ?) -HSa12 /2 width=1/
qed.
+
+definition NF_sn: ∀A. relation A → relation A → predicate A ≝
+ λA,R,S,a2. ∀a1. R a1 a2 → S a2 a1.
+
+inductive SN_sn (A) (R,S:relation A): predicate A ≝
+| SN_sn_intro: ∀a2. (∀a1. R a1 a2 → (S a2 a1 → ⊥) → SN_sn A R S a1) → SN_sn A R S a2
+.
+
+lemma NF_to_SN_sn: ∀A,R,S,a. NF_sn A R S a → SN_sn A R S a.
+#A #R #S #a2 #Ha2
+@SN_sn_intro #a1 #HRa12 #HSa12
+elim (HSa12 ?) -HSa12 /2 width=1/
+qed.
["}"; "❵"; "⦄" ] ;
["□"; "◽"; "▪"; "◾"; ];
["◊"; "♢"; "⧫"; "♦"; "⟐"; "⟠"; ] ;
- [">"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; ] ;
+ [">"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; ] ;
+ ["≥"; "≽"; ];
["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ;
["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; ] ;
["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; ] ;
projects / helm.git / commitdiff