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 "ground_2A/ynat/ynat_plus.ma".
16 include "basic_2A/notation/relations/freestar_4.ma".
17 include "basic_2A/substitution/lift_neg.ma".
18 include "basic_2A/substitution/drop.ma".
20 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
22 inductive frees: relation4 ynat lenv term nat ≝
23 | frees_eq: ∀L,U,l,i. (∀T. ⬆[i, 1] T ≡ U → ⊥) → frees l L U i
24 | frees_be: ∀I,L,K,U,W,l,i,j. l ≤ yinj j → j < i →
25 (∀T. ⬆[j, 1] T ≡ U → ⊥) → ⬇[j]L ≡ K.ⓑ{I}W →
26 frees 0 K W (i-j-1) → frees l L U i.
29 "context-sensitive free variables (term)"
30 'FreeStar L i l U = (frees l L U i).
32 definition frees_trans: predicate (relation3 lenv term term) ≝
33 λR. ∀L,U1,U2,i. R L U1 U2 → L ⊢ i ϵ 𝐅*[0]⦃U2⦄ → L ⊢ i ϵ 𝐅*[0]⦃U1⦄.
35 (* Basic inversion lemmas ***************************************************)
37 lemma frees_inv: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
38 (∀T. ⬆[i, 1] T ≡ U → ⊥) ∨
39 ∃∃I,K,W,j. l ≤ yinj j & j < i & (∀T. ⬆[j, 1] T ≡ U → ⊥) &
40 ⬇[j]L ≡ K.ⓑ{I}W & K ⊢ (i-j-1) ϵ 𝐅*[yinj 0]⦃W⦄.
41 #L #U #l #i * -L -U -l -i /4 width=9 by ex5_4_intro, or_intror, or_introl/
44 lemma frees_inv_sort: ∀L,l,i,k. L ⊢ i ϵ 𝐅*[l]⦃⋆k⦄ → ⊥.
45 #L #l #i #k #H elim (frees_inv … H) -H [|*] /2 width=2 by/
48 lemma frees_inv_gref: ∀L,l,i,p. L ⊢ i ϵ 𝐅*[l]⦃§p⦄ → ⊥.
49 #L #l #i #p #H elim (frees_inv … H) -H [|*] /2 width=2 by/
52 lemma frees_inv_lref: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ →
54 ∃∃I,K,W. l ≤ yinj j & j < i & ⬇[j] L ≡ K.ⓑ{I}W & K ⊢ (i-j-1) ϵ 𝐅*[yinj 0]⦃W⦄.
55 #L #l #x #i #H elim (frees_inv … H) -H
56 [ /4 width=2 by nlift_inv_lref_be_SO, or_introl/
57 | * #I #K #W #j #Hlj #Hji #Hnx #HLK #HW
58 >(nlift_inv_lref_be_SO … Hnx) -x /3 width=5 by ex4_3_intro, or_intror/
62 lemma frees_inv_lref_free: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → |L| ≤ j → j = i.
63 #L #l #j #i #H #Hj elim (frees_inv_lref … H) -H //
64 * #I #K #W #_ #_ #HLK lapply (drop_fwd_length_lt2 … HLK) -I
65 #H elim (lt_refl_false j) /2 width=3 by lt_to_le_to_lt/
68 lemma frees_inv_lref_skip: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → yinj j < l → j = i.
69 #L #l #j #i #H #Hjl elim (frees_inv_lref … H) -H //
70 * #I #K #W #Hlj elim (ylt_yle_false … Hlj) -Hlj //
73 lemma frees_inv_lref_ge: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → i ≤ j → j = i.
74 #L #l #j #i #H #Hij elim (frees_inv_lref … H) -H //
75 * #I #K #W #_ #Hji elim (lt_refl_false j) -I -L -K -W -l /2 width=3 by lt_to_le_to_lt/
78 lemma frees_inv_lref_lt: ∀L,l,j,i.L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → j < i →
79 ∃∃I,K,W. l ≤ yinj j & ⬇[j] L ≡ K.ⓑ{I}W & K ⊢ (i-j-1) ϵ 𝐅*[yinj 0]⦃W⦄.
80 #L #l #j #i #H #Hji elim (frees_inv_lref … H) -H
81 [ #H elim (lt_refl_false j) //
82 | * /2 width=5 by ex3_3_intro/
86 lemma frees_inv_bind: ∀a,I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃ⓑ{a,I}W.U⦄ →
87 L ⊢ i ϵ 𝐅*[l]⦃W⦄ ∨ L.ⓑ{I}W ⊢ i+1 ϵ 𝐅*[⫯l]⦃U⦄ .
88 #a #J #L #V #U #l #i #H elim (frees_inv … H) -H
89 [ #HnX elim (nlift_inv_bind … HnX) -HnX
90 /4 width=2 by frees_eq, or_intror, or_introl/
91 | * #I #K #W #j #Hlj #Hji #HnX #HLK #HW elim (nlift_inv_bind … HnX) -HnX
92 [ /4 width=9 by frees_be, or_introl/
93 | #HnT @or_intror @(frees_be … HnT) -HnT
94 [4,5,6: /2 width=1 by drop_drop, yle_succ, lt_minus_to_plus/
95 |7: >minus_plus_plus_l //
102 lemma frees_inv_flat: ∀I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃ⓕ{I}W.U⦄ →
103 L ⊢ i ϵ 𝐅*[l]⦃W⦄ ∨ L ⊢ i ϵ 𝐅*[l]⦃U⦄ .
104 #J #L #V #U #l #i #H elim (frees_inv … H) -H
105 [ #HnX elim (nlift_inv_flat … HnX) -HnX
106 /4 width=2 by frees_eq, or_intror, or_introl/
107 | * #I #K #W #j #Hlj #Hji #HnX #HLK #HW elim (nlift_inv_flat … HnX) -HnX
108 /4 width=9 by frees_be, or_intror, or_introl/
112 (* Basic properties *********************************************************)
114 lemma frees_lref_eq: ∀L,l,i. L ⊢ i ϵ 𝐅*[l]⦃#i⦄.
115 /3 width=7 by frees_eq, lift_inv_lref2_be/ qed.
117 lemma frees_lref_be: ∀I,L,K,W,l,i,j. l ≤ yinj j → j < i → ⬇[j]L ≡ K.ⓑ{I}W →
118 K ⊢ i-j-1 ϵ 𝐅*[0]⦃W⦄ → L ⊢ i ϵ 𝐅*[l]⦃#j⦄.
119 /3 width=9 by frees_be, lift_inv_lref2_be/ qed.
121 lemma frees_bind_sn: ∀a,I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃W⦄ →
122 L ⊢ i ϵ 𝐅*[l]⦃ⓑ{a,I}W.U⦄.
123 #a #I #L #W #U #l #i #H elim (frees_inv … H) -H [|*]
124 /4 width=9 by frees_be, frees_eq, nlift_bind_sn/
127 lemma frees_bind_dx: ∀a,I,L,W,U,l,i. L.ⓑ{I}W ⊢ i+1 ϵ 𝐅*[⫯l]⦃U⦄ →
128 L ⊢ i ϵ 𝐅*[l]⦃ⓑ{a,I}W.U⦄.
129 #a #J #L #V #U #l #i #H elim (frees_inv … H) -H
130 [ /4 width=9 by frees_eq, nlift_bind_dx/
131 | * #I #K #W #j #Hlj #Hji #HnU #HLK #HW
132 elim (yle_inv_succ1 … Hlj) -Hlj <yminus_SO2 #Hyj #H
133 lapply (ylt_O … H) -H #Hj
134 >(plus_minus_m_m j 1) in HnU; // <minus_le_minus_minus_comm in HW;
135 /4 width=9 by frees_be, nlift_bind_dx, drop_inv_drop1_lt, lt_plus_to_minus/
139 lemma frees_flat_sn: ∀I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃W⦄ →
140 L ⊢ i ϵ 𝐅*[l]⦃ⓕ{I}W.U⦄.
141 #I #L #W #U #l #i #H elim (frees_inv … H) -H [|*]
142 /4 width=9 by frees_be, frees_eq, nlift_flat_sn/
145 lemma frees_flat_dx: ∀I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
146 L ⊢ i ϵ 𝐅*[l]⦃ⓕ{I}W.U⦄.
147 #I #L #W #U #l #i #H elim (frees_inv … H) -H [|*]
148 /4 width=9 by frees_be, frees_eq, nlift_flat_dx/
151 lemma frees_weak: ∀L,U,l1,i. L ⊢ i ϵ 𝐅*[l1]⦃U⦄ →
152 ∀l2. l2 ≤ l1 → L ⊢ i ϵ 𝐅*[l2]⦃U⦄.
153 #L #U #l1 #i #H elim H -L -U -l1 -i
154 /3 width=9 by frees_be, frees_eq, yle_trans/
157 (* Advanced inversion lemmas ************************************************)
159 lemma frees_inv_bind_O: ∀a,I,L,W,U,i. L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄ →
160 L ⊢ i ϵ 𝐅*[0]⦃W⦄ ∨ L.ⓑ{I}W ⊢ i+1 ϵ 𝐅*[0]⦃U⦄ .
161 #a #I #L #W #U #i #H elim (frees_inv_bind … H) -H
162 /3 width=3 by frees_weak, or_intror, or_introl/