LDWS := $(shell find -name "*.ldw.xml")
TBLS := $(shell find -name "*.tbl")
+all:
+ @echo " MATITAC $(PACKAGES)"
+ $(H)../../matitac.opt $(PACKAGES)
+
# MAS ########################################################################
define MAS_TEMPLATE
$(foreach PKG, $(PACKAGES), $(eval $(call MAS_TEMPLATE,$(PKG))))
-all:
- @echo " MATITAC $(PACKAGES)"
- $(H)../../matitac.opt $(MAS)
-
# XMAS #######################################################################
define XMAS_TEMPLATE
[ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1)
#U2 #HVU2 @(ex3_intro … U2)
[1,3: /3 width=7 by fqu_drop, cpxs_delta, drop_pair, drop_drop/
- | #H destruct /2 width=7 by lift_inv_lref2_be/
+ | #H destruct
+ lapply (lift_inv_lref2_be … HVU2 ? ?) -HVU2 //
]
| #I #G #L #V1 #T #V2 #HV12 #H @(ex3_intro … (②{I}V2.T))
[1,3: /2 width=4 by fqu_pair_sn, cpxs_pair_sn/
G ⊢ ⬊*[h, g, V, l] K.
#h #g #G #L #l * -L -l /2 width=1 by or_introl/
[ #I #L #T #_ #x #H elim (ysucc_inv_O_sn … H)
-| #I #L #T #l #HT #HL #x #H <(ysucc_inj … H) -x
+| #I #L #T #l #HT #HL #x #H <(ysucc_inv_inj … H) -x
/3 width=6 by ex3_3_intro, or_intror/
]
qed-.
#h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2 //
[ #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #l #HL #H
elim (ylt_split i l) #Hli [ -H | -HL ]
- [ <(ymax_pre_sn l (⫯i)) /2 width=1 by ylt_fwd_le_succ/
+ [ <(ymax_pre_sn l (⫯i)) /2 width=1 by ylt_fwd_le_succ1/
elim (lcosx_drop_trans_lt … HL … HLK) // -HL -Hli
lapply (drop_fwd_drop2 … HLK) -HLK /3 width=7 by lsx_lift_ge/
| lapply (lsx_fwd_lref_be … H … HLK) // -H -Hli
| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #l #HL #H
elim (lsx_inv_flat … H) -H /3 width=1 by lsx_flat/
| #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #l #HL #H
- elim (lsx_inv_bind … H) -H
- /4 width=9 by lcosx_pair, lsx_inv_lift_ge, drop_drop/
+ elim (lsx_inv_bind … H) -H #HV #HU1
+ <(ypred_succ l) <yminus_SO2
+ /4 width=7 by lcosx_pair, lsx_inv_lift_ge, drop_drop/
| #G #L #V #T1 #T2 #_ #IHT12 #l #HL #H
elim (lsx_inv_flat … H) -H /2 width=1 by/
| #G #L #V1 #V2 #T #_ #IHV12 #l #HL #H
elim (lsx_inv_flat … H) -H #HV1 #H
elim (lsx_inv_bind … H) -H #HW1 #HT1
@lsx_bind /2 width=1 by/ (**) (* explicit constructor *)
- @lsx_flat [ /3 width=7 by lsx_lift_ge, drop_drop/ ]
+ @lsx_flat [ <yplus_SO2 /3 width=7 by lsx_lift_ge, drop_drop/ ]
@(lsx_lreq_conf … (L.ⓓW1)) /3 width=1 by lcosx_pair, lreq_succ/
]
qed-.
>(lift_inv_sort1 … H) -X -K -l -m //
| #I #G #K #K0 #V #i #HK0 #_ #IHV #L #s #l #m #HLK #X #H
elim (lift_inv_lref1 … H) * #Hil #H destruct
- [ elim (drop_trans_le … HLK … HK0) -K /2 width=2 by lt_to_le/ #X #HL0 #H
- elim (drop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hil #L0 #W #HLK0 #HVW #H destruct
+ [ elim (drop_trans_le … HLK … HK0) -K /2 width=2 by ylt_fwd_le/ #X #HL0 #H
+ elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil #L0 #W #HLK0 #HVW #H destruct
/3 width=9 by snv_lref/
| lapply (drop_trans_ge … HLK … HK0 ?) -K
/3 width=9 by snv_lref, drop_inv_gen/
>(lift_inv_sort2 … H) -X -L -l -m //
| #I #G #L #L0 #W #i #HL0 #_ #IHW #K #s #l #m #HLK #X #H
elim (lift_inv_lref2 … H) * #Hil #H destruct
- [ elim (drop_conf_le … HLK … HL0) -L /2 width=2 by lt_to_le/ #X #HK0 #H
- elim (drop_inv_skip1 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hil #K0 #V #HLK0 #HVW #H destruct
+ [ elim (drop_conf_le … HLK … HL0) -L /2 width=2 by ylt_fwd_le/ #X #HK0 #H
+ elim (drop_inv_skip1 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K0 #V #HLK0 #HVW #H destruct
/3 width=12 by snv_lref/
| lapply (drop_conf_ge … HLK … HL0 ?) -L /3 width=9 by snv_lref/
]
#T #T2 #_ #HT2 #IHT1 <(cpy_inv_refl_O2 … HT2) -HT2 //
qed-.
-lemma cpys_inv_lift1_eq: ∀G,L,U1,U2. ∀l,m:nat.
- ⦃G, L⦄ ⊢ U1 ▶*[l, m] U2 → ∀T1. ⬆[l, m] T1 ≡ U1 → U1 = U2.
+lemma cpys_inv_lift1_eq: ∀G,L,U1,U2,l,m.
+ ⦃G, L⦄ ⊢ U1 ▶*[l, yinj m] U2 → ∀T1. ⬆[l, m] T1 ≡ U1 → U1 = U2.
#G #L #U1 #U2 #l #m #H #T1 #HTU1 @(cpys_ind … H) -U2
/2 width=7 by cpy_inv_lift1_eq/
qed-.
lapply (drop_fwd_drop2 … HLK) #H0LK
lapply (cpy_weak … H 0 (l+m) ? ?) -H // #H
elim (cpy_inv_lift1_be … H … H0LK … HVW2) -H -H0LK -HVW2
- /3 width=7 by cpysa_subst, ylt_fwd_le_succ/
+ /3 width=7 by cpysa_subst, ylt_fwd_le_succ1/
| #a #I #G #L #V1 #V #T1 #T #l #m #_ #_ #IHV1 #IHT1 #X #H
elim (cpy_inv_bind1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct
/5 width=5 by cpysa_bind, lsuby_cpy_trans, lsuby_succ/
lemma cpys_inv_lift1_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
- l ≤ lt → lt ≤ yinj l + m → yinj l + m ≤ lt + mt →
- ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[l, lt + mt - (yinj l + m)] T2 &
+ l ≤ lt → lt ≤ l + m → l + m ≤ lt + mt →
+ ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[l, lt + mt - (l + m)] T2 &
⬆[l, m] T2 ≡ U2.
#G #L #U1 #U2 #lt #mt #HU12 #K #s #l #m #HLK #T1 #HTU1 #Hllt #Hltlm #Hlmlmt
elim (cpys_split_up … HU12 (l + m)) -HU12 // -Hlmlmt #U #HU1 #HU2
#HW2 >(cpys_inv_lift1_eq … HW2) -HW2 //
| elim (drop_O1_le (Ⓕ) … Hi) -Hi #K2 #HLK2
elim (cpys_inv_lift1_ge_up … HW2 … HLK2 … HVW2 ? ? ?) -HW2 -HLK2 -HVW2
- /2 width=1 by ylt_fwd_le_succ, yle_succ_dx/ -Hli -Hilm
- #X #_ #H elim (lift_inv_lref2_be … H) -H //
+ /2 width=1 by ylt_fwd_le_succ1, yle_succ_dx/ -Hli -Hilm
+ #X #_ #H elim (lift_inv_lref2_be … H) -H /2 width=1 by ylt_inj/
]
| #a #I #G #L1 #V1 #V2 #T1 #T2 #l #m #_ #_ #IHV12 #IHT12 #L2 #H elim (cpys_inv_bind1 … H) -H
#V #T #HV2 #HT2 #H destruct
lapply (cpy_lift_ge … HU1 … HLK HU0 HU12 ?) -HU1 -HLK -HU0 -HU12 // #HU02
lapply (cpy_weak … HU02 l m ? ?) -HU02
[2,3: /2 width=3 by cpys_strap1, yle_succ_dx/ ]
- >yplus_O1 <yplus_inj >ymax_pre_sn_comm /2 width=1 by ylt_fwd_le_succ/
+ >yplus_O1 <yplus_inj >ymax_pre_sn_comm /2 width=1 by ylt_fwd_le_succ1/
]
qed.
| * #J #K #V1 #V #i #Hli #Hilm #HLK #HV1 #HVT #HI
lapply (drop_fwd_drop2 … HLK) #H
elim (cpy_inv_lift1_ge_up … HT2 … H … HVT) -HT2 -H -HVT
- [2,3,4: /2 width=1 by ylt_fwd_le_succ, yle_succ_dx/ ]
+ [2,3,4: /2 width=1 by ylt_fwd_le_succ1, yle_succ_dx/ ]
/4 width=11 by cpys_strap1, ex6_5_intro, or_intror/
]
]
& l ≤ i
& i < l + m.
#G #L #T2 #i #l #m #H #I #K #V1 #HLK #V2 #HVT2 elim (cpys_inv_lref1 … H) -H
-[ #H destruct elim (lift_inv_lref2_be … HVT2) -HVT2 -HLK //
+[ #H destruct elim (lift_inv_lref2_be … HVT2) -HVT2 -HLK /2 width=1 by ylt_inj/
| * #Z #Y #X1 #X2 #Hli #Hilm #HLY #HX12 #HXT2
lapply (lift_inj … HXT2 … HVT2) -T2 #H destruct
lapply (drop_mono … HLY … HLK) -L #H destruct
(* Properties on relocation *************************************************)
lemma cpys_lift_le: ∀G,K,T1,T2,lt,mt. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt] T2 →
- ∀L,U1,s,l,m. lt + mt ≤ yinj l → ⬇[s, l, m] L ≡ K →
+ ∀L,U1,s,l,m. lt + mt ≤ l → ⬇[s, l, m] L ≡ K →
⬆[l, m] T1 ≡ U1 → ∀U2. ⬆[l, m] T2 ≡ U2 →
⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2.
#G #K #T1 #T2 #lt #mt #H #L #U1 #s #l #m #Hlmtl #HLK #HTU1 @(cpys_ind … H) -T2
qed-.
lemma cpys_lift_be: ∀G,K,T1,T2,lt,mt. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt] T2 →
- ∀L,U1,s,l,m. lt ≤ yinj l → l ≤ lt + mt →
+ ∀L,U1,s,l,m. lt ≤ l → l ≤ lt + mt →
⬇[s, l, m] L ≡ K → ⬆[l, m] T1 ≡ U1 →
∀U2. ⬆[l, m] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ▶*[lt, mt + m] U2.
#G #K #T1 #T2 #lt #mt #H #L #U1 #s #l #m #Hltl #Hllmt #HLK #HTU1 @(cpys_ind … H) -T2
qed-.
lemma cpys_lift_ge: ∀G,K,T1,T2,lt,mt. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt] T2 →
- ∀L,U1,s,l,m. yinj l ≤ lt → ⬇[s, l, m] L ≡ K →
+ ∀L,U1,s,l,m. l ≤ lt → ⬇[s, l, m] L ≡ K →
⬆[l, m] T1 ≡ U1 → ∀U2. ⬆[l, m] T2 ≡ U2 →
⦃G, L⦄ ⊢ U1 ▶*[lt+m, mt] U2.
#G #K #T1 #T2 #lt #mt #H #L #U1 #s #l #m #Hllt #HLK #HTU1 @(cpys_ind … H) -T2
lemma cpys_inv_lift1_be: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
- lt ≤ l → yinj l + m ≤ lt + mt →
+ lt ≤ l → l + m ≤ lt + mt →
∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt - m] T2 & ⬆[l, m] T2 ≡ U2.
#G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hltl #Hlmlmt @(cpys_ind … H) -U2
[ /2 width=3 by ex2_intro/
lemma cpys_inv_lift1_ge: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
- yinj l + m ≤ lt →
+ l + m ≤ lt →
∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[lt - m, mt] T2 & ⬆[l, m] T2 ≡ U2.
#G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hlmlt @(cpys_ind … H) -U2
[ /2 width=3 by ex2_intro/
lemma cpys_inv_lift1_ge_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
- l ≤ lt → lt ≤ yinj l + m → yinj l + m ≤ lt + mt →
- ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[l, lt + mt - (yinj l + m)] T2 &
+ l ≤ lt → lt ≤ l + m → l + m ≤ lt + mt →
+ ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[l, lt + mt - (l + m)] T2 &
⬆[l, m] T2 ≡ U2.
#G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hllt #Hltlm #Hlmlmt @(cpys_ind … H) -U2
[ /2 width=3 by ex2_intro/
lemma cpys_inv_lift1_be_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
- lt ≤ l → lt + mt ≤ yinj l + m →
+ lt ≤ l → lt + mt ≤ l + m →
∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[lt, l - lt] T2 & ⬆[l, m] T2 ≡ U2.
#G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hltl #Hlmtlm @(cpys_ind … H) -U2
[ /2 width=3 by ex2_intro/
lemma cpys_inv_lift1_le_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
- lt ≤ l → l ≤ lt + mt → lt + mt ≤ yinj l + m →
+ lt ≤ l → l ≤ lt + mt → lt + mt ≤ l + m →
∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[lt, l - lt] T2 & ⬆[l, m] T2 ≡ U2.
#G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hltl #Hllmt #Hlmtlm @(cpys_ind … H) -U2
[ /2 width=3 by ex2_intro/
qed-.
lemma cpys_inv_lift1_subst: ∀G,L,W1,W2,l,m. ⦃G, L⦄ ⊢ W1 ▶*[l, m] W2 →
- ∀K,V1,i. ⬇[i+1] L ≡ K → ⬆[O, i+1] V1 ≡ W1 →
+ ∀K,V1,i. ⬇[i+1] L ≡ K → ⬆[O, i+1] V1 ≡ W1 →
l ≤ yinj i → i < l + m →
∃∃V2. ⦃G, K⦄ ⊢ V1 ▶*[O, ⫰(l+m-i)] V2 & ⬆[O, i+1] V2 ≡ W2.
#G #L #W1 #W2 #l #m #HW12 #K #V1 #i #HLK #HVW1 #Hli #Hilm
(* ITERATED LOCAL ENVIRONMENT SLICING ***************************************)
-inductive drops (s:bool): list2 nat nat → relation lenv ≝
+inductive drops (s:bool): list2 ynat nat → relation lenv ≝
| drops_nil : ∀L. drops s (◊) L L
| drops_cons: ∀L1,L,L2,cs,l,m.
drops s cs L1 L → ⬇[s, l, m] L ≡ L2 → drops s ({l, m} @ cs) L1 L2
>(drops_inv_nil … H) -L1 /2 width=7 by lifts_nil, minuss_nil, ex4_3_intro, drops_nil/
| #cs #cs2 #l #m #i #Hil #_ #IHcs2 #L1 #K2 #V2 #H
elim (drops_inv_cons … H) -H #L #HL1 #H
- elim (drop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ #K #V >minus_plus #HK2 #HV2 #H destruct
+ elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ #K #V <yminus_succ2 #HK2 #HV2 #H destruct
elim (IHcs2 … HL1) -IHcs2 -HL1 #K1 #V1 #cs1 #Hcs1 #HK1 #HV1 #X destruct
@(ex4_3_intro … K1 V1 … ) // [3,4: /2 width=7 by lifts_cons, drops_cons/ | skip ]
- normalize >plus_minus /3 width=1 by minuss_lt, lt_minus_to_plus/ (**) (* explicit constructors *)
+ >pluss_SO2 >pluss_SO2
+ >yminus_succ2 >ylt_inv_O1 /2 width=1 by ylt_to_minus/ <yminus_succ >commutative_plus (**) (* <yminus_succ1_inj does not work *)
+ /3 width=1 by minuss_lt, ylt_succ/
| #cs #cs2 #l #m #i #Hil #_ #IHcs2 #L1 #K2 #V2 #H
elim (IHcs2 … H) -IHcs2 -H #K1 #V1 #cs1 #Hcs1 #HK1 #HV1 #X destruct
- /4 width=7 by minuss_ge, ex4_3_intro, le_S_S/
+ /4 width=7 by minuss_ge, yle_succ, ex4_3_intro/
]
qed-.
#L1 #L #cs #H elim H -L1 -L -cs
[ /2 width=7 by drops_nil, minuss_nil, at_nil, ex4_3_intro/
| #L1 #L0 #L #cs #l #m #_ #HL0 #IHL0 #L2 #i #HL2
- elim (lt_or_ge i l) #Hil
- [ elim (drop_trans_le … HL0 … HL2) -L /2 width=2 by lt_to_le/
+ elim (ylt_split i l) #Hil
+ [ elim (drop_trans_le … HL0 … HL2) -L /2 width=2 by ylt_fwd_le/
#L #HL0 #HL2 elim (IHL0 … HL0) -L0 /3 width=7 by drops_cons, minuss_lt, at_lt, ex4_3_intro/
| lapply (drop_trans_ge … HL0 … HL2 ?) -L // #HL02
elim (IHL0 … HL02) -L0 /3 width=7 by minuss_ge, at_ge, ex4_3_intro/
(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
-inductive frees: relation4 ynat lenv term nat ≝
+inductive frees: relation4 ynat lenv term ynat ≝
| frees_eq: ∀L,U,l,i. (∀T. ⬆[i, 1] T ≡ U → ⊥) → frees l L U i
-| frees_be: ∀I,L,K,U,W,l,i,j. l ≤ yinj j → j < i →
+| frees_be: ∀I,L,K,U,W,l,i,j. l ≤ yinj j → yinj j < i →
(∀T. ⬆[j, 1] T ≡ U → ⊥) → ⬇[j]L ≡ K.ⓑ{I}W →
- frees 0 K W (i-j-1) → frees l L U i.
+ frees 0 K W (⫰(i-j)) → frees l L U i.
interpretation
"context-sensitive free variables (term)"
lemma frees_inv: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
(∀T. ⬆[i, 1] T ≡ U → ⊥) ∨
∃∃I,K,W,j. l ≤ yinj j & j < i & (∀T. ⬆[j, 1] T ≡ U → ⊥) &
- ⬇[j]L ≡ K.ⓑ{I}W & K ⊢ (i-j-1) ϵ 𝐅*[yinj 0]⦃W⦄.
+ ⬇[j]L ≡ K.ⓑ{I}W & K ⊢ ⫰(i-j) ϵ 𝐅*[yinj 0]⦃W⦄.
#L #U #l #i * -L -U -l -i /4 width=9 by ex5_4_intro, or_intror, or_introl/
qed-.
qed-.
lemma frees_inv_lref: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ →
- j = i ∨
- ∃∃I,K,W. l ≤ yinj j & j < i & ⬇[j] L ≡ K.ⓑ{I}W & K ⊢ (i-j-1) ϵ 𝐅*[yinj 0]⦃W⦄.
+ yinj j = i ∨
+ ∃∃I,K,W. l ≤ yinj j & yinj j < i & ⬇[j] L ≡ K.ⓑ{I}W & K ⊢ ⫰(i-j) ϵ 𝐅*[yinj 0]⦃W⦄.
#L #l #x #i #H elim (frees_inv … H) -H
[ /4 width=2 by nlift_inv_lref_be_SO, or_introl/
| * #I #K #W #j #Hlj #Hji #Hnx #HLK #HW
- >(nlift_inv_lref_be_SO … Hnx) -x /3 width=5 by ex4_3_intro, or_intror/
+ lapply (nlift_inv_lref_be_SO … Hnx) -Hnx #H
+ lapply (yinj_inj … H) -H #H destruct
+ /3 width=5 by ex4_3_intro, or_intror/
]
qed-.
-lemma frees_inv_lref_free: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → |L| ≤ j → j = i.
+lemma frees_inv_lref_free: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → |L| ≤ j → yinj j = i.
#L #l #j #i #H #Hj elim (frees_inv_lref … H) -H //
* #I #K #W #_ #_ #HLK lapply (drop_fwd_length_lt2 … HLK) -I
#H elim (lt_refl_false j) /2 width=3 by lt_to_le_to_lt/
qed-.
-lemma frees_inv_lref_skip: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → yinj j < l → j = i.
+lemma frees_inv_lref_skip: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → yinj j < l → yinj j = i.
#L #l #j #i #H #Hjl elim (frees_inv_lref … H) -H //
* #I #K #W #Hlj elim (ylt_yle_false … Hlj) -Hlj //
qed-.
-lemma frees_inv_lref_ge: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → i ≤ j → j = i.
+lemma frees_inv_lref_ge: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → i ≤ j → yinj j = i.
#L #l #j #i #H #Hij elim (frees_inv_lref … H) -H //
-* #I #K #W #_ #Hji elim (lt_refl_false j) -I -L -K -W -l /2 width=3 by lt_to_le_to_lt/
+* #I #K #W #_ #Hji elim (ylt_yle_false … Hji Hij)
qed-.
lemma frees_inv_lref_lt: ∀L,l,j,i.L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → j < i →
- ∃∃I,K,W. l ≤ yinj j & ⬇[j] L ≡ K.ⓑ{I}W & K ⊢ (i-j-1) ϵ 𝐅*[yinj 0]⦃W⦄.
+ ∃∃I,K,W. l ≤ yinj j & ⬇[j] L ≡ K.ⓑ{I}W & K ⊢ ⫰(i-j) ϵ 𝐅*[yinj 0]⦃W⦄.
#L #l #j #i #H #Hji elim (frees_inv_lref … H) -H
-[ #H elim (lt_refl_false j) //
+[ #H elim (ylt_yle_false … Hji) //
| * /2 width=5 by ex3_3_intro/
]
qed-.
lemma frees_inv_bind: ∀a,I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃ⓑ{a,I}W.U⦄ →
- L ⊢ i ϵ 𝐅*[l]⦃W⦄ ∨ L.ⓑ{I}W ⊢ i+1 ϵ 𝐅*[⫯l]⦃U⦄ .
+ L ⊢ i ϵ 𝐅*[l]⦃W⦄ ∨ L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[⫯l]⦃U⦄ .
#a #J #L #V #U #l #i #H elim (frees_inv … H) -H
[ #HnX elim (nlift_inv_bind … HnX) -HnX
/4 width=2 by frees_eq, or_intror, or_introl/
| * #I #K #W #j #Hlj #Hji #HnX #HLK #HW elim (nlift_inv_bind … HnX) -HnX
[ /4 width=9 by frees_be, or_introl/
| #HnT @or_intror @(frees_be … HnT) -HnT
- [4,5,6: /2 width=1 by drop_drop, yle_succ, lt_minus_to_plus/
- |7: >minus_plus_plus_l //
+ [4: lapply (yle_succ … Hlj) // (**)
+ |5: lapply (ylt_succ … Hji) // (**)
+ |6: /2 width=4 by drop_drop/
+ |7: <yminus_succ in HW; // (**)
|*: skip
]
]
(* Basic properties *********************************************************)
lemma frees_lref_eq: ∀L,l,i. L ⊢ i ϵ 𝐅*[l]⦃#i⦄.
-/3 width=7 by frees_eq, lift_inv_lref2_be/ qed.
+/4 width=7 by frees_eq, lift_inv_lref2_be, ylt_inj/ qed.
lemma frees_lref_be: ∀I,L,K,W,l,i,j. l ≤ yinj j → j < i → ⬇[j]L ≡ K.ⓑ{I}W →
- K ⊢ i-j-1 ϵ 𝐅*[0]⦃W⦄ → L ⊢ i ϵ 𝐅*[l]⦃#j⦄.
-/3 width=9 by frees_be, lift_inv_lref2_be/ qed.
+ K ⊢ ⫰(i-j) ϵ 𝐅*[0]⦃W⦄ → L ⊢ i ϵ 𝐅*[l]⦃#j⦄.
+/4 width=9 by frees_be, lift_inv_lref2_be, ylt_inj/ qed.
lemma frees_bind_sn: ∀a,I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃W⦄ →
L ⊢ i ϵ 𝐅*[l]⦃ⓑ{a,I}W.U⦄.
/4 width=9 by frees_be, frees_eq, nlift_bind_sn/
qed.
-lemma frees_bind_dx: ∀a,I,L,W,U,l,i. L.ⓑ{I}W ⊢ i+1 ϵ 𝐅*[⫯l]⦃U⦄ →
+lemma frees_bind_dx: ∀a,I,L,W,U,l,i. L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[⫯l]⦃U⦄ →
L ⊢ i ϵ 𝐅*[l]⦃ⓑ{a,I}W.U⦄.
#a #J #L #V #U #l #i #H elim (frees_inv … H) -H
[ /4 width=9 by frees_eq, nlift_bind_dx/
-| * #I #K #W #j #Hlj #Hji #HnU #HLK #HW
- elim (yle_inv_succ1 … Hlj) -Hlj <yminus_SO2 #Hyj #H
- lapply (ylt_O … H) -H #Hj
- >(plus_minus_m_m j 1) in HnU; // <minus_le_minus_minus_comm in HW;
- /4 width=9 by frees_be, nlift_bind_dx, drop_inv_drop1_lt, lt_plus_to_minus/
+| * #I #K #W #j #Hlj elim (yle_inv_succ1 … Hlj) -Hlj #Hlj
+ #Hj <Hj >yminus_succ
+ lapply (ylt_O … Hj) -Hj #Hj #H
+ lapply (ylt_inv_succ … H) -H #Hji #HnU #HLK #HW
+ @(frees_be … Hlj Hji … HW) -HW -Hlj -Hji (**) (* explicit constructor *)
+ [2: #X #H lapply (nlift_bind_dx … H) /2 width=2 by/ (**)
+ |3: lapply (drop_inv_drop1_lt … HLK ?) -HLK //
+ |*: skip
]
qed.
(* Advanced inversion lemmas ************************************************)
lemma frees_inv_bind_O: ∀a,I,L,W,U,i. L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄ →
- L ⊢ i ϵ 𝐅*[0]⦃W⦄ ∨ L.ⓑ{I}W ⊢ i+1 ϵ 𝐅*[0]⦃U⦄ .
+ L ⊢ i ϵ 𝐅*[0]⦃W⦄ ∨ L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[0]⦃U⦄ .
#a #I #L #W #U #i #H elim (frees_inv_bind … H) -H
/3 width=3 by frees_weak, or_intror, or_introl/
qed-.
#I #L2 #K2 #U #W #l #i #j #Hlj #Hji #HnU #HLK2 #_ #IHW #Hi #L1
lapply (drop_fwd_length_minus2 … HLK2) normalize #H0
lapply (drop_O1_append_sn_le … HLK2 … L1) -HLK2
-[ -I -L1 -K2 -U -W -l /3 width=3 by lt_to_le, lt_to_le_to_lt/
+[ -I -L1 -K2 -U -W -l /4 width=3 by ylt_yle_trans, ylt_inv_inj, lt_to_le/
| #HLK2 @(frees_be … HnU HLK2) // -HnU -HLK2 @IHW -IHW
- >(minus_plus_m_m (|K2|) 1) >H0 -H0 /2 width=1 by monotonic_le_minus_l2/
+ >(minus_plus_m_m (|K2|) 1) >H0 -H0 <yminus_inj >yminus_SO2
+ /3 width=1 by monotonic_yle_minus_dx, yle_pred/
]
qed.
i ≤ |L2| → L2 ⊢ i ϵ 𝐅*[l]⦃U⦄.
#L #U #l #i #H elim H -L -U -l -i /3 width=2 by frees_eq/
#Z #L #Y #U #X #l #i #j #Hlj #Hji #HnU #HLY #_ #IHW #L1 #L2 #H #Hi destruct
-elim (drop_O1_lt (Ⓕ) L2 j) [2: -Z -Y -L1 -X -U -l /2 width=3 by lt_to_le_to_lt/ ]
+elim (drop_O1_lt (Ⓕ) L2 j) [2: -Z -Y -L1 -X -U -l /3 width=3 by ylt_yle_trans, ylt_inv_inj/ ]
#I #K2 #W #HLK2 lapply (drop_fwd_length_minus2 … HLK2) normalize #H0
lapply (drop_O1_inv_append1_le … HLY … HLK2) -HLY
-[ -Z -I -Y -K2 -L1 -X -U -W -l /3 width=3 by lt_to_le, lt_to_le_to_lt/
+[ -Z -I -Y -K2 -L1 -X -U -W -l /4 width=3 by ylt_yle_trans, ylt_inv_inj, lt_to_le/
| normalize #H destruct
@(frees_be … HnU HLK2) -HnU -HLK2 // @IHW -IHW //
- >(minus_plus_m_m (|K2|) 1) >H0 -H0 /2 width=1 by monotonic_le_minus_l2/
+ >(minus_plus_m_m (|K2|) 1) >H0 -H0 <yminus_inj >yminus_SO2
+ /3 width=1 by monotonic_yle_minus_dx, yle_pred/
]
qed-.
(* *)
(**************************************************************************)
+include "ground_2/ynat/ynat_max.ma".
include "basic_2/substitution/drop_drop.ma".
include "basic_2/multiple/frees.ma".
#L #U @(f2_ind … rfw … L U) -L -U
#x #IH #L * *
[ -IH /3 width=5 by frees_inv_sort, or_intror/
-| #j #Hx #l #i elim (lt_or_eq_or_gt i j) #Hji
- [ -x @or_intror #H elim (lt_refl_false i)
- lapply (frees_inv_lref_ge … H ?) -L -l /2 width=1 by lt_to_le/
+| #j #Hx #l #i elim (ylt_split_eq i j) #Hji
+ [ -x @or_intror #H elim (ylt_yle_false … Hji)
+ lapply (frees_inv_lref_ge … H ?) -L -l /2 width=1 by ylt_fwd_le/
| -x /2 width=1 by or_introl/
| elim (ylt_split j l) #Hli
- [ -x @or_intror #H elim (lt_refl_false i)
+ [ -x @or_intror #H elim (ylt_yle_false … Hji)
lapply (frees_inv_lref_skip … H ?) -L //
| elim (lt_or_ge j (|L|)) #Hj
[ elim (drop_O1_lt (Ⓕ) L j) // -Hj #I #K #W #HLK destruct
elim (IH K W … 0 (i-j-1)) -IH [1,3: /3 width=5 by frees_lref_be, drop_fwd_rfw, or_introl/ ] #HnW
@or_intror #H elim (frees_inv_lref_lt … H) // #Z #Y #X #_ #HLY -l
lapply (drop_mono … HLY … HLK) -L #H destruct /2 width=1 by/
- | -x @or_intror #H elim (lt_refl_false i)
+ | -x @or_intror #H elim (ylt_yle_false … Hji)
lapply (frees_inv_lref_free … H ?) -l //
]
]
qed-.
lemma frees_S: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[yinj l]⦃U⦄ → ∀I,K,W. ⬇[l] L ≡ K.ⓑ{I}W →
- (K ⊢ i-l-1 ϵ 𝐅*[0]⦃W⦄ → ⊥) → L ⊢ i ϵ 𝐅*[⫯l]⦃U⦄.
+ (K ⊢ ⫰(i-l) ϵ 𝐅*[0]⦃W⦄ → ⊥) → L ⊢ i ϵ 𝐅*[⫯l]⦃U⦄.
#L #U #l #i #H elim (frees_inv … H) -H /3 width=2 by frees_eq/
* #I #K #W #j #Hlj #Hji #HnU #HLK #HW #I0 #K0 #W0 #HLK0 #HnW0
lapply (yle_inv_inj … Hlj) -Hlj #Hlj
qed.
(* Note: lemma 1250 *)
-lemma frees_bind_dx_O: ∀a,I,L,W,U,i. L.ⓑ{I}W ⊢ i+1 ϵ 𝐅*[0]⦃U⦄ →
+lemma frees_bind_dx_O: ∀a,I,L,W,U,i. L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[0]⦃U⦄ →
L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄.
#a #I #L #W #U #i #HU elim (frees_dec L W 0 i)
/4 width=5 by frees_S, frees_bind_dx, frees_bind_sn/
[ #K #T #l #i #HnT #L #s #l0 #m0 #_ #U #HTU #Hl0i -K -s
@frees_eq #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
| #I #K #K0 #T #V #l #i #j #Hlj #Hji #HnT #HK0 #HV #IHV #L #s #l0 #m0 #HLK #U #HTU #Hl0i
- elim (lt_or_ge j l0) #H1
- [ elim (drop_trans_lt … HLK … HK0) // -K #L0 #W #HL0 #HLK0 #HVW
- @(frees_be … HL0) -HL0 -HV
- /3 width=3 by lt_plus_to_minus_r, lt_to_le_to_lt/
- [ #X #HXU >(plus_minus_m_m l0 1) in HTU; /2 width=2 by ltn_to_ltO/ #HTU
- elim (lift_div_le … HXU … HTU ?) -U /2 width=2 by monotonic_pred/
- | >minus_plus <plus_minus // <minus_plus
- /3 width=5 by monotonic_le_minus_l2/
+ elim (ylt_split j l0) #H0
+ [ elim (drop_trans_lt … HLK … HK0) // -K #L0 #W #HL0 >yminus_SO2 #HLK0 #HVW
+ @(frees_be … HL0) -HL0 -HV /3 width=3 by ylt_plus_dx2_trans/
+ [ lapply (ylt_fwd_lt_O1 … H0) #H1
+ #X #HXU <(ymax_pre_sn l0 1) in HTU; /2 width=1 by ylt_fwd_le_succ1/ #HTU
+ <(ylt_inv_O1 l0) in H0; // -H1 #H0
+ elim (lift_div_le … HXU … HTU ?) -U /2 width=2 by ylt_fwd_succ2/
+ | >yplus_minus_comm_inj /2 width=1 by ylt_fwd_le/
+ <yplus_pred1 /4 width=5 by monotonic_yle_minus_dx, yle_pred, ylt_to_minus/
]
| lapply (drop_trans_ge … HLK … HK0 ?) // -K #HLK0
lapply (drop_inv_gen … HLK0) >commutative_plus -HLK0 #HLK0
@(frees_be … HLK0) -HLK0 -IHV
- /2 width=1 by yle_plus_dx1_trans, lt_minus_to_plus/
- #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
+ /2 width=1 by monotonic_ylt_plus_dx, yle_plus_dx1_trans/
+ [ #X <yplus_inj #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
+ | <yplus_minus_assoc_comm_inj //
+ ]
]
]
qed.
[ #L #U #l #i #HnU #K #s #l0 #m0 #_ #T #HTU #Hl0i #Hilm0
elim (lift_split … HTU i m0) -HTU /2 width=2 by/
| #I #L #K0 #U #W #l #i #j #Hli #Hij #HnU #HLK0 #_ #IHW #K #s #l0 #m0 #HLK #T #HTU #Hl0i #Hilm0
- elim (lt_or_ge j l0) #H1
+ elim (ylt_split j l0) #H1
[ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
@(IHW … HKL0 … HVW)
- [ /2 width=1 by monotonic_le_minus_l2/
- | >minus_plus >minus_plus >plus_minus /2 width=1 by monotonic_le_minus_l/
+ [ /3 width=1 by monotonic_yle_minus_dx, yle_pred/
+ | >yplus_pred1 /2 width=1 by ylt_to_minus/
+ <yplus_minus_comm_inj /3 width=1 by monotonic_yle_minus_dx, yle_pred, ylt_fwd_le/
]
- | elim (lift_split … HTU j m0) -HTU /3 width=3 by lt_to_le_to_lt, lt_to_le/
+ | elim (lift_split … HTU j m0) -HTU /3 width=3 by ylt_yle_trans, ylt_fwd_le/
]
]
qed-.
K ⊢ i-m0 ϵ𝐅*[l-yinj m0]⦃T⦄.
#L #U #l #i #H elim H -L -U -l -i
[ #L #U #l #i #HnU #K #s #l0 #m0 #HLK #T #HTU #Hlm0i -L -s
- elim (le_inv_plus_l … Hlm0i) -Hlm0i #Hl0im0 #Hm0i @frees_eq #X #HXT -K
- elim (lift_trans_le … HXT … HTU) -T // <plus_minus_m_m /2 width=2 by/
+ elim (yle_inv_plus_inj2 … Hlm0i) -Hlm0i #Hl0im0 #Hm0i @frees_eq #X #HXT -K
+ elim (lift_trans_le … HXT … HTU) -T // >ymax_pre_sn /2 width=2 by/
| #I #L #K0 #U #W #l #i #j #Hli #Hij #HnU #HLK0 #_ #IHW #K #s #l0 #m0 #HLK #T #HTU #Hlm0i
- elim (lt_or_ge j l0) #H1
+ elim (ylt_split j l0) #H1
[ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
- elim (le_inv_plus_l … Hlm0i) #H0 #Hm0i
+ elim (yle_inv_plus_inj2 … Hlm0i) #H0 #Hm0i
@(frees_be … H) -H
[ /3 width=1 by yle_plus_dx1_trans, monotonic_yle_minus_dx/
- | /2 width=3 by lt_to_le_to_lt/
- | #X #HXT elim (lift_trans_ge … HXT … HTU) -T /2 width=2 by/
+ | /2 width=3 by ylt_yle_trans/
+ | #X #HXT elim (lift_trans_ge … HXT … HTU) -T /2 width=2 by ylt_fwd_le_succ1/
| lapply (IHW … HKL0 … HVW ?) // -I -K -K0 -L0 -V -W -T -U -s
- >minus_plus >minus_plus >plus_minus /2 width=1 by monotonic_le_minus_l/
+ >yplus_pred1 /2 width=1 by ylt_to_minus/
+ <yplus_minus_comm_inj /3 width=1 by monotonic_yle_minus_dx, yle_pred, ylt_fwd_le/
]
- | elim (lt_or_ge j (l0+m0)) [ >commutative_plus |] #H2
- [ -L -I -W lapply (lt_plus_to_minus ???? H2) // -H2 #H2
- elim (lift_split … HTU j (m0-1)) -HTU //
- [ >minus_minus_associative /2 width=2 by ltn_to_ltO/ <minus_n_n
- #X #_ #H elim (HnU … H)
- | >commutative_plus /3 width=1 by le_minus_to_plus, monotonic_pred/
+ | elim (ylt_split j (l0+m0)) #H2
+ [ -L -I -W elim (yle_inv_inj2 … H1) -H1 #x #H1 #H destruct
+ lapply (ylt_plus2_to_minus_inj1 … H2) /2 width=1 by yle_inj/ #H3
+ lapply (ylt_fwd_lt_O1 … H3) -H3 #H3
+ elim (lift_split … HTU j (m0-1)) -HTU /2 width=1 by yle_inj/
+ [ >minus_minus_associative /2 width=1 by ylt_inv_inj/ <minus_n_n
+ -H2 #X #_ #H elim (HnU … H)
+ | <yminus_inj >yminus_SO2 >yplus_pred2 /2 width=1 by ylt_fwd_le_pred2/
]
| lapply (drop_conf_ge … HLK … HLK0 ?) // -L #HK0
- elim (le_inv_plus_l … H2) -H2 #H2 #Hm0j
+ elim ( yle_inv_plus_inj2 … H2) -H2 #H2 #Hm0j
@(frees_be … HK0)
[ /2 width=1 by monotonic_yle_minus_dx/
- | /2 width=1 by monotonic_lt_minus_l/
- | #X #HXT elim (lift_trans_le … HXT … HTU) -T // <plus_minus_m_m /2 width=2 by/
- | >arith_b1 /2 width=5 by/
+ | /2 width=1 by monotonic_ylt_minus_dx/
+ | #X #HXT elim (lift_trans_le … HXT … HTU) -T //
+ <yminus_inj >ymax_pre_sn /2 width=2 by/
+ | <yminus_inj >yplus_minus_assoc_comm_inj //
+ >ymax_pre_sn /3 width=5 by yle_trans, ylt_fwd_le/
]
]
]
(* GENERIC TERM RELOCATION **************************************************)
-inductive lifts: list2 nat nat → relation term ≝
+inductive lifts: list2 ynat nat → relation term ≝
| lifts_nil : ∀T. lifts (◊) T T
| lifts_cons: ∀T1,T,T2,cs,l,m.
⬆[l,m] T1 ≡ T → lifts cs T T2 → lifts ({l, m} @ cs) T1 T2
(* *)
(**************************************************************************)
+include "ground_2/ynat/ynat_max.ma".
include "basic_2/substitution/lift_lift.ma".
include "basic_2/multiple/mr2_minus.ma".
include "basic_2/multiple/lifts.ma".
∀T1,T0. ⬆*[cs0] T1 ≡ T0 →
∀T2. ⬆[O, i0 + 1] T0 ≡ T2 →
∃∃T. ⬆[0, i + 1] T1 ≡ T & ⬆*[cs] T ≡ T2.
-#cs elim cs -cs normalize
+#cs elim cs -cs
[ #i #x #H1 #cs0 #H2 #T1 #T0 #HT10 #T2
<(at_inv_nil … H1) -x #HT02
lapply (minuss_inv_nil1 … H2) -H2 #H
>(lifts_inv_nil … H) -T1 /2 width=3 by lifts_nil, ex2_intro/
| #l #m #cs #IHcs #i #i0 #H1 #cs0 #H2 #T1 #T0 #HT10 #T2 #HT02
elim (at_inv_cons … H1) -H1 * #Hil #Hi0
- [ elim (minuss_inv_cons1_lt … H2) -H2 [2: /2 width=1 by lt_minus_to_plus/ ] #cs1 #Hcs1 <minus_le_minus_minus_comm // <minus_plus_m_m #H
+ [ elim (minuss_inv_cons1_lt … H2) -H2 /2 width=1 by ylt_succ/ #cs1 #Hcs1
+ <yplus_inj >yplus_SO2 >yplus_SO2 >yminus_succ #H
elim (pluss_inv_cons2 … H) -H #cs2 #H1 #H2 destruct
- elim (lifts_inv_cons … HT10) -HT10 #T >minus_plus #HT1 #HT0
+ elim (lifts_inv_cons … HT10) -HT10 #T #HT1 #HT0
elim (IHcs … Hi0 … Hcs1 … HT0 … HT02) -IHcs -Hi0 -Hcs1 -T0 #T0 #HT0 #HT02
- elim (lift_trans_le … HT1 … HT0) -T /2 width=1 by/ #T #HT1 <plus_minus_m_m /3 width=5 by lifts_cons, ex2_intro/
+ elim (lift_trans_le … HT1 … HT0) -T /2 width=1 by/ #T #HT1
+ <yminus_plus2 <yplus_inj >yplus_SO2 >ymax_pre_sn
+ /3 width=5 by lifts_cons, ex2_intro, ylt_fwd_le_succ1/
| >commutative_plus in Hi0; #Hi0
- lapply (minuss_inv_cons1_ge … H2 ?) -H2
[ /2 width=1 by le_S_S/ ] <associative_plus #Hcs0
+ lapply (minuss_inv_cons1_ge … H2 ?) -H2
/2 width=1 by yle_succ/ <associative_plus #Hcs0
elim (IHcs … Hi0 … Hcs0 … HT10 … HT02) -IHcs -Hi0 -Hcs0 -T0 #T0 #HT0 #HT02
- elim (lift_split … HT0 l (i+1)) -HT0 /3 width=5 by lifts_cons, le_S, ex2_intro/
+ elim (lift_split … HT0 l (i+1)) -HT0 /3 width=5 by lifts_cons, yle_succ, yle_pred_sn, ex2_intro/
]
]
qed-.
(* GENERIC TERM VECTOR RELOCATION *******************************************)
-inductive liftsv (cs:list2 nat nat) : relation (list term) ≝
+inductive liftsv (cs:list2 ynat nat) : relation (list term) ≝
| liftsv_nil : liftsv cs (◊) (◊)
| liftsv_cons: ∀T1s,T2s,T1,T2.
⬆*[cs] T1 ≡ T2 → liftsv cs T1s T2s →
lemma lleq_inv_lift_be: ∀L1,L2,U,lt. L1 ≡[U, lt] L2 →
∀K1,K2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 →
- ∀T. ⬆[l, m] T ≡ U → l ≤ lt → lt ≤ yinj l + m → K1 ≡[T, l] K2.
+ ∀T. ⬆[l, m] T ≡ U → l ≤ lt → lt ≤ l + m → K1 ≡[T, l] K2.
/2 width=11 by llpx_sn_inv_lift_be/ qed-.
lemma lleq_inv_lift_ge: ∀L1,L2,U,lt. L1 ≡[U, lt] L2 →
∀K1,K2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 →
- ∀T. ⬆[l, m] T ≡ U → yinj l + m ≤ lt → K1 ≡[T, lt-m] K2.
+ ∀T. ⬆[l, m] T ≡ U → l + m ≤ lt → K1 ≡[T, lt-m] K2.
/2 width=9 by llpx_sn_inv_lift_ge/ qed-.
(* Inversion lemmas on negated lazy quivalence for local environments *******)
lapply (drop_O1_inv_append1_le … HLK … HLY) /2 width=1 by lt_to_le/ -HLK normalize #H destruct
elim (IH … HLY1 HLY2 HLY) -IH -HLY1 -HLY2 -HLY *
[ /3 width=1 by and3_intro, or3_intro0/
- | /6 width=2 by frees_inv_append, lt_to_le, or3_intro1, and3_intro/
- | /5 width=1 by frees_append, lt_to_le, or3_intro2, and4_intro/
+ | /7 width=2 by frees_inv_append, yle_inj, lt_to_le, or3_intro1, and3_intro/
+ | /6 width=1 by frees_append, yle_inj, lt_to_le, or3_intro2, and4_intro/
]
| -IH -HLK1 destruct
lapply (drop_O1_inv_append1_le … HLK2 … (⋆) ?) // -HLK2 normalize #H destruct
lapply (drop_O1_inv_append1_le … HLK … HLY) /2 width=1 by lt_to_le/ -HLK normalize #H destruct
elim (IH … HLY1 HLY2 HLY) -IH -HLY1 -HLY2 -HLY *
[ /3 width=1 by and3_intro, or3_intro0/
- | /6 width=2 by frees_inv_append, lt_to_le, or3_intro1, and3_intro/
- | /5 width=1 by frees_append, lt_to_le, or3_intro2, and4_intro/
+ | /7 width=2 by frees_inv_append, yle_inj, lt_to_le, or3_intro1, and3_intro/
+ | /6 width=1 by frees_append, yle_inj, lt_to_le, or3_intro2, and4_intro/
]
| -IH -HLK2 destruct
lapply (drop_O1_inv_append1_le … HLK1 … (⋆) ?) // -HLK1 normalize #H destruct
[ lapply (llpx_sn_fwd_length … HW1) -HW1 #HK12
lapply (drop_fwd_length … HLK1) lapply (drop_fwd_length … HLK2)
normalize in ⊢ (%→%→?); -I -W1 -W2 -lt /3 width=1 by llpx_sn_skip, ylt_inj/
- | /4 width=9 by llpx_sn_lref, yle_inj, le_plus_b/
+ | /3 width=9 by llpx_sn_lref, yle_fwd_plus_sn1/
]
| /2 width=1 by llpx_sn_free/
| #L1 #L2 #lt #p #HL12 #X #l #m #H #_ >(lift_inv_gref2 … H) -H /2 width=1 by llpx_sn_gref/
| #a #I #L1 #L2 #W #U #lt #_ #_ #IHV #IHT #X #l #m #H #Hltlm destruct
- elim (lift_inv_bind2 … H) -H #V #T #HVW >commutative_plus #HTU #H destruct
+ elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct
@(llpx_sn_bind) /2 width=4 by/ (**) (* full auto fails *)
@(IHT … HTU) /2 width=1 by yle_succ/
| #I #L1 #L2 #W #U #lt #_ #_ #IHV #IHT #X #l #m #H #Hltlm destruct
#HL12 #IHU @conj //
#I1 #I2 #K1 #K2 #V1 #V2 #i #Hli #H #HLK1 #HLK2 elim (frees_inv … H) -H
[ -x #HnU elim (IHU … HnU HLK1 HLK2) -IHU -HnU -HLK1 -HLK2 /2 width=1 by conj/
-| * #J1 #K10 #W10 #j #Hlj #Hji #HnU #HLK10 #HnW10 destruct
+| * #J1 #K10 #W10 #j #Hlj #Hji #HnU #HLK10 <yminus_SO2 >yminus_inj >yminus_inj #HnW10 destruct
lapply (drop_fwd_drop2 … HLK10) #H
- lapply (drop_conf_ge … H … HLK1 ?) -H /2 width=1 by lt_to_le/ <minus_plus #HK10
+ lapply (drop_conf_ge … H … HLK1 ?) -H /2 width=1 by ylt_fwd_le_succ1/ <minus_plus #HK10
elim (drop_O1_lt (Ⓕ) L2 j) [2: <HL12 /2 width=5 by drop_fwd_length_lt2/ ] #J2 #K20 #W20 #HLK20
lapply (drop_fwd_drop2 … HLK20) #H
- lapply (drop_conf_ge … H … HLK2 ?) -H /2 width=1 by lt_to_le/ <minus_plus #HK20
- elim (IHx K10 W10 … K20 0) -IHx -HL12 /3 width=6 by drop_fwd_rfw/
- elim (IHU … HnU HLK10 HLK20) -IHU -HnU -HLK10 -HLK20 //
+ lapply (drop_conf_ge … H … HLK2 ?) -H /2 width=1 by ylt_fwd_le_succ1/ <minus_plus #HK20
+ elim (IHx K10 W10 … K20 0 ?) -IHx -HL12 /3 width=6 by drop_fwd_rfw/
+ elim (IHU … HnU HLK10 HLK20) -IHU -HnU -HLK10 -HLK20 /2 width=6 by/
]
qed.
@conj [ @(drop_fwd_length_eq1 … H1 H2) // ] -HL12
#Z1 #Z2 #Y1 #Y2 #X1 #X2 #j #_
>(minus_plus_m_m j (i+1)) in ⊢ (%→?); >commutative_plus <minus_plus
+<yminus_inj <yminus_inj >yminus_SO2
#HnV1 #HKY1 #HKY2 (**) (* full auto too slow *)
lapply (drop_trans_ge … H1 … HKY1 ?) -H1 -HKY1 // #HLY1
lapply (drop_trans_ge … H2 … HKY2 ?) -H2 -HKY2 // #HLY2
-/4 width=14 by frees_be, yle_plus_dx2_trans, yle_succ_dx/
+/4 width=9 by frees_be, yle_plus_dx2_trans, yle_succ_dx, ylt_inj/
qed-.
#I1 #I2 #K1 #K2 #V1 #V2 #i #Hli #H #HLK1 #HLK2
[ elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2
/3 width=9 by nlift_bind_sn, and3_intro/
-| lapply (yle_inv_succ1 … Hli) -Hli * #Hli #Hi
+| lapply (yle_inv_succ1 … Hli) -Hli * #Hli #Hi <yminus_SO2 in Hli; #Hli
lapply (drop_inv_drop1_lt … HLK1 ?) -HLK1 /2 width=1 by ylt_O/ #HLK1
lapply (drop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/ #HLK2
- elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 /2 width=1 by and3_intro/
- @nlift_bind_dx <plus_minus_m_m /2 width=2 by ylt_O/
+ elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 /3 width=9 by nlift_bind_dx, and3_intro/
]
qed-.
#R #L1 #L2 #l #i #HL1 #_ #HL12 @llpx_sn_alt_r_intro_alt // -HL12
#I1 #I2 #K1 #K2 #V1 #V2 #j #_ #H #HLK1 elim (H (#(i-1))) -H
lapply (drop_fwd_length_lt2 … HLK1) -HLK1
-/3 width=3 by lift_lref_ge_minus, lt_to_le_to_lt/
+/4 width=3 by lift_lref_ge_minus, yle_inj, transitive_le/
qed.
lemma llpx_sn_alt_r_lref: ∀R,I,L1,L2,K1,K2,V1,V2,l,i. l ≤ yinj i →
@(drop_fwd_length_eq2 … HLK1 HLK2) normalize //
| #Z1 #Z2 #Y1 #Y2 #X1 #X2 #j #Hlj #H #HLY1 #HLY2
elim (lt_or_eq_or_gt i j) #Hij destruct
- [ elim (H (#i)) -H /2 width=1 by lift_lref_lt/
+ [ elim (H (#i)) -H /3 width=1 by lift_lref_lt, ylt_inj/
| lapply (drop_mono … HLY1 … HLK1) -HLY1 -HLK1 #H destruct
lapply (drop_mono … HLY2 … HLK2) -HLY2 -HLK2 #H destruct /2 width=1 by and3_intro/
- | elim (H (#(i-1))) -H /2 width=1 by lift_lref_ge_minus/
+ | elim (H (#(i-1))) -H /3 width=1 by lift_lref_ge_minus, yle_inj/
]
]
qed.
/3 width=10 by llpx_sn_lref/
| lapply (drop_conf_ge … HLK1 … HLK11 ?) // -L1
lapply (drop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hil0
- elim (le_inv_plus_l … Hil) -Hil /4 width=9 by llpx_sn_lref, yle_trans, yle_inj/ (**) (* slow *)
+ elim (yle_inv_plus_inj2 … Hil) -Hil /4 width=9 by llpx_sn_lref, yle_trans, yle_inj/ (**) (* slow *)
]
| #L1 #L2 #l0 #i #HL1 #HL2 #HL12 #K1 #K2 #l #m #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_lref2 … H) -H
* #_ #H destruct
lemma llpx_sn_inv_lift_be: ∀R,L1,L2,U,l0. llpx_sn R l0 U L1 L2 →
∀K1,K2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 →
- ∀T. ⬆[l, m] T ≡ U → l ≤ l0 → l0 ≤ yinj l + m → llpx_sn R l T K1 K2.
+ ∀T. ⬆[l, m] T ≡ U → l ≤ l0 → l0 ≤ l + m → llpx_sn R l T K1 K2.
#R #L1 #L2 #U #l0 #H elim H -L1 -L2 -U -l0
[ #L1 #L2 #l0 #k #HL12 #K1 #K2 #l #m #HLK1 #HLK2 #X #H #_ #_ >(lift_inv_sort2 … H) -X
lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l0 -m
/3 width=3 by ylt_yle_trans, ylt_inj/
| lapply (drop_conf_ge … HLK1 … HLK11 ?) // -L1
lapply (drop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hil0 -Hl0 -Hl0m
- elim (le_inv_plus_l … Hil) -Hil /3 width=9 by llpx_sn_lref, yle_inj/
+ elim (yle_inv_plus_inj2 … Hil) -Hil /3 width=9 by llpx_sn_lref, yle_inj/
]
| #L1 #L2 #l0 #i #HL1 #HL2 #HL12 #K1 #K2 #l #m #HLK1 #HLK2 #X #H #Hl0 #Hl0m elim (lift_inv_lref2 … H) -H
* #_ #H destruct
lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l0 -m
/2 width=1 by llpx_sn_gref/
| #a #I #L1 #L2 #W #U #l0 #_ #_ #IHW #IHU #K1 #K2 #l #m #HLK1 #HLK2 #X #H #Hl0 #Hl0m elim (lift_inv_bind2 … H) -H
- >commutative_plus #V #T #HVW #HTU #H destruct
+ #V #T #HVW #HTU #H destruct
@llpx_sn_bind [ /2 width=5 by/ ] -IHW (**) (* explicit constructor *)
@(IHU … HTU) -IHU -HTU /2 width=1 by drop_skip, yle_succ/
| #I #L1 #L2 #W #U #l0 #_ #_ #IHW #IHU #K1 #K2 #l #m #HLK1 #HLK2 #X #H #Hl0 #Hl0m elim (lift_inv_flat2 … H) -H
lemma llpx_sn_inv_lift_ge: ∀R,L1,L2,U,l0. llpx_sn R l0 U L1 L2 →
∀K1,K2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 →
- ∀T. ⬆[l, m] T ≡ U → yinj l + m ≤ l0 → llpx_sn R (l0-m) T K1 K2.
+ ∀T. ⬆[l, m] T ≡ U → l + m ≤ l0 → llpx_sn R (l0-m) T K1 K2.
#R #L1 #L2 #U #l0 #H elim H -L1 -L2 -U -l0
[ #L1 #L2 #l0 #k #HL12 #K1 #K2 #l #m #HLK1 #HLK2 #X #H #_ >(lift_inv_sort2 … H) -X
lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l
* #Hil #H destruct [ -Hil0 | -Hlml0 ]
lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2
[ /4 width=3 by llpx_sn_skip, yle_plus1_to_minus_inj2, ylt_yle_trans, ylt_inj/
- | elim (le_inv_plus_l … Hil) -Hil #_
- /4 width=1 by llpx_sn_skip, monotonic_ylt_minus_dx, yle_inj/
+ | elim (yle_inv_plus_inj2 … Hil) -Hil
+ /3 width=1 by llpx_sn_skip, monotonic_ylt_minus_dx/
]
| #I #L1 #L2 #K11 #K22 #W1 #W2 #l0 #i #Hil0 #HLK11 #HLK22 #HK12 #HW12 #_ #K1 #K2 #l #m #HLK1 #HLK2 #X #H #Hlml0 elim (lift_inv_lref2 … H) -H
* #Hil #H destruct
(* *)
(**************************************************************************)
+include "ground_2/ynat/ynat_lt.ma".
include "basic_2/notation/relations/rat_3.ma".
include "basic_2/grammar/term_vector.ma".
(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
-inductive at: list2 nat nat → relation nat ≝
+inductive at: list2 ynat nat → relation nat ≝
| at_nil: ∀i. at (◊) i i
-| at_lt : ∀cs,l,m,i1,i2. i1 < l →
+| at_lt : ∀cs,l,m,i1,i2. yinj i1 < l →
at cs i1 i2 → at ({l, m} @ cs) i1 i2
-| at_ge : ∀cs,l,m,i1,i2. l ≤ i1 →
+| at_ge : ∀cs,l,m,i1,i2. l ≤ yinj i1 →
at cs (i1 + m) i2 → at ({l, m} @ cs) i1 i2
.
i1 < l → @⦃i1, cs⦄ ≡ i2.
#cs #l #m #i1 #m2 #H
elim (at_inv_cons … H) -H * // #Hli1 #_ #Hi1l
-lapply (le_to_lt_to_lt … Hli1 Hi1l) -Hli1 -Hi1l #Hl
-elim (lt_refl_false … Hl)
+elim (ylt_yle_false … Hi1l Hli1)
qed-.
lemma at_inv_cons_ge: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 →
l ≤ i1 → @⦃i1 + m, cs⦄ ≡ i2.
#cs #l #m #i1 #m2 #H
elim (at_inv_cons … H) -H * // #Hi1l #_ #Hli1
-lapply (le_to_lt_to_lt … Hli1 Hi1l) -Hli1 -Hi1l #Hl
-elim (lt_refl_false … Hl)
+elim (ylt_yle_false … Hi1l Hli1)
qed-.
(* *)
(**************************************************************************)
+include "ground_2/ynat/ynat_minus.ma".
include "basic_2/notation/relations/rminus_3.ma".
include "basic_2/multiple/mr2.ma".
(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
-inductive minuss: nat → relation (list2 nat nat) ≝
+inductive minuss: nat → relation (list2 ynat nat) ≝
| minuss_nil: ∀i. minuss i (◊) (◊)
-| minuss_lt : ∀cs1,cs2,l,m,i. i < l → minuss i cs1 cs2 →
+| minuss_lt : ∀cs1,cs2,l,m,i. yinj i < l → minuss i cs1 cs2 →
minuss i ({l, m} @ cs1) ({l - i, m} @ cs2)
-| minuss_ge : ∀cs1,cs2,l,m,i. l ≤ i → minuss (m + i) cs1 cs2 →
+| minuss_ge : ∀cs1,cs2,l,m,i. l ≤ yinj i → minuss (m + i) cs1 cs2 →
minuss i ({l, m} @ cs1) cs2
.
l ≤ i → cs1 ▭ m + i ≡ cs2.
#cs1 #cs2 #l #m #i #H
elim (minuss_inv_cons1 … H) -H * // #cs #Hil #_ #_ #Hli
-lapply (lt_to_le_to_lt … Hil Hli) -Hil -Hli #Hi
-elim (lt_refl_false … Hi)
+elim (ylt_yle_false … Hil Hli)
qed-.
lemma minuss_inv_cons1_lt: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 →
i < l →
∃∃cs. cs1 ▭ i ≡ cs & cs2 = {l - i, m} @ cs.
#cs1 #cs2 #l #m #i #H elim (minuss_inv_cons1 … H) -H * /2 width=3 by ex2_intro/
-#Hli #_ #Hil lapply (lt_to_le_to_lt … Hil Hli) -Hil -Hli
-#Hi elim (lt_refl_false … Hi)
+#Hli #_ #Hil elim (ylt_yle_false … Hil Hli)
qed-.
(* *)
(**************************************************************************)
+include "ground_2/ynat/ynat_plus.ma".
include "basic_2/multiple/mr2.ma".
(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
-let rec pluss (cs:list2 nat nat) (i:nat) on cs ≝ match cs with
+let rec pluss (cs:list2 ynat nat) (i:nat) on cs ≝ match cs with
[ nil2 ⇒ ◊
| cons2 l m cs ⇒ {l + i, m} @ pluss cs i
].
interpretation "plus (multiple relocation with pairs)"
'plus x y = (pluss x y).
+(* Basic properties *********************************************************)
+
+lemma pluss_SO2: ∀l,m,cs. ({l, m} @ cs) + 1 = {⫯l, m} @ cs + 1.
+// qed.
+
(* Basic inversion lemmas ***************************************************)
lemma pluss_inv_nil2: ∀i,cs. cs + i = ◊ → cs = ◊.
lemma pluss_inv_cons2: ∀i,l,m,cs2,cs. cs + i = {l, m} @ cs2 →
∃∃cs1. cs1 + i = cs2 & cs = {l - i, m} @ cs1.
-#i #l #m #cs2 * normalize
-[ #H destruct
-| #l1 #m1 #cs1 #H destruct /2 width=3 by ex2_intro/
+#i #l #m #cs2 *
+[ normalize #H destruct
+| #l1 #m1 #cs1 whd in ⊢ (??%?→?); #H destruct
+ >yplus_minus_inj /2 width=3 by ex2_intro/
]
qed-.
#G #L #K #V #i #HLK #H
elim (lift_total V 0 (i+1)) #W #HVW
lapply (H W ?) -H [ /3 width=6 by cpr_delta/ ] -HLK #H destruct
-elim (lift_inv_lref2_be … HVW) -HVW //
+elim (lift_inv_lref2_be … HVW) -HVW /2 width=1 by ylt_inj/
qed-.
lemma cnr_inv_abst: ∀a,G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓛ{a}V.T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃V⦄ ∧ ⦃G, L.ⓛV⦄ ⊢ ➡ 𝐍⦃T⦄.
#h #g #I #G #L #K #V #i #HLK #H
elim (lift_total V 0 (i+1)) #W #HVW
lapply (H W ?) -H [ /3 width=7 by cpx_delta/ ] -HLK #H destruct
-elim (lift_inv_lref2_be … HVW) -HVW //
+elim (lift_inv_lref2_be … HVW) -HVW /2 width=1 by ylt_inj/
qed-.
lemma cnx_inv_abst: ∀h,g,a,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃ⓛ{a}V.T⦄ →
#G #K #V #T1 elim T1 -T1
[ * /2 width=4 by cpr_atom, lift_sort, lift_gref, ex2_2_intro/
#i #L #l #HLK elim (lt_or_eq_or_gt i l)
- #Hil [1,3: /3 width=4 by cpr_atom, lift_lref_ge_minus, lift_lref_lt, ex2_2_intro/ ]
+ #Hil [1,3: /4 width=4 by lift_lref_ge_minus, lift_lref_lt, ylt_inj, yle_inj, ex2_2_intro/ ]
destruct
elim (lift_total V 0 (i+1)) #W #HVW
elim (lift_split … HVW i i) /3 width=6 by cpr_delta, ex2_2_intro/
d = 0 → ⦃G, L⦄ ⊢ T1 ➡ T2.
#h #G #L #T1 #T2 #d #H elim H -G -L -T1 -T2 -d
/3 width=1 by cpr_eps, cpr_flat, cpr_bind/
-[ #G #L #d #k #H0 destruct normalize //
-| #G #L #K #V1 #V2 #W2 #i #d #HLK #_ #HVW2 #IHV12 #H destruct
+[ #G #L #K #V1 #V2 #W2 #i #d #HLK #_ #HVW2 #IHV12 #H destruct
/3 width=6 by cpr_delta/
| #G #L #K #V1 #V2 #W2 #i #d #_ #_ #_ #_ <plus_n_Sm #H destruct
]
(* *)
(**************************************************************************)
+include "ground_2/ynat/ynat_max.ma".
include "basic_2/substitution/drop_drop.ma".
include "basic_2/reduction/cpr.ma".
>(lift_mono … H1 … H2) -H1 -H2 //
| #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #s #l #m #HLK #U1 #H #U2 #HWU2
elim (lift_inv_lref1 … H) * #Hil #H destruct
- [ elim (lift_trans_ge … HVW2 … HWU2) -W2 // <minus_plus #W2 #HVW2 #HWU2
- elim (drop_trans_le … HLK … HKV) -K /2 width=2 by lt_to_le/ #X #HLK #H
- elim (drop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hil
+ [ elim (lift_trans_ge … HVW2 … HWU2) -W2 /2 width=1 by ylt_fwd_le_succ1/ #W2 #HVW2 #HWU2
+ elim (drop_trans_le … HLK … HKV) -K /2 width=2 by ylt_fwd_le/ #X #HLK #H
+ elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil
#K #Y #HKV #HVY #H destruct /3 width=9 by cpr_delta/
- | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 /2 width=1 by le_S/ >plus_plus_comm_23 #HVU2
+ | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 /2 width=1 by yle_succ_dx/ >plus_plus_comm_23 #HVU2
lapply (drop_trans_ge_comm … HLK … HKV ?) -K // -Hil /3 width=6 by cpr_delta, drop_inv_gen/
]
| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #s #l #m #HLK #U1 #H1 #U2 #H2
elim (lift_inv_lref2 … H) -H * #Hil #H destruct
[ elim (drop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV
elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2
- elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus <plus_minus_m_m /3 width=8 by cpr_delta, ex2_intro/
- | elim (le_inv_plus_l … Hil) #Hlim #Hmi
+ elim (lift_trans_le … HUV2 … HVW2) -V2 // <yminus_succ2 <yplus_inj >yplus_SO2 >ymax_pre_sn /3 width=8 by cpr_delta, ylt_fwd_le_succ1, ex2_intro/
+ | elim (yle_inv_plus_inj2 … Hil) #Hlim #Hmi
+ lapply (yle_inv_inj … Hmi) -Hmi #Hmi
lapply (drop_conf_ge … HLK … HLV ?) -L // #HKLV
- elim (lift_split … HVW2 l (i - m + 1)) -HVW2 [2,3,4: /2 width=1 by le_S_S, le_S/ ] -Hil -Hlim
+ elim (lift_split … HVW2 l (i - m + 1)) -HVW2 [2,3,4: /2 width=1 by yle_succ_dx, le_S_S/ ] -Hil -Hlim
#V1 #HV1 >plus_minus // <minus_minus /2 width=1 by le_S/ <minus_n_n <plus_n_O
/3 width=8 by cpr_delta, ex2_intro/
]
∃∃T2,T. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 & ⬆[l, 1] T ≡ T2.
#h #g #I #G #K #V #T1 elim T1 -T1
[ * #i #L #l /2 width=4 by cpx_atom, lift_sort, lift_gref, ex2_2_intro/
- elim (lt_or_eq_or_gt i l) #Hil [1,3: /3 width=4 by cpx_atom, lift_lref_ge_minus, lift_lref_lt, ex2_2_intro/ ]
+ elim (lt_or_eq_or_gt i l) #Hil [1,3: /4 width=4 by cpx_atom, lift_lref_ge_minus, lift_lref_lt, ylt_inj, yle_inj, ex2_2_intro/ ]
destruct
elim (lift_total V 0 (i+1)) #W #HVW
elim (lift_split … HVW i i) /3 width=7 by cpx_delta, ex2_2_intro/
(* *)
(**************************************************************************)
+include "ground_2/ynat/ynat_max.ma".
include "basic_2/substitution/drop_drop.ma".
include "basic_2/multiple/fqus_alt.ma".
include "basic_2/static/da.ma".
>(lift_inv_sort1 … H2) -U2 /2 width=2 by cpx_st/
| #I #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #s #l #m #HLK #U1 #H #U2 #HWU2
elim (lift_inv_lref1 … H) * #Hil #H destruct
- [ elim (lift_trans_ge … HVW2 … HWU2) -W2 // <minus_plus #W2 #HVW2 #HWU2
- elim (drop_trans_le … HLK … HKV) -K /2 width=2 by lt_to_le/ #X #HLK #H
- elim (drop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hil
+ [ elim (lift_trans_ge … HVW2 … HWU2) -W2 /2 width=1 by ylt_fwd_le_succ1/ #W2 #HVW2 #HWU2
+ elim (drop_trans_le … HLK … HKV) -K /2 width=2 by ylt_fwd_le/ #X #HLK #H
+ elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil
#K #Y #HKV #HVY #H destruct /3 width=10 by cpx_delta/
- | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 /2 width=1 by le_S/ >plus_plus_comm_23 #HVU2
+ | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 /2 width=1 by yle_succ_dx/ >plus_plus_comm_23 #HVU2
lapply (drop_trans_ge_comm … HLK … HKV ?) -K /3 width=7 by cpx_delta, drop_inv_gen/
]
| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #s #l #m #HLK #U1 #H1 #U2 #H2
elim (lift_inv_lref2 … H) -H * #Hil #H destruct
[ elim (drop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV
elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2
- elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus <plus_minus_m_m /3 width=9 by cpx_delta, ex2_intro/
- | elim (le_inv_plus_l … Hil) #Hlim #Hmi
+ elim (lift_trans_le … HUV2 … HVW2) -V2 // <yminus_succ2 <yplus_inj >yplus_SO2 >ymax_pre_sn /3 width=9 by cpx_delta, ylt_fwd_le_succ1, ex2_intro/
+ | elim (yle_inv_plus_inj2 … Hil) #Hlim #Hmi
+ lapply (yle_inv_inj … Hmi) -Hmi #Hmi
lapply (drop_conf_ge … HLK … HLV ?) -L // #HKLV
- elim (lift_split … HVW2 l (i - m + 1)) -HVW2 /3 width=1 by le_S, le_S_S/ -Hil -Hlim
+ elim (lift_split … HVW2 l (i - m + 1)) -HVW2 /3 width=1 by yle_succ, yle_pred_sn, le_S_S/ -Hil -Hlim
#V1 #HV1 >plus_minus // <minus_minus /2 width=1 by le_S/ <minus_n_n <plus_n_O /3 width=9 by cpx_delta, ex2_intro/
]
| #a #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #s #l #m #HLK #X #H
[ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1)
#U2 #HVU2 @(ex3_intro … U2)
[1,3: /3 width=7 by fqu_drop, cpx_delta, drop_pair, drop_drop/
- | #H destruct /2 width=7 by lift_inv_lref2_be/
+ | #H destruct
+ lapply (lift_inv_lref2_be … HVU2 ? ?) -HVU2 //
]
| #I #G #L #V1 #T #V2 #HV12 #H @(ex3_intro … (②{I}V2.T))
[1,3: /2 width=4 by fqu_pair_sn, cpx_pair_sn/
| * #I #K1 #W1 #W0 #HLK1 #HW10 #HW0U2
lapply (drop_fwd_drop2 … HLK1) #H0
elim (lpx_drop_conf … H0 … HL12) -H0 -HL12 #K2 #HK12 #HLK2
- elim (lt_or_ge i (j+1)) #Hji
- [ -IH elim (frees_inv_lift_be … H2 … HLK2 … HW0U2) /2 width=1 by monotonic_pred/
- | lapply (frees_inv_lift_ge … H2 … HLK2 … HW0U2 ?) -L2 -U2 // <minus_plus destruct
- /4 width=11 by frees_lref_be, fqup_lref/
+ elim (ylt_split i (j+1)) >yplus_SO2 #Hji
+ [ -IH elim (frees_inv_lift_be … H2 … HLK2 … HW0U2) /2 width=1 by ylt_fwd_succ2/
+ | lapply (frees_inv_lift_ge … H2 … HLK2 … HW0U2 ?) -L2 -U2 // destruct
+ /4 width=11 by frees_lref_be, fqup_lref, yle_succ1_inj/
]
]
| -IH #p #HG #HL #HU #U2 #H1 >(cpx_inv_gref1 … H1) -H1 destruct
>(lift_inv_sort1 … H) -H //
| #I #G #L1 #K1 #V1 #B #i #HLK1 #_ #IHB #L2 #s #l #m #HL21 #T2 #H
elim (lift_inv_lref1 … H) -H * #Hil #H destruct
- [ elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by lt_to_le/ #X #HLK2 #H
- elim (drop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hil #K2 #V2 #HK21 #HV12 #H destruct
+ [ elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by ylt_fwd_le/ #X #HLK2 #H
+ elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K2 #V2 #HK21 #HV12 #H destruct
/3 width=9 by aaa_lref/
| lapply (drop_trans_ge … HL21 … HLK1 ?) -L1
/3 width=9 by aaa_lref, drop_inv_gen/
>(lift_inv_sort1 … H) -X /2 width=1 by da_sort/
| #G #L1 #K1 #V1 #i #d #HLK1 #_ #IHV1 #L2 #s #l #m #HL21 #X #H
elim (lift_inv_lref1 … H) * #Hil #H destruct
- [ elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by lt_to_le/ #X #HLK2 #H
- elim (drop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hil #K2 #V2 #HK21 #HV12 #H destruct
+ [ elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by ylt_fwd_le/ #X #HLK2 #H
+ elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K2 #V2 #HK21 #HV12 #H destruct
/3 width=9 by da_ldef/
| lapply (drop_trans_ge … HL21 … HLK1 ?) -L1
/3 width=8 by da_ldef, drop_inv_gen/
]
| #G #L1 #K1 #W1 #i #d #HLK1 #_ #IHW1 #L2 #s #l #m #HL21 #X #H
elim (lift_inv_lref1 … H) * #Hil #H destruct
- [ elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by lt_to_le/ #X #HLK2 #H
- elim (drop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hil #K2 #W2 #HK21 #HW12 #H destruct
+ [ elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by ylt_fwd_le/ #X #HLK2 #H
+ elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K2 #W2 #HK21 #HW12 #H destruct
/3 width=8 by da_ldec/
| lapply (drop_trans_ge … HL21 … HLK1 ?) -L1
/3 width=8 by da_ldec, drop_inv_gen/
[ * #i #L #l #HLK
/2 width=4 by lift_sort, lift_gref, ex2_2_intro/
elim (lt_or_eq_or_gt i l) #Hil
- /3 width=4 by lift_lref_ge_minus, lift_lref_lt, ex2_2_intro/
+ /4 width=4 by lift_lref_ge_minus, lift_lref_lt, ex2_2_intro, ylt_inj, yle_inj/ (**) (* was /3 width=4/ without inj *)
destruct
elim (lift_total V 0 (i+1)) #W #HVW
elim (lift_split … HVW i i)
lapply (drop_fwd_length_lt2 … HLK)
/4 width=5 by cpy_subst, ylt_yle_trans, ylt_inj/
| #a #I #G #L #V1 #V2 normalize in match (|L.ⓑ{I}V2|); (**) (* |?| does not work *)
+ <yplus_inj >yplus_SO2 >yminus_succ
/2 width=1 by cpy_bind/
| /2 width=1 by cpy_flat/
]
| #I #G #L #K #V #W #i #lt #mt #Hlti #Hilmt #HLK #HVW #T1 #l #m #H #Hllt #Hlmlmt
elim (lift_inv_lref2 … H) -H * #Hil #H destruct [ -V -Hilmt -Hlmlmt | -Hlti -Hllt ]
[ elim (ylt_yle_false … Hllt) -Hllt /3 width=3 by yle_ylt_trans, ylt_inj/
- | elim (le_inv_plus_l … Hil) #Hlim #Hmi
- elim (lift_split … HVW l (i-m+1) ? ? ?) [2,3,4: /2 width=1 by le_S_S, le_S/ ] -Hlim
- #T2 #_ >plus_minus /
/ <minus_minus /2 width=1 by le_S/ <minus_n_n <plus_n_O #H -Hmi
+ | elim (yle_inv_plus_inj2 … Hil) #Hlim #Hmi
+ elim (lift_split … HVW l (i-m+1) ? ? ?) [2,3,4: /2 width=1 by yle_succ_dx, le_S_S/ ] -Hlim
+ #T2 #_ >plus_minus /
2 width=1 by yle_inv_inj/ <minus_minus /3 width=1 by le_S, yle_inv_inj/ <minus_n_n <plus_n_O #H -Hmi
@(ex2_intro … H) -H @(cpy_subst … HLK HVW) /2 width=1 by yle_inj/ >ymax_pre_sn_comm // (**) (* explicit constructor *)
]
| #a #I #G #L #W1 #W2 #U1 #U2 #lt #mt #_ #_ #IHW12 #IHU12 #X #l #m #H #Hllt #Hlmlmt
elim (cpy_inv_atom1 … H) -H
[ #H destruct //
| * #J #K #V #i #Hl2i #Hilm2 #HLK #HVT2 #H destruct
- lapply (ylt_yle_trans … (l+m) … Hilm2) /2 width=5 by cpy_subst, monotonic_yle_plus_dx/
+ lapply (ylt_yle_trans … (l+m) … Hilm2)
+ /2 width=5 by cpy_subst, monotonic_yle_plus_sn/
]
| #I #G #L #K #V #V2 #i #l #m #Hli #Hilm #HLK #HVW #T2 #HVT2 #Hm
lapply (cpy_weak … HVT2 0 (i+1) ? ?) -HVT2 /3 width=1 by yle_plus_dx2_trans, yle_succ/
>(lift_mono … H1 … H2) -H1 -H2 //
| #I #G #K #KV #V #W #i #lt #mt #Hlti #Hilmt #HKV #HVW #L #U1 #U2 #s #l #m #HLK #H #HWU2 #Hlmtl
lapply (ylt_yle_trans … Hlmtl … Hilmt) -Hlmtl #Hil
- lapply (ylt_inv_inj … Hil) -Hil #Hil
lapply (lift_inv_lref1_lt … H … Hil) -H #H destruct
- elim (lift_trans_ge … HVW … HWU2) -W // <minus_plus #W #HVW #HWU2
- elim (drop_trans_le … HLK … HKV) -K /2 width=2 by lt_to_le/ #X #HLK #H
- elim (drop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hil #K #Y #_ #HVY
+ elim (lift_trans_ge … HVW … HWU2) -W /2 width=1 by ylt_fwd_le_succ1/
+ <yplus_inj >yplus_SO2 >yminus_succ2 #W #HVW #HWU2
+ elim (drop_trans_le … HLK … HKV) -K /2 width=2 by ylt_fwd_le/ #X #HLK #H
+ elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K #Y #_ #HVY
>(lift_mono … HVY … HVW) -Y -HVW #H destruct /2 width=5 by cpy_subst/
| #a #I #G #K #V1 #V2 #T1 #T2 #lt #mt #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #l #m #HLK #H1 #H2 #Hlmtl
elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1
elim (lift_inv_lref1 … H) -H * #Hil #H destruct
[ -Hltl
lapply (ylt_yle_trans … (lt+mt+m) … Hilmt) // -Hilmt #Hilmtm
- elim (lift_trans_ge … HVW … HWU2) -W // <minus_plus #W #HVW #HWU2
- elim (drop_trans_le … HLK … HKV) -K /2 width=2 by lt_to_le/ #X #HLK #H
- elim (drop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hil #K #Y #_ #HVY
+ elim (lift_trans_ge … HVW … HWU2) -W <yplus_inj >yplus_SO2
+ [2: >yplus_O1 /2 width=1 by ylt_fwd_le_succ1/ ] >yminus_succ2 #W #HVW #HWU2
+ elim (drop_trans_le … HLK … HKV) -K /2 width=1 by ylt_fwd_le/ #X #HLK #H
+ elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K #Y #_ #HVY
>(lift_mono … HVY … HVW) -V #H destruct /2 width=5 by cpy_subst/
| -Hlti
- elim (yle_inv_inj2 … Hltl) -Hltl #ltt #Hltl #H destruct
- lapply (transitive_le … Hltl Hil) -Hltl #Hlti
- lapply (lift_trans_be … HVW … HWU2 ? ?) -W /2 width=1 by le_S/ >plus_plus_comm_23 #HVU2
+ lapply (yle_trans … Hltl … Hil) -Hltl #Hlti
+ lapply (lift_trans_be … HVW … HWU2 ? ?) -W /2 width=1 by yle_succ_dx/ >plus_plus_comm_23 #HVU2
lapply (drop_trans_ge_comm … HLK … HKV ?) -K // -Hil
- /4 width=5 by cpy_subst, drop_inv_gen, monotonic_ylt_plus_dx, yle_plus_dx1_trans, yle_inj/
+ /3 width=5 by cpy_subst, drop_inv_gen, monotonic_ylt_plus_dx, yle_plus_dx1_trans/
]
| #a #I #G #K #V1 #V2 #T1 #T2 #lt #mt #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #l #m #HLK #H1 #H2 #Hltl #Hllmt
elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1
>(lift_mono … H1 … H2) -H1 -H2 //
| #I #G #K #KV #V #W #i #lt #mt #Hlti #Hilmt #HKV #HVW #L #U1 #U2 #s #l #m #HLK #H #HWU2 #Hllt
lapply (yle_trans … Hllt … Hlti) -Hllt #Hil
- elim (yle_inv_inj2 … Hil) -Hil #ll #Hlli #H0 destruct
- lapply (lift_inv_lref1_ge … H … Hlli) -H #H destruct
- lapply (lift_trans_be … HVW … HWU2 ? ?) -W /2 width=1 by le_S/ >plus_plus_comm_23 #HVU2
- lapply (drop_trans_ge_comm … HLK … HKV ?) -K // -Hlli
+ lapply (lift_inv_lref1_ge … H … Hil) -H #H destruct
+ lapply (lift_trans_be … HVW … HWU2 ? ?) -W /2 width=1 by yle_succ_dx/ >plus_plus_comm_23 #HVU2
+ lapply (drop_trans_ge_comm … HLK … HKV ?) -K // -Hil
/3 width=5 by cpy_subst, drop_inv_gen, monotonic_ylt_plus_dx, monotonic_yle_plus_dx/
| #a #I #G #K #V1 #V2 #T1 #T2 #lt #mt #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #l #m #HLK #H1 #H2 #Hllt
elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1
]
| #I #G #L #KV #V #W #i #lt #mt #Hlti #Hilmt #HLKV #HVW #K #s #l #m #HLK #T1 #H #Hlmtl
lapply (ylt_yle_trans … Hlmtl … Hilmt) -Hlmtl #Hil
- lapply (ylt_inv_inj … Hil) -Hil #Hil
lapply (lift_inv_lref2_lt … H … Hil) -H #H destruct
elim (drop_conf_lt … HLK … HLKV) -L // #L #U #HKL #_ #HUV
- elim (lift_trans_le … HUV … HVW) -V // >minus_plus <plus_minus_m_m // -Hil /3 width=5 by cpy_subst, ex2_intro/
+ elim (lift_trans_le … HUV … HVW) -V // >minus_plus <plus_minus_m_m //
+ <yminus_succ2 <yplus_inj >yplus_SO2 >ymax_pre_sn /2 width=1 by ylt_fwd_le_succ1/ -Hil
+ /3 width=5 by cpy_subst, ex2_intro/
| #a #I #G #L #W1 #W2 #U1 #U2 #lt #mt #_ #_ #IHW12 #IHU12 #K #s #l #m #HLK #X #H #Hlmtl
elim (lift_inv_bind2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
elim (IHW12 … HLK … HVW1) -IHW12 // #V2 #HV12 #HVW2
lemma cpy_inv_lift1_be: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶[lt, mt] U2 →
∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
- lt ≤ l → yinj l + m ≤ lt + mt →
+ lt ≤ l → l + m ≤ lt + mt →
∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[lt, mt-m] T2 & ⬆[l, m] T2 ≡ U2.
#G #L #U1 #U2 #lt #mt #H elim H -G -L -U1 -U2 -lt -mt
[ * #i #G #L #lt #mt #K #s #l #m #_ #T1 #H #_ #_
| elim (lift_inv_lref2 … H) -H * #Hil #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/
| lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/
]
-| #I #G #L #KV #V #W #i #lt #mt #Hlti #Hilmt #HLKV #HVW #K #s #l #m #HLK #T1 #H #Hltl #Hlmlmt
- lapply (yle_fwd_plus_ge_inj … Hltl Hlmlmt) #Hmmt
+| #I #G #L #KV #V #W #i #x #mt #Hlti #Hilmt #HLKV #HVW #K #s #l #m #HLK #T1 #H #Hltl #Hlmlmt
+ elim (yle_inv_inj2 … Hlti) -Hlti #lt #Hlti #H destruct
+ lapply (yle_fwd_plus_yge … Hltl Hlmlmt) #Hmmt
elim (lift_inv_lref2 … H) -H * #Hil #H destruct [ -Hltl -Hilmt | -Hlti -Hlmlmt ]
- [ lapply (ylt_yle_trans i l (lt+(mt-m)) ? ?) /2 width=1 by ylt_inj/
+ [ lapply (ylt_yle_trans i l (lt+(mt-m)) ? ?) //
[ >yplus_minus_assoc_inj /2 width=1 by yle_plus1_to_minus_inj2/ ] -Hlmlmt #Hilmtm
elim (drop_conf_lt … HLK … HLKV) -L // #L #U #HKL #_ #HUV
- elim (lift_trans_le … HUV … HVW) -V // >minus_plus <plus_minus_m_m // -Hil
- /3 width=5 by cpy_subst, ex2_intro/
- | elim (le_inv_plus_l … Hil) #Hlim #Hmi
- lapply (yle_trans … Hltl (i-m) ?) /2 width=1 by yle_inj/ -Hltl #Hltim
+ elim (lift_trans_le … HUV … HVW) -V //
+ <yminus_succ2 <yplus_inj >yplus_SO2 >ymax_pre_sn /2 width=1 by ylt_fwd_le_succ1/ -Hil
+ /4 width=5 by cpy_subst, ex2_intro, yle_inj/
+ | elim (yle_inv_plus_inj2 … Hil) #Hlim #Hmi
+ lapply (yle_inv_inj … Hmi) -Hmi #Hmi
+ lapply (yle_trans … Hltl (i-m) ?) // -Hltl #Hltim
lapply (drop_conf_ge … HLK … HLKV ?) -L // #HKV
- elim (lift_split … HVW l (i-m+1)) -HVW [2,3,4: /2 width=1 by le_S_S, le_S/ ] -Hil -Hlim
+ elim (lift_split … HVW l (i-m+1)) -HVW [2,3,4: /2 width=1 by yle_succ_dx, le_S_S/ ] -Hil -Hlim
#V1 #HV1 >plus_minus // <minus_minus /2 width=1 by le_S/ <minus_n_n <plus_n_O #H
@(ex2_intro … H) @(cpy_subst … HKV HV1) // (**) (* explicit constructor *)
>yplus_minus_assoc_inj /3 width=1 by monotonic_ylt_minus_dx, yle_inj/
(* Basic_1: was: subst1_gen_lift_ge *)
lemma cpy_inv_lift1_ge: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶[lt, mt] U2 →
∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
- yinj l + m ≤ lt →
+ l + m ≤ lt →
∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[lt-m, mt] T2 & ⬆[l, m] T2 ≡ U2.
#G #L #U1 #U2 #lt #mt #H elim H -G -L -U1 -U2 -lt -mt
[ * #i #G #L #lt #mt #K #s #l #m #_ #T1 #H #_
lapply (yle_trans … Hlmlt … Hlti) #Hlmi
elim (yle_inv_plus_inj2 … Hlmlt) -Hlmlt #_ #Hmlt
elim (yle_inv_plus_inj2 … Hlmi) #Hlim #Hmi
- lapply (lift_inv_lref2_ge … H ?) -H /2 width=1 by yle_inv_inj/ #H destruct
- lapply (drop_conf_ge … HLK … HLKV ?) -L /2 width=1 by yle_inv_inj/ #HKV
- elim (lift_split … HVW l (i-m+1)) -HVW [2,3,4: /3 width=1 by yle_inv_inj, le_S_S, le_S/ ] -Hlmi -Hlim
- #V0 #HV10 >plus_minus /2 width=1 by yle_inv_inj/ <minus_minus /3 width=1 by yle_inv_inj, le_S/ <minus_n_n <plus_n_O #H
+ lapply (yle_inv_inj … Hmi) -Hmi #Hmi
+ lapply (lift_inv_lref2_ge … H ?) -H // #H destruct
+ lapply (drop_conf_ge … HLK … HLKV ?) -L // #HKV
+ elim (lift_split … HVW l (i-m+1)) -HVW [2,3,4: /3 width=1 by yle_succ, yle_pred_sn, le_S_S/ ] -Hlmi -Hlim
+ #V0 #HV10 >plus_minus // <minus_minus /3 width=1 by le_S/ <minus_n_n <plus_n_O #H
@(ex2_intro … H) @(cpy_subst … HKV HV10) (**) (* explicit constructor *)
[ /2 width=1 by monotonic_yle_minus_dx/
- | <yplus_minus_comm_inj /2 width=1 by monotonic_ylt_minus_dx/
+ | <yminus_inj <yplus_minus_comm_inj // /3 width=1 by monotonic_ylt_minus_dx, yle_inj/
]
| #a #I #G #L #W1 #W2 #U1 #U2 #lt #mt #_ #_ #IHW12 #IHU12 #K #s #l #m #HLK #X #H #Hlmtl
elim (lift_inv_bind2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
lemma cpy_inv_lift1_ge_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶[lt, mt] U2 →
∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
- l ≤ lt → lt ≤ yinj l + m → yinj l + m ≤ lt + mt →
- ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[l, lt + mt - (yinj l + m)] T2 & ⬆[l, m] T2 ≡ U2.
+ l ≤ lt → lt ≤ l + m → l + m ≤ lt + mt →
+ ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[l, lt + mt - (l + m)] T2 & ⬆[l, m] T2 ≡ U2.
#G #L #U1 #U2 #lt #mt #HU12 #K #s #l #m #HLK #T1 #HTU1 #Hllt #Hltlm #Hlmlmt
elim (cpy_split_up … HU12 (l + m)) -HU12 // -Hlmlmt #U #HU1 #HU2
lapply (cpy_weak … HU1 l m ? ?) -HU1 // [ >ymax_pre_sn_comm // ] -Hllt -Hltlm #HU1
lemma cpy_inv_lift1_be_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶[lt, mt] U2 →
∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
- lt ≤ l → lt + mt ≤ yinj l + m →
+ lt ≤ l → lt + mt ≤ l + m →
∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[lt, l-lt] T2 & ⬆[l, m] T2 ≡ U2.
#G #L #U1 #U2 #lt #mt #HU12 #K #s #l #m #HLK #T1 #HTU1 #Hltl #Hlmtlm
lapply (cpy_weak … HU12 lt (l+m-lt) ? ?) -HU12 //
lemma cpy_inv_lift1_le_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶[lt, mt] U2 →
∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
- lt ≤ l → l ≤ lt + mt → lt + mt ≤ yinj l + m →
+ lt ≤ l → l ≤ lt + mt → lt + mt ≤ l + m →
∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[lt, l - lt] T2 & ⬆[l, m] T2 ≡ U2.
#G #L #U1 #U2 #lt #mt #HU12 #K #s #l #m #HLK #T1 #HTU1 #Hltl #Hllmt #Hlmtlm
elim (cpy_split_up … HU12 l) -HU12 // #U #HU1 #HU2
(* Inversion lemmas on negated relocation ***********************************)
lemma cpy_fwd_nlift2_ge: ∀G,L,U1,U2,l,m. ⦃G, L⦄ ⊢ U1 ▶[l, m] U2 →
- ∀i. l ≤ yinj i → (∀T2. ⬆[i, 1] T2 ≡ U2 → ⊥) →
+ ∀i. l ≤ i → (∀T2. ⬆[i, 1] T2 ≡ U2 → ⊥) →
(∀T1. ⬆[i, 1] T1 ≡ U1 → ⊥) ∨
∃∃I,K,W,j. l ≤ yinj j & j < i & ⬇[j]L ≡ K.ⓑ{I}W &
- (∀V. ⬆[i-j-1, 1] V ≡ W → ⊥) & (∀T1. ⬆[j, 1] T1 ≡ U1 → ⊥).
+ (∀V. ⬆[⫰(i-j), 1] V ≡ W → ⊥) & (∀T1. ⬆[j, 1] T1 ≡ U1 → ⊥).
#G #L #U1 #U2 #l #m #H elim H -G -L -U1 -U2 -l -m
[ /3 width=2 by or_introl/
| #I #G #L #K #V #W #j #l #m #Hlj #Hjlm #HLK #HVW #i #Hli #HnW
- elim (lt_or_ge j i) #Hij
+ elim (ylt_split j i) #Hij
[ @or_intror @(ex5_4_intro … HLK) // -HLK
- [ #X #HXV elim (lift_trans_le … HXV … HVW ?) -V //
- #Y #HXY >minus_plus <plus_minus_m_m /2 width=2 by/
- | -HnW /2 width=7 by lift_inv_lref2_be/
+ [ #X #HXV elim (lift_trans_le … HXV … HVW ?) -V // #Y #HXY
+ <yminus_succ2 <yplus_inj >yplus_SO2 >ymax_pre_sn /2 width=2 by ylt_fwd_le_succ1/
+ | -HnW /3 width=7 by lift_inv_lref2_be, ylt_inj/
]
| elim (lift_split … HVW i j) -HVW //
#X #_ #H elim HnW -HnW //
]
| #HnU2 elim (IHU12 … HnU2) -IHU12 -HnU2 -IHW12 /2 width=1 by yle_succ/
[ /4 width=9 by nlift_bind_dx, or_introl/
- | * #J #K #W #j #Hlj #Hji #HLK #HnW
- elim (yle_inv_succ1 … Hlj) -Hlj #Hlj #Hj
- lapply (ylt_O … Hj) -Hj #Hj
- lapply (drop_inv_drop1_lt … HLK ?) // -HLK #HLK
- >(plus_minus_m_m j 1) in ⊢ (%→?); [2: /3 width=3 by yle_trans, yle_inv_inj/ ]
- #HnU1 <minus_le_minus_minus_comm in HnW;
- /5 width=9 by nlift_bind_dx, monotonic_lt_pred, lt_plus_to_minus_r, ex5_4_intro, or_intror/
+ | * #J #K #W #j #Hlj elim (yle_inv_succ1 … Hlj) -Hlj #Hlj #Hj
+ <Hj >yminus_succ #Hji #HLK #HnW
+ lapply (drop_inv_drop1_lt … HLK ?) /2 width=1 by ylt_O/ -HLK #HLK
+ <yminus_SO2 in Hlj; #Hlj #H4
+ @or_intror @(ex5_4_intro … HLK) (**) (* explicit constructors *)
+ /3 width=9 by nlift_bind_dx, ylt_pred, ylt_inj/
]
]
| #I #G #L #W1 #W2 #U1 #U2 #l #m #_ #_ #IHW12 #IHU12 #i #Hli #H elim (nlift_inv_flat … H) -H
(* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************)
(* Basic_1: includes: drop_skip_bind *)
-inductive drop (s:bool): relation4 nat nat lenv lenv ≝
+inductive drop (s:bool): relation4 ynat nat lenv lenv ≝
| drop_atom: ∀l,m. (s = Ⓕ → m = 0) → drop s l m (⋆) (⋆)
| drop_pair: ∀I,L,V. drop s 0 0 (L.ⓑ{I}V) (L.ⓑ{I}V)
| drop_drop: ∀I,L1,L2,V,m. drop s 0 m L1 L2 → drop s 0 (m+1) (L1.ⓑ{I}V) L2
| drop_skip: ∀I,L1,L2,V1,V2,l,m.
drop s l m L1 L2 → ⬆[l, m] V2 ≡ V1 →
- drop s (l+1) m (L1.ⓑ{I}V1) (L2.ⓑ{I}V2)
+ drop s (⫯l) m (L1.ⓑ{I}V1) (L2.ⓑ{I}V2)
.
interpretation
*)
interpretation
"basic slicing (local environment) lget"
- 'RDrop m L1 L2 = (drop false O m L1 L2).
+ 'RDrop m L1 L2 = (drop false (yinj O) m L1 L2).
definition d_liftable: predicate (lenv → relation term) ≝
λR. ∀K,T1,T2. R K T1 T2 → ∀L,s,l,m. ⬇[s, l, m] L ≡ K →
lemma drop_inv_atom1: ∀L2,s,l,m. ⬇[s, l, m] ⋆ ≡ L2 → L2 = ⋆ ∧ (s = Ⓕ → m = 0).
/2 width=4 by drop_inv_atom1_aux/ qed-.
-fact drop_inv_O1_pair1_aux: ∀L1,L2,s,l,m. ⬇[s, l, m] L1 ≡ L2 → l = 0 →
+fact drop_inv_O1_pair1_aux: ∀L1,L2,s,l,m. ⬇[s, l, m] L1 ≡ L2 → l = yinj 0 →
∀K,I,V. L1 = K.ⓑ{I}V →
(m = 0 ∧ L2 = K.ⓑ{I}V) ∨
(0 < m ∧ ⬇[s, l, m-1] K ≡ L2).
[ #l #m #_ #_ #K #J #W #H destruct
| #I #L #V #_ #K #J #W #HX destruct /3 width=1 by or_introl, conj/
| #I #L1 #L2 #V #m #HL12 #_ #K #J #W #H destruct /3 width=1 by or_intror, conj/
-| #I #L1 #L2 #V1 #V2 #l #m #_ #_ >commutative_plus normalize #H destruct
+| #I #L1 #L2 #V1 #V2 #l #m #_ #_ #H elim (ysucc_inv_O_dx … H)
]
qed-.
-lemma drop_inv_O1_pair1: ∀I,K,L2,V,s,m. ⬇[s, 0, m] K. ⓑ{I} V ≡ L2 →
+lemma drop_inv_O1_pair1: ∀I,K,L2,V,s,m. ⬇[s, yinj 0, m] K. ⓑ{I} V ≡ L2 →
(m = 0 ∧ L2 = K.ⓑ{I}V) ∨
- (0 < m ∧ ⬇[s, 0, m-1] K ≡ L2).
+ (0 < m ∧ ⬇[s, yinj 0, m-1] K ≡ L2).
/2 width=3 by drop_inv_O1_pair1_aux/ qed-.
lemma drop_inv_pair1: ∀I,K,L2,V,s. ⬇[s, 0, 0] K.ⓑ{I}V ≡ L2 → L2 = K.ⓑ{I}V.
(* Basic_1: was: drop_gen_drop *)
lemma drop_inv_drop1_lt: ∀I,K,L2,V,s,m.
- ⬇[s, 0, m] K.ⓑ{I}V ≡ L2 → 0 < m → ⬇[s, 0, m-1] K ≡ L2.
+ ⬇[s, yinj 0, m] K.ⓑ{I}V ≡ L2 → 0 < m → ⬇[s, yinj 0, m-1] K ≡ L2.
#I #K #L2 #V #s #m #H #Hm
elim (drop_inv_O1_pair1 … H) -H * // #H destruct
elim (lt_refl_false … Hm)
fact drop_inv_skip1_aux: ∀L1,L2,s,l,m. ⬇[s, l, m] L1 ≡ L2 → 0 < l →
∀I,K1,V1. L1 = K1.ⓑ{I}V1 →
- ∃∃K2,V2. ⬇[s, l-1, m] K1 ≡ K2 &
- ⬆[l-1, m] V2 ≡ V1 &
+ ∃∃K2,V2. ⬇[s, ⫰l, m] K1 ≡ K2 &
+ ⬆[⫰l, m] V2 ≡ V1 &
L2 = K2.ⓑ{I}V2.
#L1 #L2 #s #l #m * -L1 -L2 -l -m
[ #l #m #_ #_ #J #K1 #W1 #H destruct
-| #I #L #V #H elim (lt_refl_false … H)
-| #I #L1 #L2 #V #m #_ #H elim (lt_refl_false … H)
+| #I #L #V #H elim (ylt_yle_false … H) -H //
+| #I #L1 #L2 #V #m #_ #H elim (ylt_yle_false … H) -H //
| #I #L1 #L2 #V1 #V2 #l #m #HL12 #HV21 #_ #J #K1 #W1 #H destruct /2 width=5 by ex3_2_intro/
]
qed-.
(* Basic_1: was: drop_gen_skip_l *)
lemma drop_inv_skip1: ∀I,K1,V1,L2,s,l,m. ⬇[s, l, m] K1.ⓑ{I}V1 ≡ L2 → 0 < l →
- ∃∃K2,V2. ⬇[s, l-1, m] K1 ≡ K2 &
- ⬆[l-1, m] V2 ≡ V1 &
+ ∃∃K2,V2. ⬇[s, ⫰l, m] K1 ≡ K2 &
+ ⬆[⫰l, m] V2 ≡ V1 &
L2 = K2.ⓑ{I}V2.
/2 width=3 by drop_inv_skip1_aux/ qed-.
-lemma drop_inv_O1_pair2: ∀I,K,V,s,m,L1. ⬇[s, 0, m] L1 ≡ K.ⓑ{I}V →
+lemma drop_inv_O1_pair2: ∀I,K,V,s,m,L1. ⬇[s, yinj 0, m] L1 ≡ K.ⓑ{I}V →
(m = 0 ∧ L1 = K.ⓑ{I}V) ∨
- ∃∃I1,K1,V1. ⬇[s, 0, m-1] K1 ≡ K.ⓑ{I}V & L1 = K1.ⓑ{I1}V1 & 0 < m.
+ ∃∃I1,K1,V1. ⬇[s, yinj 0, m-1] K1 ≡ K.ⓑ{I}V & L1 = K1.ⓑ{I1}V1 & 0 < m.
#I #K #V #s #m *
[ #H elim (drop_inv_atom1 … H) -H #H destruct
| #L1 #I1 #V1 #H
fact drop_inv_skip2_aux: ∀L1,L2,s,l,m. ⬇[s, l, m] L1 ≡ L2 → 0 < l →
∀I,K2,V2. L2 = K2.ⓑ{I}V2 →
- ∃∃K1,V1. ⬇[s, l-1, m] K1 ≡ K2 &
- ⬆[l-1, m] V2 ≡ V1 &
+ ∃∃K1,V1. ⬇[s, ⫰l, m] K1 ≡ K2 &
+ ⬆[⫰l, m] V2 ≡ V1 &
L1 = K1.ⓑ{I}V1.
#L1 #L2 #s #l #m * -L1 -L2 -l -m
[ #l #m #_ #_ #J #K2 #W2 #H destruct
-| #I #L #V #H elim (lt_refl_false … H)
-| #I #L1 #L2 #V #m #_ #H elim (lt_refl_false … H)
+| #I #L #V #H elim (ylt_yle_false … H) -H //
+| #I #L1 #L2 #V #m #_ #H elim (ylt_yle_false … H) -H //
| #I #L1 #L2 #V1 #V2 #l #m #HL12 #HV21 #_ #J #K2 #W2 #H destruct /2 width=5 by ex3_2_intro/
]
qed-.
(* Basic_1: was: drop_gen_skip_r *)
lemma drop_inv_skip2: ∀I,L1,K2,V2,s,l,m. ⬇[s, l, m] L1 ≡ K2.ⓑ{I}V2 → 0 < l →
- ∃∃K1,V1. ⬇[s, l-1, m] K1 ≡ K2 & ⬆[l-1, m] V2 ≡ V1 &
+ ∃∃K1,V1. ⬇[s, ⫰l, m] K1 ≡ K2 & ⬆[⫰l, m] V2 ≡ V1 &
L1 = K1.ⓑ{I}V1.
/2 width=3 by drop_inv_skip2_aux/ qed-.
-lemma drop_inv_O1_gt: ∀L,K,m,s. ⬇[s, 0, m] L ≡ K → |L| < m →
+lemma drop_inv_O1_gt: ∀L,K,m,s. ⬇[s, yinj 0, m] L ≡ K → |L| < m →
s = Ⓣ ∧ K = ⋆.
#L elim L -L [| #L #Z #X #IHL ] #K #m #s #H normalize in ⊢ (?%?→?); #H1m
[ elim (drop_inv_atom1 … H) -H elim s -s /2 width=1 by conj/
]
qed-.
+lemma drop_inv_Y1: ∀L,K,m,s. ⬇[s, ∞, m] L ≡ K →
+ L = K ∧ (s = Ⓕ → m = 0).
+#L elim L -L
+[ #Y #m #s #H elim (drop_inv_atom1 … H) -H /3 width=1 by conj/
+| #L #I #V #IHL #Y #m #s #H elim (drop_inv_skip1 … H) -H //
+ #K #W #HLK #HWV #H destruct
+ lapply (lift_inv_Y1 … HWV) -HWV #H destruct
+ elim (IHL … HLK) -IHL -HLK /3 width=1 by conj/
+]
+qed-.
+
(* Basic properties *********************************************************)
lemma drop_refl_atom_O2: ∀s,l. ⬇[s, l, O] ⋆ ≡ ⋆.
/2 width=1 by drop_atom/ qed.
+lemma drop_Y1: ∀m,s. (s = Ⓕ → m = 0) → ∀L. ⬇[s, ∞, m] L ≡ L.
+#m #s #H #L elim L -L /3 width=3 by drop_atom, drop_skip/
+qed.
+
(* Basic_1: was by definition: drop_refl *)
lemma drop_refl: ∀L,l,s. ⬇[s, l, 0] L ≡ L.
#L elim L -L //
-#L #I #V #IHL #l #s @(nat_ind_plus … l) -l /2 width=1 by drop_pair, drop_skip/
+#L #I #V #IHL #x #s elim (ynat_cases x)
+[ #H destruct //
+| * #l #H destruct /2 width=1 by drop_skip/
+]
qed.
lemma drop_drop_lt: ∀I,L1,L2,V,s,m.
- ⬇[s, 0, m-1] L1 ≡ L2 → 0 < m → ⬇[s, 0, m] L1.ⓑ{I}V ≡ L2.
+ ⬇[s, yinj 0, m-1] L1 ≡ L2 → 0 < m → ⬇[s, yinj 0, m] L1.ⓑ{I}V ≡ L2.
#I #L1 #L2 #V #s #m #HL12 #Hm >(plus_minus_m_m m 1) /2 width=1 by drop_drop/
qed.
lemma drop_skip_lt: ∀I,L1,L2,V1,V2,s,l,m.
- ⬇[s, l-1, m] L1 ≡ L2 → ⬆[l-1, m] V2 ≡ V1 → 0 < l →
+ ⬇[s, ⫰l, m] L1 ≡ L2 → ⬆[⫰l, m] V2 ≡ V1 → 0 < l →
⬇[s, l, m] L1. ⓑ{I} V1 ≡ L2.ⓑ{I}V2.
-#I #L1 #L2 #V1 #V2 #s #l #m #HL12 #HV21 #Hl >(plus_minus_m_m l 1) /2 width=1 by drop_skip/
+#I #L1 #L2 #V1 #V2 #s #l #m #HL12 #HV21 #Hl <(ylt_inv_O1 … Hl) -Hl
+/2 width=1 by drop_skip/
qed.
lemma drop_O1_le: ∀s,m,L. m ≤ |L| → ∃K. ⬇[s, 0, m] L ≡ K.
]
qed-.
-lemma drop_O1_pair: ∀L,K,m,s. ⬇[s, 0, m] L ≡ K → m ≤ |L| → ∀I,V.
- ∃∃J,W. ⬇[s, 0, m] L.ⓑ{I}V ≡ K.ⓑ{J}W.
+lemma drop_O1_pair: ∀L,K,m,s. ⬇[s, yinj 0, m] L ≡ K → m ≤ |L| → ∀I,V.
+ ∃∃J,W. ⬇[s, yinj 0, m] L.ⓑ{I}V ≡ K.ⓑ{J}W.
#L elim L -L [| #L #Z #X #IHL ] #K #m #s #H normalize #Hm #I #V
[ elim (drop_inv_atom1 … H) -H #H <(le_n_O_to_eq … Hm) -m
#Hs destruct /2 width=3 by ex1_2_intro/
qed-.
lemma drop_fwd_length_ge: ∀L1,L2,l,m,s. ⬇[s, l, m] L1 ≡ L2 → |L1| ≤ l → |L2| = |L1|.
-#L1 #L2 #l #m #s #H elim H -L1 -L2 -l -m // normalize
-[ #I #L1 #L2 #V #m #_ #_ #H elim (le_plus_xSy_O_false … H)
-| /4 width=2 by le_plus_to_le_r, eq_f/
+#L1 #L2 #l #m #s #H elim H -L1 -L2 -l -m //
+[ #I #L1 #L2 #V #m #_ #_ #H elim (ylt_yle_false … H) -H normalize //
+| #I #L1 #L2 #V1 #V2 #l #m #_ #_ #IH <yplus_inj >yplus_SO2 #H
+ lapply (yle_inv_succ … H) -H #H normalize /3 width=1 by eq_f2/
]
qed-.
lemma drop_fwd_length_le_le: ∀L1,L2,l,m,s. ⬇[s, l, m] L1 ≡ L2 → l ≤ |L1| → m ≤ |L1| - l → |L2| = |L1| - m.
-#L1 #L2 #l #m #s #H elim H -L1 -L2 -l -m // normalize
-[ /3 width=2 by le_plus_to_le_r/
-| #I #L1 #L2 #V1 #V2 #l #m #_ #_ #IHL12 >minus_plus_plus_l
- #Hl #Hm lapply (le_plus_to_le_r … Hl) -Hl
- #Hl >IHL12 // -L2 >plus_minus /2 width=3 by transitive_le/
+#L1 #L2 #l #m #s #H elim H -L1 -L2 -l -m //
+[ #I #L1 #L2 #V #m #_ <yplus_inj normalize #IH #_
+ >minus_plus_plus_l <yplus_inj >yplus_SO2 /3 width=1 by yle_inv_succ/
+| #I #L1 #L2 #V1 #V2 #l #m #_ #_ #IHL12 <yplus_inj >yplus_SO2 #H
+ lapply (yle_inv_succ … H) -H #Hl1 >yminus_succ #Hml1 normalize
+ <plus_minus /3 width=3 by yle_trans, yle_inv_inj, eq_f2/
]
qed-.
-lemma drop_fwd_length_le_ge: ∀L1,L2,l,m,s. ⬇[s, l, m] L1 ≡ L2 → l ≤ |L1| → |L1| - l ≤ m → |L2| = l.
-#L1 #L2 #l #m #s #H elim H -L1 -L2 -l -m normalize
-[ /2 width=1 by le_n_O_to_eq/
-| #I #L #V #_ <minus_n_O #H elim (le_plus_xSy_O_false … H)
-| /3 width=2 by le_plus_to_le_r/
-| /4 width=2 by le_plus_to_le_r, eq_f/
+lemma drop_fwd_length_le_ge: ∀L1,L2,l,m,s. ⬇[s, l, m] L1 ≡ L2 → l ≤ |L1| → |L1| - l ≤ m → yinj (|L2|) = l.
+#L1 #L2 #l #m #s #H elim H -L1 -L2 -l -m
+[ #l #m #_ #H #_ normalize /2 width=1 by yle_inv_O2/
+| #I #L #V #_ normalize <yplus_inj #H elim (ylt_yle_false … H) -H //
+| #I #L1 #L2 #V #m #_ >yminus_inj >yminus_inj <minus_n_O <minus_n_O #IH #_ normalize
+ /3 width=2 by yle_inv_monotonic_plus_dx/
+| #I #L1 #L2 #V1 #v2 #l #m #_ #_ #IH
+ <yplus_inj <yplus_inj >yplus_SO2 >yplus_SO2 >yminus_succ
+ /4 width=1 by yle_inv_succ, eq_f/
]
qed-.
| #I #L #V #J #K #W #H destruct //
| #I #L1 #L2 #V #m #_ #IHL12 #J #K #W #H1 #H2 destruct
/3 width=1 by drop_drop/
-| #I #L1 #L2 #V1 #V2 #l #m #_ #_ #_ #J #K #W #_ #_
- <plus_n_Sm #H destruct
+| #I #L1 #L2 #V1 #V2 #l #m #_ #_ #_ #J #K #W #_ #_ #H
+ elim (ysucc_inv_O_dx … H)
]
qed-.
(* Properties on append for local environments ******************************)
fact drop_O1_append_sn_le_aux: ∀L1,L2,s,l,m. ⬇[s, l, m] L1 ≡ L2 →
- l = 0 → m ≤ |L1| →
- ∀L. ⬇[s, 0, m] L @@ L1 ≡ L @@ L2.
-#L1 #L2 #s #l #m #H elim H -L1 -L2 -l -m normalize
-[2,3,4: /4 width=1 by drop_skip_lt, drop_drop, arith_b1, lt_minus_to_plus_r, monotonic_pred/ ]
-#l #m #_ #_ #H <(le_n_O_to_eq … H) -H //
+ l = yinj 0 → m ≤ |L1| →
+ ∀L. ⬇[s, yinj 0, m] L @@ L1 ≡ L @@ L2.
+#L1 #L2 #s #l #m #H elim H -L1 -L2 -l -m //
+[ #l #m #_ #_ #H <(le_n_O_to_eq … H) -H //
+| normalize /4 width=1 by drop_drop, monotonic_pred/
+| #I #L1 #L2 #V1 #V2 #l #m #_ #_ #_ #H elim (ysucc_inv_O_dx … H)
+]
qed-.
-lemma drop_O1_append_sn_le: ∀L1,L2,s,m. ⬇[s, 0, m] L1 ≡ L2 → m ≤ |L1| →
- ∀L. ⬇[s, 0, m] L @@ L1 ≡ L @@ L2.
+lemma drop_O1_append_sn_le: ∀L1,L2,s,m. ⬇[s, yinj 0, m] L1 ≡ L2 → m ≤ |L1| →
+ ∀L. ⬇[s, yinj 0, m] L @@ L1 ≡ L @@ L2.
/2 width=3 by drop_O1_append_sn_le_aux/ qed.
(* Inversion lemmas on append for local environments ************************)
-lemma drop_O1_inv_append1_ge: ∀K,L1,L2,s,m. ⬇[s, 0, m] L1 @@ L2 ≡ K →
- |L2| ≤ m → ⬇[s, 0, m - |L2|] L1 ≡ K.
+lemma drop_O1_inv_append1_ge: ∀K,L1,L2,s,m. ⬇[s, yinj 0, m] L1 @@ L2 ≡ K →
+ |L2| ≤ m → ⬇[s, yinj 0, m - |L2|] L1 ≡ K.
#K #L1 #L2 elim L2 -L2 normalize //
#L2 #I #V #IHL2 #s #m #H #H1m
elim (drop_inv_O1_pair1 … H) -H * #H2m #HL12 destruct
-[ lapply (le_n_O_to_eq … H1m) -H1m -IHL2
- >commutative_plus normalize #H destruct
+[ lapply (le_n_O_to_eq … H1m) -H1m -IHL2 <plus_n_Sm #H destruct
| <minus_plus >minus_minus_comm /3 width=1 by monotonic_pred/
]
qed-.
-lemma drop_O1_inv_append1_le: ∀K,L1,L2,s,m. ⬇[s, 0, m] L1 @@ L2 ≡ K → m ≤ |L2| →
- ∀K2. ⬇[s, 0, m] L2 ≡ K2 → K = L1 @@ K2.
+lemma drop_O1_inv_append1_le: ∀K,L1,L2,s,m. ⬇[s, yinj 0, m] L1 @@ L2 ≡ K → m ≤ |L2| →
+ ∀K2. ⬇[s, yinj 0, m] L2 ≡ K2 → K = L1 @@ K2.
#K #L1 #L2 elim L2 -L2 normalize
[ #s #m #H1 #H2 #K2 #H3 lapply (le_n_O_to_eq … H2) -H2
#H2 elim (drop_inv_atom1 … H3) -H3 #H3 #_ destruct
| #I #L #K #V #m #_ #IHLK #L2 #s2 #H
lapply (drop_inv_drop1 … H) -H /2 width=2 by/
| #I #L #K1 #T #V1 #l #m #_ #HVT1 #IHLK1 #X #s2 #H
- elim (drop_inv_skip1 … H) -H // <minus_plus_m_m #K2 #V2 #HLK2 #HVT2 #H destruct
+ elim (drop_inv_skip1 … H) -H // >ypred_succ #K2 #V2 #HLK2 #HVT2 #H destruct
>(lift_inj … HVT1 … HVT2) -HVT1 -HVT2
>(IHLK1 … HLK2) -IHLK1 -HLK2 //
]
[ #l #m #_ #L2 #s2 #m2 #H #_ elim (drop_inv_atom1 … H) -H
#H #Hm destruct
@drop_atom #H >Hm // (**) (* explicit constructor *)
-| #I #L #K #V #m #_ #IHLK #L2 #s2 #m2 #H #Hm2
- lapply (drop_inv_drop1_lt … H ?) -H /2 width=2 by ltn_to_ltO/ #HL2
- <minus_plus >minus_minus_comm /3 width=1 by monotonic_pred/
+| #I #L #K #V #m #_ #IHLK #L2 #s2 #m2 #H >yplus_O1 <yplus_inj #Hm2
+ lapply (drop_inv_drop1_lt … H ?) -H /3 width=2 by yle_inv_inj, ltn_to_ltO/ #HL2
+ lapply (yle_plus1_to_minus_inj2 … Hm2) -Hm2 #Hm2
+ <minus_plus >minus_minus_comm @IHLK //
| #I #L #K #V1 #V2 #l #m #_ #_ #IHLK #L2 #s2 #m2 #H #Hlmm2
- lapply (transitive_le 1 … Hlmm2) // #Hm2
- lapply (drop_inv_drop1_lt … H ?) -H // -Hm2 #HL2
- lapply (transitive_le (1+m) … Hlmm2) // #Hmm2
- @drop_drop_lt >minus_minus_comm /3 width=1 by lt_minus_to_plus_r, monotonic_le_minus_r, monotonic_pred/ (**) (* explicit constructor *)
+ lapply (yle_plus1_to_minus_inj2 … Hlmm2) #Hlm2m
+ lapply (ylt_yle_trans 0 … Hlm2m ?) // -Hlm2m #Hm2m
+ >yplus_succ1 in Hlmm2; #Hlmm2
+ elim (yle_inv_succ1 … Hlmm2) -Hlmm2 #Hlmm2 #Hm2
+ lapply (drop_inv_drop1_lt … H ?) -H /2 width=1 by ylt_inv_inj/ -Hm2 #HL2
+ @drop_drop_lt /2 width=1 by ylt_inv_inj/ >minus_minus_comm
+ <yminus_SO2 in Hlmm2; /2 width=1 by/
]
qed.
-
+(*
(* Note: apparently this was missing in basic_1 *)
-theorem drop_conf_be: ∀L0,L1,s1,l1,m1. ⬇[s1, l1, m1] L0 ≡ L1 →
+theorem drop_conf_be: ∀L0,L1,s1,l1,m1. ⬇[s1, yinj l1, m1] L0 ≡ L1 →
∀L2,m2. ⬇[m2] L0 ≡ L2 → l1 ≤ m2 → m2 ≤ l1 + m1 →
- ∃∃L. ⬇[s1, 0, l1 + m1 - m2] L2 ≡ L & ⬇[l1] L1 ≡ L.
+ ∃∃L. ⬇[s1, yinj 0, l1 + m1 - m2] L2 ≡ L & ⬇[l1] L1 ≡ L.
#L0 #L1 #s1 #l1 #m1 #H elim H -L0 -L1 -l1 -m1
[ #l1 #m1 #Hm1 #L2 #m2 #H #Hl1 #_ elim (drop_inv_atom1 … H) -H #H #Hm2 destruct
>(Hm2 ?) in Hl1; // -Hm2 #Hl1 <(le_n_O_to_eq … Hl1) -l1
elim (IHLK0 … HL02) -L0 /3 width=3 by drop_drop, monotonic_pred, ex2_intro/
]
qed-.
-
+*)
(* Note: apparently this was missing in basic_1 *)
theorem drop_conf_le: ∀L0,L1,s1,l1,m1. ⬇[s1, l1, m1] L0 ≡ L1 →
∀L2,s2,m2. ⬇[s2, 0, m2] L0 ≡ L2 → m2 ≤ l1 →
[ #l1 #m1 #Hm1 #L2 #s2 #m2 #H elim (drop_inv_atom1 … H) -H
#H #Hm2 #_ destruct /4 width=3 by drop_atom, ex2_intro/
| #I #K0 #V0 #L2 #s2 #m2 #H1 #H2
- lapply (le_n_O_to_eq … H2) -H2 #H destruct
+ lapply (yle_inv_O2 … H2) -H2 #H destruct
lapply (drop_inv_pair1 … H1) -H1 #H destruct /2 width=3 by drop_pair, ex2_intro/
| #I #K0 #K1 #V0 #m1 #HK01 #_ #L2 #s2 #m2 #H1 #H2
- lapply (le_n_O_to_eq … H2) -H2 #H destruct
+ lapply (yle_inv_O2 … H2) -H2 #H destruct
lapply (drop_inv_pair1 … H1) -H1 #H destruct /3 width=3 by drop_drop, ex2_intro/
| #I #K0 #K1 #V0 #V1 #l1 #m1 #HK01 #HV10 #IHK01 #L2 #s2 #m2 #H #Hm2l1
elim (drop_inv_O1_pair1 … H) -H *
[ -IHK01 -Hm2l1 #H1 #H2 destruct /3 width=5 by drop_pair, drop_skip, ex2_intro/
| -HK01 -HV10 #Hm2 #HK0L2
- elim (IHK01 … HK0L2) -IHK01 -HK0L2 /2 width=1 by monotonic_pred/
- >minus_le_minus_minus_comm /3 width=3 by drop_drop_lt, ex2_intro/
+ lapply (yle_inv_succ2 … Hm2l1) -Hm2l1 <yminus_SO2 #Hm2l1
+ elim (IHK01 … HK0L2) -IHK01 -HK0L2 //
+ <yminus_inj >yplus_minus_assoc_comm_inj /2 width=1 by yle_inj/
+ >yplus_SO2 /3 width=3 by drop_drop_lt, ex2_intro/
]
]
qed-.
| /2 width=1 by drop_gen/
| /3 width=1 by drop_drop/
| #I #L1 #L2 #V1 #V2 #l #m #_ #_ #IHL12 #L #m2 #H #Hlm2
- lapply (lt_to_le_to_lt 0 … Hlm2) // #Hm2
+ elim (yle_inv_succ1 … Hlm2) -Hlm2 #Hlm2 #Hm2
+ lapply (ylt_O … Hm2) -Hm2 #Hm2
lapply (lt_to_le_to_lt … (m + m2) Hm2 ?) // #Hmm2
lapply (drop_inv_drop1_lt … H ?) -H // #HL2
- @drop_drop_lt // >le_plus_minus /3 width=1 by monotonic_pred/
+ @drop_drop_lt // >le_plus_minus <yminus_SO2 in Hlm2; /2 width=1 by/
]
qed.
#L1 #L #s1 #l1 #m1 #H elim H -L1 -L -l1 -m1
[ #l1 #m1 #Hm1 #L2 #s2 #m2 #H #_ elim (drop_inv_atom1 … H) -H
#H #Hm2 destruct /4 width=3 by drop_atom, ex2_intro/
-| #I #K #V #L2 #s2 #m2 #HL2 #H lapply (le_n_O_to_eq … H) -H
+| #I #K #V #L2 #s2 #m2 #HL2 #H lapply (yle_inv_O2 … H) -H
#H destruct /2 width=3 by drop_pair, ex2_intro/
-| #I #L1 #L2 #V #m #_ #IHL12 #L #s2 #m2 #HL2 #H lapply (le_n_O_to_eq … H) -H
+| #I #L1 #L2 #V #m #_ #IHL12 #L #s2 #m2 #HL2 #H lapply (yle_inv_O2 … H) -H
#H destruct elim (IHL12 … HL2) -IHL12 -HL2 //
#L0 #H #HL0 lapply (drop_inv_O2 … H) -H #H destruct
/3 width=5 by drop_pair, drop_drop, ex2_intro/
elim (drop_inv_O1_pair1 … H) -H *
[ -Hm2l -IHL12 #H1 #H2 destruct /3 width=5 by drop_pair, drop_skip, ex2_intro/
| -HL12 -HV12 #Hm2 #HL2
- elim (IHL12 … HL2) -L2 [ >minus_le_minus_minus_comm // /3 width=3 by drop_drop_lt, ex2_intro/ | /2 width=1 by monotonic_pred/ ]
+ lapply (yle_inv_succ2 … Hm2l) -Hm2l <yminus_SO2 #Hm2l
+ elim (IHL12 … HL2) -L2 //
+ <yminus_inj >yplus_minus_assoc_comm_inj /3 width=3 by drop_drop_lt, yle_inj, ex2_intro/
]
]
qed-.
(* Basic_1: was: drop_conf_lt *)
lemma drop_conf_lt: ∀L,L1,s1,l1,m1. ⬇[s1, l1, m1] L ≡ L1 →
∀I,K2,V2,s2,m2. ⬇[s2, 0, m2] L ≡ K2.ⓑ{I}V2 →
- m2 < l1 → let l ≝ l1 - m2 - 1 in
+ m2 < l1 → let l ≝ ⫰(l1 - m2) in
∃∃K1,V1. ⬇[s2, 0, m2] L1 ≡ K1.ⓑ{I}V1 &
⬇[s1, l, m1] K2 ≡ K1 & ⬆[l, m1] V1 ≡ V2.
#L #L1 #s1 #l1 #m1 #H1 #I #K2 #V2 #s2 #m2 #H2 #Hm2l1
-elim (drop_conf_le … H1 … H2) -L /2 width=2 by lt_to_le/ #K #HL1K #HK2
-elim (drop_inv_skip1 … HK2) -HK2 /2 width=1 by lt_plus_to_minus_r/
+elim (drop_conf_le … H1 … H2) -L /2 width=2 by ylt_fwd_le/ #K #HL1K #HK2
+elim (drop_inv_skip1 … HK2) -HK2 /2 width=1 by ylt_to_minus/
#K1 #V1 #HK21 #HV12 #H destruct /2 width=5 by ex3_2_intro/
qed-.
∃∃L0,V0. ⬇[s2, 0, m2] L1 ≡ L0.ⓑ{I}V0 &
⬇[s1, l, m1] L0 ≡ L2 & ⬆[l, m1] V2 ≡ V0.
#L1 #L #s1 #l1 #m1 #HL1 #I #L2 #V2 #s2 #m2 #HL2 #Hl21
-elim (drop_trans_le … HL1 … HL2) -L /2 width=1 by lt_to_le/ #L0 #HL10 #HL02
-elim (drop_inv_skip2 … HL02) -HL02 /2 width=1 by lt_plus_to_minus_r/ #L #V1 #HL2 #HV21 #H destruct /2 width=5 by ex3_2_intro/
+elim (drop_trans_le … HL1 … HL2) -L /2 width=1 by ylt_fwd_le/ #L0 #HL10 #HL02
+elim (drop_inv_skip2 … HL02) -HL02 /2 width=1 by ylt_to_minus/
+#L #V1 #HL2 #HV21 #H destruct /2 width=5 by ex3_2_intro/
qed-.
lemma drop_trans_ge_comm: ∀L1,L,L2,s1,l1,m1,m2.
elim (le_or_ge m1 m2) #Hm
[ lapply (drop_conf_ge … HLK1 … HLK2 ?)
| lapply (drop_conf_ge … HLK2 … HLK1 ?)
-] -HLK1 -HLK2 // #HK
+] -HLK1 -HLK2 /2 width=1 by yle_inj/ #HK
lapply (drop_fwd_length_minus2 … HK) #H
elim (discr_minus_x_xy … H) -H
[1,3: normalize <plus_n_Sm #H destruct ]
(* Advanced forward lemmas **************************************************)
-lemma drop_fwd_be: ∀L,K,s,l,m,i. ⬇[s, l, m] L ≡ K → |K| ≤ i → i < l → |L| ≤ i.
+lemma drop_fwd_be: ∀L,K,s,l,m,i. ⬇[s, l, m] L ≡ K → |K| ≤ i → yinj i < l → |L| ≤ i.
#L #K #s #l #m #i #HLK #HK #Hl elim (lt_or_ge i (|L|)) //
#HL elim (drop_O1_lt (Ⓕ) … HL) #I #K0 #V #HLK0 -HL
elim (drop_conf_lt … HLK … HLK0) // -HLK -HLK0 -Hl
[ #_ destruct >ypred_succ
/2 width=3 by drop_pair, ex2_intro/
| lapply (ylt_inv_O1 i ?) /2 width=1 by ylt_inj/
- #H <H -H #H lapply (ylt_inv_succ … H) -H
+ #H <H -H #H lapply (ylt_inv_succ … H) -H <yminus_SO2
#Him elim (IHL12 … HLK1) -IHL12 -HLK1 // -Him
>yminus_succ <yminus_inj /3 width=3 by drop_drop_lt, ex2_intro/
]
qed.
lemma fqu_lref_S_lt: ∀I,G,L,V,i. 0 < i → ⦃G, L.ⓑ{I}V, #i⦄ ⊐ ⦃G, L, #(i-1)⦄.
-/3 width=3 by fqu_drop, drop_drop, lift_lref_ge_minus/
+/4 width=3 by fqu_drop, drop_drop, lift_lref_ge_minus, yle_inj/
qed.
(* Basic forward lemmas *****************************************************)
(* *)
(**************************************************************************)
+include "ground_2/ynat/ynat_plus.ma".
include "basic_2/notation/relations/rlift_4.ma".
include "basic_2/grammar/term_weight.ma".
include "basic_2/grammar/term_simple.ma".
(* Basic_1: includes:
lift_sort lift_lref_lt lift_lref_ge lift_bind lift_flat
*)
-inductive lift: relation4 nat nat term term ≝
+inductive lift: relation4 ynat nat term term ≝
| lift_sort : ∀k,l,m. lift l m (⋆k) (⋆k)
-| lift_lref_lt: ∀i,l,m. i < l → lift l m (#i) (#i)
-| lift_lref_ge: ∀i,l,m. l ≤ i → lift l m (#i) (#(i + m))
+| lift_lref_lt: ∀i,l,m. yinj i < l → lift l m (#i) (#i)
+| lift_lref_ge: ∀i,l,m. l ≤ yinj i → lift l m (#i) (#(i + m))
| lift_gref : ∀p,l,m. lift l m (§p) (§p)
| lift_bind : ∀a,I,V1,V2,T1,T2,l,m.
- lift l m V1 V2 → lift (l + 1) m T1 T2 →
+ lift l m V1 V2 → lift (⫯l) m T1 T2 →
lift l m (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2)
| lift_flat : ∀I,V1,V2,T1,T2,l,m.
lift l m V1 V2 → lift l m T1 T2 →
lemma lift_inv_O2: ∀l,T1,T2. ⬆[l, 0] T1 ≡ T2 → T1 = T2.
/2 width=4 by lift_inv_O2_aux/ qed-.
-fact lift_inv_sort1_aux: ∀l,m,T1,T2. ⬆[l,m] T1 ≡ T2 → ∀k. T1 = ⋆k → T2 = ⋆k.
+fact lift_inv_sort1_aux: ∀l,m,T1,T2. ⬆[l, m] T1 ≡ T2 → ∀k. T1 = ⋆k → T2 = ⋆k.
#l #m #T1 #T2 * -l -m -T1 -T2 //
[ #i #l #m #_ #k #H destruct
| #a #I #V1 #V2 #T1 #T2 #l #m #_ #_ #k #H destruct
]
qed-.
-lemma lift_inv_sort1: ∀l,m,T2,k. ⬆[l,m] ⋆k ≡ T2 → T2 = ⋆k.
+lemma lift_inv_sort1: ∀l,m,T2,k. ⬆[l, m] ⋆k ≡ T2 → T2 = ⋆k.
/2 width=5 by lift_inv_sort1_aux/ qed-.
-fact lift_inv_lref1_aux: ∀l,m,T1,T2. ⬆[l,m] T1 ≡ T2 → ∀i. T1 = #i →
+fact lift_inv_lref1_aux: ∀l,m,T1,T2. ⬆[l, m] T1 ≡ T2 → ∀i. T1 = #i →
(i < l ∧ T2 = #i) ∨ (l ≤ i ∧ T2 = #(i + m)).
#l #m #T1 #T2 * -l -m -T1 -T2
[ #k #l #m #i #H destruct
-| #j #l #m #Hj #i #Hi destruct /3 width=1 by or_introl, conj/
-| #j #l #m #Hj #i #Hi destruct /3 width=1 by or_intror, conj/
+| #j #l #m #Hj #i #Hi destruct /3 width=1 by or_introl,conj/
+| #j #l #m #Hj #i #Hi destruct /3 width=1 by or_intror,conj/
| #p #l #m #i #H destruct
| #a #I #V1 #V2 #T1 #T2 #l #m #_ #_ #i #H destruct
| #I #V1 #V2 #T1 #T2 #l #m #_ #_ #i #H destruct
]
qed-.
-lemma lift_inv_lref1: ∀l,m,T2,i. ⬆[l,m] #i ≡ T2 →
+lemma lift_inv_lref1: ∀l,m,T2,i. ⬆[l, m] #i ≡ T2 →
(i < l ∧ T2 = #i) ∨ (l ≤ i ∧ T2 = #(i + m)).
/2 width=3 by lift_inv_lref1_aux/ qed-.
-lemma lift_inv_lref1_lt: ∀l,m,T2,i. ⬆[l,m] #i ≡ T2 → i < l → T2 = #i.
+lemma lift_inv_lref1_lt: ∀l,m,T2,i. ⬆[l, m] #i ≡ T2 → i < l → T2 = #i.
#l #m #T2 #i #H elim (lift_inv_lref1 … H) -H * //
-#Hli #_ #Hil lapply (le_to_lt_to_lt … Hli Hil) -Hli -Hil #Hll
-elim (lt_refl_false … Hll)
+#Hli #_ #Hil elim (ylt_yle_false … Hli) -Hli //
qed-.
-lemma lift_inv_lref1_ge: ∀l,m,T2,i. ⬆[l,m] #i ≡ T2 → l ≤ i → T2 = #(i + m).
+lemma lift_inv_lref1_ge: ∀l,m,T2,i. ⬆[l, m] #i ≡ T2 → l ≤ i → T2 = #(i + m).
#l #m #T2 #i #H elim (lift_inv_lref1 … H) -H * //
-#Hil #_ #Hli lapply (le_to_lt_to_lt … Hli Hil) -Hli -Hil #Hll
-elim (lt_refl_false … Hll)
+#Hil #_ #Hli elim (ylt_yle_false … Hli) -Hli //
qed-.
-fact lift_inv_gref1_aux: ∀l,m,T1,T2. ⬆[l,m] T1 ≡ T2 → ∀p. T1 = §p → T2 = §p.
+fact lift_inv_gref1_aux: ∀l,m,T1,T2. ⬆[l, m] T1 ≡ T2 → ∀p. T1 = §p → T2 = §p.
#l #m #T1 #T2 * -l -m -T1 -T2 //
[ #i #l #m #_ #k #H destruct
| #a #I #V1 #V2 #T1 #T2 #l #m #_ #_ #k #H destruct
]
qed-.
-lemma lift_inv_gref1: ∀l,m,T2,p. ⬆[l,m] §p ≡ T2 → T2 = §p.
+lemma lift_inv_gref1: ∀l,m,T2,p. ⬆[l, m] §p ≡ T2 → T2 = §p.
/2 width=5 by lift_inv_gref1_aux/ qed-.
-fact lift_inv_bind1_aux: ∀l,m,T1,T2. ⬆[l,m] T1 ≡ T2 →
- ∀a,I,V1,U1. T1 = ⓑ{a,I} V1.U1 →
- ∃∃V2,U2. ⬆[l,m] V1 ≡ V2 & ⬆[l+1,m] U1 ≡ U2 &
- T2 = ⓑ{a,I} V2. U2.
+fact lift_inv_bind1_aux: ∀l,m,T1,T2. ⬆[l, m] T1 ≡ T2 →
+ ∀a,I,V1,U1. T1 = ⓑ{a,I}V1.U1 →
+ ∃∃V2,U2. ⬆[l, m] V1 ≡ V2 & ⬆[⫯l, m] U1 ≡ U2 &
+ T2 = ⓑ{a,I}V2.U2.
#l #m #T1 #T2 * -l -m -T1 -T2
[ #k #l #m #a #I #V1 #U1 #H destruct
| #i #l #m #_ #a #I #V1 #U1 #H destruct
]
qed-.
-lemma lift_inv_bind1: ∀l,m,T2,a,I,V1,U1. ⬆[l,m] ⓑ{a,I} V1. U1 ≡ T2 →
- ∃∃V2,U2. ⬆[l,m] V1 ≡ V2 & ⬆[l+1,m] U1 ≡ U2 &
- T2 = ⓑ{a,I} V2. U2.
+lemma lift_inv_bind1: ∀l,m,T2,a,I,V1,U1. ⬆[l, m] ⓑ{a,I}V1.U1 ≡ T2 →
+ ∃∃V2,U2. ⬆[l, m] V1 ≡ V2 & ⬆[⫯l, m] U1 ≡ U2 &
+ T2 = ⓑ{a,I}V2.U2.
/2 width=3 by lift_inv_bind1_aux/ qed-.
-fact lift_inv_flat1_aux: ∀l,m,T1,T2. ⬆[l,m] T1 ≡ T2 →
- ∀I,V1,U1. T1 = ⓕ{I} V1.U1 →
- ∃∃V2,U2. ⬆[l,m] V1 ≡ V2 & ⬆[l,m] U1 ≡ U2 &
- T2 = ⓕ{I} V2. U2.
+fact lift_inv_flat1_aux: ∀l,m,T1,T2. ⬆[l, m] T1 ≡ T2 →
+ ∀I,V1,U1. T1 = ⓕ{I}V1.U1 →
+ ∃∃V2,U2. ⬆[l, m] V1 ≡ V2 & ⬆[l, m] U1 ≡ U2 &
+ T2 = ⓕ{I}V2.U2.
#l #m #T1 #T2 * -l -m -T1 -T2
[ #k #l #m #I #V1 #U1 #H destruct
| #i #l #m #_ #I #V1 #U1 #H destruct
]
qed-.
-lemma lift_inv_flat1: ∀l,m,T2,I,V1,U1. ⬆[l,m] ⓕ{I} V1. U1 ≡ T2 →
- ∃∃V2,U2. ⬆[l,m] V1 ≡ V2 & ⬆[l,m] U1 ≡ U2 &
- T2 = ⓕ{I} V2. U2.
+lemma lift_inv_flat1: ∀l,m,T2,I,V1,U1. ⬆[l, m] ⓕ{I}V1.U1 ≡ T2 →
+ ∃∃V2,U2. ⬆[l, m] V1 ≡ V2 & ⬆[l, m] U1 ≡ U2 &
+ T2 = ⓕ{I}V2.U2.
/2 width=3 by lift_inv_flat1_aux/ qed-.
-fact lift_inv_sort2_aux: ∀l,m,T1,T2. ⬆[l,m] T1 ≡ T2 → ∀k. T2 = ⋆k → T1 = ⋆k.
+fact lift_inv_sort2_aux: ∀l,m,T1,T2. ⬆[l, m] T1 ≡ T2 → ∀k. T2 = ⋆k → T1 = ⋆k.
#l #m #T1 #T2 * -l -m -T1 -T2 //
[ #i #l #m #_ #k #H destruct
| #a #I #V1 #V2 #T1 #T2 #l #m #_ #_ #k #H destruct
qed-.
(* Basic_1: was: lift_gen_sort *)
-lemma lift_inv_sort2: ∀l,m,T1,k. ⬆[l,m] T1 ≡ ⋆k → T1 = ⋆k.
+lemma lift_inv_sort2: ∀l,m,T1,k. ⬆[l, m] T1 ≡ ⋆k → T1 = ⋆k.
/2 width=5 by lift_inv_sort2_aux/ qed-.
-fact lift_inv_lref2_aux: ∀l,m,T1,T2. ⬆[l,m] T1 ≡ T2 → ∀i. T2 = #i →
+fact lift_inv_lref2_aux: ∀l,m,T1,T2. ⬆[l, m] T1 ≡ T2 → ∀i. T2 = #i →
(i < l ∧ T1 = #i) ∨ (l + m ≤ i ∧ T1 = #(i - m)).
#l #m #T1 #T2 * -l -m -T1 -T2
[ #k #l #m #i #H destruct
| #j #l #m #Hj #i #Hi destruct /3 width=1 by or_introl, conj/
-| #j #l #m #Hj #i #Hi destruct <minus_plus_m_m /4 width=1 by monotonic_le_plus_l, or_intror, conj/
+| #j #l #m #Hj #i #Hi destruct <minus_plus_m_m /4 width=1 by monotonic_yle_plus_dx, or_intror, conj/
| #p #l #m #i #H destruct
| #a #I #V1 #V2 #T1 #T2 #l #m #_ #_ #i #H destruct
| #I #V1 #V2 #T1 #T2 #l #m #_ #_ #i #H destruct
qed-.
(* Basic_1: was: lift_gen_lref *)
-lemma lift_inv_lref2: ∀l,m,T1,i. ⬆[l,m] T1 ≡ #i →
+lemma lift_inv_lref2: ∀l,m,T1,i. ⬆[l, m] T1 ≡ #i →
(i < l ∧ T1 = #i) ∨ (l + m ≤ i ∧ T1 = #(i - m)).
/2 width=3 by lift_inv_lref2_aux/ qed-.
(* Basic_1: was: lift_gen_lref_lt *)
-lemma lift_inv_lref2_lt: ∀l,m,T1,i. ⬆[l,m] T1 ≡ #i → i < l → T1 = #i.
+lemma lift_inv_lref2_lt: ∀l,m,T1,i. ⬆[l, m] T1 ≡ #i → i < l → T1 = #i.
#l #m #T1 #i #H elim (lift_inv_lref2 … H) -H * //
-#Hli #_ #Hil lapply (le_to_lt_to_lt … Hli Hil) -Hli -Hil #Hll
-elim (lt_inv_plus_l … Hll) -Hll #Hll
-elim (lt_refl_false … Hll)
+#H #_ #Hil lapply (yle_fwd_plus_sn1 … H) -H
+#Hli elim (ylt_yle_false … Hli) -Hli //
qed-.
(* Basic_1: was: lift_gen_lref_false *)
-lemma lift_inv_lref2_be: ∀l,m,T1,i. ⬆[l,m] T1 ≡ #i →
+lemma lift_inv_lref2_be: ∀l,m,T1,i. ⬆[l, m] T1 ≡ #i →
l ≤ i → i < l + m → ⊥.
#l #m #T1 #i #H elim (lift_inv_lref2 … H) -H *
[ #H1 #_ #H2 #_ | #H2 #_ #_ #H1 ]
-lapply (le_to_lt_to_lt … H2 H1) -H2 -H1 #H
-elim (lt_refl_false … H)
+elim (ylt_yle_false … H2) -H2 //
qed-.
(* Basic_1: was: lift_gen_lref_ge *)
-lemma lift_inv_lref2_ge: ∀l,m,T1,i. ⬆[l,m] T1 ≡ #i → l + m ≤ i → T1 = #(i - m).
+lemma lift_inv_lref2_ge: ∀l,m,T1,i. ⬆[l, m] T1 ≡ #i → l + m ≤ i → T1 = #(i - m).
#l #m #T1 #i #H elim (lift_inv_lref2 … H) -H * //
-#Hil #_ #Hli lapply (le_to_lt_to_lt … Hli Hil) -Hli -Hil #Hll
-elim (lt_inv_plus_l … Hll) -Hll #Hll
-elim (lt_refl_false … Hll)
+#Hil #_ #H lapply (yle_fwd_plus_sn1 … H) -H
+#Hli elim (ylt_yle_false … Hli) -Hli //
qed-.
-fact lift_inv_gref2_aux: ∀l,m,T1,T2. ⬆[l,m] T1 ≡ T2 → ∀p. T2 = §p → T1 = §p.
+fact lift_inv_gref2_aux: ∀l,m,T1,T2. ⬆[l, m] T1 ≡ T2 → ∀p. T2 = §p → T1 = §p.
#l #m #T1 #T2 * -l -m -T1 -T2 //
[ #i #l #m #_ #k #H destruct
| #a #I #V1 #V2 #T1 #T2 #l #m #_ #_ #k #H destruct
]
qed-.
-lemma lift_inv_gref2: ∀l,m,T1,p. ⬆[l,m] T1 ≡ §p → T1 = §p.
+lemma lift_inv_gref2: ∀l,m,T1,p. ⬆[l, m] T1 ≡ §p → T1 = §p.
/2 width=5 by lift_inv_gref2_aux/ qed-.
-fact lift_inv_bind2_aux: ∀l,m,T1,T2. ⬆[l,m] T1 ≡ T2 →
- ∀a,I,V2,U2. T2 = ⓑ{a,I} V2.U2 →
- ∃∃V1,U1. ⬆[l,m] V1 ≡ V2 & ⬆[l+1,m] U1 ≡ U2 &
- T1 = ⓑ{a,I} V1. U1.
+fact lift_inv_bind2_aux: ∀l,m,T1,T2. ⬆[l, m] T1 ≡ T2 →
+ ∀a,I,V2,U2. T2 = ⓑ{a,I}V2.U2 →
+ ∃∃V1,U1. ⬆[l, m] V1 ≡ V2 & ⬆[⫯l, m] U1 ≡ U2 &
+ T1 = ⓑ{a,I}V1.U1.
#l #m #T1 #T2 * -l -m -T1 -T2
[ #k #l #m #a #I #V2 #U2 #H destruct
| #i #l #m #_ #a #I #V2 #U2 #H destruct
qed-.
(* Basic_1: was: lift_gen_bind *)
-lemma lift_inv_bind2: ∀l,m,T1,a,I,V2,U2. ⬆[l,m] T1 ≡ ⓑ{a,I} V2. U2 →
- ∃∃V1,U1. ⬆[l,m] V1 ≡ V2 & ⬆[l+1,m] U1 ≡ U2 &
- T1 = ⓑ{a,I} V1. U1.
+lemma lift_inv_bind2: ∀l,m,T1,a,I,V2,U2. ⬆[l, m] T1 ≡ ⓑ{a,I}V2.U2 →
+ ∃∃V1,U1. ⬆[l, m] V1 ≡ V2 & ⬆[⫯l, m] U1 ≡ U2 &
+ T1 = ⓑ{a,I}V1.U1.
/2 width=3 by lift_inv_bind2_aux/ qed-.
-fact lift_inv_flat2_aux: ∀l,m,T1,T2. ⬆[l,m] T1 ≡ T2 →
- ∀I,V2,U2. T2 = ⓕ{I} V2.U2 →
- ∃∃V1,U1. ⬆[l,m] V1 ≡ V2 & ⬆[l,m] U1 ≡ U2 &
- T1 = ⓕ{I} V1. U1.
+fact lift_inv_flat2_aux: ∀l,m,T1,T2. ⬆[l, m] T1 ≡ T2 →
+ ∀I,V2,U2. T2 = ⓕ{I}V2.U2 →
+ ∃∃V1,U1. ⬆[l, m] V1 ≡ V2 & ⬆[l, m] U1 ≡ U2 &
+ T1 = ⓕ{I}V1.U1.
#l #m #T1 #T2 * -l -m -T1 -T2
[ #k #l #m #I #V2 #U2 #H destruct
| #i #l #m #_ #I #V2 #U2 #H destruct
qed-.
(* Basic_1: was: lift_gen_flat *)
-lemma lift_inv_flat2: ∀l,m,T1,I,V2,U2. ⬆[l,m] T1 ≡ ⓕ{I} V2. U2 →
- ∃∃V1,U1. ⬆[l,m] V1 ≡ V2 & ⬆[l,m] U1 ≡ U2 &
- T1 = ⓕ{I} V1. U1.
+lemma lift_inv_flat2: ∀l,m,T1,I,V2,U2. ⬆[l, m] T1 ≡ ⓕ{I}V2.U2 →
+ ∃∃V1,U1. ⬆[l, m] V1 ≡ V2 & ⬆[l, m] U1 ≡ U2 &
+ T1 = ⓕ{I}V1.U1.
/2 width=3 by lift_inv_flat2_aux/ qed-.
-lemma lift_inv_pair_xy_x: ∀l,m,I,V,T. ⬆[l, m] ②{I} V. T ≡ V → ⊥.
+lemma lift_inv_Y1: ∀T1,T2,m. ⬆[∞, m] T1 ≡ T2 → T1 = T2.
+#T1 elim T1 -T1 *
+[ #k #X #m #H lapply (lift_inv_sort1 … H) -H //
+| #i #X #m #H lapply (lift_inv_lref1_lt … H ?) -H //
+| #p #X #m #H lapply (lift_inv_gref1 … H) -H //
+| #a #I #V1 #T1 #IHV1 #IHT1 #X #m #H elim (lift_inv_bind1 … H) -H
+ #V2 #T2 #HV12 #HT12 #H destruct /3 width=2 by eq_f2/
+| #I #V1 #T1 #IHV1 #IHT1 #X #m #H elim (lift_inv_flat1 … H) -H
+ #V2 #T2 #HV12 #HT12 #H destruct /3 width=2 by eq_f2/
+]
+qed-.
+
+lemma lift_inv_pair_xy_x: ∀l,m,I,V,T. ⬆[l, m] ②{I}V.T ≡ V → ⊥.
#l #m #J #V elim V -V
[ * #i #T #H
[ lapply (lift_inv_sort2 … H) -H #H destruct
qed-.
(* Basic_1: was: thead_x_lift_y_y *)
-lemma lift_inv_pair_xy_y: ∀I,T,V,l,m. ⬆[l, m] ②{I} V. T ≡ T → ⊥.
+lemma lift_inv_pair_xy_y: ∀I,T,V,l,m. ⬆[l, m] ②{I}V.T ≡ T → ⊥.
#J #T elim T -T
[ * #i #V #l #m #H
[ lapply (lift_inv_sort2 … H) -H #H destruct
(* Basic forward lemmas *****************************************************)
-lemma lift_fwd_pair1: ∀I,T2,V1,U1,l,m. ⬆[l,m] ②{I}V1.U1 ≡ T2 →
- ∃∃V2,U2. ⬆[l,m] V1 ≡ V2 & T2 = ②{I}V2.U2.
+lemma lift_fwd_pair1: ∀I,T2,V1,U1,l,m. ⬆[l, m] ②{I}V1.U1 ≡ T2 →
+ ∃∃V2,U2. ⬆[l, m] V1 ≡ V2 & T2 = ②{I}V2.U2.
* [ #a ] #I #T2 #V1 #U1 #l #m #H
[ elim (lift_inv_bind1 … H) -H /2 width=4 by ex2_2_intro/
| elim (lift_inv_flat1 … H) -H /2 width=4 by ex2_2_intro/
]
qed-.
-lemma lift_fwd_pair2: ∀I,T1,V2,U2,l,m. ⬆[l,m] T1 ≡ ②{I}V2.U2 →
- ∃∃V1,U1. ⬆[l,m] V1 ≡ V2 & T1 = ②{I}V1.U1.
+lemma lift_fwd_pair2: ∀I,T1,V2,U2,l,m. ⬆[l, m] T1 ≡ ②{I}V2.U2 →
+ ∃∃V1,U1. ⬆[l, m] V1 ≡ V2 & T1 = ②{I}V1.U1.
* [ #a ] #I #T1 #V2 #U2 #l #m #H
[ elim (lift_inv_bind2 … H) -H /2 width=4 by ex2_2_intro/
| elim (lift_inv_flat2 … H) -H /2 width=4 by ex2_2_intro/
(* Basic properties *********************************************************)
(* Basic_1: was: lift_lref_gt *)
-lemma lift_lref_ge_minus: ∀l,m,i. l + m ≤ i → ⬆[l, m] #(i - m) ≡ #i.
-#l #m #i #H >(plus_minus_m_m i m) in ⊢ (? ? ? ? %); /3 width=2 by lift_lref_ge, le_plus_to_minus_r, le_plus_b/
+lemma lift_lref_ge_minus: ∀l,m,i. l + yinj m ≤ yinj i → ⬆[l, m] #(i - m) ≡ #i.
+#l #m #i #H >(plus_minus_m_m i m) in ⊢ (? ? ? ? %);
+elim (yle_inv_plus_inj2 … H) -H #Hlim #H
+lapply (yle_inv_inj … H) -H /2 width=1 by lift_lref_ge/
qed.
-lemma lift_lref_ge_minus_eq: ∀l,m,i,j. l + m ≤ i → j = i - m → ⬆[l, m] #j ≡ #i.
+lemma lift_lref_ge_minus_eq: ∀l,m,i,j. l + yinj m ≤ yinj i → j = i - m → ⬆[l, m] #j ≡ #i.
/2 width=1 by lift_lref_ge_minus/ qed-.
(* Basic_1: was: lift_r *)
lemma lift_refl: ∀T,l. ⬆[l, 0] T ≡ T.
#T elim T -T
-[ * #i // #l elim (lt_or_ge i l) /2 width=1 by lift_lref_lt, lift_lref_ge/
+[ * #i // #l elim (ylt_split i l) /2 width=1 by lift_lref_lt, lift_lref_ge/
| * /2 width=1 by lift_bind, lift_flat/
]
qed.
-lemma lift_total: ∀T1,l,m. ∃T2. ⬆[l,m] T1 ≡ T2.
+(* Basic_2b: first lemma *)
+lemma lift_Y1: ∀T,m. ⬆[∞, m] T ≡ T.
+#T elim T -T * /2 width=1 by lift_lref_lt, lift_bind, lift_flat/
+qed.
+
+lemma lift_total: ∀T1,l,m. ∃T2. ⬆[l, m] T1 ≡ T2.
#T1 elim T1 -T1
[ * #i /2 width=2 by lift_sort, lift_gref, ex_intro/
- #l #m elim (lt_or_ge i l) /3 width=2 by lift_lref_lt, lift_lref_ge, ex_intro/
+ #l #m elim (ylt_split i l) /3 width=2 by lift_lref_lt, lift_lref_ge, ex_intro/
| * [ #a ] #I #V1 #T1 #IHV1 #IHT1 #l #m
elim (IHV1 l m) -IHV1 #V2 #HV12
- [ elim (IHT1 (l+1) m) -IHT1 /3 width=2 by lift_bind, ex_intro/
+ [ elim (IHT1 (⫯l) m) -IHT1 /3 width=2 by lift_bind, ex_intro/
| elim (IHT1 l m) -IHT1 /3 width=2 by lift_flat, ex_intro/
]
]
(* Basic_1: was: lift_free (right to left) *)
lemma lift_split: ∀l1,m2,T1,T2. ⬆[l1, m2] T1 ≡ T2 →
- ∀l2,m1. l1 ≤ l2 → l2 ≤ l1 + m1 → m1 ≤ m2 →
+ ∀l2,m1. l1 ≤ l2 → l2 ≤ l1 + yinj m1 → m1 ≤ m2 →
∃∃T. ⬆[l1, m1] T1 ≡ T & ⬆[l2, m2 - m1] T ≡ T2.
#l1 #m2 #T1 #T2 #H elim H -l1 -m2 -T1 -T2
[ /3 width=3 by lift_sort, ex2_intro/
| #i #l1 #m2 #Hil1 #l2 #m1 #Hl12 #_ #_
- lapply (lt_to_le_to_lt … Hil1 Hl12) -Hl12 #Hil2 /4 width=3 by lift_lref_lt, ex2_intro/
+ lapply (ylt_yle_trans … Hl12 Hil1) -Hl12 #Hil2 /4 width=3 by lift_lref_lt, ex2_intro/
| #i #l1 #m2 #Hil1 #l2 #m1 #_ #Hl21 #Hm12
- lapply (transitive_le … (i+m1) Hl21 ?) /2 width=1 by monotonic_le_plus_l/ -Hl21 #Hl21
+ lapply (yle_trans … Hl21 (i+m1) ?) /2 width=1 by monotonic_yle_plus_dx/ -Hl21 #Hl21
>(plus_minus_m_m m2 m1 ?) /3 width=3 by lift_lref_ge, ex2_intro/
| /3 width=3 by lift_gref, ex2_intro/
| #a #I #V1 #V2 #T1 #T2 #l1 #m2 #_ #_ #IHV #IHT #l2 #m1 #Hl12 #Hl21 #Hm12
elim (IHV … Hl12 Hl21 Hm12) -IHV #V0 #HV0a #HV0b
- elim (IHT (l2+1) … ? ? Hm12) /3 width=5 by lift_bind, le_S_S, ex2_intro/
+ elim (IHT (⫯l2) … ? ? Hm12) /3 width=5 by lift_bind, yle_succ, ex2_intro/
| #I #V1 #V2 #T1 #T2 #l1 #m2 #_ #_ #IHV #IHT #l2 #m1 #Hl12 #Hl21 #Hm12
elim (IHV … Hl12 Hl21 Hm12) -IHV #V0 #HV0a #HV0b
elim (IHT l2 … ? ? Hm12) /3 width=5 by lift_flat, ex2_intro/
qed.
(* Basic_1: was only: dnf_dec2 dnf_dec *)
-lemma is_lift_dec: ∀T2,l,m. Decidable (∃T1. ⬆[l,m] T1 ≡ T2).
+lemma is_lift_dec: ∀T2,l,m. Decidable (∃T1. ⬆[l, m] T1 ≡ T2).
#T1 elim T1 -T1
[ * [1,3: /3 width=2 by lift_sort, lift_gref, ex_intro, or_introl/ ] #i #l #m
- elim (lt_or_ge i l) #Hli
+ elim (ylt_split i l) #Hli
[ /4 width=3 by lift_lref_lt, ex_intro, or_introl/
- | elim (lt_or_ge i (l + m)) #Hilm
+ | elim (ylt_split i (l + m)) #Hilm
[ @or_intror * #T1 #H elim (lift_inv_lref2_be … H Hli Hilm)
| -Hli /4 width=2 by lift_lref_ge_minus, ex_intro, or_introl/
]
]
| * [ #a ] #I #V2 #T2 #IHV2 #IHT2 #l #m
[ elim (IHV2 l m) -IHV2
- [ * #V1 #HV12 elim (IHT2 (l+1) m) -IHT2
+ [ * #V1 #HV12 elim (IHT2 (⫯l) m) -IHT2
[ * #T1 #HT12 @or_introl /3 width=2 by lift_bind, ex_intro/
| -V1 #HT2 @or_intror * #X #H
elim (lift_inv_bind2 … H) -H /3 width=2 by ex_intro/
(* Main properties ***********************************************************)
(* Basic_1: was: lift_inj *)
-theorem lift_inj: ∀l,m,T1,U. ⬆[l,m] T1 ≡ U → ∀T2. ⬆[l,m] T2 ≡ U → T1 = T2.
+theorem lift_inj: ∀l,m,T1,U. ⬆[l, m] T1 ≡ U → ∀T2. ⬆[l, m] T2 ≡ U → T1 = T2.
#l #m #T1 #U #H elim H -l -m -T1 -U
[ #k #l #m #X #HX
lapply (lift_inv_sort2 … HX) -HX //
| #i #l #m #Hil #X #HX
lapply (lift_inv_lref2_lt … HX ?) -HX //
| #i #l #m #Hli #X #HX
- lapply (lift_inv_lref2_ge … HX ?) -HX /2 width=1 by monotonic_le_plus_l/
+ lapply (lift_inv_lref2_ge … HX ?) -HX /2 width=1 by monotonic_yle_plus_dx/
| #p #l #m #X #HX
lapply (lift_inv_gref2 … HX) -HX //
| #a #I #V1 #V2 #T1 #T2 #l #m #_ #_ #IHV12 #IHT12 #X #HX
[ #k #l1 #m1 #l2 #m2 #T2 #Hk #Hl12
lapply (lift_inv_sort2 … Hk) -Hk #Hk destruct /3 width=3 by lift_sort, ex2_intro/
| #i #l1 #m1 #Hil1 #l2 #m2 #T2 #Hi #Hl12
- lapply (lt_to_le_to_lt … Hil1 Hl12) -Hl12 #Hil2
- lapply (lift_inv_lref2_lt … Hi ?) -Hi /3 width=3 by lift_lref_lt, lt_plus_to_minus_r, lt_to_le_to_lt, ex2_intro/
+ lapply (ylt_yle_trans … Hl12 Hil1) -Hl12 #Hil2
+ lapply (lift_inv_lref2_lt … Hi ?) -Hi /3 width=3 by lift_lref_lt, ylt_plus_dx1_trans, ex2_intro/
| #i #l1 #m1 #Hil1 #l2 #m2 #T2 #Hi #Hl12
- elim (lift_inv_lref2 … Hi) -Hi * #Hil2 #H destruct
- [ -Hl12 lapply (lt_plus_to_lt_l … Hil2) -Hil2 #Hil2 /3 width=3 by lift_lref_lt, lift_lref_ge, ex2_intro/
- | -Hil1 >plus_plus_comm_23 in Hil2; #H lapply (le_plus_to_le_r … H) -H #H
- elim (le_inv_plus_l … H) -H #Hilm2 #Hm2i
- lapply (transitive_le … Hl12 Hilm2) -Hl12 #Hl12
+ elim (lift_inv_lref2 … Hi) -Hi * <yplus_inj #Hil2 #H destruct
+ [ -Hl12 lapply (ylt_inv_monotonic_plus_dx … Hil2) -Hil2 #Hil2 /3 width=3 by lift_lref_lt, lift_lref_ge, ex2_intro/
+ | -Hil1 >yplus_comm_23 in Hil2; #H lapply ( yle_inv_monotonic_plus_dx … H) -H #H
+ elim (yle_inv_plus_inj2 … H) -H >yminus_inj #Hl2im2 #H
+ lapply (yle_inv_inj … H) -H #Hm2i
+ lapply (yle_trans … Hl12 … Hl2im2) -Hl12 #Hl1im2
>le_plus_minus_comm // >(plus_minus_m_m i m2) in ⊢ (? ? ? %);
- /4 width=3 by lift_lref_ge, ex2_intro/
+ /3 width=3 by lift_lref_ge, ex2_intro/
]
| #p #l1 #m1 #l2 #m2 #T2 #Hk #Hl12
lapply (lift_inv_gref2 … Hk) -Hk #Hk destruct /3 width=3 by lift_gref, ex2_intro/
| #a #I #W1 #W #U1 #U #l1 #m1 #_ #_ #IHW #IHU #l2 #m2 #T2 #H #Hl12
lapply (lift_inv_bind2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct
elim (IHW … HW2) // -IHW -HW2 #W0 #HW2 #HW1
- >plus_plus_comm_23 in HU2; #HU2 elim (IHU … HU2) /3 width=5 by lift_bind, le_S_S, ex2_intro/
+ <yplus_succ1 in HU2; #HU2 elim (IHU … HU2) /3 width=5 by yle_succ, lift_bind, ex2_intro/
| #I #W1 #W #U1 #U #l1 #m1 #_ #_ #IHW #IHU #l2 #m2 #T2 #H #Hl12
lapply (lift_inv_flat2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct
elim (IHW … HW2) // -IHW -HW2 #W0 #HW2 #HW1
(* Note: apparently this was missing in basic_1 *)
theorem lift_div_be: ∀l1,m1,T1,T. ⬆[l1, m1] T1 ≡ T →
- ∀m,m2,T2. ⬆[l1 + m, m2] T2 ≡ T →
+ ∀m,m2,T2. ⬆[l1 + yinj m, m2] T2 ≡ T →
m ≤ m1 → m1 ≤ m + m2 →
∃∃T0. ⬆[l1, m] T0 ≡ T2 & ⬆[l1, m + m2 - m1] T0 ≡ T1.
#l1 #m1 #T1 #T #H elim H -l1 -m1 -T1 -T
[ #k #l1 #m1 #m #m2 #T2 #H >(lift_inv_sort2 … H) -H /2 width=3 by lift_sort, ex2_intro/
| #i #l1 #m1 #Hil1 #m #m2 #T2 #H #Hm1 #Hm1m2
- >(lift_inv_lref2_lt … H) -H /3 width=3 by lift_lref_lt, lt_plus_to_minus_r, lt_to_le_to_lt, ex2_intro/
+ >(lift_inv_lref2_lt … H) -H /3 width=3 by ylt_plus_dx1_trans, lift_lref_lt, ex2_intro/
| #i #l1 #m1 #Hil1 #m #m2 #T2 #H #Hm1 #Hm1m2
- elim (lt_or_ge (i+m1) (l1+m+m2)) #Him1l1m2
- [ elim (lift_inv_lref2_be … H) -H /2 width=1 by le_plus/
+ elim (ylt_split (i+m1) (l1+m+m2)) #H0
+ [ elim (lift_inv_lref2_be … H) -H /3 width=2 by monotonic_yle_plus, yle_inj/
| >(lift_inv_lref2_ge … H ?) -H //
- lapply (le_plus_to_minus … Him1l1m2) #Hl1m21i
- elim (le_inv_plus_l … Him1l1m2) -Him1l1m2 #Hl1m12 #Hm2im1
- @ex2_intro [2: /2 width=1 by lift_lref_ge_minus/ | skip ] -Hl1m12
- @lift_lref_ge_minus_eq [ >plus_minus_associative // | /2 width=1 by minus_le_minus_minus_comm/ ]
+ lapply (yle_plus2_to_minus_inj2 … H0) #Hl1m21i
+ elim (yle_inv_plus_inj2 … H0) -H0 #Hl1m12 #Hm2im1
+ @ex2_intro [2: /2 width=1 by lift_lref_ge_minus/ | skip ]
+ @lift_lref_ge_minus_eq
+ [ <yminus_inj <yplus_inj >yplus_minus_assoc_inj /2 width=1 by yle_inj/
+ | /2 width=1 by minus_le_minus_minus_comm/
+ ]
]
| #p #l1 #m1 #m #m2 #T2 #H >(lift_inv_gref2 … H) -H /2 width=3 by lift_gref, ex2_intro/
| #a #I #V1 #V #T1 #T #l1 #m1 #_ #_ #IHV1 #IHT1 #m #m2 #X #H #Hm1 #Hm1m2
- elim (lift_inv_bind2 … H) -H #V2 #T2 #HV2 #HT2 #H destruct
- elim (IHV1 … HV2) -V // >plus_plus_comm_23 in HT2; #HT2
+ elim (lift_inv_bind2 … H) -H #V2 #T2 #HV2 <yplus_succ1 #HT2 #H destruct
+ elim (IHV1 … HV2) -V //
elim (IHT1 … HT2) -T /3 width=5 by lift_bind, ex2_intro/
| #I #V1 #V #T1 #T #l1 #m1 #_ #_ #IHV1 #IHT1 #m #m2 #X #H #Hm1 #Hm1m2
elim (lift_inv_flat2 … H) -H #V2 #T2 #HV2 #HT2 #H destruct
[ #k #l1 #m1 #l2 #m2 #T2 #HT2 #_ #_
>(lift_inv_sort1 … HT2) -HT2 //
| #i #l1 #m1 #Hil1 #l2 #m2 #T2 #HT2 #Hl12 #_
- lapply (lt_to_le_to_lt … Hil1 Hl12) -Hl12 #Hil2
+ lapply (ylt_yle_trans … Hl12 Hil1) -Hl12 #Hil2
lapply (lift_inv_lref1_lt … HT2 Hil2) /2 width=1 by lift_lref_lt/
| #i #l1 #m1 #Hil1 #l2 #m2 #T2 #HT2 #_ #Hl21
lapply (lift_inv_lref1_ge … HT2 ?) -HT2
- [ @(transitive_le … Hl21 ?) -Hl21 /2 width=1 by monotonic_le_plus_l/
+ [ @(yle_trans … Hl21) -Hl21 /2 width=1 by monotonic_yle_plus_dx/
| -Hl21 /2 width=1 by lift_lref_ge/
]
| #p #l1 #m1 #l2 #m2 #T2 #HT2 #_ #_
>(lift_inv_gref1 … HT2) -HT2 //
| #a #I #V1 #V2 #T1 #T2 #l1 #m1 #_ #_ #IHV12 #IHT12 #l2 #m2 #X #HX #Hl12 #Hl21
- elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct
+ elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct
lapply (IHV12 … HV20 ? ?) // -IHV12 -HV20 #HV10
- lapply (IHT12 … HT20 ? ?) /2 width=1 by lift_bind, le_S_S/ (**) (* full auto a bit slow *)
+ lapply (IHT12 … HT20 ? ?) /2 width=1 by lift_bind, yle_succ/ (**) (* full auto a bit slow *)
| #I #V1 #V2 #T1 #T2 #l1 #m1 #_ #_ #IHV12 #IHT12 #l2 #m2 #X #HX #Hl12 #Hl21
elim (lift_inv_flat1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct
lapply (IHV12 … HV20 ? ?) // -IHV12 -HV20 #HV10
[ #k #l1 #m1 #l2 #m2 #X #HX #_
>(lift_inv_sort1 … HX) -HX /2 width=3 by lift_sort, ex2_intro/
| #i #l1 #m1 #Hil1 #l2 #m2 #X #HX #_
- lapply (lt_to_le_to_lt … (l1+m2) Hil1 ?) // #Him2
- elim (lift_inv_lref1 … HX) -HX * #Hil2 #HX destruct /4 width=3 by lift_lref_ge_minus, lift_lref_lt, lt_minus_to_plus, monotonic_le_plus_l, ex2_intro/
+ lapply (ylt_yle_trans … (l1+m2) ? Hil1) // #Him2
+ elim (lift_inv_lref1 … HX) -HX * #Hil2 #HX destruct
+ /4 width=3 by monotonic_ylt_plus_dx, monotonic_yle_plus_dx, lift_lref_ge_minus, lift_lref_lt, ex2_intro/
| #i #l1 #m1 #Hil1 #l2 #m2 #X #HX #Hl21
- lapply (transitive_le … Hl21 Hil1) -Hl21 #Hil2
- lapply (lift_inv_lref1_ge … HX ?) -HX /2 width=3 by transitive_le/ #HX destruct
- >plus_plus_comm_23 /4 width=3 by lift_lref_ge_minus, lift_lref_ge, monotonic_le_plus_l, ex2_intro/
+ lapply (yle_trans … Hl21 … Hil1) -Hl21 #Hil2
+ lapply (lift_inv_lref1_ge … HX ?) -HX /2 width=3 by yle_plus_dx1_trans/ #HX destruct
+ >plus_plus_comm_23 /4 width=3 by monotonic_yle_plus_dx, lift_lref_ge_minus, lift_lref_ge, ex2_intro/
| #p #l1 #m1 #l2 #m2 #X #HX #_
>(lift_inv_gref1 … HX) -HX /2 width=3 by lift_gref, ex2_intro/
| #a #I #V1 #V2 #T1 #T2 #l1 #m1 #_ #_ #IHV12 #IHT12 #l2 #m2 #X #HX #Hl21
elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct
elim (IHV12 … HV20) -IHV12 -HV20 //
- elim (IHT12 … HT20) -IHT12 -HT20 /3 width=5 by lift_bind, le_S_S, ex2_intro/
+ elim (IHT12 … HT20) -IHT12 -HT20 /3 width=5 by lift_bind, yle_succ, ex2_intro/
| #I #V1 #V2 #T1 #T2 #l1 #m1 #_ #_ #IHV12 #IHT12 #l2 #m2 #X #HX #Hl21
elim (lift_inv_flat1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct
elim (IHV12 … HV20) -IHV12 -HV20 //
[ #k #l1 #m1 #l2 #m2 #X #HX #_
>(lift_inv_sort1 … HX) -HX /2 width=3 by lift_sort, ex2_intro/
| #i #l1 #m1 #Hil1 #l2 #m2 #X #HX #Hlml
- lapply (lt_to_le_to_lt … (l1+m1) Hil1 ?) // #Hil1m
- lapply (lt_to_le_to_lt … (l2-m1) Hil1 ?) /2 width=1 by le_plus_to_minus_r/ #Hil2m
- lapply (lt_to_le_to_lt … Hil1m Hlml) -Hil1m -Hlml #Hil2
+ lapply (ylt_yle_trans … (l1+m1) ? Hil1) // #Hil1m
+ lapply (ylt_yle_trans … (l2-m1) ? Hil1) /2 width=1 by yle_plus1_to_minus_inj2/ #Hil2m
+ lapply (ylt_yle_trans … Hlml Hil1m) -Hil1m -Hlml #Hil2
lapply (lift_inv_lref1_lt … HX ?) -HX // #HX destruct /3 width=3 by lift_lref_lt, ex2_intro/
| #i #l1 #m1 #Hil1 #l2 #m2 #X #HX #_
- elim (lift_inv_lref1 … HX) -HX * #Himl #HX destruct /4 width=3 by lift_lref_lt, lift_lref_ge, monotonic_le_minus_l, lt_plus_to_minus_r, transitive_le, ex2_intro/
+ elim (lift_inv_lref1 … HX) -HX * <yplus_inj #Himl #HX destruct
+ [ /4 width=3 by lift_lref_lt, lift_lref_ge, ylt_plus1_to_minus_inj2, ex2_intro/
+ | /4 width=3 by lift_lref_ge, yle_plus_dx1_trans, monotonic_yle_minus_dx, ex2_intro/
+ ]
| #p #l1 #m1 #l2 #m2 #X #HX #_
>(lift_inv_gref1 … HX) -HX /2 width=3 by lift_gref, ex2_intro/
| #a #I #V1 #V2 #T1 #T2 #l1 #m1 #_ #_ #IHV12 #IHT12 #l2 #m2 #X #HX #Hlml
+ elim (yle_inv_plus_inj2 … Hlml) #Hlm #Hml
elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct
elim (IHV12 … HV20) -IHV12 -HV20 //
- elim (IHT12 … HT20) -IHT12 -HT20 /2 width=1 by le_S_S/ #T
- <plus_minus /3 width=5 by lift_bind, le_plus_to_minus_r, le_plus_b, ex2_intro/
+ elim (IHT12 … HT20) -IHT12 -HT20 /2 width=1 by yle_succ/ -Hlml
+ #T >yminus_succ1_inj /3 width=5 by lift_bind, ex2_intro/
| #I #V1 #V2 #T1 #T2 #l1 #m1 #_ #_ #IHV12 #IHT12 #l2 #m2 #X #HX #Hlml
elim (lift_inv_flat1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct
elim (IHV12 … HV20) -IHV12 -HV20 //
qed.
lemma lift_conf_be: ∀T,T1,l,m1. ⬆[l, m1] T ≡ T1 → ∀T2,m2. ⬆[l, m2] T ≡ T2 →
- m1 ≤ m2 → ⬆[l + m1, m2 - m1] T1 ≡ T2.
+ m1 ≤ m2 → ⬆[l + yinj m1, m2 - m1] T1 ≡ T2.
#T #T1 #l #m1 #HT1 #T2 #m2 #HT2 #Hm12
elim (lift_split … HT2 (l+m1) m1) -HT2 // #X #H
>(lift_mono … H … HT1) -T //
(* Properties on negated basic relocation ***********************************)
-lemma nlift_lref_be_SO: ∀X,i. ⬆[i, 1] X ≡ #i → ⊥.
-/2 width=7 by lift_inv_lref2_be/ qed-.
+lemma nlift_lref_be_SO: ∀X,i. ⬆[yinj i, 1] X ≡ #i → ⊥.
+/3 width=7 by lift_inv_lref2_be, ylt_inj/ qed-.
lemma nlift_bind_sn: ∀W,l,m. (∀V. ⬆[l, m] V ≡ W → ⊥) →
∀a,I,U. (∀X. ⬆[l, m] X ≡ ⓑ{a,I}W.U → ⊥).
#W #l #m #HW #a #I #U #X #H elim (lift_inv_bind2 … H) -H /2 width=2 by/
qed-.
-lemma nlift_bind_dx: ∀U,l,m. (∀T. ⬆[l+1, m] T ≡ U → ⊥) →
+lemma nlift_bind_dx: ∀U,l,m. (∀T. ⬆[⫯l, m] T ≡ U → ⊥) →
∀a,I,W. (∀X. ⬆[l, m] X ≡ ⓑ{a,I}W.U → ⊥).
#U #l #m #HU #a #I #W #X #H elim (lift_inv_bind2 … H) -H /2 width=2 by/
qed-.
(* Inversion lemmas on negated basic relocation *****************************)
-lemma nlift_inv_lref_be_SO: ∀i,j. (∀X. ⬆[i, 1] X ≡ #j → ⊥) → j = i.
+lemma nlift_inv_lref_be_SO: ∀i,j. (∀X. ⬆[i, 1] X ≡ #j → ⊥) → yinj j = i.
+* [2: #j #H elim H -H // ]
#i #j elim (lt_or_eq_or_gt i j) // #Hij #H
-[ elim (H (#(j-1))) -H /2 width=1 by lift_lref_ge_minus/
-| elim (H (#j)) -H /2 width=1 by lift_lref_lt/
+[ elim (H (#(j-1))) -H /3 width=1 by lift_lref_ge_minus, yle_inj/
+| elim (H (#j)) -H /3 width=1 by lift_lref_lt, ylt_inj/
]
qed-.
lemma nlift_inv_bind: ∀a,I,W,U,l,m. (∀X. ⬆[l, m] X ≡ ⓑ{a,I}W.U → ⊥) →
- (∀V. ⬆[l, m] V ≡ W → ⊥) ∨ (∀T. ⬆[l+1, m] T ≡ U → ⊥).
+ (∀V. ⬆[l, m] V ≡ W → ⊥) ∨ (∀T. ⬆[⫯l, m] T ≡ U → ⊥).
#a #I #W #U #l #m #H elim (is_lift_dec W l m)
[ * /4 width=2 by lift_bind, or_intror/
| /4 width=2 by ex_intro, or_introl/
(* BASIC TERM VECTOR RELOCATION *********************************************)
-inductive liftv (l,m:nat) : relation (list term) ≝
+inductive liftv (l) (m): relation (list term) ≝
| liftv_nil : liftv l m (◊) (◊)
| liftv_cons: ∀T1s,T2s,T1,T2.
⬆[l, m] T1 ≡ T2 → liftv l m T1s T2s →
fact lpx_sn_dropable_aux: ∀R,L2,K2,s,l,m. ⬇[s, l, m] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 →
l = 0 → ∃∃K1. ⬇[s, 0, m] L1 ≡ K1 & lpx_sn R K1 K2.
#R #L2 #K2 #s #l #m #H elim H -L2 -K2 -l -m
-[ #l #m #Hm #X #H >(lpx_sn_inv_atom2 … H) -H
+[ #l #m #Hm #X #H >(lpx_sn_inv_atom2 … H) -H
/4 width=3 by drop_atom, lpx_sn_atom, ex2_intro/
| #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H
#K1 #V1 #HK12 #HV12 #H destruct
| #I #L2 #K2 #V2 #m #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H
#L1 #V1 #HL12 #HV12 #H destruct
elim (IHLK2 … HL12) -L2 /3 width=3 by drop_drop, ex2_intro/
-| #I #L2 #K2 #V2 #W2 #l #m #_ #_ #_ #L1 #_
- <plus_n_Sm #H destruct
+| #I #L2 #K2 #V2 #W2 #l #m #_ #_ #_ #L1 #_ #H elim (ysucc_inv_O_dx … H)
]
qed-.
/2 width=4 by drop_pair, ex2_2_intro/
| lapply (ylt_inv_O1 i ?) /2 width=1 by ylt_inj/
#H <H -H #H lapply (ylt_inv_succ … H) -H
- #Him elim (IHL12 … HLK1) -IHL12 -HLK1 // -Him
+ #Him elim (IHL12 … HLK1) -IHL12 -HLK1 [2: <yminus_inj ] // -Him
>yminus_succ <yminus_inj /3 width=4 by drop_drop_lt, ex2_2_intro/
]
| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #IHL12 #J2 #K2 #W #s #i #HLK2 #Hli
(* *)
(**************************************************************************)
+include "ground_2/ynat/ynat_max.ma".
include "basic_2/substitution/drop_drop.ma".
include "basic_2/unfold/lstas.ma".
>(lift_inv_sort1 … H2) -X2 //
| #G #L1 #K1 #V1 #W1 #W #i #d #HLK1 #_ #HW1 #IHVW1 #L2 #s #l #m #HL21 #X #H #U2 #HWU2
elim (lift_inv_lref1 … H) * #Hil #H destruct
- [ elim (lift_trans_ge … HW1 … HWU2) -W // #W2 #HW12 #HWU2
- elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by lt_to_le/ #X #HLK2 #H
- elim (drop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hil #K2 #V2 #HK21 #HV12 #H destruct
+ [ elim (lift_trans_ge … HW1 … HWU2) -W /2 width=1 by ylt_fwd_le_succ1/ #W2 #HW12 #HWU2
+ elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by ylt_fwd_le/ #X #HLK2 #H
+ elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K2 #V2 #HK21 #HV12 #H destruct
/3 width=9 by lstas_ldef/
- | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W /2 width=1 by le_S/ #HW1U2
+ | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W /2 width=1 by yle_succ_dx/ #HW1U2
lapply (drop_trans_ge … HL21 … HLK1 ?) -L1 /3 width=9 by lstas_ldef, drop_inv_gen/
]
| #G #L1 #K1 #V1 #W1 #i #HLK1 #_ #IHVW1 #L2 #s #l #m #HL21 #X #H #U2 #HWU2
>(lift_mono … HWU2 … H) -U2
elim (lift_inv_lref1 … H) * #Hil #H destruct
[ elim (lift_total W1 (l-i-1) m) #W2 #HW12
- elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by lt_to_le/ #X #HLK2 #H
- elim (drop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hil #K2 #V2 #HK21 #HV12 #H destruct
+ elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by ylt_fwd_le/ #X #HLK2 #H
+ elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K2 #V2 #HK21 #HV12 #H destruct
/3 width=10 by lstas_zero/
| lapply (drop_trans_ge … HL21 … HLK1 ?) -L1
/3 width=10 by lstas_zero, drop_inv_gen/
]
| #G #L1 #K1 #W1 #V1 #W #i #d #HLK1 #_ #HW1 #IHWV1 #L2 #s #l #m #HL21 #X #H #U2 #HWU2
elim (lift_inv_lref1 … H) * #Hil #H destruct
- [ elim (lift_trans_ge … HW1 … HWU2) -W // <minus_plus #W #HW1 #HWU2
- elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by lt_to_le/ #X #HLK2 #H
- elim (drop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hil #K2 #W2 #HK21 #HW12 #H destruct
+ [ elim (lift_trans_ge … HW1 … HWU2) -W /2 width=1 by ylt_fwd_le_succ1/ #W #HW1 #HWU2
+ elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by ylt_fwd_le/ #X #HLK2 #H
+ elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K2 #W2 #HK21 #HW12 #H destruct
/3 width=9 by lstas_succ/
- | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W /2 width=1 by le_S/ #HW1U2
+ | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W /2 width=1 by yle_succ_dx/ #HW1U2
lapply (drop_trans_ge … HL21 … HLK1 ?) -L1 /3 width=9 by lstas_succ, drop_inv_gen/
]
| #a #I #G #L1 #V1 #T1 #U1 #d #_ #IHTU1 #L2 #s #l #m #HL21 #X1 #H1 #X2 #H2
elim (lift_inv_lref2 … H) * #Hil #H destruct [ -HVW2 | -IHVW2 ]
[ elim (drop_conf_lt … HL21 … HLK2) -L2 // #K1 #V1 #HLK1 #HK21 #HV12
elim (IHVW2 … HK21 … HV12) -K2 -V2 #W1 #HW12 #HVW1
- elim (lift_trans_le … HW12 … HW2) -W2 // >minus_plus <plus_minus_m_m /3 width=8 by lstas_ldef, ex2_intro/
+ elim (lift_trans_le … HW12 … HW2) -W2 // <yminus_succ2 <yplus_inj >yplus_SO2 >ymax_pre_sn /3 width=8 by lstas_ldef, ylt_fwd_le_succ1, ex2_intro/
| lapply (drop_conf_ge … HL21 … HLK2 ?) -L2 // #HL1K2
- elim (le_inv_plus_l … Hil) -Hil #Hlim #mi
- elim (lift_split … HW2 l (i-m+1)) -HW2 /2 width=1 by le_S_S, le_S/
- #W0 #HW20 <le_plus_minus_comm // >minus_minus_m_m /3 width=8 by lstas_ldef, le_S, ex2_intro/
+ elim (yle_inv_plus_inj2 … Hil) -Hil #Hlim #mi
+ elim (lift_split … HW2 l (i-m+1)) -HW2 /2 width=1 by yle_succ_dx, le_S_S/
+ #W0 #HW20 <le_plus_minus_comm /2 width=1 by yle_inv_inj/ >minus_minus_m_m /3 width=8 by lstas_ldef, yle_inv_inj, le_S, ex2_intro/
]
| #G #L2 #K2 #W2 #V2 #i #HLK2 #HWV2 #IHWV2 #L1 #s #l #m #HL21 #X #H
elim (lift_inv_lref2 … H) * #Hil #H destruct [ -HWV2 | -IHWV2 ]
elim (lift_inv_lref2 … H) * #Hil #H destruct [ -HWV2 | -IHWV2 ]
[ elim (drop_conf_lt … HL21 … HLK2) -L2 // #K1 #W1 #HLK1 #HK21 #HW12
elim (IHWV2 … HK21 … HW12) -K2 #V1 #HV12 #HWV1
- elim (lift_trans_le … HV12 … HW2) -W2 // >minus_plus <plus_minus_m_m /3 width=8 by lstas_succ, ex2_intro/
+ elim (lift_trans_le … HV12 … HW2) -W2 // <yminus_succ2 <yplus_inj >yplus_SO2 >ymax_pre_sn /3 width=8 by lstas_succ, ylt_fwd_le_succ1, ex2_intro/
| lapply (drop_conf_ge … HL21 … HLK2 ?) -L2 // #HL1K2
- elim (le_inv_plus_l … Hil) -Hil #Hlim #mi
- elim (lift_split … HW2 l (i-m+1)) -HW2 /2 width=1 by le_S_S, le_S/
- #W0 #HW20 <le_plus_minus_comm // >minus_minus_m_m /3 width=8 by lstas_succ, le_S, ex2_intro/
+ elim (yle_inv_plus_inj2 … Hil) -Hil #Hlim #mi
+ elim (lift_split … HW2 l (i-m+1)) -HW2 /2 width=1 by yle_succ_dx, le_S_S/
+ #W0 #HW20 <le_plus_minus_comm /2 width=1 by yle_inv_inj/ >minus_minus_m_m /3 width=8 by lstas_succ, yle_inv_inj, le_S, ex2_intro/
]
| #a #I #G #L2 #V2 #T2 #U2 #d #_ #IHTU2 #L1 #s #l #m #HL21 #X #H
elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
(* ARITHMETICAL PROPERTIES **************************************************)
+(* Iota equations ***********************************************************)
+
+lemma pred_O: pred 0 = 0.
+normalize // qed.
+
+lemma pred_S: ∀m. pred (S m) = m.
+// qed.
+
(* Equations ****************************************************************)
lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m.
interpretation "iterated function" 'exp op n = (iter n ? op).
+lemma iter_O: ∀B:Type[0]. ∀f:B→B.∀b. f^0 b = b.
+// qed.
+
+lemma iter_S: ∀B:Type[0]. ∀f:B→B.∀b,l. f^(S l) b = f (f^l b).
+// qed.
+
lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^(l+1) b = f (f^l b).
#B #f #b #l >commutative_plus //
qed.
lemma yle_inv_Y1: ∀n. ∞ ≤ n → n = ∞.
/2 width=3 by yle_inv_Y1_aux/ qed-.
+(* Basic properties *********************************************************)
+
+lemma le_O1: ∀n:ynat. 0 ≤ n.
+* /2 width=1 by yle_inj/
+qed.
+
+lemma yle_refl: reflexive … yle.
+* /2 width=1 by le_n, yle_inj/
+qed.
+
+lemma yle_split: ∀x,y:ynat. x ≤ y ∨ y ≤ x.
+* /2 width=1 by or_intror/
+#x * /2 width=1 by or_introl/
+#y elim (le_or_ge x y) /3 width=1 by yle_inj, or_introl, or_intror/
+qed-.
+
(* Inversion lemmas on successor ********************************************)
fact yle_inv_succ1_aux: ∀x,y. x ≤ y → ∀m. x = ⫯m → m ≤ ⫰y ∧ ⫯⫰y = y.
#m #n #H elim (yle_inv_succ1 … H) -H //
qed-.
-(* Basic properties *********************************************************)
-
-lemma le_O1: ∀n:ynat. 0 ≤ n.
-* /2 width=1 by yle_inj/
-qed.
-
-lemma yle_refl: reflexive … yle.
-* /2 width=1 by le_n, yle_inj/
-qed.
-
-lemma yle_split: ∀x,y:ynat. x ≤ y ∨ y ≤ x.
-* /2 width=1 by or_intror/
-#x * /2 width=1 by or_introl/
-#y elim (le_or_ge x y) /3 width=1 by yle_inj, or_introl, or_intror/
+lemma yle_inv_succ2: ∀x,y. x ≤ ⫯y → ⫰x ≤ y.
+#x #y #Hxy elim (ynat_cases x)
+[ #H destruct //
+| * #m #H destruct /2 width=1 by yle_inv_succ/
+]
qed-.
(* Properties on predecessor ************************************************)
lemma yle_refl_SP_dx: ∀x. x ≤ ⫯⫰x.
* // * //
-qed.
+qed.
+
+lemma yle_succ2: ∀x,y. ⫰x ≤ y → x ≤ ⫯y.
+#x #y #Hxy elim (ynat_cases x)
+[ #H destruct //
+| * #m #H destruct /2 width=1 by yle_succ/
+]
+qed-.
(* Main properties **********************************************************)
#x #y * -x -y /2 width=2 by ex_intro/
qed-.
-lemma ylt_fwd_le_succ: ∀x,y. x < y → ⫯x ≤ y.
-#x #y * -x -y /2 width=1 by yle_inj/
+lemma ylt_fwd_lt_O1: ∀x,y:ynat. x < y → 0 < y.
+#x #y #H elim H -x -y /3 width=2 by ylt_inj, ltn_to_ltO/
qed-.
(* Basic inversion lemmas ***************************************************)
#m #n * -m -n /2 width=1 by yle_inj/
qed-.
+lemma ylt_fwd_le_pred2: ∀x,y:ynat. x < y → x ≤ ⫰y.
+#x #y #H elim H -x -y /3 width=1 by yle_inj, monotonic_pred/
+qed-.
+
lemma ylt_fwd_le: ∀m:ynat. ∀n:ynat. m < n → m ≤ n.
#m #n * -m -n /3 width=1 by lt_to_le, yle_inj/
qed-.
#m #n #H elim H -m -n /3 width=1 by ylt_inj, le_S_S/
qed.
+lemma yle_succ1_inj: ∀x,y. ⫯yinj x ≤ y → x < y.
+#x * /3 width=1 by yle_inv_inj, ylt_inj/
+qed.
+
(* Properties on order ******************************************************)
-lemma yle_split_eq: ∀m:ynat. ∀n:ynat. m ≤ n → m < n ∨ m = n.
+lemma yle_split_eq: ∀m,n:ynat. m ≤ n → m < n ∨ m = n.
#m #n * -m -n
[ #m #n #Hmn elim (le_to_or_lt_eq … Hmn) -Hmn
/3 width=1 by or_introl, ylt_inj/
]
qed-.
-lemma ylt_split: ∀m,n:ynat. m < n ∨ n ≤ m..
+lemma ylt_split: ∀m,n:ynat. m < n ∨ n ≤ m.
#m #n elim (yle_split m n) /2 width=1 by or_intror/
#H elim (yle_split_eq … H) -H /2 width=1 by or_introl, or_intror/
-qed-.
+qed-.
+
+lemma ylt_split_eq: ∀m,n:ynat. ∨∨ m < n | n = m | n < m.
+#m #n elim (ylt_split m n) /2 width=1 by or3_intro0/
+#H elim (yle_split_eq … H) -H /2 width=1 by or3_intro1, or3_intro2/
+qed-.
lemma ylt_yle_trans: ∀x:ynat. ∀y:ynat. ∀z:ynat. y ≤ z → x < y → x < z.
#x #y #z * -y -z
interpretation "ynat minus" 'minus x y = (yminus x y).
+lemma yminus_O2: ∀m:ynat. m - 0 = m.
+// qed.
+
+lemma yminus_S2: ∀m:ynat. ∀n:nat. m - S n = ⫰(m - n).
+// qed.
+
+lemma yminus_Y2: ∀m. m - (∞) = 0.
+// qed.
+
(* Basic properties *********************************************************)
-lemma yminus_inj: ∀n,m. yinj m - yinj n = yinj (m - n).
-#n elim n -n /2 width=3 by trans_eq/
+lemma yminus_inj: ∀m,n. yinj m - yinj n = yinj (m - n).
+#m #n elim n -n //
+#n #IH >yminus_S2 >IH -IH >eq_minus_S_pred //
qed.
lemma yminus_Y_inj: ∀n. ∞ - yinj n = ∞.
-#n elim n -n // normalize
-#n #IHn >IHn //
+#n elim n -n //
qed.
lemma yminus_O1: ∀x:ynat. 0 - x = 0.
* //
qed.
+lemma yminus_pred1: ∀x,y. ⫰x - y = ⫰(x-y).
+#x * // #y elim y -y //
+qed.
+
lemma yminus_pred: ∀n,m. 0 < m → 0 < n → ⫰m - ⫰n = m - n.
* // #n *
[ #m #Hm #Hn >yminus_inj >yminus_inj
(* Properties on successor **************************************************)
lemma yminus_succ: ∀n,m. ⫯m - ⫯n = m - n.
-* // #n * [2: >yminus_Y_inj // ]
-#m >yminus_inj //
-qed.
+* // qed.
lemma yminus_succ1_inj: ∀n:nat. ∀m:ynat. n ≤ m → ⫯m - n = ⫯(m - n).
#n *
(* Properties on strict order ***********************************************)
+lemma ylt_to_minus: ∀x,y:ynat. x < y → 0 < y - x.
+#x #y #H elim H -x -y /3 width=1 by ylt_inj, lt_plus_to_minus_r/
+qed.
+
+lemma yminus_to_lt: ∀x,y:ynat. 0 < y - x → x < y.
+* [2: #y #H elim (ylt_yle_false … H) // ]
+#m * /4 width=1 by ylt_inv_inj, ylt_inj, lt_minus_to_plus_r/
+qed-.
+
lemma monotonic_ylt_minus_dx: ∀x,y:ynat. x < y → ∀z:nat. z ≤ x → x - z < y - z.
#x #y * -x -y
/4 width=1 by ylt_inj, yle_inv_inj, monotonic_lt_minus_l/
interpretation "ynat plus" 'plus x y = (yplus x y).
+lemma yplus_O2: ∀m:ynat. m + 0 = m.
+// qed.
+
+lemma yplus_S2: ∀m:ynat. ∀n. m + S n = ⫯(m + n).
+// qed.
+
+lemma yplus_Y2: ∀m:ynat. m + (∞) = ∞.
+// qed.
+
(* Properties on successor **************************************************)
lemma yplus_succ2: ∀m,n. m + ⫯n = ⫯(m + n).
qed.
lemma yplus_succ1: ∀m,n. ⫯m + n = ⫯(m + n).
-#m * normalize //
+#m * // #n elim n -n //
qed.
lemma yplus_succ_swap: ∀m,n. m + ⫯n = ⫯m + n.
(* Basic properties *********************************************************)
lemma yplus_inj: ∀n,m. yinj m + yinj n = yinj (m + n).
-#n elim n -n [ normalize // ]
+#n elim n -n //
#n #IHn #m >(yplus_succ2 ? n) >IHn -IHn
<plus_n_Sm //
qed.
lemma yplus_Y1: ∀m. ∞ + m = ∞.
-* normalize //
+* // #m elim m -m //
qed.
lemma yplus_comm: commutative … yplus.
* [ #m ] * [1,3: #n ] //
-normalize >ysucc_iter_Y //
qed.
lemma yplus_assoc: associative … yplus.
lemma yplus_O1: ∀n:ynat. 0 + n = n.
#n >yplus_comm // qed.
+lemma yplus_comm_23: ∀x,y,z. x + z + y = x + y + z.
+#x #y #z >yplus_assoc //
+qed.
+
(* Basic inversion lemmas ***************************************************)
lemma yplus_inv_inj: ∀z,y,x. x + y = yinj z →
lemma monotonic_yle_plus: ∀x1,y1. x1 ≤ y1 → ∀x2,y2. x2 ≤ y2 →
x1 + x2 ≤ y1 + y2.
-/3 width=3 by monotonic_yle_plus_dx, yle_trans/ qed.
+/3 width=3 by monotonic_yle_plus_dx, monotonic_yle_plus_sn, yle_trans/ qed.
(* Forward lemmas on order **************************************************)
#x #H0 #H destruct /3 width=4 by yle_fwd_plus_ge, yle_inj/
qed-.
+lemma yle_fwd_plus_yge: ∀n2,m1:ynat. ∀n1,m2:nat. m2 ≤ m1 → m1 + n1 ≤ m2 + n2 → n1 ≤ n2.
+* // #n2 * /2 width=4 by yle_fwd_plus_ge_inj/
+qed-.
+
(* Forward lemmas on strict order *******************************************)
lemma ylt_inv_monotonic_plus_dx: ∀x,y,z. x + z < y + z → x < y.
lemma monotonic_ylt_plus_sn: ∀x,y. x < y → ∀z:nat. yinj z + x < yinj z + y.
/2 width=1 by monotonic_ylt_plus_dx/ qed.
+(* Properties on predeccessor ***********************************************)
+
+lemma yplus_pred1: ∀x,y:ynat. 0 < x → ⫰x + y = ⫰(x+y).
+#x * // #y elim y -y // #y #IH #Hx
+>yplus_S2 >yplus_S2 >IH -IH // >ylt_inv_O1
+/2 width=1 by ylt_plus_dx1_trans/
+qed-.
+
+lemma yplus_pred2: ∀x,y:ynat. 0 < y → x + ⫰y = ⫰(x+y).
+/2 width=1 by yplus_pred1/ qed-.
+
(* Properties on minus ******************************************************)
lemma yplus_minus_inj: ∀m:ynat. ∀n:nat. m + n - n = m.
#m * //
qed.
+lemma yminus_plus2: ∀z,y,x:ynat. x - (y + z) = x - y - z.
+* // #z * [2: >yplus_Y1 >yminus_O1 // ] #y *
+[ #x >yplus_inj >yminus_inj >yminus_inj >yminus_inj /2 width=1 by eq_f/
+| >yplus_inj >yminus_Y_inj //
+]
+qed.
+
(* Forward lemmas on minus **************************************************)
lemma yle_plus1_to_minus_inj2: ∀x,z:ynat. ∀y:nat. x + y ≤ z → x ≤ z - y.
-/2 width=1 by monotonic_yle_minus_dx/ qed-.
+#x #z #y #H lapply (monotonic_yle_minus_dx … H y) -H //
+qed-.
lemma yle_plus1_to_minus_inj1: ∀x,z:ynat. ∀y:nat. y + x ≤ z → x ≤ z - y.
/2 width=1 by yle_plus1_to_minus_inj2/ qed-.
]
qed-.
+lemma yplus_minus_assoc_comm_inj: ∀x:nat. ∀y,z:ynat. x ≤ y → z - (y - x) = z + x - y.
+#x *
+[ #y *
+ [ #z >yminus_inj >yminus_inj >yplus_inj >yminus_inj
+ /4 width=1 by yle_inv_inj, minus_le_minus_minus_comm, eq_f/
+ | >yminus_inj >yminus_Y_inj //
+ ]
+| >yminus_Y_inj //
+]
+qed-.
+
lemma yplus_minus_comm_inj: ∀y:nat. ∀x,z:ynat. y ≤ x → x + z - y = x - y + z.
#y * // #x * //
#z #Hxy >yplus_inj >yminus_inj <plus_minus
/2 width=1 by yle_inv_inj/
qed-.
+lemma ylt_plus1_to_minus_inj2: ∀x,z:ynat. ∀y:nat. x + y < z → x < z - y.
+#x #z #y #H lapply (monotonic_ylt_minus_dx … H y ?) -H //
+qed-.
+
+lemma ylt_plus1_to_minus_inj1: ∀x,z:ynat. ∀y:nat. y + x < z → x < z - y.
+/2 width=1 by ylt_plus1_to_minus_inj2/ qed-.
+
+lemma ylt_plus2_to_minus_inj2: ∀x,y:ynat. ∀z:nat. z ≤ x → x < y + z → x - z < y.
+/2 width=1 by monotonic_ylt_minus_dx/ qed-.
+
+lemma ylt_plus2_to_minus_inj1: ∀x,y:ynat. ∀z:nat. z ≤ x → x < z + y → x - z < y.
+/2 width=1 by ylt_plus2_to_minus_inj2/ qed-.
+
(* Inversion lemmas on minus ************************************************)
lemma yle_inv_plus_inj2: ∀x,z:ynat. ∀y:nat. x + y ≤ z → x ≤ z - y ∧ y ≤ z.
interpretation "ynat predecessor" 'Predecessor m = (ypred m).
-(* Properties ***************************************************************)
+lemma ypred_O: ⫰0 = 0.
+// qed.
+
+lemma ypred_S: ∀m:nat. ⫰(S m) = m.
+// qed.
-lemma ypred_inj_rew: ∀m:nat. ⫰m = pred m.
+lemma ypred_Y: (⫰∞) = ∞.
// qed.
(* Inversion lemmas *********************************************************)
interpretation "ynat successor" 'Successor m = (ysucc m).
+lemma ysucc_inj: ∀m:nat. ⫯m = S m.
+// qed.
+
+lemma ysucc_Y: ⫯(∞) = ∞.
+// qed.
+
(* Properties ***************************************************************)
lemma ypred_succ: ∀m. ⫰⫯m = m.
(* Inversion lemmas *********************************************************)
-lemma ysucc_inj: ∀m,n. ⫯m = ⫯n → m = n.
+lemma ysucc_inv_inj: ∀m,n. ⫯m = ⫯n → m = n.
#m #n #H <(ypred_succ m) <(ypred_succ n) //
qed-.
lemma ysucc_inv_refl: ∀m. ⫯m = m → m = ∞.
-* // normalize
+* //
#m #H lapply (yinj_inj … H) -H (**) (* destruct lemma needed *)
#H elim (lt_refl_false m) //
qed-.
projects / helm.git / commitdiff