matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.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/computation/fsb_aaa.ma".
  16 include "basic_2/dynamic/snv_da_lpr.ma".
  17 include "basic_2/dynamic/snv_lstas.ma".
  18 include "basic_2/dynamic/snv_lstas_lpr.ma".
  19 include "basic_2/dynamic/snv_lpr.ma".
  20
  21 (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
  22
  23 (* Main preservation properties *********************************************)
  24
  25 lemma snv_preserve: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] →
  26                     ∧∧ IH_da_cpr_lpr h g G L T
  27                      & IH_snv_cpr_lpr h g G L T
  28                      & IH_snv_lstas h g G L T
  29                      & IH_lstas_cpr_lpr h g G L T.
  30 #h #g #G #L #T #HT elim (snv_fwd_aaa … HT) -HT
  31 #A #HT @(aaa_ind_fpbg h g … HT) -G -L -T -A
  32 #G #L #T #A #_ #IH -A @and4_intro
  33 [ letin aux ≝ da_cpr_lpr_aux | letin aux ≝ snv_cpr_lpr_aux
  34 | letin aux ≝ snv_lstas_aux | letin aux ≝ lstas_cpr_lpr_aux
  35 ]
  36 @(aux … G L T) // #G0 #L0 #T0 #H elim (IH … H) -IH -H //
  37 qed-.
  38
  39 theorem da_cpr_lpr: ∀h,g,G,L,T. IH_da_cpr_lpr h g G L T.
  40 #h #g #G #L #T #HT elim (snv_preserve … HT) /2 width=1 by/
  41 qed-.
  42
  43 theorem snv_cpr_lpr: ∀h,g,G,L,T. IH_snv_cpr_lpr h g G L T.
  44 #h #g #G #L #T #HT elim (snv_preserve … HT) /2 width=1 by/
  45 qed-.
  46
  47 theorem snv_lstas: ∀h,g,G,L,T. IH_snv_lstas h g G L T.
  48 #h #g #G #L #T #HT elim (snv_preserve … HT) /2 width=5 by/
  49 qed-.
  50
  51 theorem lstas_cpr_lpr: ∀h,g,G,L,T. IH_lstas_cpr_lpr h g G L T.
  52 #h #g #G #L #T #HT elim (snv_preserve … HT) /2 width=3 by/
  53 qed-.
  54
  55 (* Advanced preservation properties *****************************************)
  56
  57 lemma snv_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
  58                     ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
  59 #h #g #G #L1 #T1 #HT1 #T2 #H
  60 @(cprs_ind … H) -T2 /3 width=5 by snv_cpr_lpr/
  61 qed-.