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