--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/substitution/cpys_lift.ma".
+include "basic_2/substitution/cofrees.ma".
+
+(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cofrees_inv_lref_be: ∀L,d,i,j. L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄ → d ≤ yinj j → j < i →
+ ∀I,K,W. ⇩[j]L ≡ K.ⓑ{I}W → K ⊢ i-j-1 ~ϵ 𝐅*[yinj 0]⦃W⦄.
+#L #d #i #j #Hj #Hdj #Hji #I #K #W1 #HLK #W2 #HW12 elim (lift_total W2 0 (j+1))
+#X2 #HWX2 elim (Hj X2) /2 width=7 by cpys_subst_Y2/ -I -L -K -W1 -d
+#Z2 #HZX2 elim (lift_div_le … HWX2 (i-j-1) 1 Z2) -HWX2 /2 width=2 by ex_intro/
+>minus_plus <plus_minus_m_m //
+qed-.
+
+lemma cofrees_inv_be: ∀L,U,d,i. L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ∀j. (∀T. ⇧[j, 1] T ≡ U → ⊥) →
+ ∀I,K,W. ⇩[j]L ≡ K.ⓑ{I}W → d ≤ yinj j → j < i → K ⊢ i-j-1 ~ϵ 𝐅*[yinj 0]⦃W⦄.
+#L #U @(f2_ind … rfw … L U) -L -U
+#n #IH #L * *
+[ -IH #k #_ #d #i #_ #j #H elim (H (⋆k)) -H //
+| -IH #j #_ #d #i #Hi0 #j0 #H <(nlift_inv_lref_be_SO … H) -j0
+ /2 width=9 by cofrees_inv_lref_be/
+| -IH #p #_ #d #i #_ #j #H elim (H (§p)) -H //
+| #a #J #W #U #Hn #d #i #H1 #j #H2 #I #K #V #HLK #Hdj #Hji destruct
+ elim (cofrees_inv_bind … H1) -H1 #HW #HU
+ elim (nlift_inv_bind … H2) -H2 [ -HU /3 width=9 by/ ]
+ -HW #HnU lapply (IH … HU … HnU I K V ? ? ?)
+ /2 width=1 by ldrop_drop, yle_succ, lt_minus_to_plus/ -a -I -J -L -W -U -d
+ >minus_plus_plus_l //
+| #J #W #U #Hn #d #i #H1 #j #H2 #I #K #V #HLK #Hdj #Hji destruct
+ elim (cofrees_inv_flat … H1) -H1 #HW #HU
+ elim (nlift_inv_flat … H2) -H2 [ /3 width=9 by/ ]
+ #HnU @(IH … HU … HnU … HLK) // (**) (* full auto fails *)
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma cofrees_lref_skip: ∀L,d,i,j. j < i → yinj j < d → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄.
+#L #d #i #j #Hji #Hjd #X #H elim (cpys_inv_lref1_Y2 … H) -H
+[ #H destruct /3 width=2 by lift_lref_lt, ex_intro/
+| * #I #K #W1 #W2 #Hdj elim (ylt_yle_false … Hdj) -i -I -L -K -W1 -W2 -X //
+]
+qed.
+
+lemma cofrees_lref_lt: ∀L,d,i,j. i < j → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄.
+#L #d #i #j #Hij #X #H elim (cpys_inv_lref1_Y2 … H) -H
+[ #H destruct /3 width=2 by lift_lref_ge_minus, ex_intro/
+| * #I #K #V1 #V2 #_ #_ #_ #H -I -L -K -V1 -d
+ elim (lift_split … H i j) /2 width=2 by lt_to_le, ex_intro/
+]
+qed.
+
+lemma cofrees_lref_gt: ∀I,L,K,W,d,i,j. j < i → ⇩[j] L ≡ K.ⓑ{I}W →
+ K ⊢ (i-j-1) ~ϵ 𝐅*[O]⦃W⦄ → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄.
+#I #L #K #W1 #d #i #j #Hji #HLK #HW1 #X #H elim (cpys_inv_lref1_Y2 … H) -H
+[ #H destruct /3 width=2 by lift_lref_lt, ex_intro/
+| * #I0 #K0 #W0 #W2 #Hdj #HLK0 #HW12 #HW2 lapply (ldrop_mono … HLK0 … HLK) -L
+ #H destruct elim (HW1 … HW12) -I -K -W1 -d
+ #V2 #HVW2 elim (lift_trans_le … HVW2 … HW2) -W2 //
+ >minus_plus <plus_minus_m_m /2 width=2 by ex_intro/
+]
+qed.
+
+lemma cofrees_lref_free: ∀L,d,i,j. |L| ≤ j → j < i → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄.
+#L #d #i #j #Hj #Hji #X #H elim (cpys_inv_lref1_Y2 … H) -H
+[ #H destruct /3 width=2 by lift_lref_lt, ex_intro/
+| * #I #K #W1 #W2 #_ #HLK lapply (ldrop_fwd_length_lt2 … HLK) -I
+ #H elim (lt_refl_false j) -d -i -K -W1 -W2 -X /2 width=3 by lt_to_le_to_lt/
+]
+qed.
+
+(* Advanced negated inversion lemmas ****************************************)
+
+lemma frees_inv_lref_gt: ∀L,d,i,j. j < i → (L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄ → ⊥) →
+ ∃∃I,K,W. ⇩[j] L ≡ K.ⓑ{I}W & (K ⊢ (i-j-1) ~ϵ 𝐅*[0]⦃W⦄ → ⊥) & d ≤ yinj j.
+#L #d #i #j #Hji #H elim (ylt_split j d) #Hjd
+[ elim H -H /2 width=6 by cofrees_lref_skip/
+| elim (lt_or_ge j (|L|)) #Hj
+ [ elim (ldrop_O1_lt … Hj) -Hj /4 width=10 by cofrees_lref_gt, ex3_3_intro/
+ | elim H -H /2 width=6 by cofrees_lref_free/
+ ]
+]
+qed-.
+
+lemma frees_inv_lref_free: ∀L,d,i,j. (L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄ → ⊥) → |L| ≤ j → j = i.
+#L #d #i #j #H #Hj elim (lt_or_eq_or_gt i j) //
+#Hij elim H -H /2 width=6 by cofrees_lref_lt, cofrees_lref_free/
+qed-.
+
+lemma frees_inv_gen: ∀L,U,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) →
+ ∃∃U0. ⦃⋆, L⦄ ⊢ U ▶*[d, ∞] U0 & (∀T. ⇧[i, 1] T ≡ U0 → ⊥).
+#L #U @(f2_ind … rfw … L U) -L -U
+#n #IH #L * *
+[ -IH #k #_ #d #i #H elim H -H //
+| #j #Hn #d #i #H elim (lt_or_eq_or_gt i j)
+ [ -n #Hij elim H -H /2 width=5 by cofrees_lref_lt/
+ | -H -n #H destruct /3 width=7 by lift_inv_lref2_be, ex2_intro/
+ | #Hji elim (frees_inv_lref_gt … H) // -H
+ #I #K #W1 #HLK #H #Hdj elim (IH … H) /2 width=3 by ldrop_fwd_rfw/ -H -n
+ #W2 #HW12 #HnW2 elim (lift_total W2 0 (j+1))
+ #U2 #HWU2 @(ex2_intro … U2) /2 width=7 by cpys_subst_Y2/ -I -L -K -W1 -d
+ #T2 #HTU2 elim (lift_div_le … HWU2 (i-j-1) 1 T2) /2 width=2 by/ -W2
+ >minus_plus <plus_minus_m_m //
+ ]
+| -IH #p #_ #d #i #H elim H -H //
+| #a #I #W #U #Hn #d #i #H elim (frees_inv_bind … H) -H
+ #H elim (IH … H) // -H -n
+ /4 width=9 by cpys_bind, nlift_bind_dx, nlift_bind_sn, ex2_intro/
+| #I #W #U #Hn #d #i #H elim (frees_inv_flat … H) -H
+ #H elim (IH … H) // -H -n
+ /4 width=9 by cpys_flat, nlift_flat_dx, nlift_flat_sn, ex2_intro/
+]
+qed-.
+
+lemma frees_ind: ∀L,d,i. ∀R:predicate term.
+ (∀U1. (∀T1. ⇧[i, 1] T1 ≡ U1 → ⊥) → R U1) →
+ (∀U1,U2. ⦃⋆, L⦄ ⊢ U1 ▶[d, ∞] U2 → (L ⊢ i ~ϵ 𝐅*[d]⦃U2⦄ → ⊥) → R U2 → R U1) →
+ ∀U. (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → R U.
+#L #d #i #R #IH1 #IH2 #U1 #H elim (frees_inv_gen … H) -H
+#U2 #H #HnU2 @(cpys_ind_dx … H) -U1 /4 width=8 by cofrees_inv_gen/
+qed-.
+
+(* Advanced negated properties **********************************************)
+
+lemma frees_be: ∀I,L,K,W,j. ⇩[j]L ≡ K.ⓑ{I}W →
+ ∀i. j < i → (K ⊢ i-j-1 ~ϵ 𝐅*[yinj 0]⦃W⦄ → ⊥) →
+ ∀U. (∀T. ⇧[j, 1] T ≡ U → ⊥) →
+ ∀d. d ≤ yinj j → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥).
+/4 width=11 by cofrees_inv_be/ qed-.
+
+(* Relocation properties ****************************************************)
+
+lemma cofrees_lift_be: ∀d0,e0,i. d0 ≤ i → i ≤ d0 + e0 →
+ ∀L,K,s. ⇩[s, d0, e0+1] L ≡ K → ∀T,U. ⇧[d0, e0+1] T ≡ U →
+ ∀d. L ⊢ i ~ϵ 𝐅*[d]⦃U⦄.
+#d0 #e0 #i #Hd0i #Hide0 #L #K #s #HLK #T1 #U1 #HTU1 #d #U2 #HU12
+elim (yle_split d0 d) #H1
+[ elim (yle_split d (d0+e0+1)) #H2
+ [ letin cpys_inv ≝ cpys_inv_lift1_ge_up
+ | letin cpys_inv ≝ cpys_inv_lift1_ge
+ ]
+| letin cpys_inv ≝ cpys_inv_lift1_be
+]
+elim (cpys_inv … HU12 … HLK … HTU1) // #T2 #_ #HTU2 -s -L -K -U1 -T1 -d
+elim (lift_split … HTU2 i e0) /2 width=2 by ex_intro/
+qed.
+
+lemma cofrees_lift_ge: ∀d0,e0,i. d0 + e0 ≤ i →
+ ∀L,K,s. ⇩[s, d0, e0] L ≡ K → ∀T,U. ⇧[d0, e0] T ≡ U →
+ ∀d. K ⊢ i-e0 ~ϵ 𝐅*[d-yinj e0]⦃T⦄ → L ⊢ i ~ϵ 𝐅*[d]⦃U⦄.
+#d0 #e0 #i #Hde0i #L #K #s #HLK #T1 #U1 #HTU1 #d #HT1 #U2 #HU12
+elim (le_inv_plus_l … Hde0i) -Hde0i #Hd0ie0 #He0i
+elim (yle_split d0 d) #H1
+[ elim (yle_split d (d0+e0)) #H2
+ [ elim (cpys_inv_lift1_ge_up … HU12 … HLK … HTU1) // >yplus_inj >yminus_Y_inj #T2 #HT12
+ lapply (cpys_weak … HT12 (d-yinj e0) (∞) ? ?) /2 width=1 by yle_plus2_to_minus_inj2/ -HT12
+ | elim (cpys_inv_lift1_ge … HU12 … HLK … HTU1) // #T2
+ ]
+| elim (cpys_inv_lift1_be … HU12 … HLK … HTU1) // >yminus_Y_inj #T2 #HT12
+ lapply (cpys_weak … HT12 (d-yinj e0) (∞) ? ?) // -HT12
+]
+-s -L #HT12 #HTU2
+elim (HT1 … HT12) -T1 #V2 #HVT2
+elim (lift_trans_le … HVT2 … HTU2 ?) // <plus_minus_m_m /2 width=2 by ex_intro/
+qed.
projects / helm.git / blobdiff