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/substitution/drop.ma".
18 include "basic_2/static/sd.ma".
20 (* DEGREE ASSIGNMENT FOR TERMS **********************************************)
23 inductive da (h:sh) (o:sd h): relation4 genv lenv term nat ≝
24 | da_sort: ∀G,L,s,d. deg h o s d → da h o G L (⋆s) d
25 | da_ldef: ∀G,L,K,V,i,d. ⬇[i] L ≡ K.ⓓV → da h o G K V d → da h o G L (#i) d
26 | da_ldec: ∀G,L,K,W,i,d. ⬇[i] L ≡ K.ⓛW → da h o G K W d → da h o G L (#i) (d+1)
27 | da_bind: ∀a,I,G,L,V,T,d. da h o G (L.ⓑ{I}V) T d → da h o G L (ⓑ{a,I}V.T) d
28 | da_flat: ∀I,G,L,V,T,d. da h o G L T d → da h o G L (ⓕ{I}V.T) d
31 interpretation "degree assignment (term)"
32 'Degree h o G L T d = (da h o G L T d).
34 (* Basic inversion lemmas ***************************************************)
36 fact da_inv_sort_aux: ∀h,o,G,L,T,d. ⦃G, L⦄ ⊢ T ▪[h, o] d →
37 ∀s0. T = ⋆s0 → deg h o s0 d.
38 #h #o #G #L #T #d * -G -L -T -d
39 [ #G #L #s #d #Hkd #s0 #H destruct //
40 | #G #L #K #V #i #d #_ #_ #s0 #H destruct
41 | #G #L #K #W #i #d #_ #_ #s0 #H destruct
42 | #a #I #G #L #V #T #d #_ #s0 #H destruct
43 | #I #G #L #V #T #d #_ #s0 #H destruct
47 lemma da_inv_sort: ∀h,o,G,L,s,d. ⦃G, L⦄ ⊢ ⋆s ▪[h, o] d → deg h o s d.
48 /2 width=5 by da_inv_sort_aux/ qed-.
50 fact da_inv_lref_aux: ∀h,o,G,L,T,d. ⦃G, L⦄ ⊢ T ▪[h, o] d → ∀j. T = #j →
51 (∃∃K,V. ⬇[j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ▪[h, o] d) ∨
52 (∃∃K,W,d0. ⬇[j] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, o] d0 &
55 #h #o #G #L #T #d * -G -L -T -d
56 [ #G #L #s #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,o,G,L,j,d. ⦃G, L⦄ ⊢ #j ▪[h, o] d →
65 (∃∃K,V. ⬇[j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ▪[h, o] d) ∨
66 (∃∃K,W,d0. ⬇[j] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, o] d0 & d = d0+1).
67 /2 width=3 by da_inv_lref_aux/ qed-.
69 fact da_inv_gref_aux: ∀h,o,G,L,T,d. ⦃G, L⦄ ⊢ T ▪[h, o] d → ∀p0. T = §p0 → ⊥.
70 #h #o #G #L #T #d * -G -L -T -d
71 [ #G #L #s #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,o,G,L,p,d. ⦃G, L⦄ ⊢ §p ▪[h, o] d → ⊥.
80 /2 width=9 by da_inv_gref_aux/ qed-.
82 fact da_inv_bind_aux: ∀h,o,G,L,T,d. ⦃G, L⦄ ⊢ T ▪[h, o] d →
83 ∀b,J,X,Y. T = ⓑ{b,J}Y.X → ⦃G, L.ⓑ{J}Y⦄ ⊢ X ▪[h, o] d.
84 #h #o #G #L #T #d * -G -L -T -d
85 [ #G #L #s #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,o,b,J,G,L,Y,X,d. ⦃G, L⦄ ⊢ ⓑ{b,J}Y.X ▪[h, o] d → ⦃G, L.ⓑ{J}Y⦄ ⊢ X ▪[h, o] d.
94 /2 width=4 by da_inv_bind_aux/ qed-.
96 fact da_inv_flat_aux: ∀h,o,G,L,T,d. ⦃G, L⦄ ⊢ T ▪[h, o] d →
97 ∀J,X,Y. T = ⓕ{J}Y.X → ⦃G, L⦄ ⊢ X ▪[h, o] d.
98 #h #o #G #L #T #d * -G -L -T -d
99 [ #G #L #s #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,o,J,G,L,Y,X,d. ⦃G, L⦄ ⊢ ⓕ{J}Y.X ▪[h, o] d → ⦃G, L⦄ ⊢ X ▪[h, o] d.
108 /2 width=5 by da_inv_flat_aux/ qed-.