matita/matita/contribs/lambdadelta/basic_2/computation/lsx_fpbc.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/lpxs_lpxs.ma".
  16 include "basic_2/computation/fpbs.ma".
  17 include "basic_2/computation/fpbc.ma".
  18 include "basic_2/computation/csx_lift.ma".
  19 include "basic_2/computation/csx_lpxs.ma".
  20 include "basic_2/computation/lsx_csx.ma".
  21
  22 (* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
  23
  24 (* Advanced eliminators for context-sensitive ext. strongly norm. terms *****)
  25
  26 lemma tollens: ∀R1,R2,R3:Prop. (R1 → R2) → (R2 → R3) → R1 → R3.
  27 /3 width=1/ qed-.
  28
  29 axiom fqus_lpxs_trans_nlleq: ∀h,g,G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ →
  30                              ∀L2. ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 → (K2 ⋕[O, T2] L2 →⊥) →
  31                              ∃∃L1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 &
  32                                    K1 ⋕[O, T1] L1 → ⊥ & ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄.
  33
  34 axiom fpbs_lpxs_trans_nlleq: ∀h,g,G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ≥[h, g] ⦃G2, K2, T2⦄ →
  35                              ∀L2. ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 → (K2 ⋕[O, T2] L2 →⊥) →
  36                              ∃∃L1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 &
  37                                    K1 ⋕[O, T1] L1 → ⊥ & ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
  38
  39
  40 lemma csx_ind_fpbc_fpbs: ∀h,g. ∀R:relation3 genv lenv term.
  41                          (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
  42                                      (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
  43                                      R G1 L1 T1
  44                          ) →
  45                          ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
  46                          ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
  47                          R G2 L2 T2.
  48 #h #g #R #IH1 #G1 #L1 #T1 #H @(csx_ind_alt … H) -T1
  49 #T1 #HT1 @(lsx_ind h g T1 G1 … L1) /2 width=1 by csx_lsx/ -L1
  50 #L1 @(fqup_wf_ind … G1 L1 T1) -G1 -L1 -T1
  51 #G1 #L1 #T1 #IH2 #H1 #IH3 #IH4 #G2 #L2 #T2 #H12
  52 @IH1 -IH1 (* /4 width=5 by lsx_inv_csx, csx_lpxs_conf, csx_fqus_conf/ *)
  53 [2: #G #L #T *
  54     [
  55     |
  56     | #L0 #HL20 #HnT2 elim (fpbs_lpxs_trans_nlleq … H12 … HL20 HnT2) -L2
  57       #L2 #HL12 #HnT1 #H12 @(IH3 … HL12 HnT1 … H12) -IH3
  58       #H26 #H27 #H28 #H29 #H30 #H31 #H32
  59       @(IH4) … H27 H28)
  60
  61   [ #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24
  62     lapply (fqup_fqus_trans … H15 … H21) -H15 -H21 #H
  63     @(IH3 … H23 H24)
  64
  65   #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10
  66   @(IH4 … H3 … H10) -IH4 -H10 -H3 //
  67
  68
  69
  70  [ -IH4 | -H1 -IH2 -IH4 | -H1 -H2 -IH2 -IH3 ]
  71 [ #G0 #L0 #T0 #H20 elim (lpxs_lleq_fqup_trans … H20 … HYL2 HT2) -L2
  72   #L2 #H20 #HL20 lapply (fqus_fqup_trans … H12 H20) -G2 -Y -T2
  73   #H10 @(IH2 … H10) -IH2 /2 width=5 by csx_fqup_conf/
  74 (*
  75   #T2 #HT02 #H #G3 #L3 #T3 #HT23 elim (fqup_cpxs_trans_neq … H10 … HT02 H) -T0
  76   /4 width=8 by fqup_fqus_trans, fqup_fqus/
  77 *)
  78 | (* #T0 #HT20 #H elim (fqus_cpxs_trans_neq … H12 … HT20 H) -T2 /3 width=4 by/ *)
  79 | #L0 #HL20 #HnT2 @(IH4 L0) /3 width=3 by lpxs_trans, lleq_canc_sn/
  80
  81
  82
  83
  84
  85   | /3 width=3 by /
  86   [ /2 width=3
  87
  88  lapply (lpxs_trans … HYL2 … HL20)
  89   #HYL0 lapply (tollens ???? HnT2) [ @(lleq_canc_sn … HT2) | skip ] -L2
  90   #HnT2 elim (fqus_lpxs_trans_nlleq … H12 … HYL0 HnT2)      -
  91
  92
  93   lapply (lleq_canc_sn … L0 … HT2)
  94
  95
  96
  97   |
  98
  99 elim (lpxs_lleq_fqup_trans … H12 … HYL2 HT2) -L2
 100
 101
 102 ]
 103 qed-.
 104
 105 lemma csx_ind_fpbc: ∀h,g. ∀R:relation3 genv lenv term.
 106                     (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
 107                                 (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
 108                                 R G1 L1 T1
 109                     ) →
 110                     ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R G L T.
 111 /4 width=8 by csx_ind_fpbc_fqus/ qed-.