1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2/substitution/cpys_lift.ma".
16 include "basic_2/substitution/cofrees.ma".
18 (* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************)
20 (* Advanced inversion lemmas ************************************************)
22 lemma cofrees_inv_lref_lt: ∀L,i,j. L ⊢ i ~ϵ 𝐅*⦃#j⦄ → j < i →
23 ∀I,K,W. ⇩[j]L ≡ K.ⓑ{I}W → K ⊢ i-j-1 ~ϵ 𝐅*⦃W⦄.
24 #L #i #j #Hj #Hji #I #K #W1 #HLK #W2 #HW12 elim (lift_total W2 0 (j+1))
25 #X2 #HWX2 elim (Hj X2) /2 width=7 by cpys_delta/ -I -L -K -W1
26 #Z2 #HZX2 elim (lift_div_le … HWX2 (i-j-1) 1 Z2) -HWX2 /2 width=2 by ex_intro/
27 >minus_plus <plus_minus_m_m //
30 lemma cofrees_inv_lt: ∀L,U,i. L ⊢ i ~ϵ 𝐅*⦃U⦄ → ∀j. (∀T. ⇧[j, 1] T ≡ U → ⊥) →
31 ∀I,K,W. ⇩[j]L ≡ K.ⓑ{I}W → j < i → K ⊢ i-j-1 ~ϵ 𝐅*⦃W⦄.
32 #L #U @(f2_ind … rfw … L U) -L -U
34 [ -IH #k #_ #i #_ #j #H elim (H (⋆k)) -H //
35 | -IH #j #_ #i #Hi0 #j0 #H <(nlift_inv_lref_be_SO … H) -j0
36 /2 width=7 by cofrees_inv_lref_lt/
37 | -IH #p #_ #i #_ #j #H elim (H (§p)) -H //
38 | #a #J #W #U #Hn #i #H1 #j #H2 #I #K #V #HLK #Hji destruct
39 elim (cofrees_inv_bind … H1) -H1 #HW #HU
40 elim (nlift_inv_bind … H2) -H2 [ -HU /3 width=7 by/ ]
41 -HW #HnU lapply (IH … HU … HnU I K V ? ?)
42 /2 width=1 by ldrop_drop, lt_minus_to_plus/ -a -I -J -L -W -U
44 | #J #W #U #Hn #i #H1 #j #H2 #I #K #V #HLK #Hji destruct
45 elim (cofrees_inv_flat … H1) -H1 #HW #HU
46 elim (nlift_inv_flat … H2) -H2 [ /3 width=7 by/ ]
47 #HnU @(IH … HU … HnU … HLK) // (**) (* full auto fails *)
51 (* Advanced properties ******************************************************)
53 lemma cofrees_lref_gt: ∀L,i,j. i < j → L ⊢ i ~ϵ 𝐅*⦃#j⦄.
54 #L #i #j #Hij #X #H elim (cpys_inv_lref1 … H) -H
55 [ #H destruct /3 width=2 by lift_lref_ge_minus, ex_intro/
56 | * #I #K #V1 #V2 #_ #_ #H -I -L -K -V1
57 elim (lift_split … H i j) /2 width=2 by lt_to_le, ex_intro/
61 lemma cofrees_lref_lt: ∀I,L,K,W,i,j. j < i → ⇩[j] L ≡ K.ⓑ{I}W →
62 K ⊢ (i-j-1) ~ϵ 𝐅*⦃W⦄ → L ⊢ i ~ϵ 𝐅*⦃#j⦄.
63 #I #L #K #W1 #i #j #Hji #HLK #HW1 #X #H elim (cpys_inv_lref1 … H) -H
64 [ #H destruct /3 width=2 by lift_lref_lt, ex_intro/
65 | * #I0 #K0 #W0 #W2 #HLK0 #HW12 #HW2 lapply (ldrop_mono … HLK0 … HLK) -L
66 #H destruct elim (HW1 … HW12) -I -K -W1
67 #V2 #HVW2 elim (lift_trans_le … HVW2 … HW2) -W2 //
68 >minus_plus <plus_minus_m_m /2 width=2 by ex_intro/
72 lemma cofrees_lref_free: ∀L,i,j. |L| ≤ j → j < i → L ⊢ i ~ϵ 𝐅*⦃#j⦄.
73 #L #i #j #Hj #Hji #X #H elim (cpys_inv_lref1 … H) -H
74 [ #H destruct /3 width=2 by lift_lref_lt, ex_intro/
75 | * #I #K #W1 #W2 #HLK lapply (ldrop_fwd_length_lt2 … HLK) -I
76 #H elim (lt_refl_false j) -K -W1 -W2 -X -i /2 width=3 by lt_to_le_to_lt/
80 (* Advanced negated inversion lemmas ****************************************)
82 lemma frees_inv_lref_lt: ∀L,i,j. j < i → (L ⊢ i ~ϵ 𝐅*⦃#j⦄ → ⊥) →
83 ∃∃I,K,W. ⇩[j] L ≡ K.ⓑ{I}W & (K ⊢ (i-j-1) ~ϵ 𝐅*⦃W⦄ → ⊥).
84 #L #i #j #Hji #H elim (lt_or_ge j (|L|)) #Hj
85 [ elim (ldrop_O1_lt (Ⓕ) … Hj) -Hj /4 width=9 by cofrees_lref_lt, ex2_3_intro/
86 | elim H -H /2 width=5 by cofrees_lref_free/
90 lemma frees_inv_lref_free: ∀L,i,j. (L ⊢ i ~ϵ 𝐅*⦃#j⦄ → ⊥) → |L| ≤ j → j = i.
91 #L #i #j #H #Hj elim (lt_or_eq_or_gt i j) //
92 #Hij elim H -H /2 width=5 by cofrees_lref_gt, cofrees_lref_free/
95 lemma frees_inv_gen: ∀L,U,i. (L ⊢ i ~ϵ 𝐅*⦃U⦄ → ⊥) →
96 ∃∃U0. ⦃⋆, L⦄ ⊢ U ▶* U0 & (∀T. ⇧[i, 1] T ≡ U0 → ⊥).
97 #L #U @(f2_ind … rfw … L U) -L -U
99 [ -IH #k #_ #i #H elim H -H //
100 | #j #Hn #i #H elim (lt_or_eq_or_gt i j)
101 [ -n #Hij elim H -H /2 width=4 by cofrees_lref_gt/
102 | -H -n #H destruct /3 width=7 by lift_inv_lref2_be, ex2_intro/
103 | #Hji elim (frees_inv_lref_lt … H) // -H
104 #I #K #W1 #HLK #H elim (IH … H) /2 width=3 by ldrop_fwd_rfw/ -H -n
105 #W2 #HW12 #HnW2 elim (lift_total W2 0 (j+1))
106 #U2 #HWU2 @(ex2_intro … U2) /2 width=7 by cpys_delta/ -I -L -K -W1
107 #T2 #HTU2 elim (lift_div_le … HWU2 (i-j-1) 1 T2) /2 width=2 by/ -W2
108 >minus_plus <plus_minus_m_m //
110 | -IH #p #_ #i #H elim H -H //
111 | #a #I #W #U #Hn #i #H elim (frees_inv_bind … H) -H
112 #H elim (IH … H) // -H -n
113 #X #HX #HnX [ @(ex2_intro … (ⓑ{a,I}X.U)) | @(ex2_intro … (ⓑ{a,I}W.X)) ] (**) (* explicit constructor *)
114 /3 width=9 by cpys_bind, nlift_bind_dx, nlift_bind_sn/
115 | #I #W #U #Hn #i #H elim (frees_inv_flat … H) -H
116 #H elim (IH … H) // -H -n
117 #X #HX #HnX [ @(ex2_intro … (ⓕ{I}X.U)) | @(ex2_intro … (ⓕ{I}W.X)) ] (**) (* explicit constructor *)
118 /3 width=8 by cpys_flat, nlift_flat_dx, nlift_flat_sn/
122 (* Advanced negated properties **********************************************)
124 lemma frees_lt: ∀I,L,K,W,j. ⇩[j]L ≡ K.ⓑ{I}W →
125 ∀i. j < i → (K ⊢ i-j-1 ~ϵ 𝐅*⦃W⦄ → ⊥) →
126 ∀U. (∀T. ⇧[j, 1] T ≡ U → ⊥) →
127 (L ⊢ i ~ϵ 𝐅*⦃U⦄ → ⊥).
128 /4 width=9 by cofrees_inv_lt/ qed-.
130 (* Relocation properties ****************************************************)
132 lemma cofrees_lift_be: ∀d,e,i. d ≤ i → i ≤ d + e →
133 ∀L,K,s. ⇩[s, d, e+1] L ≡ K → ∀T,U. ⇧[d, e+1] T ≡ U →
135 #d #e #i #Hdi #Hide #L #K #s #HLK #T1 #U1 #HTU1 #U2 #HU12
136 elim (cpys_inv_lift1 … HU12 … HLK … HTU1) #T2 #HTU2 #_ -s -L -K -U1 -T1
137 elim (lift_split … HTU2 i e) /2 width=2 by ex_intro/
140 lemma cofrees_lift_ge: ∀d,e,i. d + e ≤ i →
141 ∀L,K,s. ⇩[s, d, e] L ≡ K → ∀T,U. ⇧[d, e] T ≡ U →
142 K ⊢ i-e ~ϵ 𝐅*⦃T⦄ → L ⊢ i ~ϵ 𝐅*⦃U⦄.
143 #d #e #i #Hdei #L #K #s #HLK #T1 #U1 #HTU1 #HT1 #U2 #HU12
144 elim (le_inv_plus_l … Hdei) -Hdei #Hdie #Hei
145 elim (cpys_inv_lift1 … HU12 … HLK … HTU1) -s -L #T2 #HTU2 #HT12
146 elim (HT1 … HT12) -T1 #V2 #HVT2
147 elim (lift_trans_le … HVT2 … HTU2 ?) // <plus_minus_m_m /2 width=2 by ex_intro/