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