matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_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 "ground_2/lib/arith_2b.ma".
  16 include "basic_2/rt_computation/cpms_aaa.ma".
  17 include "basic_2/rt_computation/lprs_cpms.ma".
  18 include "basic_2/dynamic/cnv.ma".
  19
  20 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
  21
  22 (* Forward lemmas on atomic arity assignment for terms **********************)
  23
  24 (* Basic_2A1: uses: snv_fwd_aaa *)
  25 lemma cnv_fwd_aaa (a) (h): ∀G,L,T. ⦃G,L⦄ ⊢ T ![a,h] → ∃A. ⦃G,L⦄ ⊢ T ⁝ A.
  26 #a #h #G #L #T #H elim H -G -L -T
  27 [ /2 width=2 by aaa_sort, ex_intro/
  28 | #I #G #L #V #_ * /3 width=2 by aaa_zero, ex_intro/
  29 | #I #G #L #K #_ * /3 width=2 by aaa_lref, ex_intro/
  30 | #p * #G #L #V #T #_ #_ * #B #HV * #A #HA
  31   /3 width=2 by aaa_abbr, aaa_abst, ex_intro/
  32 | #n #p #G #L #V #W #T0 #U0 #_ #_ #_ #HVW #HTU0 * #B #HV * #X #HT
  33   lapply (cpms_aaa_conf … HV … HVW) -HVW #H1W
  34   lapply (cpms_aaa_conf … HT … HTU0) -HTU0 #H
  35   elim (aaa_inv_abst … H) -H #B0 #A #H2W #HU #H destruct
  36   lapply (aaa_mono … H2W … H1W) -W #H destruct
  37   /3 width=4 by aaa_appl, ex_intro/
  38 | #G #L #U #T #U0 #_ #_ #HU0 #HTU0 * #B #HU * #A #HT
  39   lapply (cpms_aaa_conf … HU … HU0) -HU0 #HU0
  40   lapply (cpms_aaa_conf … HT … HTU0) -HTU0 #H
  41   lapply (aaa_mono … H … HU0) -U0 #H destruct
  42   /3 width=3 by aaa_cast, ex_intro/
  43 ]
  44 qed-.
  45
  46 (* Forward lemmas with t_bound rt_transition for terms **********************)
  47
  48 lemma cnv_fwd_cpm_SO (a) (h) (G) (L):
  49       ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∃U. ⦃G,L⦄ ⊢ T ➡[1,h] U.
  50 #a #h #G #L #T #H
  51 elim (cnv_fwd_aaa … H) -H #A #HA
  52 /2 width=2 by aaa_cpm_SO/
  53 qed-.
  54
  55 (* Forward lemmas with t_bound rt_computation for terms *********************)
  56
  57 lemma cnv_fwd_cpms_total (a) (h) (n) (G) (L):
  58       ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∃U. ⦃G,L⦄ ⊢ T ➡*[n,h] U.
  59 #a #h #n #G #L #T #H
  60 elim (cnv_fwd_aaa … H) -H #A #HA
  61 /2 width=2 by cpms_total_aaa/
  62 qed-.
  63
  64 (* Advanced inversion lemmas ************************************************)
  65
  66 lemma cnv_inv_appl_pred (a) (h) (G) (L):
  67       ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![yinj a,h] →
  68       ∃∃p,W0,U0. ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] &
  69                    ⦃G,L⦄ ⊢ V ➡*[1,h] W0 & ⦃G,L⦄ ⊢ T ➡*[↓a,h] ⓛ{p}W0.U0.
  70 #a #h #G #L #V #T #H
  71 elim (cnv_inv_appl … H) -H #n #p #W #U #Ha #HV #HT #HVW #HTU
  72 lapply (ylt_inv_inj … Ha) -Ha #Ha
  73 elim (cnv_fwd_aaa … HT) #A #HA
  74 elim (cpms_total_aaa h … (a-↑n) … (ⓛ{p}W.U))
  75 [|*: /2 width=8 by cpms_aaa_conf/ ] -HA #X #HU0
  76 elim (cpms_inv_abst_sn … HU0) #W0 #U0 #HW0 #_ #H destruct
  77 lapply (cpms_trans … HVW … HW0) -HVW -HW0 #HVW0
  78 lapply (cpms_trans … HTU … HU0) -HTU -HU0
  79 >(arith_m2 … Ha) -Ha #HTU0
  80 /2 width=5 by ex4_3_intro/
  81 qed-.