matita/matita/contribs/lambdadelta/basic_2A/dynamic/snv_scpes.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/computation/fpbg_fpbs.ma".
  16 include "basic_2A/equivalence/scpes_cpcs.ma".
  17 include "basic_2A/equivalence/scpes_scpes.ma".
  18 include "basic_2A/dynamic/snv.ma".
  19
  20 (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
  21
  22 (* Inductive premises for the preservation results **************************)
  23
  24 definition IH_snv_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
  25                            λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
  26                            ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
  27
  28 definition IH_da_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
  29                           λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
  30                           ∀d. ⦃G, L1⦄ ⊢ T1 ▪[h, g] d →
  31                           ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
  32                           ⦃G, L2⦄ ⊢ T2 ▪[h, g] d.
  33
  34 definition IH_lstas_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
  35                              λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
  36                              ∀d1,d2. d2 ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] d1 →
  37                              ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d2] U1 →
  38                              ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
  39                              ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, d2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
  40
  41 definition IH_snv_lstas: ∀h:sh. sd h → relation3 genv lenv term ≝
  42                          λh,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] →
  43                          ∀d1,d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ T ▪[h, g] d1 →
  44                          ∀U. ⦃G, L⦄ ⊢ T •*[h, d2] U → ⦃G, L⦄ ⊢ U ¡[h, g].
  45
  46 (* Properties for the preservation results **********************************)
  47
  48 fact snv_cprs_lpr_aux: ∀h,g,G0,L0,T0.
  49                        (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
  50                        ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
  51                        ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
  52 #h #g #G0 #L0 #T0 #IH #G #L1 #T1 #HLT0 #HT1 #T2 #H
  53 @(cprs_ind … H) -T2 /4 width=6 by fpbg_fpbs_trans, cprs_fpbs/
  54 qed-.
  55
  56 fact da_cprs_lpr_aux: ∀h,g,G0,L0,T0.
  57                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
  58                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
  59                       ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
  60                       ∀d. ⦃G, L1⦄ ⊢ T1 ▪[h, g] d →
  61                       ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] d.
  62 #h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #d #Hd #T2 #H
  63 @(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbg_fpbs_trans, cprs_fpbs/
  64 qed-.
  65
  66 fact da_scpds_lpr_aux: ∀h,g,G0,L0,T0.
  67                        (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) →
  68                        (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
  69                        (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
  70                        ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
  71                        ∀d1. ⦃G, L1⦄ ⊢ T1 ▪[h, g] d1 →
  72                        ∀T2,d2. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g, d2] T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
  73                        d2 ≤ d1 ∧ ⦃G, L2⦄ ⊢ T2 ▪[h, g] d1-d2.
  74 #h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #d1 #Hd1 #T2 #d2 * #T #d0 #Hd20 #H #HT1 #HT2 #L2 #HL12
  75 lapply (da_mono … H … Hd1) -H #H destruct
  76 lapply (lstas_da_conf … HT1 … Hd1) #Hd12
  77 lapply (da_cprs_lpr_aux … IH2 IH1 … Hd12 … HT2 … HL12) -IH2 -IH1 -HT2 -HL12
  78 /3 width=8 by fpbg_fpbs_trans, lstas_fpbs, conj/
  79 qed-.
  80
  81 fact da_scpes_aux: ∀h,g,G0,L0,T0.
  82                    (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) →
  83                    (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
  84                    (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
  85                    ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
  86                    ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] →
  87                    ∀d11. ⦃G, L⦄ ⊢ T1 ▪[h, g] d11 → ∀d12. ⦃G, L⦄ ⊢ T2 ▪[h, g] d12 →
  88                    ∀d21,d22. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, d21, d22] T2 →
  89                    ∧∧ d21 ≤ d11 & d22 ≤ d12 & d11 - d21 = d12 - d22.
  90 #h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L #T1 #HLT01 #HT1 #T2 #HLT02 #HT2 #d11 #Hd11 #d12 #Hd12 #d21 #d22 * #T #HT1 #HT2
  91 elim (da_scpds_lpr_aux … IH3 IH2 IH1 … Hd11 … HT1 … L) -Hd11 -HT1 //
  92 elim (da_scpds_lpr_aux … IH3 IH2 IH1 … Hd12 … HT2 … L) -Hd12 -HT2 //
  93 /3 width=7 by da_mono, and3_intro/
  94 qed-.
  95
  96 fact lstas_cprs_lpr_aux: ∀h,g,G0,L0,T0.
  97                          (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
  98                          (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
  99                          (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
 100                          ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
 101                          ∀d1,d2. d2 ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] d1 →
 102                          ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d2] U1 →
 103                          ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
 104                          ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, d2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
 105 #h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #d1 #d2 #Hd21 #Hd1 #U1 #HTU1 #T2 #H
 106 @(cprs_ind … H) -T2 [ /2 width=10 by/ ]
 107 #T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
 108 elim (IHT1 L1) // -IHT1 #U #HTU #HU1
 109 elim (IH1 … Hd21 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2
 110 [2: /3 width=12 by da_cprs_lpr_aux/
 111 |3: /3 width=10 by snv_cprs_lpr_aux/
 112 |4: /3 width=5 by fpbg_fpbs_trans, cprs_fpbs/
 113 ] -G0 -L0 -T0 -T1 -T -d1
 114 /4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/
 115 qed-.
 116
 117 fact scpds_cpr_lpr_aux: ∀h,g,G0,L0,T0.
 118                         (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
 119                         (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
 120                         ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
 121                         ∀U1,d. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g, d] U1 →
 122                         ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
 123                         ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g, d] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2.
 124 #h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #U1 #d2 * #W1 #d1 #Hd21 #HTd1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12
 125 elim (IH1 … H01 … HTW1 … HT12 … HL12) -IH1 // #W2 #HTW2 #HW12
 126 lapply (IH2 … H01 … HTd1 … HT12 … HL12) -L0 -T0 // -T1
 127 lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1
 128 lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H
 129 elim (cpcs_inv_cprs … H) -H /3 width=6 by ex4_2_intro, ex2_intro/
 130 qed-.
 131
 132 fact scpes_cpr_lpr_aux: ∀h,g,G0,L0,T0.
 133                         (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
 134                         (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
 135                         ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
 136                         ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, g] →
 137                         ∀d1,d2. ⦃G, L1⦄ ⊢ T1 •*⬌*[h, g, d1, d2] T2 →
 138                         ∀U1. ⦃G, L1⦄ ⊢ T1 ➡ U1 → ∀U2. ⦃G, L1⦄ ⊢ T2 ➡ U2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
 139                         ⦃G, L2⦄ ⊢ U1 •*⬌*[h, g, d1, d2] U2.
 140 #h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #T2 #HT02 #HT2 #d1 #d2 * #T0 #HT10 #HT20 #U1 #HTU1 #U2 #HTU2 #L2 #HL12
 141 elim (scpds_cpr_lpr_aux … IH2 IH1 … HT10 … HTU1 … HL12) -HT10 -HTU1 // #X1 #HUX1 #H1
 142 elim (scpds_cpr_lpr_aux … IH2 IH1 … HT20 … HTU2 … HL12) -HT20 -HTU2 // #X2 #HUX2 #H2
 143 elim (cprs_conf … H1 … H2) -T0
 144 /3 width=5 by scpds_div, scpds_cprs_trans/
 145 qed-.
 146
 147 fact lstas_scpds_aux: ∀h,g,G0,L0,T0.
 148                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) →
 149                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
 150                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
 151                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
 152                       ∀G,L,T. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] →
 153                       ∀d,d1. d1 ≤ d → ⦃G, L⦄ ⊢ T ▪[h, g] d → ∀T1. ⦃G, L⦄ ⊢ T •*[h, d1] T1 →
 154                       ∀T2,d2. ⦃G, L⦄ ⊢ T •*➡*[h, g, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, d2-d1, d1-d2] T2.
 155 #h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T #H0 #HT #d #d1 #Hd1 #HTd #T1 #HT1 #T2 #d2 * #X #d0 #Hd20 #H #HTX #HXT2
 156 lapply (da_mono … H … HTd) -H #H destruct
 157 lapply (lstas_da_conf … HT1 … HTd) #HTd1
 158 lapply (lstas_da_conf … HTX … HTd) #HXd
 159 lapply (da_cprs_lpr_aux … IH3 IH2 … HXd … HXT2 L ?)
 160 [1,2,3: /3 width=8 by fpbg_fpbs_trans, lstas_fpbs/ ] #HTd2
 161 elim (le_or_ge d1 d2) #Hd12 >(eq_minus_O … Hd12)
 162 [ elim (da_lstas … HTd2 0) #X2 #HTX2 #_ -IH4 -IH3 -IH2 -IH1 -H0 -HT -HTd -HXd
 163   /5 width=6 by lstas_scpds, scpds_div, cprs_strap1, lstas_cpr, lstas_conf_le, monotonic_le_minus_l, ex4_2_intro/
 164 | elim (da_lstas … HTd1 0) #X1 #HTX1 #_
 165   lapply (lstas_conf_le … HTX … HT1) // #HXT1 -HT1
 166   elim (lstas_cprs_lpr_aux … IH3 IH2 IH1 … HXd … HXT1 … HXT2 L) -IH3 -IH2 -IH1 -HXd -HXT1 -HXT2
 167   /4 width=8 by cpcs_scpes, cpcs_cpr_conf, fpbg_fpbs_trans, lstas_fpbs, lstas_cpr, monotonic_le_minus_l/
 168 ]
 169 qed-.
 170
 171 fact scpes_le_aux: ∀h,g,G0,L0,T0.
 172                    (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) →
 173                    (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
 174                    (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
 175                    (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
 176                    ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
 177                    ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] →
 178                    ∀d11. ⦃G, L⦄ ⊢ T1 ▪[h, g] d11 → ∀d12. ⦃G, L⦄ ⊢ T2 ▪[h, g] d12 →
 179                    ∀d21,d22,d. d21 + d ≤ d11 → d22 + d ≤ d12 →
 180                    ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, d21, d22] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, d21+d, d22+d] T2.
 181 #h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T1 #H01 #HT1 #T2 #H02 #HT2 #d11 #Hd11 #Hd12 #Hd12 #d21 #d22 #d #H1 #H2 * #T0 #HT10 #HT20
 182 elim (da_lstas … Hd11 (d21+d)) #X1 #HTX1 #_
 183 elim (da_lstas … Hd12 (d22+d)) #X2 #HTX2 #_
 184 lapply (lstas_scpds_aux … IH4 IH3 IH2 IH1 … Hd11 … HTX1 … HT10) -HT10
 185 [1,2,3: // | >eq_minus_O [2: // ] <minus_plus_m_m_commutative #HX1 ]
 186 lapply (lstas_scpds_aux … IH4 IH3 IH2 IH1 … Hd12 … HTX2 … HT20) -HT20
 187 [1,2,3: // | >eq_minus_O [2: // ] <minus_plus_m_m_commutative #HX2 ]
 188 lapply (lstas_scpes_trans … Hd11 … HTX1 … HX1) [ // ] -Hd11 -HTX1 -HX1 -H1 #H1
 189 lapply (lstas_scpes_trans … Hd12 … HTX2 … HX2) [ // ] -Hd12 -HTX2 -HX2 -H2 #H2
 190 /2 width=4 by scpes_canc_dx/ (**) (* full auto fails *)
 191 qed-.
 192
 193 (* Advanced properties ******************************************************)
 194
 195 lemma snv_cast_scpes: ∀h,g,G,L,U,T. ⦃G, L⦄ ⊢ U ¡[h, g] →  ⦃G, L⦄ ⊢ T ¡[h, g] →
 196                       ⦃G, L⦄ ⊢ U •*⬌*[h, g, 0, 1] T → ⦃G, L⦄ ⊢ ⓝU.T ¡[h, g].
 197 #h #g #G #L #U #T #HU #HT * /2 width=3 by snv_cast/
 198 qed.