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