matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.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/dynamic/cnv_cpm_conf.ma".
  16 include "basic_2/dynamic/cnv_cpms_tdeq_conf.ma".
  17
  18 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
  19
  20 (* Sub confluence propery with t-bound rt-computation for terms *************)
  21
  22 fact cnv_cpms_conf_lpr_tdeq_tdeq_aux (a) (h) (G0) (L0) (T0):
  23      (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) →
  24      (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) →
  25      ⦃G0,L0⦄ ⊢ T0 ![a,h] →
  26      ∀n1,T1. ⦃G0,L0⦄ ⊢ T0 ➡*[n1,h] T1 → T0 ≛ T1 →
  27      ∀n2,T2. ⦃G0,L0⦄ ⊢ T0 ➡*[n2,h] T2 → T0 ≛ T2 →
  28      ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 →
  29      ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G0,L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
  30 #a #h #G #L0 #T0 #IH2 #IH1 #HT0
  31 #n1 #T1 #H1T01 #H2T01 #n2 #T2 #H1T02 #H2T02
  32 #L1 #HL01 #L2 #HL02
  33 elim (cnv_cpms_tdeq_conf_lpr_aux … IH2 IH1 … H1T01 … H1T02 … HL01 … HL02) -IH2 -IH1 -H1T01 -H1T02 -HL01 -HL02
  34 /2 width=3 by ex2_intro/
  35 qed-.
  36
  37 fact cnv_cpms_conf_lpr_refl_tdneq_sub (a) (h) (G0) (L0) (T0) (m21) (m22):
  38      (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) →
  39      (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) →
  40      ⦃G0,L0⦄ ⊢ T0 ![a,h] →
  41      ∀X2. ⦃G0,L0⦄ ⊢ T0 ➡[m21,h] X2 → (T0 ≛ X2 → ⊥) → ∀T2. ⦃G0,L0⦄ ⊢ X2 ➡*[m22,h] T2 →
  42      ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 →
  43      ∃∃T. ⦃G0,L1⦄ ⊢ T0 ➡*[m21+m22,h] T& ⦃G0,L2⦄ ⊢ T2 ➡*[h] T.
  44 #a #h #G0 #L0 #T0 #m21 #m22 #IH2 #IH1 #H0
  45 #X2 #HX02 #HnX02 #T2 #HXT2
  46 #L1 #HL01 #L2 #HL02
  47 lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX02 … L0 ?) // #HX2
  48 elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … HX02 … 0 T0 … L0 … HL01) //
  49 <minus_n_O <minus_O_n #Y1 #HXY1 #HTY1
  50 elim (cnv_cpms_strip_lpr_sub … IH1 … HXT2 0 X2 … HL02 L0) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ]
  51 <minus_n_O <minus_O_n #Y2 #HTY2 #HXY2 -HXT2
  52 elim (IH1 … HXY1 … HXY2 … HL01 … HL02) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ]
  53 -a -L0 -X2 <minus_n_O <minus_O_n #Y #HY1 #HY2
  54 lapply (cpms_trans … HTY1 … HY1) -Y1 #HT0Y
  55 lapply (cpms_trans … HTY2 … HY2) -Y2 #HT2Y
  56 /2 width=3 by ex2_intro/
  57 qed-.
  58
  59 fact cnv_cpms_conf_lpr_step_tdneq_sub (a) (h) (G0) (L0) (T0) (m11) (m12) (m21) (m22):
  60      (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) →
  61      (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) →
  62      ⦃G0,L0⦄ ⊢ T0 ![a,h] →
  63      ∀X1. ⦃G0,L0⦄ ⊢ T0 ➡[m11,h] X1 → T0 ≛ X1 → ∀T1. ⦃G0,L0⦄ ⊢ X1 ➡*[m12,h] T1 → X1 ≛ T1 →
  64      ∀X2. ⦃G0,L0⦄ ⊢ T0 ➡[m21,h] X2 → (T0 ≛ X2 → ⊥) → ∀T2. ⦃G0,L0⦄ ⊢ X2 ➡*[m22,h] T2 →
  65      ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 →
  66      ((∀G,L,T. ⦃G0,L0,X1⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) →
  67       (∀G,L,T. ⦃G0,L0,X1⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) →
  68       ∀m21,m22.
  69       ∀X2. ⦃G0,L0⦄ ⊢ X1 ➡[m21,h] X2 → (X1 ≛ X2 → ⊥) →
  70       ∀T2. ⦃G0,L0⦄ ⊢ X2 ➡*[m22,h] T2 →
  71       ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 →
  72       ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[m21+m22-m12,h] T & ⦃G0,L2⦄ ⊢ T2 ➡*[m12-(m21+m22),h]T
  73      ) →
  74      ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[m21+m22-(m11+m12),h] T & ⦃G0,L2⦄ ⊢ T2 ➡*[m11+m12-(m21+m22),h] T.
  75 #a #h #G0 #L0 #T0 #m11 #m12 #m21 #m22 #IH2 #IH1 #HT0
  76 #X1 #H1X01 #H2X01 #T1 #H1XT1 #H2XT1 #X2 #H1X02 #H2X02 #T2 #HXT2
  77 #L1 #HL01 #L2 #HL02 #IH
  78 lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … H1X01 … L0 ?) // #HX1
  79 lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … H1X02 … L0 ?) // #HX2
  80 elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … H1X01 … H1X02 … L0 … L0) // #Z0 #HXZ10 #HXZ20
  81 cut (⦃G0,L0,T0⦄ >[h] ⦃G0,L0,X2⦄) [ /4 width=5 by cpms_fwd_fpbs, cpm_fpb, ex2_3_intro/ ] #H1fpbg (**) (* cut *)
  82 lapply (fpbg_fpbs_trans ?? G0 ? L0 ? Z0 ? … H1fpbg) [ /2 width=2 by cpms_fwd_fpbs/ ] #H2fpbg
  83 lapply (cnv_cpms_trans_lpr_sub … IH2 … HXZ20 … L0 ?) // #HZ0
  84 elim (IH1 … HXT2 … HXZ20 … L2 … L0) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HXT2 -HXZ20 #Z2 #HTZ2 #HZ02
  85 elim (tdeq_dec X1 Z0) #H2XZ
  86 [ -IH
  87   elim (cnv_cpms_conf_lpr_tdeq_tdeq_aux … HX1 … H1XT1 H2XT1 … HXZ10 H2XZ … L1 … L0) [2,3: // |4,5: /4 width=5 by cpm_fpbq, fpbq_fpbg_trans/ ]
  88 | -H1XT1 -H2XT1
  89   elim (cpms_tdneq_fwd_step_sn_aux … HXZ10 HX1 H2XZ) [|*: /4 width=5 by cpm_fpbq, fpbq_fpbg_trans/ ]
  90   -HXZ10 -H2XZ #n1 #n2 #X0 #H1X10 #H2X10 #HXZ0 #Hn
  91   elim (IH … H1X10 H2X10 … HXZ0 … L1 … L0) [2,3: // |4,5: /4 width=5 by cpm_fpbq, fpbq_fpbg_trans/ ]
  92   >Hn -n1 -n2 -X0 -IH
  93 ]
  94 #Z1 #HTZ1 #HZ01
  95 elim (IH1 … HZ01 … HZ02  L1 … L2) // -L0 -T0 -X1 -X2 -Z0 #Z #HZ01 #HZ02
  96 lapply (cpms_trans … HTZ1 … HZ01) -Z1 <arith_l4 #HT1Z
  97 lapply (cpms_trans … HTZ2 … HZ02) -Z2 <arith_l4 #HT2Z
  98 /2 width=3 by ex2_intro/
  99 qed-.
 100
 101 fact cnv_cpms_conf_lpr_tdeq_tdneq_aux (a) (h) (G0) (L0) (T0) (n1) (m21) (m22):
 102      (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) →
 103      (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) →
 104      ⦃G0,L0⦄ ⊢ T0 ![a,h] →
 105      ∀T1. ⦃G0,L0⦄ ⊢ T0 ➡*[n1,h] T1 → T0 ≛ T1 →
 106      ∀X2. ⦃G0,L0⦄ ⊢ T0 ➡[m21,h] X2 → (T0 ≛ X2 → ⊥) → ∀T2. ⦃G0,L0⦄ ⊢ X2 ➡*[m22,h] T2 →
 107      ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 →
 108      ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[m21+m22-n1,h] T & ⦃G0,L2⦄ ⊢ T2 ➡*[n1-(m21+m22),h] T.
 109 #a #h #G0 #L0 #T0 #n1 #m21 #m22 #IH2 #IH1 #HT0
 110 #T1 #H1T01 #H2T01
 111 generalize in match m22; generalize in match m21; -m21 -m22
 112 generalize in match IH1; generalize in match IH2;
 113 @(cpms_tdeq_ind_sn … H1T01 HT0 H2T01 IH1 IH2) -n1 -T0
 114 [ #HT1 #IH2 #IH1 #m21 #m22
 115   #X2 #HX02 #HnX02 #T2 #HXT2 #L1 #HL01 #L2 #HL02
 116   <minus_O_n <minus_n_O
 117   @(cnv_cpms_conf_lpr_refl_tdneq_sub … IH2 IH1) -IH2 -IH1 /2 width=4 by/
 118 | #m11 #m12 #T0 #X1 #H1X01 #HT0 #H2X01 #H1XT1 #_ #H2XT1 #IH #IH2 #IH1 #m21 #m22
 119   #X2 #HX02 #HnX02 #T2 #HXT2 #L1 #HL01 #L2 #HL02
 120   @(cnv_cpms_conf_lpr_step_tdneq_sub … IH2 IH1 … IH) -IH2 -IH1 -IH /2 width=4 by/
 121 ]
 122 qed-.
 123
 124 fact cnv_cpms_conf_lpr_tdneq_tdneq_aux (a) (h) (G0) (L0) (T0) (m11) (m12) (m21) (m22):
 125      (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) →
 126      (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) →
 127      ⦃G0,L0⦄ ⊢ T0 ![a,h] →
 128      ∀X1. ⦃G0,L0⦄ ⊢ T0 ➡[m11,h] X1 → (T0 ≛ X1 → ⊥) → ∀T1. ⦃G0,L0⦄ ⊢ X1 ➡*[m12,h] T1 →
 129      ∀X2. ⦃G0,L0⦄ ⊢ T0 ➡[m21,h] X2 → (T0 ≛ X2 → ⊥) → ∀T2. ⦃G0,L0⦄ ⊢ X2 ➡*[m22,h] T2 →
 130      ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 →
 131      ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[m21+m22-(m11+m12),h] T & ⦃G0,L2⦄ ⊢ T2 ➡*[m11+m12-(m21+m22),h] T.
 132 #a #h #G0 #L0 #T0 #m11 #m12 #m21 #m22 #IH2 #IH1 #H0
 133 #X1 #HX01 #HnX01 #T1 #HXT1 #X2 #HX02 #HnX02 #T2 #HXT2
 134 #L1 #HL01 #L2 #HL02
 135 lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX01 … L0 ?) // #HX1
 136 lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX02 … L0 ?) // #HX2
 137 elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … HX01 … HX02 … L0 … L0) // #Z0 #HXZ10 #HXZ20
 138 cut (⦃G0,L0,T0⦄ >[h] ⦃G0,L0,X1⦄) [ /4 width=5 by cpms_fwd_fpbs, cpm_fpb, ex2_3_intro/ ] #H1fpbg (**) (* cut *)
 139 lapply (fpbg_fpbs_trans ?? G0 ? L0 ? Z0 ? … H1fpbg) [ /2 width=2 by cpms_fwd_fpbs/ ] #H2fpbg
 140 lapply (cnv_cpms_trans_lpr_sub … IH2 … HXZ10 … L0 ?) // #HZ0
 141 elim (IH1 … HXT1 … HXZ10 … L1 … L0) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HXT1 -HXZ10 #Z1 #HTZ1 #HZ01
 142 elim (IH1 … HXT2 … HXZ20 … L2 … L0) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HXT2 -HXZ20 #Z2 #HTZ2 #HZ02
 143 elim (IH1 … HZ01 … HZ02  L1 … L2) // -L0 -T0 -X1 -X2 -Z0 #Z #HZ01 #HZ02
 144 lapply (cpms_trans … HTZ1 … HZ01) -Z1 <arith_l4 #HT1Z
 145 lapply (cpms_trans … HTZ2 … HZ02) -Z2 <arith_l4 #HT2Z
 146 /2 width=3 by ex2_intro/
 147 qed-.
 148
 149 fact cnv_cpms_conf_lpr_aux (a) (h) (G0) (L0) (T0):
 150                            (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) →
 151                            (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) →
 152                            ∀G,L,T. G0 = G → L0 = L → T0 = T → IH_cnv_cpms_conf_lpr a h G L T.
 153 #a #h #G #L #T #IH2 #IH1 #G0 #L0 #T0 #HG #HL #HT
 154 #HT0 #n1 #T1 #HT01 #n2 #T2 #HT02 #L1 #HL01 #L2 #HL02 destruct
 155 elim (tdeq_dec T0 T1) #H2T01
 156 elim (tdeq_dec T0 T2) #H2T02
 157 [ @(cnv_cpms_conf_lpr_tdeq_tdeq_aux … IH2 IH1) -IH2 -IH1 /2 width=1 by/
 158 | elim (cpms_tdneq_fwd_step_sn_aux … HT02 HT0 H2T02 IH1 IH2) -HT02 -H2T02
 159   #m21 #m22 #X2 #HX02 #HnX02 #HXT2 #H2 destruct
 160   @(cnv_cpms_conf_lpr_tdeq_tdneq_aux … IH2 IH1) -IH2 -IH1 /2 width=4 by/
 161 | elim (cpms_tdneq_fwd_step_sn_aux … HT01 HT0 H2T01 IH1 IH2) -HT01 -H2T01
 162   #m11 #m12 #X1 #HX01 #HnX01 #HXT1 #H1 destruct
 163   @ex2_commute @(cnv_cpms_conf_lpr_tdeq_tdneq_aux … IH2 IH1) -IH2 -IH1 /2 width=4 by/
 164 | elim (cpms_tdneq_fwd_step_sn_aux … HT01 HT0 H2T01 IH1 IH2) -HT01 -H2T01
 165   elim (cpms_tdneq_fwd_step_sn_aux … HT02 HT0 H2T02 IH1 IH2) -HT02 -H2T02
 166   #m21 #m22 #X2 #HX02 #HnX02 #HXT2 #H2 #m11 #m12 #X1 #HX01 #HnX01 #HXT1 #H1 destruct
 167   @(cnv_cpms_conf_lpr_tdneq_tdneq_aux … IH2 IH1) -IH2 -IH1 /2 width=4 by/
 168 ]
 169 qed-.