matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_lpce_1.etc

   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/rt_conversion/cpce_drops.ma".
  16 include "basic_2/rt_conversion/lpce_drops.ma".
  17 include "basic_2/dynamic/cnv_preserve.ma".
  18
  19 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
  20
  21 definition IH_cnv_cpce_cpm_conf (h) (a): relation3 genv lenv term ≝
  22            λG,L0,T0. ⦃G,L0⦄ ⊢ T0 ![h,a] →
  23            ∀n,T1. ⦃G,L0⦄ ⊢ T0 ➡[n,h] T1 → ∀T2. ⦃G,L0⦄ ⊢ T0 ⬌η[h] T2 →
  24            ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L0⦄ ⊢ ⬌η[h] L2 →
  25            ∃∃T. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T & ⦃G,L2⦄ ⊢ T2 ➡*[n,h] T.
  26
  27 definition IH_cnv_cpce_cpms_conf (h) (a): relation3 genv lenv term ≝
  28            λG,L0,T0. ⦃G,L0⦄ ⊢ T0 ![h,a] →
  29            ∀n,T1. ⦃G,L0⦄ ⊢ T0 ➡*[n,h] T1 → ∀T2. ⦃G,L0⦄ ⊢ T0 ⬌η[h] T2 →
  30            ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L0⦄ ⊢ ⬌η[h] L2 →
  31            ∃∃T. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T & ⦃G,L2⦄ ⊢ T2 ➡*[n,h] T.
  32
  33 (* Properties with eta-conversion for full local environments ***************)
  34
  35 fact cnv_cpce_cpms_conf_sub (h) (a) (G0) (L0) (T0):
  36      (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpce_cpm_conf h a G L T) →
  37      ∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpce_cpms_conf h a G L T.
  38 #h #a #GX #LX #TX #HX #G #L0 #T0 #HX0 #HT0 #n #X1 #HX1
  39 @(cpms_ind_dx … HX1) -n -X1
  40 [ #T2 #HT02 #L1 #HL01 #L2 #HL02
  41   /2 width=8 by/
  42 | #n1 #n2 #T3 #T1 #HT03 #IH #HT31 #T2 #HT02 #L1 #HL01 #L2 #HL02
  43   lapply (cnv_cpms_trans … HT0 … HT03) -HT0 #HT3
  44   elim (IH … HT02 … L0 … HL02) -IH -HT02 [| // ] #T4 #HT34 #HT24
  45   elim (HX … HT3 … HT31 … HT34 … HL01 … HL02)
  46   [| /2 width=4 by fpbg_cpms_trans/ ] -GX -LX -L0 -TX -T0 -T3 #T3 #HT13 #HT43
  47   /3 width=5 by cpms_trans, ex2_intro/
  48 ]
  49 qed-.
  50
  51 fact cnv_cpce_cpm_conf_aux (h) (a) (G0) (L0) (T0):
  52      (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpce_cpm_conf h a G L T) →
  53      IH_cnv_cpce_cpm_conf h a G0 L0 T0.
  54 #h #a #G0 #L0 * * [|||| * ]
  55 [ #s #_ #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
  56   elim (cpm_inv_sort1 … HX1) -HX1 #H #Hn destruct
  57   lapply (cpce_inv_sort_sn … HX2) -HX2 #H destruct
  58   /3 width=3 by cpce_sort, ex2_intro/
  59 | #i #IH #H0 #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
  60   elim (cnv_inv_lref_drops … H0) -H0 #I #K0 #W0 #HLK0 #HW0
  61   elim (lpr_drops_conf … HLK0 … HL01) [| // ] #Y1 #H1 #HLK1
  62   elim (lpr_inv_pair_sn … H1) -H1 #K1 #W1 #HK01 #HW01 #H destruct
  63   elim (lpce_drops_conf … HLK0 … HL02) [| // ] #Y2 #H2 #HLK2
  64   elim (lpce_inv_pair_sn … H2) -H2 #K2 #W2 #HK02 #HW02 #H destruct
  65   elim (cpm_inv_lref1_drops … HX1) -HX1 *
  66   [ #H1 #H2 destruct
  67     elim (cpce_inv_lref_sn_drops_pair … HX2 … HLK0) -HX2 *
  68     [ #H1 #H2 destruct -L0 -K0 -W0
  69       /3 width=3 by cpce_ldef_drops, ex2_intro/
  70     | #H1 #HW #H2 destruct -L0 -W2 -HW0 -HK02
  71       @(ex2_intro … (#i)) [| // ]
  72       @(cpce_ldec_drops … HLK1) -HLK1 #n #p #V0 #U0 #HWU0
  73       /4 width=10 by lpr_cpms_trans, cpms_step_sn/
  74     | lapply (drops_isuni_fwd_drop2 … HLK2) [ // ] -W2 #HLK2
  75       #n #p #W01 #W02 #V0 #V01 #V02 #U0 #H1 #HWU0 #HW001 #HW012 #HV001 #HV012 #H2 destruct
  76       lapply (cnv_cpms_trans … HW0 … HWU0) #H
  77       elim (cnv_inv_bind … H) -H #HV0 #_
  78       elim (cnv_cpms_conf_lpr … HW0 … HWU0 0 W1 … K0 … HK01) [| // ]
  79       [| /2 width=1 by cpm_cpms/ ] <minus_O_n <minus_n_O #X #H #HWU1
  80       elim (cpms_inv_abst_sn … H) -H #V1 #U1 #HV01 #HU01 #H destruct
  81       elim (IH … HW0 … HW01 … HW001 … HK01 … HK02) -HW01 -HW001
  82       [| /3 width=2 by fqup_fpbg, fqup_lref/ ] #W11 #HW11 #HW011
  83       elim (cnv_cpce_cpms_conf_sub … IH … HV0 … HV01 … HV001 … HK01 … HK02) -HV0 -HV01 -HV001
  84       [| /4 width=6 by fqup_cpms_fwd_fpbg, fpbg_fqu_trans, fqup_lref/ ] #V11 #HV11 #HV011
  85       elim (cpms_lifts_sn … HW011 … HLK2 … HW012) -W01 #W12 #HW112 #HW012
  86       elim (cpms_lifts_sn … HV011 … HLK2 … HV012) -V01 #V12 #HV112 #HV012
  87       @(ex2_intro …(ⓝW12.+ⓛV12.ⓐ#O.#(↑i)))
  88       [ /2 width=14 by cpce_eta_drops/ | /3 width=1 by cpms_cast, cpms_bind/ ]
  89     ]
  90   | lapply (drops_isuni_fwd_drop2 … HLK1) [ // ] -W1 #HLK1
  91     #Y0 #X0 #W1 #HLY0 #HW01 #HWX1 -HL01 -HL02
  92     lapply (drops_mono … HLY0 … HLK0) -HLY0 #H destruct
  93     lapply (cpce_inv_lref_sn_drops_ldef … HX2 … HLK0) -HX2 #H destruct
  94     elim (IH … HW0 … HW01 … HW02 … HK01 … HK02)
  95     [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2
  96     elim (lifts_total W (𝐔❴↑i❵)) #V #HWV
  97     /3 width=9 by cpce_lifts_bi, cpms_delta_drops, ex2_intro/
  98   | lapply (drops_isuni_fwd_drop2 … HLK1) [ // ] -W1 #HLK1
  99     #m #Y0 #X0 #W1 #HLY0 #HW01 #HWX1 #H destruct -HL01 -HL02
 100     lapply (drops_mono … HLY0 … HLK0) -HLY0 #H destruct
 101     elim (cpce_inv_lref_sn_drops_ldec … HX2 … HLK0) -HX2 *
 102     [ #_ #H destruct
 103       elim (IH … HW0 … HW01 … HW02 … HK01 … HK02)
 104       [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2
 105       elim (lifts_total W (𝐔❴↑i❵)) #V #HWV
 106       /3 width=9 by cpce_lifts_bi, cpms_ell_drops, ex2_intro/
 107     | lapply (drops_isuni_fwd_drop2 … HLK2) [ // ] -W2 #HLK2
 108       #n #p #W01 #W02 #V0 #V01 #V02 #U0 #_ #HW001 #HW012 #_ #_ #H destruct -V0 -V01 -U0
 109       elim (IH … HW0 … HW01 … HW001 … HK01 … HK02)
 110       [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2
 111       elim (lifts_total W (𝐔❴↑i❵)) #V #HWV
 112       /4 width=11 by cpce_lifts_bi, cpms_lifts_bi, cpms_ee, ex2_intro/
 113     ]
 114   ]
 115 | #l #_ #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
 116   elim (cpm_inv_gref1 … HX1) -HX1 #H1 #H2 destruct
 117   lapply (cpce_inv_gref_sn … HX2) -HX2 #H destruct
 118   /3 width=3 by cpce_gref, cpm_cpms, ex2_intro/
 119 | #p #I #V0 #T0 #IH #H0 #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
 120   elim (cnv_inv_bind … H0) -H0 #HV0 #HT0
 121   elim (cpce_inv_bind_sn … HX2) -HX2 #V2 #T2 #HV02 #HT02 #H destruct
 122   elim (cpm_inv_bind1 … HX1) -HX1 *
 123   [ #V1 #T1 #HV01 #HT01 #H destruct
 124     elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0
 125     [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
 126     elim (IH … HT0 … HT01 … HT02 … (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) -HT0 -HT01 -HT02
 127     [|*: /2 width=1 by lpce_pair, fqup_fpbg, lpr_pair/ ] -L0 -V0 -T0 #T #HT1 #HT2
 128     /3 width=5 by cpce_bind, cpms_bind, ex2_intro/
 129   | #X0 #HXT0 #HX01 #H1 #H2 destruct -HV0 -HV02
 130     lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HXT0) -HT0
 131     [ /3 width=1 by drops_refl, drops_drop/ ] #HX0
 132     elim (cpce_inv_lifts_sn … HT02 (Ⓣ) … L0 … HXT0) -HT02
 133     [| /3 width=1 by drops_refl, drops_drop/ ] #X2 #HXT2 #HX02
 134     elim (IH … HX0 … HX01 … HX02 … HL01 … HL02) -HX0 -HX01 -HX02
 135     [| /3 width=1 by fqup_fpbg, fqup_zeta/ ] -V0 -T0 -X0 #X #HX1 #HX2
 136     /3 width=5 by cpms_zeta, ex2_intro/
 137   ]
 138 | #V0 #T0 #IH #H0 #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
 139   elim (cnv_inv_appl … H0) -H0 #m #p #W0 #U0 #_ #HV0 #HT0 #_ #_ -m -p -W0 -U0
 140   elim (cpce_inv_flat_sn … HX2) -HX2 #V2 #T2 #HV02 #HT02 #H destruct
 141   elim (cpm_inv_appl1 … HX1) -HX1 *
 142   [ #V1 #T1 #HV01 #HT01 #H destruct
 143     elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
 144     [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
 145     elim (IH … HT0 … HT01 … HT02 … HL01 … HL02) -HT0 -HT01 -HT02
 146     [|*: /2 width=1 by fqup_fpbg/ ] -L0 -V0 -T0 #T #HT1 #HT2
 147     /3 width=5 by cpce_flat, cpms_appl, ex2_intro/
 148   | #p #V1 #W0 #W1 #X0 #T1 #HV01 #HW01 #HT01 #H1 #H2 destruct
 149     elim (cnv_inv_bind … HT0) -HT0 #HW0 #HT0
 150     elim (cpce_inv_bind_sn … HT02) -HT02 #W2 #X2 #HW02 #HT02 #H destruct
 151     elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
 152     [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
 153     elim (IH … HW0 … HW01 … HW02 … HL01 … HL02) -HW0
 154     [| /2 width=1 by fqup_fpbg/ ] #W #HW1 #HW2
 155     elim (IH … HT0 … HT01 … HT02 … (L1.ⓛW1) … (L2.ⓛW2)) -HT0 -HT01 -HT02
 156     [|*: /2 width=1 by lpce_pair, fqup_fpbg, lpr_pair/ ] -L0 -V0 -X0 #T #HT1 #HT2
 157     @(ex2_intro … (ⓓ{p}ⓝW.V.T))
 158     [ @cpce_bind [ /2 width=1 by cpce_flat/ ]
 159     | @(cpms_beta) //
 160     ]
 161   | #p #V1 #U1 #W0 #W1 #X0 #T1 #HV01 #HVU1 #HW01 #HT01 #H1 #H2 destruct
 162     elim (cnv_inv_bind … HT0) -HT0 #HW0 #HT0
 163     elim (cpce_inv_bind_sn … HT02) -HT02 #W2 #X2 #HW02 #HT02 #H destruct
 164     elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
 165     [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
 166     elim (IH … HW0 … HW01 … HW02 … HL01 … HL02) -HW0
 167     [| /2 width=1 by fqup_fpbg/ ] #W #HW1 #HW2
 168     elim (IH … HT0 … HT01 … HT02 … (L1.ⓓW1) … (L2.ⓓW2)) -HT0 -HT01 -HT02
 169     [|*: /2 width=1 by lpce_pair, fqup_fpbg, lpr_pair/ ] -L0 -V0 -X0 #T #HT1 #HT2
 170     elim (cpce_lifts_sn … HV1 (Ⓣ) … (L1.ⓓW1) … HVU1) -V1
 171     [| /3 width=1 by drops_refl, drops_drop/ ] #U #HVU #HU1
 172     /4 width=9 by cpms_theta, cpce_bind, cpce_flat, ex2_intro/
 173   ]
 174 | #V0 #T0 #IH #H0 #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
 175   elim (cnv_inv_cast … H0) -H0 #U0 #HV0 #HT0 #_ #_ -U0
 176   elim (cpce_inv_flat_sn … HX2) -HX2 #V2 #T2 #HV02 #HT02 #H destruct
 177   elim (cpm_inv_cast1 … HX1) -HX1 [ * || * ]
 178   [ #V1 #T1 #HV01 #HT01 #H destruct
 179     elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
 180     [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
 181     elim (IH … HT0 … HT01 … HT02 … HL01 … HL02) -HT0 -HT01 -HT02
 182     [|*: /2 width=1 by fqup_fpbg/ ] -L0 -V0 -T0 #T #HT1 #HT2
 183     /3 width=5 by cpce_flat, cpms_cast, ex2_intro/
 184   | #HT01 -HV0 -HV02
 185     elim (IH … HT0 … HT01 … HT02 … HL01 … HL02) -HT0 -HT01 -HT02
 186     [|*: /2 width=1 by fqup_fpbg/ ] -L0 -V0 -T0 #T #HT1 #HT2
 187     /3 width=3 by cpms_eps, ex2_intro/
 188   | #m #HV01 #H destruct -HT0 -HT02
 189     elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
 190     [| /2 width=1 by fqup_fpbg/ ] -L0 -V0 -T0 #V #HV1 #HV2
 191     /3 width=3 by cpms_ee, ex2_intro/
 192   ]
 193 ]