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/degree_6.ma".
16 include "basic_2/grammar/genv.ma".
17 include "basic_2/relocation/ldrop.ma".
18 include "basic_2/static/sd.ma".
20 (* DEGREE ASSIGNMENT FOR TERMS **********************************************)
23 inductive da (h:sh) (g:sd h): relation4 genv lenv term nat ≝
24 | da_sort: ∀G,L,k,l. deg h g k l → da h g G L (⋆k) l
25 | da_ldef: ∀G,L,K,V,i,l. ⇩[0, i] L ≡ K.ⓓV → da h g G K V l → da h g G L (#i) l
26 | da_ldec: ∀G,L,K,W,i,l. ⇩[0, i] L ≡ K.ⓛW → da h g G K W l → da h g G L (#i) (l+1)
27 | da_bind: ∀a,I,G,L,V,T,l. da h g G (L.ⓑ{I}V) T l → da h g G L (ⓑ{a,I}V.T) l
28 | da_flat: ∀I,G,L,V,T,l. da h g G L T l → da h g G L (ⓕ{I}V.T) l
31 interpretation "degree assignment (term)"
32 'Degree h g G L T l = (da h g G L T l).
34 (* Basic inversion lemmas ***************************************************)
36 fact da_inv_sort_aux: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l →
37 ∀k0. T = ⋆k0 → deg h g k0 l.
38 #h #g #G #L #T #l * -G -L -T -l
39 [ #G #L #k #l #Hkl #k0 #H destruct //
40 | #G #L #K #V #i #l #_ #_ #k0 #H destruct
41 | #G #L #K #W #i #l #_ #_ #k0 #H destruct
42 | #a #I #G #L #V #T #l #_ #k0 #H destruct
43 | #I #G #L #V #T #l #_ #k0 #H destruct
47 lemma da_inv_sort: ∀h,g,G,L,k,l. ⦃G, L⦄ ⊢ ⋆k ▪[h, g] l → deg h g k l.
48 /2 width=5 by da_inv_sort_aux/ qed-.
50 fact da_inv_lref_aux: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l → ∀j. T = #j →
51 (∃∃K,V. ⇩[0, j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ▪[h, g] l) ∨
52 (∃∃K,W,l0. ⇩[0, j] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, g] l0 &
55 #h #g #G #L #T #l * -G -L -T -l
56 [ #G #L #k #l #_ #j #H destruct
57 | #G #L #K #V #i #l #HLK #HV #j #H destruct /3 width=4/
58 | #G #L #K #W #i #l #HLK #HW #j #H destruct /3 width=6/
59 | #a #I #G #L #V #T #l #_ #j #H destruct
60 | #I #G #L #V #T #l #_ #j #H destruct
64 lemma da_inv_lref: ∀h,g,G,L,j,l. ⦃G, L⦄ ⊢ #j ▪[h, g] l →
65 (∃∃K,V. ⇩[0, j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ▪[h, g] l) ∨
66 (∃∃K,W,l0. ⇩[0, j] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, g] l0 & l = l0+1).
67 /2 width=3 by da_inv_lref_aux/ qed-.
69 fact da_inv_gref_aux: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l → ∀p0. T = §p0 → ⊥.
70 #h #g #G #L #T #l * -G -L -T -l
71 [ #G #L #k #l #_ #p0 #H destruct
72 | #G #L #K #V #i #l #_ #_ #p0 #H destruct
73 | #G #L #K #W #i #l #_ #_ #p0 #H destruct
74 | #a #I #G #L #V #T #l #_ #p0 #H destruct
75 | #I #G #L #V #T #l #_ #p0 #H destruct
79 lemma da_inv_gref: ∀h,g,G,L,p,l. ⦃G, L⦄ ⊢ §p ▪[h, g] l → ⊥.
80 /2 width=9 by da_inv_gref_aux/ qed-.
82 fact da_inv_bind_aux: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l →
83 ∀b,J,X,Y. T = ⓑ{b,J}Y.X → ⦃G, L.ⓑ{J}Y⦄ ⊢ X ▪[h, g] l.
84 #h #g #G #L #T #l * -G -L -T -l
85 [ #G #L #k #l #_ #b #J #X #Y #H destruct
86 | #G #L #K #V #i #l #_ #_ #b #J #X #Y #H destruct
87 | #G #L #K #W #i #l #_ #_ #b #J #X #Y #H destruct
88 | #a #I #G #L #V #T #l #HT #b #J #X #Y #H destruct //
89 | #I #G #L #V #T #l #_ #b #J #X #Y #H destruct
93 lemma da_inv_bind: ∀h,g,b,J,G,L,Y,X,l. ⦃G, L⦄ ⊢ ⓑ{b,J}Y.X ▪[h, g] l → ⦃G, L.ⓑ{J}Y⦄ ⊢ X ▪[h, g] l.
94 /2 width=4 by da_inv_bind_aux/ qed-.
96 fact da_inv_flat_aux: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l →
97 ∀J,X,Y. T = ⓕ{J}Y.X → ⦃G, L⦄ ⊢ X ▪[h, g] l.
98 #h #g #G #L #T #l * -G -L -T -l
99 [ #G #L #k #l #_ #J #X #Y #H destruct
100 | #G #L #K #V #i #l #_ #_ #J #X #Y #H destruct
101 | #G #L #K #W #i #l #_ #_ #J #X #Y #H destruct
102 | #a #I #G #L #V #T #l #_ #J #X #Y #H destruct
103 | #I #G #L #V #T #l #HT #J #X #Y #H destruct //
107 lemma da_inv_flat: ∀h,g,J,G,L,Y,X,l. ⦃G, L⦄ ⊢ ⓕ{J}Y.X ▪[h, g] l → ⦃G, L⦄ ⊢ X ▪[h, g] l.
108 /2 width=5 by da_inv_flat_aux/ qed-.