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/notation/relations/statictype_6.ma".
16 include "basic_2/static/da.ma".
18 (* STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS ******************************)
21 inductive ssta (h) (g): relation4 genv lenv term term ≝
22 | ssta_sort: ∀G,L,k. ssta h g G L (⋆k) (⋆(next h k))
23 | ssta_ldef: ∀G,L,K,V,U,W,i. ⇩[0, i] L ≡ K.ⓓV → ssta h g G K V W →
24 ⇧[0, i + 1] W ≡ U → ssta h g G L (#i) U
25 | ssta_ldec: ∀G,L,K,W,U,l,i. ⇩[0, i] L ≡ K.ⓛW → ⦃G, K⦄ ⊢ W ▪[h, g] l →
26 ⇧[0, i + 1] W ≡ U → ssta h g G L (#i) U
27 | ssta_bind: ∀a,I,G,L,V,T,U. ssta h g G (L.ⓑ{I}V) T U →
28 ssta h g G L (ⓑ{a,I}V.T) (ⓑ{a,I}V.U)
29 | ssta_appl: ∀G,L,V,T,U. ssta h g G L T U → ssta h g G L (ⓐV.T) (ⓐV.U)
30 | ssta_cast: ∀G,L,W,T,U. ssta h g G L T U → ssta h g G L (ⓝW.T) U
33 interpretation "stratified static type assignment (term)"
34 'StaticType h g G L T U = (ssta h g G L T U).
36 (* Basic inversion lemmas ************************************************)
38 fact ssta_inv_sort1_aux: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h, g] U → ∀k0. T = ⋆k0 →
40 #h #g #G #L #T #U * -G -L -T -U
41 [ #G #L #k #k0 #H destruct //
42 | #G #L #K #V #U #W #i #_ #_ #_ #k0 #H destruct
43 | #G #L #K #W #U #l #i #_ #_ #_ #k0 #H destruct
44 | #a #I #G #L #V #T #U #_ #k0 #H destruct
45 | #G #L #V #T #U #_ #k0 #H destruct
46 | #G #L #W #T #U #_ #k0 #H destruct
50 lemma ssta_inv_sort1: ∀h,g,G,L,U,k. ⦃G, L⦄ ⊢ ⋆k •[h, g] U → U = ⋆(next h k).
51 /2 width=6 by ssta_inv_sort1_aux/ qed-.
53 fact ssta_inv_lref1_aux: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h, g] U → ∀j. T = #j →
54 (∃∃K,V,W. ⇩[0, j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V •[h, g] W &
57 (∃∃K,W,l. ⇩[0, j] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, g] l &
60 #h #g #G #L #T #U * -G -L -T -U
61 [ #G #L #k #j #H destruct
62 | #G #L #K #V #U #W #i #HLK #HVW #HWU #j #H destruct /3 width=6/
63 | #G #L #K #W #U #l #i #HLK #HWl #HWU #j #H destruct /3 width=6/
64 | #a #I #G #L #V #T #U #_ #j #H destruct
65 | #G #L #V #T #U #_ #j #H destruct
66 | #G #L #W #T #U #_ #j #H destruct
70 lemma ssta_inv_lref1: ∀h,g,G,L,U,i. ⦃G, L⦄ ⊢ #i •[h, g] U →
71 (∃∃K,V,W. ⇩[0, i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V •[h, g] W &
74 (∃∃K,W,l. ⇩[0, i] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, g] l &
77 /2 width=3 by ssta_inv_lref1_aux/ qed-.
79 fact ssta_inv_gref1_aux: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h, g] U → ∀p0. T = §p0 → ⊥.
80 #h #g #G #L #T #U * -G -L -T -U
81 [ #G #L #k #p0 #H destruct
82 | #G #L #K #V #U #W #i #_ #_ #_ #p0 #H destruct
83 | #G #L #K #W #U #l #i #_ #_ #_ #p0 #H destruct
84 | #a #I #G #L #V #T #U #_ #p0 #H destruct
85 | #G #L #V #T #U #_ #p0 #H destruct
86 | #G #L #W #T #U #_ #p0 #H destruct
90 lemma ssta_inv_gref1: ∀h,g,G,L,U,p. ⦃G, L⦄ ⊢ §p •[h, g] U → ⊥.
91 /2 width=9 by ssta_inv_gref1_aux/ qed-.
93 fact ssta_inv_bind1_aux: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h, g] U →
94 ∀b,J,X,Y. T = ⓑ{b,J}Y.X →
95 ∃∃Z. ⦃G, L.ⓑ{J}Y⦄ ⊢ X •[h, g] Z & U = ⓑ{b,J}Y.Z.
96 #h #g #G #L #T #U * -G -L -T -U
97 [ #G #L #k #b #J #X #Y #H destruct
98 | #G #L #K #V #U #W #i #_ #_ #_ #b #J #X #Y #H destruct
99 | #G #L #K #W #U #l #i #_ #_ #_ #b #J #X #Y #H destruct
100 | #a #I #G #L #V #T #U #HTU #b #J #X #Y #H destruct /2 width=3/
101 | #G #L #V #T #U #_ #b #J #X #Y #H destruct
102 | #G #L #W #T #U #_ #b #J #X #Y #H destruct
106 lemma ssta_inv_bind1: ∀h,g,b,J,G,L,Y,X,U. ⦃G, L⦄ ⊢ ⓑ{b,J}Y.X •[h, g] U →
107 ∃∃Z. ⦃G, L.ⓑ{J}Y⦄ ⊢ X •[h, g] Z & U = ⓑ{b,J}Y.Z.
108 /2 width=3 by ssta_inv_bind1_aux/ qed-.
110 fact ssta_inv_appl1_aux: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h, g] U → ∀X,Y. T = ⓐY.X →
111 ∃∃Z. ⦃G, L⦄ ⊢ X •[h, g] Z & U = ⓐY.Z.
112 #h #g #G #L #T #U * -G -L -T -U
113 [ #G #L #k #X #Y #H destruct
114 | #G #L #K #V #U #W #i #_ #_ #_ #X #Y #H destruct
115 | #G #L #K #W #U #l #i #_ #_ #_ #X #Y #H destruct
116 | #a #I #G #L #V #T #U #_ #X #Y #H destruct
117 | #G #L #V #T #U #HTU #X #Y #H destruct /2 width=3/
118 | #G #L #W #T #U #_ #X #Y #H destruct
122 lemma ssta_inv_appl1: ∀h,g,G,L,Y,X,U. ⦃G, L⦄ ⊢ ⓐY.X •[h, g] U →
123 ∃∃Z. ⦃G, L⦄ ⊢ X •[h, g] Z & U = ⓐY.Z.
124 /2 width=3 by ssta_inv_appl1_aux/ qed-.
126 fact ssta_inv_cast1_aux: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h, g] U → ∀X,Y. T = ⓝY.X →
127 ⦃G, L⦄ ⊢ X •[h, g] U.
128 #h #g #G #L #T #U * -G -L -T -U
129 [ #G #L #k #X #Y #H destruct
130 | #G #L #K #V #U #W #i #_ #_ #_ #X #Y #H destruct
131 | #G #L #K #W #U #l #i #_ #_ #_ #X #Y #H destruct
132 | #a #I #G #L #V #T #U #_ #X #Y #H destruct
133 | #G #L #V #T #U #_ #X #Y #H destruct
134 | #G #L #W #T #U #HTU #X #Y #H destruct //
138 lemma ssta_inv_cast1: ∀h,g,G,L,X,Y,U. ⦃G, L⦄ ⊢ ⓝY.X •[h, g] U → ⦃G, L⦄ ⊢ X •[h, g] U.
139 /2 width=4 by ssta_inv_cast1_aux/ qed-.
141 (* Inversion lemmas on degree assignment for terms **************************)
143 lemma ssta_inv_da: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h, g] U →
144 ∃l. ⦃G, L⦄ ⊢ T ▪[h, g] l.
145 #h #g #G #L #T #U #H elim H -G -L -T -U
146 [ #G #L #k elim (deg_total h g k) /3 width=2/
147 | #G #L #K #V #U #W #i #HLK #_ #_ * /3 width=5/
148 | #G #L #K #W #U #l #i #HLK #HWl #_ /3 width=5/
149 | #a #I #G #L #V #T #U #_ * /3 width=2/
150 | #G #L #V #T #U #_ * /3 width=2/
151 | #G #L #W #T #U #_ * /3 width=2/
155 (* Properties on degree assignment for terms ********************************)
157 lemma da_ssta: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l →
158 ∃U. ⦃G, L⦄ ⊢ T •[h, g] U.
159 #h #g #G #L #T #l #H elim H -G -L -T -l
161 | #G #L #K #V #i #l #HLK #_ * #W #HVW
162 elim (lift_total W 0 (i+1)) /3 width=7/
163 | #G #L #K #W #i #l #HLK #HW #_
164 elim (lift_total W 0 (i+1)) /3 width=7/
165 | #a #I #G #L #V #T #l #_ * /3 width=2/
166 | * #G #L #V #T #l #_ * /3 width=2/
170 (* Basic_1: removed theorems 7:
171 sty0_gen_sort sty0_gen_lref sty0_gen_bind sty0_gen_appl sty0_gen_cast
172 sty0_lift sty0_correct