matita/matita/contribs/lambdadelta/basic_2A/static/da.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  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".
  19
  20 (* DEGREE ASSIGNMENT FOR TERMS **********************************************)
  21
  22 (* activate genv *)
  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
  29 .
  30
  31 interpretation "degree assignment (term)"
  32    'Degree h g G L T d = (da h g G L T d).
  33
  34 (* Basic inversion lemmas ***************************************************)
  35
  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
  44 ]
  45 qed-.
  46
  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-.
  49
  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 &
  53                                  d = d0 + 1
  54                        ).
  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
  61 ]
  62 qed-.
  63
  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-.
  68
  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
  76 ]
  77 qed-.
  78
  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-.
  81
  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
  90 ]
  91 qed-.
  92
  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-.
  95
  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 //
 104 ]
 105 qed-.
 106
 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-.