#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/
qed.
-
-(* Properties on relocation *************************************************)
-
-lemma frees_lift_ge: ∀K,T,l,i. K ⊢ i ϵ𝐅*[l]⦃T⦄ →
- ∀L,s,l0,m0. ⬇[s, l0, m0] L ≡ K →
- ∀U. ⬆[l0, m0] T ≡ U → l0 ≤ i →
- L ⊢ i+m0 ϵ 𝐅*[l]⦃U⦄.
-#K #T #l #i #H elim H -K -T -l -i
-[ #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 (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 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.
-
-(* Inversion lemmas on relocation *******************************************)
-
-lemma frees_inv_lift_be: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
- ∀K,s,l0,m0. ⬇[s, l0, m0+1] L ≡ K →
- ∀T. ⬆[l0, m0+1] T ≡ U → l0 ≤ i → i ≤ l0 + m0 → ⊥.
-#L #U #l #i #H elim H -L -U -l -i
-[ #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 (ylt_split j l0) #H1
- [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
- @(IHW … HKL0 … HVW)
- [ /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 ylt_yle_trans, ylt_fwd_le/
- ]
-]
-qed-.
-
-lemma frees_inv_lift_ge: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
- ∀K,s,l0,m0. ⬇[s, l0, m0] L ≡ K →
- ∀T. ⬆[l0, m0] T ≡ U → l0 + m0 ≤ i →
- 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 (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 (ylt_split j l0) #H1
- [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
- 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 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
- >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 (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 ( yle_inv_plus_inj2 … H2) -H2 #H2 #Hm0j
- @(frees_be … HK0)
- [ /2 width=1 by monotonic_yle_minus_dx/
- | /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/
- ]
- ]
- ]
-]
-qed-.
(* Basic_1: was: flt_shift *)
lemma rfw_shift: ∀p,I,K,V,T. ♯{K.ⓑ{I}V, T} < ♯{K, ⓑ{p,I}V.T}.
-normalize //
+normalize /2 width=1 by monotonic_le_plus_r/
qed.
lemma rfw_tpair_sn: ∀I,L,V,T. ♯{L, V} < ♯{L, ②{I}V.T}.
(* Basic_1: was: flt_shift *)
lemma fw_shift: ∀p,I,G,K,V,T. ♯{G, K.ⓑ{I}V, T} < ♯{G, K, ⓑ{p,I}V.T}.
-normalize //
+normalize /2 width=1 by monotonic_le_plus_r/
qed.
lemma fw_tpair_sn: ∀I,G,L,V,T. ♯{G, L, V} < ♯{G, L, ②{I}V.T}.
#b #L1 #L2 @eq_repl_sym /2 width=3 by drops_eq_repl_back/ (**) (* full auto fails *)
qed-.
-lemma drops_inv_tls_at: ∀f,i1,i2. @⦃i1,f⦄ ≡ i2 →
- ∀b,L1,L2. ⬇*[b,⫱*[i2]f] L1 ≡ L2 →
- ⬇*[b,↑⫱*[⫯i2]f] L1 ≡ L2.
-/3 width=3 by drops_eq_repl_fwd, at_inv_tls/ qed-.
-
(* Basic_2A1: includes: drop_FT *)
lemma drops_TF: ∀f,L1,L2. ⬇*[Ⓣ, f] L1 ≡ L2 → ⬇*[Ⓕ, f] L1 ≡ L2.
#f #L1 #L2 #H elim H -f -L1 -L2
* /2 width=1 by drops_TF/
qed-.
-(* Basic_2A1: includes: drop_refl *)
-lemma drops_refl: ∀b,L,f. 𝐈⦃f⦄ → ⬇*[b, f] L ≡ L.
-#b #L elim L -L /2 width=1 by drops_atom/
-#L #I #V #IHL #f #Hf elim (isid_inv_gen … Hf) -Hf
-/3 width=1 by drops_skip, lifts_refl/
-qed.
-
-(* Basic_2A1: includes: drop_split *)
-lemma drops_split_trans: ∀b,f,L1,L2. ⬇*[b, f] L1 ≡ L2 → ∀f1,f2. f1 ⊚ f2 ≡ f → 𝐔⦃f1⦄ →
- ∃∃L. ⬇*[b, f1] L1 ≡ L & ⬇*[b, f2] L ≡ L2.
-#b #f #L1 #L2 #H elim H -f -L1 -L2
-[ #f #H0f #f1 #f2 #Hf #Hf1 @(ex2_intro … (⋆)) @drops_atom
- #H lapply (H0f H) -b
- #H elim (after_inv_isid3 … Hf H) -f //
-| #f #I #L1 #L2 #V #HL12 #IHL12 #f1 #f2 #Hf #Hf1 elim (after_inv_xxn … Hf) -Hf [1,3: * |*: // ]
- [ #g1 #g2 #Hf #H1 #H2 destruct
- lapply (isuni_inv_push … Hf1 ??) -Hf1 [1,2: // ] #Hg1
- elim (IHL12 … Hf) -f
- /4 width=5 by drops_drop, drops_skip, lifts_refl, isuni_isid, ex2_intro/
- | #g1 #Hf #H destruct elim (IHL12 … Hf) -f
- /3 width=5 by ex2_intro, drops_drop, isuni_inv_next/
- ]
-| #f #I #L1 #L2 #V1 #V2 #_ #HV21 #IHL12 #f1 #f2 #Hf #Hf1 elim (after_inv_xxp … Hf) -Hf [2,3: // ]
- #g1 #g2 #Hf #H1 #H2 destruct elim (lifts_split_trans … HV21 … Hf) -HV21
- elim (IHL12 … Hf) -f /3 width=5 by ex2_intro, drops_skip, isuni_fwd_push/
-]
-qed-.
-
-lemma drops_split_div: ∀b,f1,L1,L. ⬇*[b, f1] L1 ≡ L → ∀f2,f. f1 ⊚ f2 ≡ f → 𝐔⦃f2⦄ →
- ∃∃L2. ⬇*[Ⓕ, f2] L ≡ L2 & ⬇*[Ⓕ, f] L1 ≡ L2.
-#b #f1 #L1 #L #H elim H -f1 -L1 -L
-[ #f1 #Hf1 #f2 #f #Hf #Hf2 @(ex2_intro … (⋆)) @drops_atom #H destruct
-| #f1 #I #L1 #L #V #HL1 #IH #f2 #f #Hf #Hf2 elim (after_inv_nxx … Hf) -Hf [2,3: // ]
- #g #Hg #H destruct elim (IH … Hg) -IH -Hg /3 width=5 by drops_drop, ex2_intro/
-| #f1 #I #L1 #L #V1 #V #HL1 #HV1 #IH #f2 #f #Hf #Hf2
- elim (after_inv_pxx … Hf) -Hf [1,3: * |*: // ]
- #g2 #g #Hg #H2 #H0 destruct
- [ lapply (isuni_inv_push … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -IH
- lapply (after_isid_inv_dx … Hg … Hg2) -Hg #Hg
- /5 width=7 by drops_eq_repl_back, drops_F, drops_refl, drops_skip, lifts_eq_repl_back, isid_push, ex2_intro/
- | lapply (isuni_inv_next … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -HL1 -HV1
- elim (IH … Hg) -f1 /3 width=3 by drops_drop, ex2_intro/
- ]
-]
-qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-(* Basic_1: includes: drop_gen_refl *)
-(* Basic_2A1: includes: drop_inv_O2 *)
-lemma drops_fwd_isid: ∀b,f,L1,L2. ⬇*[b, f] L1 ≡ L2 → 𝐈⦃f⦄ → L1 = L2.
-#b #f #L1 #L2 #H elim H -f -L1 -L2 //
-[ #f #I #L1 #L2 #V #_ #_ #H elim (isid_inv_next … H) //
-| /5 width=5 by isid_inv_push, lifts_fwd_isid, eq_f3, sym_eq/
-]
-qed-.
-
-fact drops_fwd_drop2_aux: ∀b,f2,X,Y. ⬇*[b, f2] X ≡ Y → ∀I,K,V. Y = K.ⓑ{I}V →
- ∃∃f1,f. 𝐈⦃f1⦄ & f2 ⊚ ⫯f1 ≡ f & ⬇*[b, f] X ≡ K.
-#b #f2 #X #Y #H elim H -f2 -X -Y
-[ #f2 #Hf2 #J #K #W #H destruct
-| #f2 #I #L1 #L2 #V #_ #IHL #J #K #W #H elim (IHL … H) -IHL
- /3 width=7 by after_next, ex3_2_intro, drops_drop/
-| #f2 #I #L1 #L2 #V1 #V2 #HL #_ #_ #J #K #W #H destruct
- lapply (after_isid_dx 𝐈𝐝 … f2) /3 width=9 by after_push, ex3_2_intro, drops_drop/
-]
-qed-.
-
-lemma drops_fwd_drop2: ∀b,f2,I,X,K,V. ⬇*[b, f2] X ≡ K.ⓑ{I}V →
- ∃∃f1,f. 𝐈⦃f1⦄ & f2 ⊚ ⫯f1 ≡ f & ⬇*[b, f] X ≡ K.
-/2 width=5 by drops_fwd_drop2_aux/ qed-.
-
-lemma drops_after_fwd_drop2: ∀b,f2,I,X,K,V. ⬇*[b, f2] X ≡ K.ⓑ{I}V →
- ∀f1,f. 𝐈⦃f1⦄ → f2 ⊚ ⫯f1 ≡ f → ⬇*[b, f] X ≡ K.
-#b #f2 #I #X #K #V #H #f1 #f #Hf1 #Hf elim (drops_fwd_drop2 … H) -H
-#g1 #g #Hg1 #Hg #HK lapply (after_mono_eq … Hg … Hf ??) -Hg -Hf
-/3 width=5 by drops_eq_repl_back, isid_inv_eq_repl, eq_next/
-qed-.
-
-(* Basic_1: was: drop_S *)
-(* Basic_2A1: was: drop_fwd_drop2 *)
-lemma drops_isuni_fwd_drop2: ∀b,f,I,X,K,V. 𝐔⦃f⦄ → ⬇*[b, f] X ≡ K.ⓑ{I}V → ⬇*[b, ⫯f] X ≡ K.
-/3 width=7 by drops_after_fwd_drop2, after_isid_isuni/ qed-.
-
-(* Forward lemmas with test for finite colength *****************************)
-
-lemma drops_fwd_isfin: ∀f,L1,L2. ⬇*[Ⓣ, f] L1 ≡ L2 → 𝐅⦃f⦄.
-#f #L1 #L2 #H elim H -f -L1 -L2
-/3 width=1 by isfin_next, isfin_push, isfin_isid/
-qed-.
-
(* Basic inversion lemmas ***************************************************)
fact drops_inv_atom1_aux: ∀b,f,X,Y. ⬇*[b, f] X ≡ Y → X = ⋆ →
∃∃K1,V1. ⬇*[b, f] K1 ≡ K2 & ⬆*[f] V2 ≡ V1 & X = K1.ⓑ{I}V1.
/2 width=5 by drops_inv_skip2_aux/ qed-.
-fact drops_inv_TF_aux: ∀f,L1,L2. ⬇*[Ⓕ, f] L1 ≡ L2 → 𝐔⦃f⦄ →
- ∀I,K,V. L2 = K.ⓑ{I}V →
- ⬇*[Ⓣ, f] L1 ≡ K.ⓑ{I}V.
-#f #L1 #L2 #H elim H -f -L1 -L2
-[ #f #_ #_ #J #K #W #H destruct
-| #f #I #L1 #L2 #V #_ #IH #Hf #J #K #W #H destruct
- /4 width=3 by drops_drop, isuni_inv_next/
-| #f #I #L1 #L2 #V1 #V2 #HL12 #HV21 #_ #Hf #J #K #W #H destruct
- lapply (isuni_inv_push … Hf ??) -Hf [1,2: // ] #Hf
- <(drops_fwd_isid … HL12) -K // <(lifts_fwd_isid … HV21) -V1
- /3 width=3 by drops_refl, isid_push/
+(* Basic forward lemmas *****************************************************)
+
+fact drops_fwd_drop2_aux: ∀b,f2,X,Y. ⬇*[b, f2] X ≡ Y → ∀I,K,V. Y = K.ⓑ{I}V →
+ ∃∃f1,f. 𝐈⦃f1⦄ & f2 ⊚ ⫯f1 ≡ f & ⬇*[b, f] X ≡ K.
+#b #f2 #X #Y #H elim H -f2 -X -Y
+[ #f2 #Hf2 #J #K #W #H destruct
+| #f2 #I #L1 #L2 #V #_ #IHL #J #K #W #H elim (IHL … H) -IHL
+ /3 width=7 by after_next, ex3_2_intro, drops_drop/
+| #f2 #I #L1 #L2 #V1 #V2 #HL #_ #_ #J #K #W #H destruct
+ lapply (after_isid_dx 𝐈𝐝 … f2) /3 width=9 by after_push, ex3_2_intro, drops_drop/
]
qed-.
-(* Basic_2A1: includes: drop_inv_FT *)
-lemma drops_inv_TF: ∀f,I,L,K,V. ⬇*[Ⓕ, f] L ≡ K.ⓑ{I}V → 𝐔⦃f⦄ →
- ⬇*[Ⓣ, f] L ≡ K.ⓑ{I}V.
-/2 width=3 by drops_inv_TF_aux/ qed-.
+lemma drops_fwd_drop2: ∀b,f2,I,X,K,V. ⬇*[b, f2] X ≡ K.ⓑ{I}V →
+ ∃∃f1,f. 𝐈⦃f1⦄ & f2 ⊚ ⫯f1 ≡ f & ⬇*[b, f] X ≡ K.
+/2 width=5 by drops_fwd_drop2_aux/ qed-.
-(* Advanced inversion lemmas ************************************************)
+(* Properties with test for identity ****************************************)
-lemma drops_inv_atom2: ∀b,L,f. ⬇*[b,f] L ≡ ⋆ →
- ∃∃n,f1. ⬇*[b,𝐔❴n❵] L ≡ ⋆ & 𝐔❴n❵ ⊚ f1 ≡ f.
-#b #L elim L -L
-[ /3 width=4 by drops_atom, after_isid_sn, ex2_2_intro/
-| #L #I #V #IH #f #H elim (pn_split f) * #g #H0 destruct
- [ elim (drops_inv_skip1 … H) -H #K #W #_ #_ #H destruct
- | lapply (drops_inv_drop1 … H) -H #HL
- elim (IH … HL) -IH -HL /3 width=8 by drops_drop, after_next, ex2_2_intro/
- ]
+(* Basic_2A1: includes: drop_refl *)
+lemma drops_refl: ∀b,L,f. 𝐈⦃f⦄ → ⬇*[b, f] L ≡ L.
+#b #L elim L -L /2 width=1 by drops_atom/
+#L #I #V #IHL #f #Hf elim (isid_inv_gen … Hf) -Hf
+/3 width=1 by drops_skip, lifts_refl/
+qed.
+
+(* Forward lemmas test for identity *****************************************)
+
+(* Basic_1: includes: drop_gen_refl *)
+(* Basic_2A1: includes: drop_inv_O2 *)
+lemma drops_fwd_isid: ∀b,f,L1,L2. ⬇*[b, f] L1 ≡ L2 → 𝐈⦃f⦄ → L1 = L2.
+#b #f #L1 #L2 #H elim H -f -L1 -L2 //
+[ #f #I #L1 #L2 #V #_ #_ #H elim (isid_inv_next … H) //
+| /5 width=5 by isid_inv_push, lifts_fwd_isid, eq_f3, sym_eq/
]
qed-.
-(* Basic_2A1: includes: drop_inv_gen *)
-lemma drops_inv_gen: ∀b,f,I,L,K,V. ⬇*[b, f] L ≡ K.ⓑ{I}V → 𝐔⦃f⦄ →
- ⬇*[Ⓣ, f] L ≡ K.ⓑ{I}V.
-* /2 width=1 by drops_inv_TF/
+
+lemma drops_after_fwd_drop2: ∀b,f2,I,X,K,V. ⬇*[b, f2] X ≡ K.ⓑ{I}V →
+ ∀f1,f. 𝐈⦃f1⦄ → f2 ⊚ ⫯f1 ≡ f → ⬇*[b, f] X ≡ K.
+#b #f2 #I #X #K #V #H #f1 #f #Hf1 #Hf elim (drops_fwd_drop2 … H) -H
+#g1 #g #Hg1 #Hg #HK lapply (after_mono_eq … Hg … Hf ??) -Hg -Hf
+/3 width=5 by drops_eq_repl_back, isid_inv_eq_repl, eq_next/
qed-.
-(* Basic_2A1: includes: drop_inv_T *)
-lemma drops_inv_F: ∀b,f,I,L,K,V. ⬇*[Ⓕ, f] L ≡ K.ⓑ{I}V → 𝐔⦃f⦄ →
- ⬇*[b, f] L ≡ K.ⓑ{I}V.
-* /2 width=1 by drops_inv_TF/
+(* Forward lemmas with test for finite colength *****************************)
+
+lemma drops_fwd_isfin: ∀f,L1,L2. ⬇*[Ⓣ, f] L1 ≡ L2 → 𝐅⦃f⦄.
+#f #L1 #L2 #H elim H -f -L1 -L2
+/3 width=1 by isfin_next, isfin_push, isfin_isid/
+qed-.
+
+(* Properties with uniform relocations **************************************)
+
+lemma drops_uni_ex: ∀L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ ∨ ∃∃I,K,V. ⬇*[i] L ≡ K.ⓑ{I}V.
+#L elim L -L /2 width=1 by or_introl/
+#L #I #V #IH * /4 width=4 by drops_refl, ex1_3_intro, or_intror/
+#i elim (IH i) -IH /3 width=1 by drops_drop, or_introl/
+* /4 width=4 by drops_drop, ex1_3_intro, or_intror/
+qed-.
+
+(* Basic_2A1: includes: drop_split *)
+lemma drops_split_trans: ∀b,f,L1,L2. ⬇*[b, f] L1 ≡ L2 → ∀f1,f2. f1 ⊚ f2 ≡ f → 𝐔⦃f1⦄ →
+ ∃∃L. ⬇*[b, f1] L1 ≡ L & ⬇*[b, f2] L ≡ L2.
+#b #f #L1 #L2 #H elim H -f -L1 -L2
+[ #f #H0f #f1 #f2 #Hf #Hf1 @(ex2_intro … (⋆)) @drops_atom
+ #H lapply (H0f H) -b
+ #H elim (after_inv_isid3 … Hf H) -f //
+| #f #I #L1 #L2 #V #HL12 #IHL12 #f1 #f2 #Hf #Hf1 elim (after_inv_xxn … Hf) -Hf [1,3: * |*: // ]
+ [ #g1 #g2 #Hf #H1 #H2 destruct
+ lapply (isuni_inv_push … Hf1 ??) -Hf1 [1,2: // ] #Hg1
+ elim (IHL12 … Hf) -f
+ /4 width=5 by drops_drop, drops_skip, lifts_refl, isuni_isid, ex2_intro/
+ | #g1 #Hf #H destruct elim (IHL12 … Hf) -f
+ /3 width=5 by ex2_intro, drops_drop, isuni_inv_next/
+ ]
+| #f #I #L1 #L2 #V1 #V2 #_ #HV21 #IHL12 #f1 #f2 #Hf #Hf1 elim (after_inv_xxp … Hf) -Hf [2,3: // ]
+ #g1 #g2 #Hf #H1 #H2 destruct elim (lifts_split_trans … HV21 … Hf) -HV21
+ elim (IHL12 … Hf) -f /3 width=5 by ex2_intro, drops_skip, isuni_fwd_push/
+]
+qed-.
+
+lemma drops_split_div: ∀b,f1,L1,L. ⬇*[b, f1] L1 ≡ L → ∀f2,f. f1 ⊚ f2 ≡ f → 𝐔⦃f2⦄ →
+ ∃∃L2. ⬇*[Ⓕ, f2] L ≡ L2 & ⬇*[Ⓕ, f] L1 ≡ L2.
+#b #f1 #L1 #L #H elim H -f1 -L1 -L
+[ #f1 #Hf1 #f2 #f #Hf #Hf2 @(ex2_intro … (⋆)) @drops_atom #H destruct
+| #f1 #I #L1 #L #V #HL1 #IH #f2 #f #Hf #Hf2 elim (after_inv_nxx … Hf) -Hf [2,3: // ]
+ #g #Hg #H destruct elim (IH … Hg) -IH -Hg /3 width=5 by drops_drop, ex2_intro/
+| #f1 #I #L1 #L #V1 #V #HL1 #HV1 #IH #f2 #f #Hf #Hf2
+ elim (after_inv_pxx … Hf) -Hf [1,3: * |*: // ]
+ #g2 #g #Hg #H2 #H0 destruct
+ [ lapply (isuni_inv_push … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -IH
+ lapply (after_isid_inv_dx … Hg … Hg2) -Hg #Hg
+ /5 width=7 by drops_eq_repl_back, drops_F, drops_refl, drops_skip, lifts_eq_repl_back, isid_push, ex2_intro/
+ | lapply (isuni_inv_next … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -HL1 -HV1
+ elim (IH … Hg) -f1 /3 width=3 by drops_drop, ex2_intro/
+ ]
+]
qed-.
(* Inversion lemmas with test for uniformity ********************************)
]
qed-.
+fact drops_inv_TF_aux: ∀f,L1,L2. ⬇*[Ⓕ, f] L1 ≡ L2 → 𝐔⦃f⦄ →
+ ∀I,K,V. L2 = K.ⓑ{I}V →
+ ⬇*[Ⓣ, f] L1 ≡ K.ⓑ{I}V.
+#f #L1 #L2 #H elim H -f -L1 -L2
+[ #f #_ #_ #J #K #W #H destruct
+| #f #I #L1 #L2 #V #_ #IH #Hf #J #K #W #H destruct
+ /4 width=3 by drops_drop, isuni_inv_next/
+| #f #I #L1 #L2 #V1 #V2 #HL12 #HV21 #_ #Hf #J #K #W #H destruct
+ lapply (isuni_inv_push … Hf ??) -Hf [1,2: // ] #Hf
+ <(drops_fwd_isid … HL12) -K // <(lifts_fwd_isid … HV21) -V1
+ /3 width=3 by drops_refl, isid_push/
+]
+qed-.
+
+(* Basic_2A1: includes: drop_inv_FT *)
+lemma drops_inv_TF: ∀f,I,L,K,V. ⬇*[Ⓕ, f] L ≡ K.ⓑ{I}V → 𝐔⦃f⦄ →
+ ⬇*[Ⓣ, f] L ≡ K.ⓑ{I}V.
+/2 width=3 by drops_inv_TF_aux/ qed-.
+
+(* Basic_2A1: includes: drop_inv_gen *)
+lemma drops_inv_gen: ∀b,f,I,L,K,V. ⬇*[b, f] L ≡ K.ⓑ{I}V → 𝐔⦃f⦄ →
+ ⬇*[Ⓣ, f] L ≡ K.ⓑ{I}V.
+* /2 width=1 by drops_inv_TF/
+qed-.
+
+(* Basic_2A1: includes: drop_inv_T *)
+lemma drops_inv_F: ∀b,f,I,L,K,V. ⬇*[Ⓕ, f] L ≡ K.ⓑ{I}V → 𝐔⦃f⦄ →
+ ⬇*[b, f] L ≡ K.ⓑ{I}V.
+* /2 width=1 by drops_inv_TF/
+qed-.
+
+(* Forward lemmas with test for uniformity **********************************)
+
+(* Basic_1: was: drop_S *)
+(* Basic_2A1: was: drop_fwd_drop2 *)
+lemma drops_isuni_fwd_drop2: ∀b,f,I,X,K,V. 𝐔⦃f⦄ → ⬇*[b, f] X ≡ K.ⓑ{I}V → ⬇*[b, ⫯f] X ≡ K.
+/3 width=7 by drops_after_fwd_drop2, after_isid_isuni/ qed-.
+
(* Inversion lemmas with uniform relocations ********************************)
+lemma drops_inv_atom2: ∀b,L,f. ⬇*[b, f] L ≡ ⋆ →
+ ∃∃n,f1. ⬇*[b, 𝐔❴n❵] L ≡ ⋆ & 𝐔❴n❵ ⊚ f1 ≡ f.
+#b #L elim L -L
+[ /3 width=4 by drops_atom, after_isid_sn, ex2_2_intro/
+| #L #I #V #IH #f #H elim (pn_split f) * #g #H0 destruct
+ [ elim (drops_inv_skip1 … H) -H #K #W #_ #_ #H destruct
+ | lapply (drops_inv_drop1 … H) -H #HL
+ elim (IH … HL) -IH -HL /3 width=8 by drops_drop, after_next, ex2_2_intro/
+ ]
+]
+qed-.
+
lemma drops_inv_succ: ∀l,L1,L2. ⬇*[⫯l] L1 ≡ L2 →
∃∃I,K,V. ⬇*[l] K ≡ L2 & L1 = K.ⓑ{I}V.
#l #L1 #L2 #H elim (drops_inv_isuni … H) -H // *
]
qed-.
-(* Properties with uniform relocations **************************************)
+(* Properties with application **********************************************)
-lemma drops_uni_ex: ∀L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ ∨ ∃∃I,K,V. ⬇*[i] L ≡ K.ⓑ{I}V.
-#L elim L -L /2 width=1 by or_introl/
-#L #I #V #IH * /4 width=4 by drops_refl, ex1_3_intro, or_intror/
-#i elim (IH i) -IH /3 width=1 by drops_drop, or_introl/
-* /4 width=4 by drops_drop, ex1_3_intro, or_intror/
-qed-.
+lemma drops_tls_at: ∀f,i1,i2. @⦃i1,f⦄ ≡ i2 →
+ ∀b,L1,L2. ⬇*[b,⫱*[i2]f] L1 ≡ L2 →
+ ⬇*[b,↑⫱*[⫯i2]f] L1 ≡ L2.
+/3 width=3 by drops_eq_repl_fwd, at_inv_tls/ qed-.
+
+lemma drops_split_trans_pair2: ∀b,f,I,L,K0,V. ⬇*[b, f] L ≡ K0.ⓑ{I}V → ∀n. @⦃O, f⦄ ≡ n →
+ ∃∃K,W. ⬇*[n]L ≡ K.ⓑ{I}W & ⬇*[b, ⫱*[⫯n]f] K ≡ K0 & ⬆*[⫱*[⫯n]f] V ≡ W.
+#b #f #I #L #K0 #V #H #n #Hf
+elim (drops_split_trans … H) -H [ |5: @(after_uni_dx … Hf) |2,3: skip ] /2 width=1 by after_isid_dx/ #Y #HLY #H
+lapply (drops_tls_at … Hf … H) -H #H
+elim (drops_inv_skip2 … H) -H #K #W #HK0 #HVW #H destruct
+/3 width=5 by drops_inv_gen, ex3_2_intro/
+qed-.
(* Basic_2A1: removed theorems 12:
drops_inv_nil drops_inv_cons d1_liftable_liftables
(* Properties with generic slicing for local environments *******************)
+(* Note: it should use drops_split_trans_pair2 *)
lemma cpg_lifts: ∀c,h,G. d_liftable2 (cpg h c G).
#c #h #G #K #T generalize in match c; -c
@(fqup_wf_ind_eq … G K T) -G -K -T #G0 #K0 #T0 #IH #G #K * *
elim (lifts_inv_lref1 … H1) -H1 #i2 #Hf #H destruct
lapply (drops_trans … HLK … HK0 ??) -HLK [3,6: |*: // ] #H
elim (drops_split_trans … H) -H [1,6: |*: /2 width=6 by after_uni_dx/ ] #Y #HL0 #HY
- lapply (drops_inv_tls_at … Hf … HY) -HY #HY
+ lapply (drops_tls_at … Hf … HY) -HY #HY
elim (drops_inv_skip2 … HY) -HY #L0 #W #HLK0 #HVW #H destruct
elim (IH … HV2 … HLK0 … HVW) -IH /2 width=2 by fqup_lref/ -K -K0 -V #W2 #HVW2 #HW2
elim (lifts_total W2 (𝐔❴⫯i2❵)) #U2 #HWU2
elim (lifts_inv_lref2 … H1) -H1 #i1 #Hf #H destruct
lapply (drops_split_div … HLK (𝐔❴i1❵) ???) -HLK [4,8: * |*: // ] #Y0 #HK0 #HLY0
lapply (drops_conf … HL0 … HLY0 ??) -HLY0 [3,6: |*: /2 width=6 by after_uni_dx/ ] #HLY0
- lapply (drops_inv_tls_at … Hf … HLY0) -HLY0 #HLY0
+ lapply (drops_tls_at … Hf … HLY0) -HLY0 #HLY0
elim (drops_inv_skip1 … HLY0) -HLY0 #K0 #V #HLK0 #HVW #H destruct
elim (IH … HW2 … HLK0 … HVW) -IH /2 width=2 by fqup_lref/ -L -L0 -W #V2 #HVW2 #HV2
lapply (lifts_trans … HVW2 … HWU2 ??) -W2 [3,6: |*: // ] #HVU2
(* Properties with generic slicing for local environments *******************)
(* Basic_2A1: includes: aaa_lift *)
+(* Note: it should use drops_split_trans_pair2 *)
lemma aaa_lifts: ∀G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ∀b,f,L2. ⬇*[b, f] L2 ≡ L1 →
∀T2. ⬆*[f] T1 ≡ T2 → ⦃G, L2⦄ ⊢ T2 ⁝ A.
@fqup_wf_ind_eq #G0 #L0 #T0 #IH #G #L1 * *
elim (lifts_inv_lref1 … HX) -HX #i2 #Hf #H destruct
lapply (drops_trans … HL21 … HLK1 ??) -HL21 [1,2: // ] #H
elim (drops_split_trans … H) -H [ |*: /2 width=6 by after_uni_dx/ ] #Y #HLK2 #HY
- lapply (drops_inv_tls_at … Hf … HY) -HY #HY -Hf
+ lapply (drops_tls_at … Hf … HY) -HY #HY -Hf
elim (drops_inv_skip2 … HY) -HY #K2 #V2 #HK21 #HV12 #H destruct
/4 width=12 by aaa_lref_drops, fqup_lref, drops_inv_gen/
| #l #HG #HL #HT #A #H #b #f #L2 #HL21 #X #HX -b -f -IH
elim (lifts_inv_lref2 … HX) -HX #i1 #Hf #H destruct
lapply (drops_split_div … HL21 (𝐔❴i1❵) ???) -HL21 [4: * |*: // ] #Y #HLK1 #HY
lapply (drops_conf … HLK2 … HY ??) -HY [1,2: /2 width=6 by after_uni_dx/ ] #HY
- lapply (drops_inv_tls_at … Hf … HY) -HY #HY -Hf
+ lapply (drops_tls_at … Hf … HY) -HY #HY -Hf
elim (drops_inv_skip1 … HY) -HY #K1 #V1 #HK21 #HV12 #H destruct
/4 width=12 by aaa_lref_drops, fqup_lref, drops_inv_F/
| #l #HG #HL #HT #A #H #b #f #L1 #HL21 #X #HX -IH -b -f
/4 width=3 by frees_eq_repl_back, frees_gref, frees_atom, eq_push_inv_isid/
qed.
-(* Basic_2A1: removed theorems 27:
+(* Basic_2A1: removed theorems 30:
frees_eq frees_be frees_inv
frees_inv_sort frees_inv_gref frees_inv_lref frees_inv_lref_free
frees_inv_lref_skip frees_inv_lref_ge frees_inv_lref_lt
frees_inv_bind frees_inv_flat frees_inv_bind_O
frees_lref_eq frees_lref_be frees_weak
frees_bind_sn frees_bind_dx frees_flat_sn frees_flat_dx
+ frees_lift_ge frees_inv_lift_be frees_inv_lift_ge
lreq_frees_trans frees_lreq_conf
llor_atom llor_skip llor_total
llor_tail_frees llor_tail_cofrees
(* *)
(**************************************************************************)
-include "ground_2/relocation/rtmap_pushs.ma".
include "ground_2/relocation/rtmap_coafter.ma".
include "basic_2/relocation/drops_drops.ma".
include "basic_2/static/frees.ma".
]
qed.
+lemma frees_sort_pushs: ∀f,K,s. K ⊢ 𝐅*⦃⋆s⦄ ≡ f →
+ ∀i,L. ⬇*[i] L ≡ K → L ⊢ 𝐅*⦃⋆s⦄ ≡ ↑*[i] f.
+#f #K #s #Hf #i elim i -i
+[ #L #H lapply (drops_fwd_isid … H ?) -H //
+| #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_sort/
+]
+qed.
+
+lemma frees_lref_pushs: ∀f,K,j. K ⊢ 𝐅*⦃#j⦄ ≡ f →
+ ∀i,L. ⬇*[i] L ≡ K → L ⊢ 𝐅*⦃#(i+j)⦄ ≡ ↑*[i] f.
+#f #K #j #Hf #i elim i -i
+[ #L #H lapply (drops_fwd_isid … H ?) -H //
+| #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_lref/
+]
+qed.
+
+lemma frees_gref_pushs: ∀f,K,l. K ⊢ 𝐅*⦃§l⦄ ≡ f →
+ ∀i,L. ⬇*[i] L ≡ K → L ⊢ 𝐅*⦃§l⦄ ≡ ↑*[i] f.
+#f #K #l #Hf #i elim i -i
+[ #L #H lapply (drops_fwd_isid … H ?) -H //
+| #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_gref/
+]
+qed.
+
(* Advanced inversion lemmas ************************************************)
lemma frees_inv_lref_drops: ∀i,f,L. L ⊢ 𝐅*⦃#i⦄ ≡ f →
(* Properties with generic slicing for local environments *******************)
-axiom coafter_inv_xpx: ∀g2,f1,g. g2 ~⊚ ↑f1 ≡ g → ∀n. @⦃0, g2⦄ ≡ n →
- ∃∃f2,f. f2 ~⊚ f1 ≡ f & ⫱*[n]g2 = ↑f2 & ⫱*[n]g = ↑f.
-(*
-#g2 #g1 #g #Hg #n #Hg2
-lapply (coafter_tls … Hg2 … Hg) -Hg #Hg
-lapply (at_pxx_tls … Hg2) -Hg2 #H
-elim (at_inv_pxp … H) -H [ |*: // ] #f2 #H2
-elim (coafter_inv_pxx … Hg … H2) -Hg * #f1 #f #Hf #H1 #H0 destruct
-<tls_rew_S <tls_rew_S <H2 <H0 -g2 -g -n //
-qed.
-*)
-
-lemma coafter_tls_succ: ∀g2,g1,g. g2 ~⊚ g1 ≡ g →
- ∀n. @⦃0, g2⦄ ≡ n → ⫱*[⫯n]g2 ~⊚ ⫱g1 ≡ ⫱*[⫯n]g.
-#g2 #g1 #g #Hg #n #Hg2
-lapply (coafter_tls … Hg2 … Hg) -Hg #Hg
-lapply (at_pxx_tls … Hg2) -Hg2 #H
-elim (at_inv_pxp … H) -H [ |*: // ] #f2 #H2
-elim (coafter_inv_pxx … Hg … H2) -Hg * #f1 #f #Hf #H1 #H0 destruct
-<tls_rew_S <tls_rew_S <H2 <H0 -g2 -g -n //
-qed.
-
lemma frees_lifts: ∀b,f1,K,T. K ⊢ 𝐅*⦃T⦄ ≡ f1 →
∀f,L. ⬇*[b, f] L ≡ K → ∀U. ⬆*[f] T ≡ U →
∀f2. f ~⊚ f1 ≡ f2 → L ⊢ 𝐅*⦃U⦄ ≡ f2.
| #f1 #I #K #V #s #_ #IH #Hf1 #f #L #H1 #U #H2 #f2 #H3
lapply (isfin_fwd_push … Hf1 ??) -Hf1 [3: |*: // ] #Hf1
lapply (lifts_inv_sort1 … H2) -H2 #H destruct
- lapply (at_total 0 f) #H
- elim (drops_split_trans … H1) -H1
- [5: @(after_uni_dx … H) /2 width=1 by after_isid_dx/ |2,3: skip
- |4: // ] #X #HLX #HXK
- lapply (drops_inv_tls_at … H … HXK) -HXK #HXK
- elim (drops_inv_skip2 … HXK) -HXK
- #Y #W #HYK #HVW #H0 destruct
-(*
-
- elim (coafter_inv_xpx … H3 ??) -H3 [ |*: // ] #g2 #g #Hg #H2 #H0
- lapply (IH … Hg) -IH -Hg
- [1,5: // | skip
- |
- |6: #H
-*)
-
+ elim (drops_split_trans_pair2 … H1) -H1 [ |*: // ] #Y #W #HLY #HYK #_
+ elim (coafter_fwd_xpx_pushs … H3) [ |*: // ] #g2 #H2 destruct
lapply (coafter_tls_succ … H3 ??) -H3 [3: |*: // ] #H3
- lapply (IH … HYK … H3) -IH -H3 -HYK
- [1,3: // | skip ]
- #H lapply (frees_sort … H)
-
- ]
-
-
- elim (coafter_inv_xxp … H3) -H3 [1,3: * |*: // ]
- [ #g #g1 #Hf2 #H #H0 destruct
- elim (drops_inv_skip1 … H1) -H1 #K #V #HLK #_ #H destruct
- | #g #Hf2 #H destruct
- lapply (drops_inv_drop1 … H1) -H1
- ] /3 width=4 by frees_sort/
-
-|
-|
-|
+ lapply (IH … HYK … H3) -IH -H3 -HYK [1,3: // | skip ]
+ /3 width=5 by drops_isuni_fwd_drop2, frees_sort_pushs/
+| #f1 #I #K #V #_ #IH #Hf1 #f #L #H1 #U #H2 #f2 #H3
+ lapply (isfin_inv_next … Hf1 ??) -Hf1 [3: |*: // ] #Hf1
+ lapply (lifts_inv_lref1 … H2) -H2 * #j #Hf #H destruct
+ elim (drops_split_trans_pair2 … H1) -H1 [ |*: // ] #Y #W #HLY #HYK #HVW
+ elim (coafter_fwd_xnx_pushs … H3) [ |*: // ] #g2 #H2 destruct
+ lapply (coafter_tls_succ … H3 ??) -H3 [3: |*: // ]
+ <tls_S in ⊢ (???%→?); <tls_pushs <tl_next_rew <tl_next_rew #H3
+ lapply (IH … HYK … HVW … H3) -IH -H3 -HYK -HVW //
+ /2 width=5 by frees_lref_pair/
+| #f1 #I #K #V #i #_ #IH #Hf1 #f #L #H1 #U #H2 #f2 #H3
+ lapply (isfin_fwd_push … Hf1 ??) -Hf1 [3: |*: // ] #Hf1
+ lapply (lifts_inv_lref1 … H2) -H2 * #x #Hf #H destruct
+ elim (at_inv_nxx … Hf) -Hf [ |*: // ] #j #Hf #H destruct
+ elim (drops_split_trans_pair2 … H1) -H1 [ |*: // ] #Y #W #HLY #HYK #_
+ elim (coafter_fwd_xpx_pushs … H3) [ |*: // ] #g2 #H2 destruct
+ lapply (coafter_tls_succ … H3 ??) -H3 [3: |*: // ] <tls_pushs #H3
+ lapply (drops_isuni_fwd_drop2 … HLY) -HLY // #HLY
+ lapply (IH … HYK … H3) -IH -H3 -HYK [4: |*: /2 width=2 by lifts_lref/ ]
+ >plus_S1 /2 width=3 by frees_lref_pushs/ (**) (* full auto fails *)
+| #f1 #I #K #V #l #_ #IH #Hf1 #f #L #H1 #U #H2 #f2 #H3
+ lapply (isfin_fwd_push … Hf1 ??) -Hf1 [3: |*: // ] #Hf1
+ lapply (lifts_inv_gref1 … H2) -H2 #H destruct
+ elim (drops_split_trans_pair2 … H1) -H1 [ |*: // ] #Y #W #HLY #HYK #_
+ elim (coafter_fwd_xpx_pushs … H3) [ |*: // ] #g2 #H2 destruct
+ lapply (coafter_tls_succ … H3 ??) -H3 [3: |*: // ] #H3
+ lapply (IH … HYK … H3) -IH -H3 -HYK [1,3: // | skip ]
+ /3 width=5 by drops_isuni_fwd_drop2, frees_gref_pushs/
| #f1V #f1T #f1 #p #I #K #V #T #_ #_ #H1f1 #IHV #IHT #H2f1 #f #L #H1 #Y #H2 #f2 #H3
elim (sor_inv_isfin3 … H1f1) // #Hf1V #H
lapply (isfin_inv_tl … H) -H
elim (coafter_sor … H3 … H1f1)
/3 width=5 by coafter_isfin2_fwd, frees_flat/
]
+qed-.
(* Inversion lemmas with generic slicing for local environments *************)
lemma pred_S: ∀m. pred (S m) = m.
// qed.
+lemma plus_S1: ∀x,y. ⫯(x+y) = (⫯x) + y.
+// qed.
+
lemma max_O1: ∀n. n = (0 ∨ n).
// qed.
lemma after_tls: ∀n,f1,f2,f. @⦃0, f1⦄ ≡ n →
f1 ⊚ f2 ≡ f → ⫱*[n]f1 ⊚ f2 ≡ ⫱*[n]f.
#n elim n -n //
-#n #IH #f1 #f2 #f #Hf1 #Hf cases (at_inv_pxn … Hf1) -Hf1 [ |*: // ]
-#g1 #Hg1 #H1 cases (after_inv_nxx … Hf … H1) -Hf /2 width=1 by/
+#n #IH #f1 #f2 #f #Hf1 #Hf
+cases (at_inv_pxn … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1
+cases (after_inv_nxx … Hf … H1) -Hf #g #Hg #H0 destruct
+<tls_xn <tls_xn /2 width=1 by/
qed.
(* Properties on isid *******************************************************)
elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
[ #g2 #j1 #Hg2 #H1 #H2 destruct
elim (after_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
- /3 width=5 by after_next/
+ <tls_xn /3 width=5 by after_next/
| #g2 #Hg2 #H2 destruct
elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
- /3 width=5 by after_next/
+ <tls_xn /3 width=5 by after_next/
]
]
qed.
elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
[ #g2 #j1 #Hg2 #H1 #H2 destruct
elim (after_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
- /3 width=5 by after_next/
+ <tls_xn /3 width=5 by after_next/
| #g2 #Hg2 #H2 destruct
elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
- /3 width=5 by after_next/
+ <tls_xn /3 width=5 by after_next/
]
]
qed.
lemma at_pxx_tls: ∀n,f. @⦃0, f⦄ ≡ n → @⦃0, ⫱*[n]f⦄ ≡ 0.
#n elim n -n //
-#n #IH #f #Hf cases (at_inv_pxn … Hf) -Hf /2 width=3 by/
+#n #IH #f #Hf
+cases (at_inv_pxn … Hf) -Hf [ |*: // ] #g #Hg #H0 destruct
+<tls_xn /2 width=1 by/
qed.
lemma at_tls: ∀i2,f. ↑⫱*[⫯i2]f ≗ ⫱*[i2]f → ∃i1. @⦃i1, f⦄ ≡ i2.
(* Inversion lemmas with tls ************************************************)
+lemma at_inv_nxx: ∀n,g,i1,j2. @⦃⫯i1, g⦄ ≡ j2 → @⦃0, g⦄ ≡ n →
+ ∃∃i2. @⦃i1, ⫱*[⫯n]g⦄ ≡ i2 & ⫯(n+i2) = j2.
+#n elim n -n
+[ #g #i1 #j2 #Hg #H
+ elim (at_inv_pxp … H) -H [ |*: // ] #f #H0
+ elim (at_inv_npx … Hg … H0) -Hg [ |*: // ] #x2 #Hf #H2 destruct
+ /2 width=3 by ex2_intro/
+| #n #IH #g #i1 #j2 #Hg #H
+ elim (at_inv_pxn … H) -H [ |*: // ] #f #Hf2 #H0
+ elim (at_inv_xnx … Hg … H0) -Hg #x2 #Hf1 #H2 destruct
+ elim (IH … Hf1 Hf2) -IH -Hf1 -Hf2 #i2 #Hf #H2 destruct
+ /2 width=3 by ex2_intro/
+]
+qed-.
+
lemma at_inv_tls: ∀i2,i1,f. @⦃i1, f⦄ ≡ i2 → ↑⫱*[⫯i2]f ≗ ⫱*[i2]f.
#i2 elim i2 -i2
[ #i1 #f #Hf elim (at_inv_xxp … Hf) -Hf // #g #H1 #H destruct
/2 width=1 by eq_refl/
-| #i2 #IH #i1 #f #Hf elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ] /2 width=2 by/
+| #i2 #IH #i1 #f #Hf
+ elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ]
+ [ #g #j1 #Hg #H1 #H2 | #g #Hg #Ho ] destruct
+ <tls_xn /2 width=2 by/
]
qed-.
f1 ≗ g1 → f2 ≗ g2 → f ≗ g.
/4 width=4 by coafter_mono, coafter_eq_repl_back1, coafter_eq_repl_back2/ qed-.
+(* Inversion lemmas with pushs **********************************************)
+
+lemma coafter_fwd_pushs: ∀n,g2,g1,g. g2 ~⊚ g1 ≡ g → @⦃0, g2⦄ ≡ n →
+ ∃f. ↑*[n]f = g.
+#n elim n -n /2 width=2 by ex_intro/
+#n #IH #g2 #g1 #g #Hg #Hg2
+cases (at_inv_pxn … Hg2) -Hg2 [ |*: // ] #f2 #Hf2 #H2
+cases (coafter_inv_nxx … Hg … H2) -Hg -H2 #f #Hf #H0 destruct
+elim (IH … Hf Hf2) -g1 -g2 -f2 /2 width=2 by ex_intro/
+qed-.
+
(* Inversion lemmas with tail ***********************************************)
lemma coafter_inv_tl1: ∀g2,g1,g. g2 ~⊚ ⫱g1 ≡ g →
#n elim n -n //
#n #IH #f1 #f2 #f #Hf1 #Hf
cases (at_inv_pxn … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1
-cases (coafter_inv_nxx … Hf … H1) -Hf /2 width=1 by/
+cases (coafter_inv_nxx … Hf … H1) -Hf #g #Hg #H0 destruct
+<tls_xn <tls_xn /2 width=1 by/
qed.
+lemma coafter_tls_succ: ∀g2,g1,g. g2 ~⊚ g1 ≡ g →
+ ∀n. @⦃0, g2⦄ ≡ n → ⫱*[⫯n]g2 ~⊚ ⫱g1 ≡ ⫱*[⫯n]g.
+#g2 #g1 #g #Hg #n #Hg2
+lapply (coafter_tls … Hg2 … Hg) -Hg #Hg
+lapply (at_pxx_tls … Hg2) -Hg2 #H
+elim (at_inv_pxp … H) -H [ |*: // ] #f2 #H2
+elim (coafter_inv_pxx … Hg … H2) -Hg * #f1 #f #Hf #H1 #H0 destruct
+<tls_S <tls_S <H2 <H0 -g2 -g -n //
+qed.
+
+lemma coafter_fwd_xpx_pushs: ∀g2,f1,g,n. g2 ~⊚ ↑f1 ≡ g → @⦃0, g2⦄ ≡ n →
+ ∃f. ↑*[⫯n]f = g.
+#g2 #g1 #g #n #Hg #Hg2
+elim (coafter_fwd_pushs … Hg Hg2) #f #H0 destruct
+lapply (coafter_tls … Hg2 Hg) -Hg <tls_pushs #Hf
+lapply (at_pxx_tls … Hg2) -Hg2 #H
+elim (at_inv_pxp … H) -H [ |*: // ] #f2 #H2
+elim (coafter_inv_pxx … Hf … H2) -Hf -H2 * #f1 #g #_ #H1 #H0 destruct
+[ /2 width=2 by ex_intro/
+| elim (discr_next_push … H1)
+]
+qed-.
+
+lemma coafter_fwd_xnx_pushs: ∀g2,f1,g,n. g2 ~⊚ ⫯f1 ≡ g → @⦃0, g2⦄ ≡ n →
+ ∃f. ↑*[n] ⫯f = g.
+#g2 #g1 #g #n #Hg #Hg2
+elim (coafter_fwd_pushs … Hg Hg2) #f #H0 destruct
+lapply (coafter_tls … Hg2 Hg) -Hg <tls_pushs #Hf
+lapply (at_pxx_tls … Hg2) -Hg2 #H
+elim (at_inv_pxp … H) -H [ |*: // ] #f2 #H2
+elim (coafter_inv_pxx … Hf … H2) -Hf -H2 * #f1 #g #_ #H1 #H0 destruct
+[ elim (discr_push_next … H1)
+| /2 width=2 by ex_intro/
+]
+qed-.
+
(* Properties on isid *******************************************************)
corec lemma coafter_isid_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ~⊚ f2 ≡ f2.
#n elim n -n /3 width=5 by eq_push/
qed.
-(* Advancedd properties *****************************************************)
+(* Advanced properties ******************************************************)
lemma pushs_xn: ∀n,f. ↑*[n] ↑f = ↑*[⫯n] f.
#n elim n -n //
(**************************************************************************)
include "ground_2/notation/functions/droppreds_2.ma".
+include "ground_2/relocation/rtmap_pushs.ma".
include "ground_2/relocation/rtmap_tl.ma".
(* RELOCATION MAP ***********************************************************)
(* Basic properties *********************************************************)
-lemma tls_rew_O: ∀f. f = ⫱*[0] f.
+lemma tls_O: ∀f. f = ⫱*[0] f.
// qed.
-lemma tls_rew_S: ∀f,n. ⫱ ⫱*[n] f = ⫱*[⫯n] f.
+lemma tls_S: ∀f,n. ⫱ ⫱*[n] f = ⫱*[⫯n] f.
// qed.
lemma tls_eq_repl: ∀n. eq_repl (λf1,f2. ⫱*[n] f1 ≗ ⫱*[n] f2).
#n elim n -n /3 width=1 by tl_eq_repl/
qed.
-(* Advancedd properties *****************************************************)
+(* Advanced properties ******************************************************)
lemma tls_xn: ∀n,f. ⫱*[n] ⫱f = ⫱*[⫯n] f.
#n elim n -n //
qed.
+
+(* Properties with pushs ****************************************************)
+
+lemma tls_pushs: ∀n,f. f = ⫱*[n] ↑*[n] f.
+#n elim n -n //
+#n #IH #f <tls_xn //
+qed.
projects / helm.git / commitdiff