matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_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/dynamic/cnv_aaa.ma".
  16 include "basic_2/dynamic/nta.ma".
  17
  18 (* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
  19
  20 (* Forward lemmas with atomic arity assignment for terms ********************)
  21
  22 (* Note: this means that no type is a universe *)
  23 lemma nta_fwd_aaa (h) (a) (G) (L):
  24       ∀T,U. ❪G,L❫ ⊢ T :[h,a] U → ∃∃A. ❪G,L❫ ⊢ T ⁝ A & ❪G,L❫ ⊢ U ⁝ A.
  25 #h #a #G #L #T #U #H
  26 elim (cnv_fwd_aaa … H) -H #A #H
  27 elim (aaa_inv_cast … H) -H #HU #HT
  28 /2 width=3 by ex2_intro/
  29 qed-.
  30
  31 (* Advanced inversion lemmas ************************************************)
  32
  33 (* Basic_1: uses: ty3_predicative *)
  34 lemma nta_abst_predicative (h) (a) (p) (G) (L):
  35       ∀W,T. ❪G,L❫ ⊢ ⓛ[p]W.T :[h,a] W → ⊥.
  36 #h #a #p #G #L #W #T #H
  37 elim (nta_fwd_aaa … H) -a -h #X #H #H1W
  38 elim (aaa_inv_abst … H) -p #B #A #H2W #_ #H destruct -T
  39 lapply (aaa_mono … H1W … H2W) -G -L -W #H
  40 elim (discr_apair_xy_x … H)
  41 qed-.
  42
  43 (* Basic_1: uses: ty3_repellent *)
  44 theorem nta_abst_repellent (h) (a) (p) (G) (K):
  45         ∀W,T,U1. ❪G,K❫ ⊢ ⓛ[p]W.T :[h,a] U1 →
  46         ∀U2. ❪G,K.ⓛW❫ ⊢ T :[h,a] U2 → ⇧[1] U1 ≘ U2 → ⊥.
  47 #h #a #p #G #K #W #T #U1 #H1 #U2 #H2 #HU12
  48 elim (nta_fwd_aaa … H2) -H2 #A2 #H2T #H2U2
  49 elim (nta_fwd_aaa … H1) -H1 #X1 #H1 #HU1
  50 elim (aaa_inv_abst … H1) -a -h -p #B #A1 #_ #H1T #H destruct
  51 lapply (aaa_mono … H1T … H2T) -T #H destruct
  52 lapply (aaa_inv_lifts … H2U2 (Ⓣ) … K … HU12)
  53 [ /3 width=1 by drops_refl, drops_drop/ ] -W -U2 #H2U1
  54 lapply (aaa_mono … HU1 … H2U1) -G -K -U1 #H
  55 elim (discr_apair_xy_y … H)
  56 qed-.