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_be: āL,d,i,j. L ā¢ i ~Ļµ š
*[d]ā¦#jā¦ ā d ā¤ yinj j ā j < i ā
23 āI,K,W. ā©[j]L ā” K.ā{I}W ā K ā¢ i-j-1 ~Ļµ š
*[yinj 0]ā¦Wā¦.
24 #L #d #i #j #Hj #Hdj #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_subst_Y2/ -I -L -K -W1 -d
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_be: āL,U,d,i. L ā¢ i ~Ļµ š
*[d]ā¦Uā¦ ā āj. (āT. ā§[j, 1] T ā” U ā ā„) ā
31 āI,K,W. ā©[j]L ā” K.ā{I}W ā d ā¤ yinj j ā j < i ā K ā¢ i-j-1 ~Ļµ š
*[yinj 0]ā¦Wā¦.
32 #L #U @(f2_ind ā¦ rfw ā¦ L U) -L -U
34 [ -IH #k #_ #d #i #_ #j #H elim (H (āk)) -H //
35 | -IH #j #_ #d #i #Hi0 #j0 #H <(nlift_inv_lref_be_SO ā¦ H) -j0
36 /2 width=9 by cofrees_inv_lref_be/
37 | -IH #p #_ #d #i #_ #j #H elim (H (Ā§p)) -H //
38 | #a #J #W #U #Hn #d #i #H1 #j #H2 #I #K #V #HLK #Hdj #Hji destruct
39 elim (cofrees_inv_bind ā¦ H1) -H1 #HW #HU
40 elim (nlift_inv_bind ā¦ H2) -H2 [ -HU /3 width=9 by/ ]
41 -HW #HnU lapply (IH ā¦ HU ā¦ HnU I K V ? ? ?)
42 /2 width=1 by ldrop_drop, yle_succ, lt_minus_to_plus/ -a -I -J -L -W -U -d
44 | #J #W #U #Hn #d #i #H1 #j #H2 #I #K #V #HLK #Hdj #Hji destruct
45 elim (cofrees_inv_flat ā¦ H1) -H1 #HW #HU
46 elim (nlift_inv_flat ā¦ H2) -H2 [ /3 width=9 by/ ]
47 #HnU @(IH ā¦ HU ā¦ HnU ā¦ HLK) // (**) (* full auto fails *)
51 (* Advanced properties ******************************************************)
53 lemma cofrees_lref_skip: āL,d,i,j. j < i ā yinj j < d ā L ā¢ i ~Ļµ š
*[d]ā¦#jā¦.
54 #L #d #i #j #Hji #Hjd #X #H elim (cpys_inv_lref1_Y2 ā¦ H) -H
55 [ #H destruct /3 width=2 by lift_lref_lt, ex_intro/
56 | * #I #K #W1 #W2 #Hdj elim (ylt_yle_false ā¦ Hdj) -i -I -L -K -W1 -W2 -X //
60 lemma cofrees_lref_lt: āL,d,i,j. i < j ā L ā¢ i ~Ļµ š
*[d]ā¦#jā¦.
61 #L #d #i #j #Hij #X #H elim (cpys_inv_lref1_Y2 ā¦ H) -H
62 [ #H destruct /3 width=2 by lift_lref_ge_minus, ex_intro/
63 | * #I #K #V1 #V2 #_ #_ #_ #H -I -L -K -V1 -d
64 elim (lift_split ā¦ H i j) /2 width=2 by lt_to_le, ex_intro/
68 lemma cofrees_lref_gt: āI,L,K,W,d,i,j. j < i ā ā©[j] L ā” K.ā{I}W ā
69 K ā¢ (i-j-1) ~Ļµ š
*[O]ā¦Wā¦ ā L ā¢ i ~Ļµ š
*[d]ā¦#jā¦.
70 #I #L #K #W1 #d #i #j #Hji #HLK #HW1 #X #H elim (cpys_inv_lref1_Y2 ā¦ H) -H
71 [ #H destruct /3 width=2 by lift_lref_lt, ex_intro/
72 | * #I0 #K0 #W0 #W2 #Hdj #HLK0 #HW12 #HW2 lapply (ldrop_mono ā¦ HLK0 ā¦ HLK) -L
73 #H destruct elim (HW1 ā¦ HW12) -I -K -W1 -d
74 #V2 #HVW2 elim (lift_trans_le ā¦ HVW2 ā¦ HW2) -W2 //
75 >minus_plus <plus_minus_m_m /2 width=2 by ex_intro/
79 lemma cofrees_lref_free: āL,d,i,j. |L| ā¤ j ā j < i ā L ā¢ i ~Ļµ š
*[d]ā¦#jā¦.
80 #L #d #i #j #Hj #Hji #X #H elim (cpys_inv_lref1_Y2 ā¦ H) -H
81 [ #H destruct /3 width=2 by lift_lref_lt, ex_intro/
82 | * #I #K #W1 #W2 #_ #HLK lapply (ldrop_fwd_length_lt2 ā¦ HLK) -I
83 #H elim (lt_refl_false j) -d -i -K -W1 -W2 -X /2 width=3 by lt_to_le_to_lt/
87 (* Advanced negated inversion lemmas ****************************************)
89 lemma frees_inv_lref_gt: āL,d,i,j. j < i ā (L ā¢ i ~Ļµ š
*[d]ā¦#jā¦ ā ā„) ā
90 āāI,K,W. ā©[j] L ā” K.ā{I}W & (K ā¢ (i-j-1) ~Ļµ š
*[0]ā¦Wā¦ ā ā„) & d ā¤ yinj j.
91 #L #d #i #j #Hji #H elim (ylt_split j d) #Hjd
92 [ elim H -H /2 width=6 by cofrees_lref_skip/
93 | elim (lt_or_ge j (|L|)) #Hj
94 [ elim (ldrop_O1_lt ā¦ Hj) -Hj /4 width=10 by cofrees_lref_gt, ex3_3_intro/
95 | elim H -H /2 width=6 by cofrees_lref_free/
100 lemma frees_inv_lref_free: āL,d,i,j. (L ā¢ i ~Ļµ š
*[d]ā¦#jā¦ ā ā„) ā |L| ā¤ j ā j = i.
101 #L #d #i #j #H #Hj elim (lt_or_eq_or_gt i j) //
102 #Hij elim H -H /2 width=6 by cofrees_lref_lt, cofrees_lref_free/
105 lemma frees_inv_gen: āL,U,d,i. (L ā¢ i ~Ļµ š
*[d]ā¦Uā¦ ā ā„) ā
106 āāU0. ā¦ā, Lā¦ ā¢ U ā¶*[d, ā] U0 & (āT. ā§[i, 1] T ā” U0 ā ā„).
107 #L #U @(f2_ind ā¦ rfw ā¦ L U) -L -U
109 [ -IH #k #_ #d #i #H elim H -H //
110 | #j #Hn #d #i #H elim (lt_or_eq_or_gt i j)
111 [ -n #Hij elim H -H /2 width=5 by cofrees_lref_lt/
112 | -H -n #H destruct /3 width=7 by lift_inv_lref2_be, ex2_intro/
113 | #Hji elim (frees_inv_lref_gt ā¦ H) // -H
114 #I #K #W1 #HLK #H #Hdj elim (IH ā¦ H) /2 width=3 by ldrop_fwd_rfw/ -H -n
115 #W2 #HW12 #HnW2 elim (lift_total W2 0 (j+1))
116 #U2 #HWU2 @(ex2_intro ā¦ U2) /2 width=7 by cpys_subst_Y2/ -I -L -K -W1 -d
117 #T2 #HTU2 elim (lift_div_le ā¦ HWU2 (i-j-1) 1 T2) /2 width=2 by/ -W2
118 >minus_plus <plus_minus_m_m //
120 | -IH #p #_ #d #i #H elim H -H //
121 | #a #I #W #U #Hn #d #i #H elim (frees_inv_bind ā¦ H) -H
122 #H elim (IH ā¦ H) // -H -n
123 /4 width=9 by cpys_bind, nlift_bind_dx, nlift_bind_sn, ex2_intro/
124 | #I #W #U #Hn #d #i #H elim (frees_inv_flat ā¦ H) -H
125 #H elim (IH ā¦ H) // -H -n
126 /4 width=9 by cpys_flat, nlift_flat_dx, nlift_flat_sn, ex2_intro/
130 lemma frees_ind: āL,d,i. āR:predicate term.
131 (āU1. (āT1. ā§[i, 1] T1 ā” U1 ā ā„) ā R U1) ā
132 (āU1,U2. ā¦ā, Lā¦ ā¢ U1 ā¶[d, ā] U2 ā (L ā¢ i ~Ļµ š
*[d]ā¦U2ā¦ ā ā„) ā R U2 ā R U1) ā
133 āU. (L ā¢ i ~Ļµ š
*[d]ā¦Uā¦ ā ā„) ā R U.
134 #L #d #i #R #IH1 #IH2 #U1 #H elim (frees_inv_gen ā¦ H) -H
135 #U2 #H #HnU2 @(cpys_ind_dx ā¦ H) -U1 /4 width=8 by cofrees_inv_gen/
138 (* Advanced negated properties **********************************************)
140 lemma frees_be: āI,L,K,W,j. ā©[j]L ā” K.ā{I}W ā
141 āi. j < i ā (K ā¢ i-j-1 ~Ļµ š
*[yinj 0]ā¦Wā¦ ā ā„) ā
142 āU. (āT. ā§[j, 1] T ā” U ā ā„) ā
143 ād. d ā¤ yinj j ā (L ā¢ i ~Ļµ š
*[d]ā¦Uā¦ ā ā„).
144 /4 width=11 by cofrees_inv_be/ qed-.