matita/matita/contribs/lambdadelta/static_2/static/aaa.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 "static_2/notation/relations/atomicarity_4.ma".
  16 include "static_2/syntax/aarity.ma".
  17 include "static_2/syntax/lenv.ma".
  18 include "static_2/syntax/genv.ma".
  19
  20 (* ATONIC ARITY ASSIGNMENT FOR TERMS ****************************************)
  21
  22 (* activate genv *)
  23 inductive aaa: relation4 genv lenv term aarity ≝
  24 | aaa_sort: ∀G,L,s. aaa G L (⋆s) (⓪)
  25 | aaa_zero: ∀I,G,L,V,B. aaa G L V B → aaa G (L.ⓑ{I}V) (#0) B
  26 | aaa_lref: ∀I,G,L,A,i. aaa G L (#i) A → aaa G (L.ⓘ{I}) (#↑i) A
  27 | aaa_abbr: ∀p,G,L,V,T,B,A.
  28             aaa G L V B → aaa G (L.ⓓV) T A → aaa G L (ⓓ{p}V.T) A
  29 | aaa_abst: ∀p,G,L,V,T,B,A.
  30             aaa G L V B → aaa G (L.ⓛV) T A → aaa G L (ⓛ{p}V.T) (②B.A)
  31 | aaa_appl: ∀G,L,V,T,B,A. aaa G L V B → aaa G L T (②B.A) → aaa G L (ⓐV.T) A
  32 | aaa_cast: ∀G,L,V,T,A. aaa G L V A → aaa G L T A → aaa G L (ⓝV.T) A
  33 .
  34
  35 interpretation "atomic arity assignment (term)"
  36    'AtomicArity G L T A = (aaa G L T A).
  37
  38 (* Basic inversion lemmas ***************************************************)
  39
  40 fact aaa_inv_sort_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀s. T = ⋆s → A = ⓪.
  41 #G #L #T #A * -G -L -T -A //
  42 [ #I #G #L #V #B #_ #s #H destruct
  43 | #I #G #L #A #i #_ #s #H destruct
  44 | #p #G #L #V #T #B #A #_ #_ #s #H destruct
  45 | #p #G #L #V #T #B #A #_ #_ #s #H destruct
  46 | #G #L #V #T #B #A #_ #_ #s #H destruct
  47 | #G #L #V #T #A #_ #_ #s #H destruct
  48 ]
  49 qed-.
  50
  51 lemma aaa_inv_sort: ∀G,L,A,s. ⦃G, L⦄ ⊢ ⋆s ⁝ A → A = ⓪.
  52 /2 width=6 by aaa_inv_sort_aux/ qed-.
  53
  54 fact aaa_inv_zero_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → T = #0 →
  55                        ∃∃I,K,V. L = K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ⁝ A.
  56 #G #L #T #A * -G -L -T -A /2 width=5 by ex2_3_intro/
  57 [ #G #L #s #H destruct
  58 | #I #G #L #A #i #_ #H destruct
  59 | #p #G #L #V #T #B #A #_ #_ #H destruct
  60 | #p #G #L #V #T #B #A #_ #_ #H destruct
  61 | #G #L #V #T #B #A #_ #_ #H destruct
  62 | #G #L #V #T #A #_ #_ #H destruct
  63 ]
  64 qed-.
  65
  66 lemma aaa_inv_zero: ∀G,L,A. ⦃G, L⦄ ⊢ #0 ⁝ A →
  67                     ∃∃I,K,V. L = K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ⁝ A.
  68 /2 width=3 by aaa_inv_zero_aux/ qed-.
  69
  70 fact aaa_inv_lref_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀i. T = #(↑i) →
  71                        ∃∃I,K. L = K.ⓘ{I} & ⦃G, K⦄ ⊢ #i ⁝ A.
  72 #G #L #T #A * -G -L -T -A
  73 [ #G #L #s #j #H destruct
  74 | #I #G #L #V #B #_ #j #H destruct
  75 | #I #G #L #A #i #HA #j #H destruct /2 width=4 by ex2_2_intro/
  76 | #p #G #L #V #T #B #A #_ #_ #j #H destruct
  77 | #p #G #L #V #T #B #A #_ #_ #j #H destruct
  78 | #G #L #V #T #B #A #_ #_ #j #H destruct
  79 | #G #L #V #T #A #_ #_ #j #H destruct
  80 ]
  81 qed-.
  82
  83 lemma aaa_inv_lref: ∀G,L,A,i. ⦃G, L⦄ ⊢ #↑i ⁝ A →
  84                     ∃∃I,K. L = K.ⓘ{I} & ⦃G, K⦄ ⊢ #i ⁝ A.
  85 /2 width=3 by aaa_inv_lref_aux/ qed-.
  86
  87 fact aaa_inv_gref_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀l. T = §l → ⊥.
  88 #G #L #T #A * -G -L -T -A
  89 [ #G #L #s #k #H destruct
  90 | #I #G #L #V #B #_ #k #H destruct
  91 | #I #G #L #A #i #_ #k #H destruct
  92 | #p #G #L #V #T #B #A #_ #_ #k #H destruct
  93 | #p #G #L #V #T #B #A #_ #_ #k #H destruct
  94 | #G #L #V #T #B #A #_ #_ #k #H destruct
  95 | #G #L #V #T #A #_ #_ #k #H destruct
  96 ]
  97 qed-.
  98
  99 lemma aaa_inv_gref: ∀G,L,A,l. ⦃G, L⦄ ⊢ §l ⁝ A → ⊥.
 100 /2 width=7 by aaa_inv_gref_aux/ qed-.
 101
 102 fact aaa_inv_abbr_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀p,W,U. T = ⓓ{p}W.U →
 103                        ∃∃B. ⦃G, L⦄ ⊢ W ⁝ B & ⦃G, L.ⓓW⦄ ⊢ U ⁝ A.
 104 #G #L #T #A * -G -L -T -A
 105 [ #G #L #s #q #W #U #H destruct
 106 | #I #G #L #V #B #_ #q #W #U #H destruct
 107 | #I #G #L #A #i #_ #q #W #U #H destruct
 108 | #p #G #L #V #T #B #A #HV #HT #q #W #U #H destruct /2 width=2 by ex2_intro/
 109 | #p #G #L #V #T #B #A #_ #_ #q #W #U #H destruct
 110 | #G #L #V #T #B #A #_ #_ #q #W #U #H destruct
 111 | #G #L #V #T #A #_ #_ #q #W #U #H destruct
 112 ]
 113 qed-.
 114
 115 lemma aaa_inv_abbr: ∀p,G,L,V,T,A. ⦃G, L⦄ ⊢ ⓓ{p}V.T ⁝ A →
 116                     ∃∃B. ⦃G, L⦄ ⊢ V ⁝ B & ⦃G, L.ⓓV⦄ ⊢ T ⁝ A.
 117 /2 width=4 by aaa_inv_abbr_aux/ qed-.
 118
 119 fact aaa_inv_abst_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀p,W,U. T = ⓛ{p}W.U →
 120                        ∃∃B1,B2. ⦃G, L⦄ ⊢ W ⁝ B1 & ⦃G, L.ⓛW⦄ ⊢ U ⁝ B2 & A = ②B1.B2.
 121 #G #L #T #A * -G -L -T -A
 122 [ #G #L #s #q #W #U #H destruct
 123 | #I #G #L #V #B #_ #q #W #U #H destruct
 124 | #I #G #L #A #i #_ #q #W #U #H destruct
 125 | #p #G #L #V #T #B #A #_ #_ #q #W #U #H destruct
 126 | #p #G #L #V #T #B #A #HV #HT #q #W #U #H destruct /2 width=5 by ex3_2_intro/
 127 | #G #L #V #T #B #A #_ #_ #q #W #U #H destruct
 128 | #G #L #V #T #A #_ #_ #q #W #U #H destruct
 129 ]
 130 qed-.
 131
 132 lemma aaa_inv_abst: ∀p,G,L,W,T,A. ⦃G, L⦄ ⊢ ⓛ{p}W.T ⁝ A →
 133                     ∃∃B1,B2. ⦃G, L⦄ ⊢ W ⁝ B1 & ⦃G, L.ⓛW⦄ ⊢ T ⁝ B2 & A = ②B1.B2.
 134 /2 width=4 by aaa_inv_abst_aux/ qed-.
 135
 136 fact aaa_inv_appl_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀W,U. T = ⓐW.U →
 137                        ∃∃B. ⦃G, L⦄ ⊢ W ⁝ B & ⦃G, L⦄ ⊢ U ⁝ ②B.A.
 138 #G #L #T #A * -G -L -T -A
 139 [ #G #L #s #W #U #H destruct
 140 | #I #G #L #V #B #_ #W #U #H destruct
 141 | #I #G #L #A #i #_ #W #U #H destruct
 142 | #p #G #L #V #T #B #A #_ #_ #W #U #H destruct
 143 | #p #G #L #V #T #B #A #_ #_ #W #U #H destruct
 144 | #G #L #V #T #B #A #HV #HT #W #U #H destruct /2 width=3 by ex2_intro/
 145 | #G #L #V #T #A #_ #_ #W #U #H destruct
 146 ]
 147 qed-.
 148
 149 lemma aaa_inv_appl: ∀G,L,V,T,A. ⦃G, L⦄ ⊢ ⓐV.T ⁝ A →
 150                     ∃∃B. ⦃G, L⦄ ⊢ V ⁝ B & ⦃G, L⦄ ⊢ T ⁝ ②B.A.
 151 /2 width=3 by aaa_inv_appl_aux/ qed-.
 152
 153 fact aaa_inv_cast_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀W,U. T = ⓝW.U →
 154                        ⦃G, L⦄ ⊢ W ⁝ A ∧ ⦃G, L⦄ ⊢ U ⁝ A.
 155 #G #L #T #A * -G -L -T -A
 156 [ #G #L #s #W #U #H destruct
 157 | #I #G #L #V #B #_ #W #U #H destruct
 158 | #I #G #L #A #i #_ #W #U #H destruct
 159 | #p #G #L #V #T #B #A #_ #_ #W #U #H destruct
 160 | #p #G #L #V #T #B #A #_ #_ #W #U #H destruct
 161 | #G #L #V #T #B #A #_ #_ #W #U #H destruct
 162 | #G #L #V #T #A #HV #HT #W #U #H destruct /2 width=1 by conj/
 163 ]
 164 qed-.
 165
 166 lemma aaa_inv_cast: ∀G,L,W,T,A. ⦃G, L⦄ ⊢ ⓝW.T ⁝ A →
 167                     ⦃G, L⦄ ⊢ W ⁝ A ∧ ⦃G, L⦄ ⊢ T ⁝ A.
 168 /2 width=3 by aaa_inv_cast_aux/ qed-.