matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_dxprs.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/ygt.ma".
  16 include "basic_2/dynamic/snv_cpr.ma".
  17
  18 (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
  19
  20 (* Properties on context-free parallel computation for closures *************)
  21
  22 fact ssta_cprs_aux: ∀h,g,L0,T0. (
  23                        ∀L,T2. h ⊢ ⦃L0, T0⦄ >[g] ⦃L, T2⦄ →
  24                        ∀T1. L ⊢ T1 ⬌* T2 → ⦃h, L⦄ ⊩ T1 :[g] → ⦃h, L⦄ ⊩ T2 :[g] →
  25                        ∀U1,l1. ⦃h, L⦄ ⊢ T1 •[g, l1] U1 →
  26                        ∀U2,l2. ⦃h, L⦄ ⊢ T2 •[g, l2] U2 →
  27                        L ⊢ U1 ⬌* U2 ∧ l1 = l2
  28                     ) → (
  29                        ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊩ T1 :[g] →
  30                        ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → ⦃h, L2⦄ ⊩ T2 :[g]
  31                     ) → (
  32                        ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ →
  33                        ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → ⦃h, L1⦄ ⊩ T1 :[g] →
  34                        ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T2. L2 ⊢ T1 ➡* T2 →
  35                        ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄
  36                    ) →
  37                    ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 → L0 = L1 → T0 = T1 →
  38                    ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → ⦃h, L1⦄ ⊩ T1 :[g] →
  39                    ∃∃U2. ⦃h, L1⦄ ⊢ T2 •[g, l] U2 & L1 ⊢ U1 ⬌* U2.
  40 #h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #T2 #H
  41 @(cprs_ind_dx … H) -T1 [ /2 width=3/ ]
  42 #T1 #T #HT1T #HTT2 #IH #H1 #H2 #U1 #l #HTU1 #HT1 destruct
  43 elim (term_eq_dec T1 T) #H destruct [ /2 width=1/ ] -IH
  44 elim (ssta_cpr_aux … HTU1 … HT1T HT1) -HTU1
  45 [2: // |3: skip |4,5,6: /3 width=9 by inj, dxprs_strap2, fw_ygt/ ] -IH3 #U #HTU #HU1
  46 lapply (snv_cpr_aux … HT1 … HT1T) -HT1
  47 [ // | skip |3,4: /3 width=6 by inj, fw_ygt/ ] -IH2 #HT
  48 elim (IH1 … HTU HT … HTT2) -IH1 -HTU -HT -HTT2 // [2: /3 width=1/ ] -T #U2 #HTU2 #HU2
  49 lapply (fpcs_inv_cpcs … HU2) -HU2 #HU2
  50 lapply (cpcs_trans … HU1 … HU2) -U /2 width=3/
  51 qed-.
  52
  53 fact snv_cprs_aux: ∀h,g,L0,T0. (
  54                       ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ →
  55                       ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 →
  56                       ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T2. L2 ⊢ T1 ➡* T2 → ⦃h, L1⦄ ⊩ T1 :[g] →
  57                       ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄
  58                    ) → (
  59                       ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊩ T1 :[g] →
  60                       ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → ⦃h, L2⦄ ⊩ T2 :[g]
  61                    ) →
  62                    ∀L1,T1. L0 = L1 → T0 = T1 → ⦃h, L1⦄ ⊩ T1 :[g] →
  63                    ∀T2. L1 ⊢ T1 ➡* T2 → ⦃h, L1⦄ ⊩ T2 :[g].
  64 #h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H1 #H2 #HT1 #T2 #H
  65 @(cprs_ind … H) -T2 // -HT1
  66 #T #T2 #HT1T #HTT2 #HT destruct
  67 lapply (snv_cpr_aux … HT … HTT2) -HT -HTT2 [1,5: // |2: skip ]
  68 /4 width=6 by cprs_ygt_trans, inj, fw_ygt/
  69 qed-.