(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "basic_2/rt_conversion/cpce_drops.ma".
include "basic_2/rt_conversion/lpce_drops.ma".
include "basic_2/dynamic/cnv_preserve.ma".

(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)

definition IH_cnv_cpce_cpm_conf (h) (a): relation3 genv lenv term ≝
           λG,L0,T0. ⦃G,L0⦄ ⊢ T0 ![h,a] →
           ∀n,T1. ⦃G,L0⦄ ⊢ T0 ➡[n,h] T1 → ∀T2. ⦃G,L0⦄ ⊢ T0 ⬌η[h] T2 →
           ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L0⦄ ⊢ ⬌η[h] L2 →
           ∃∃T. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T & ⦃G,L2⦄ ⊢ T2 ➡*[n,h] T.

definition IH_cnv_cpce_cpms_conf (h) (a): relation3 genv lenv term ≝
           λG,L0,T0. ⦃G,L0⦄ ⊢ T0 ![h,a] →
           ∀n,T1. ⦃G,L0⦄ ⊢ T0 ➡*[n,h] T1 → ∀T2. ⦃G,L0⦄ ⊢ T0 ⬌η[h] T2 →
           ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L0⦄ ⊢ ⬌η[h] L2 →
           ∃∃T. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T & ⦃G,L2⦄ ⊢ T2 ➡*[n,h] T.

(* Properties with eta-conversion for full local environments ***************)

fact cnv_cpce_cpms_conf_sub (h) (a) (G0) (L0) (T0):
     (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpce_cpm_conf h a G L T) →
     ∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpce_cpms_conf h a G L T.
#h #a #GX #LX #TX #HX #G #L0 #T0 #HX0 #HT0 #n #X1 #HX1
@(cpms_ind_dx … HX1) -n -X1
[ #T2 #HT02 #L1 #HL01 #L2 #HL02
  /2 width=8 by/
| #n1 #n2 #T3 #T1 #HT03 #IH #HT31 #T2 #HT02 #L1 #HL01 #L2 #HL02
  lapply (cnv_cpms_trans … HT0 … HT03) -HT0 #HT3
  elim (IH … HT02 … L0 … HL02) -IH -HT02 [| // ] #T4 #HT34 #HT24
  elim (HX … HT3 … HT31 … HT34 … HL01 … HL02)
  [| /2 width=4 by fpbg_cpms_trans/ ] -GX -LX -L0 -TX -T0 -T3 #T3 #HT13 #HT43
  /3 width=5 by cpms_trans, ex2_intro/
]
qed-.

fact cnv_cpce_cpm_conf_aux (h) (a) (G0) (L0) (T0):
     (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpce_cpm_conf h a G L T) →
     IH_cnv_cpce_cpm_conf h a G0 L0 T0.
#h #a #G0 #L0 * * [|||| * ]
[ #s #_ #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
  elim (cpm_inv_sort1 … HX1) -HX1 #H #Hn destruct
  lapply (cpce_inv_sort_sn … HX2) -HX2 #H destruct
  /3 width=3 by cpce_sort, ex2_intro/
| #i #IH #H0 #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
  elim (cnv_inv_lref_drops … H0) -H0 #I #K0 #W0 #HLK0 #HW0
  elim (lpr_drops_conf … HLK0 … HL01) [| // ] #Y1 #H1 #HLK1
  elim (lpr_inv_pair_sn … H1) -H1 #K1 #W1 #HK01 #HW01 #H destruct
  elim (lpce_drops_conf … HLK0 … HL02) [| // ] #Y2 #H2 #HLK2
  elim (lpce_inv_pair_sn … H2) -H2 #K2 #W2 #HK02 #HW02 #H destruct
  elim (cpm_inv_lref1_drops … HX1) -HX1 *
  [ #H1 #H2 destruct
    elim (cpce_inv_lref_sn_drops_pair … HX2 … HLK0) -HX2 *
    [ #H1 #H2 destruct -L0 -K0 -W0
      /3 width=3 by cpce_ldef_drops, ex2_intro/
    | #H1 #HW #H2 destruct -L0 -W2 -HW0 -HK02
      @(ex2_intro … (#i)) [| // ]
      @(cpce_ldec_drops … HLK1) -HLK1 #n #p #V0 #U0 #HWU0
      /4 width=10 by lpr_cpms_trans, cpms_step_sn/
    | lapply (drops_isuni_fwd_drop2 … HLK2) [ // ] -W2 #HLK2
      #n #p #W01 #W02 #V0 #V01 #V02 #U0 #H1 #HWU0 #HW001 #HW012 #HV001 #HV012 #H2 destruct
      lapply (cnv_cpms_trans … HW0 … HWU0) #H
      elim (cnv_inv_bind … H) -H #HV0 #_
      elim (cnv_cpms_conf_lpr … HW0 … HWU0 0 W1 … K0 … HK01) [| // ]
      [| /2 width=1 by cpm_cpms/ ] <minus_O_n <minus_n_O #X #H #HWU1
      elim (cpms_inv_abst_sn … H) -H #V1 #U1 #HV01 #HU01 #H destruct
      elim (IH … HW0 … HW01 … HW001 … HK01 … HK02) -HW01 -HW001
      [| /3 width=2 by fqup_fpbg, fqup_lref/ ] #W11 #HW11 #HW011
      elim (cnv_cpce_cpms_conf_sub … IH … HV0 … HV01 … HV001 … HK01 … HK02) -HV0 -HV01 -HV001
      [| /4 width=6 by fqup_cpms_fwd_fpbg, fpbg_fqu_trans, fqup_lref/ ] #V11 #HV11 #HV011
      elim (cpms_lifts_sn … HW011 … HLK2 … HW012) -W01 #W12 #HW112 #HW012
      elim (cpms_lifts_sn … HV011 … HLK2 … HV012) -V01 #V12 #HV112 #HV012
      @(ex2_intro …(ⓝW12.+ⓛV12.ⓐ#O.#(↑i)))
      [ /2 width=14 by cpce_eta_drops/ | /3 width=1 by cpms_cast, cpms_bind/ ]
    ]
  | lapply (drops_isuni_fwd_drop2 … HLK1) [ // ] -W1 #HLK1
    #Y0 #X0 #W1 #HLY0 #HW01 #HWX1 -HL01 -HL02
    lapply (drops_mono … HLY0 … HLK0) -HLY0 #H destruct
    lapply (cpce_inv_lref_sn_drops_ldef … HX2 … HLK0) -HX2 #H destruct
    elim (IH … HW0 … HW01 … HW02 … HK01 … HK02)
    [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2
    elim (lifts_total W (𝐔❴↑i❵)) #V #HWV
    /3 width=9 by cpce_lifts_bi, cpms_delta_drops, ex2_intro/
  | lapply (drops_isuni_fwd_drop2 … HLK1) [ // ] -W1 #HLK1
    #m #Y0 #X0 #W1 #HLY0 #HW01 #HWX1 #H destruct -HL01 -HL02
    lapply (drops_mono … HLY0 … HLK0) -HLY0 #H destruct
    elim (cpce_inv_lref_sn_drops_ldec … HX2 … HLK0) -HX2 *
    [ #_ #H destruct
      elim (IH … HW0 … HW01 … HW02 … HK01 … HK02)
      [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2
      elim (lifts_total W (𝐔❴↑i❵)) #V #HWV
      /3 width=9 by cpce_lifts_bi, cpms_ell_drops, ex2_intro/
    | lapply (drops_isuni_fwd_drop2 … HLK2) [ // ] -W2 #HLK2
      #n #p #W01 #W02 #V0 #V01 #V02 #U0 #_ #HW001 #HW012 #_ #_ #H destruct -V0 -V01 -U0
      elim (IH … HW0 … HW01 … HW001 … HK01 … HK02)
      [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2
      elim (lifts_total W (𝐔❴↑i❵)) #V #HWV
      /4 width=11 by cpce_lifts_bi, cpms_lifts_bi, cpms_ee, ex2_intro/
    ]
  ]
| #l #_ #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
  elim (cpm_inv_gref1 … HX1) -HX1 #H1 #H2 destruct
  lapply (cpce_inv_gref_sn … HX2) -HX2 #H destruct
  /3 width=3 by cpce_gref, cpm_cpms, ex2_intro/
| #p #I #V0 #T0 #IH #H0 #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
  elim (cnv_inv_bind … H0) -H0 #HV0 #HT0
  elim (cpce_inv_bind_sn … HX2) -HX2 #V2 #T2 #HV02 #HT02 #H destruct
  elim (cpm_inv_bind1 … HX1) -HX1 *
  [ #V1 #T1 #HV01 #HT01 #H destruct
    elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0
    [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
    elim (IH … HT0 … HT01 … HT02 … (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) -HT0 -HT01 -HT02
    [|*: /2 width=1 by lpce_pair, fqup_fpbg, lpr_pair/ ] -L0 -V0 -T0 #T #HT1 #HT2
    /3 width=5 by cpce_bind, cpms_bind, ex2_intro/
  | #X0 #HXT0 #HX01 #H1 #H2 destruct -HV0 -HV02
    lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HXT0) -HT0
    [ /3 width=1 by drops_refl, drops_drop/ ] #HX0
    elim (cpce_inv_lifts_sn … HT02 (Ⓣ) … L0 … HXT0) -HT02
    [| /3 width=1 by drops_refl, drops_drop/ ] #X2 #HXT2 #HX02
    elim (IH … HX0 … HX01 … HX02 … HL01 … HL02) -HX0 -HX01 -HX02
    [| /3 width=1 by fqup_fpbg, fqup_zeta/ ] -V0 -T0 -X0 #X #HX1 #HX2
    /3 width=5 by cpms_zeta, ex2_intro/
  ]
| #V0 #T0 #IH #H0 #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
  elim (cnv_inv_appl … H0) -H0 #m #p #W0 #U0 #_ #HV0 #HT0 #_ #_ -m -p -W0 -U0
  elim (cpce_inv_flat_sn … HX2) -HX2 #V2 #T2 #HV02 #HT02 #H destruct
  elim (cpm_inv_appl1 … HX1) -HX1 *
  [ #V1 #T1 #HV01 #HT01 #H destruct
    elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
    [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
    elim (IH … HT0 … HT01 … HT02 … HL01 … HL02) -HT0 -HT01 -HT02
    [|*: /2 width=1 by fqup_fpbg/ ] -L0 -V0 -T0 #T #HT1 #HT2
    /3 width=5 by cpce_flat, cpms_appl, ex2_intro/
  | #p #V1 #W0 #W1 #X0 #T1 #HV01 #HW01 #HT01 #H1 #H2 destruct
    elim (cnv_inv_bind … HT0) -HT0 #HW0 #HT0
    elim (cpce_inv_bind_sn … HT02) -HT02 #W2 #X2 #HW02 #HT02 #H destruct
    elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
    [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
    elim (IH … HW0 … HW01 … HW02 … HL01 … HL02) -HW0
    [| /2 width=1 by fqup_fpbg/ ] #W #HW1 #HW2
    elim (IH … HT0 … HT01 … HT02 … (L1.ⓛW1) … (L2.ⓛW2)) -HT0 -HT01 -HT02
    [|*: /2 width=1 by lpce_pair, fqup_fpbg, lpr_pair/ ] -L0 -V0 -X0 #T #HT1 #HT2
    @(ex2_intro … (ⓓ{p}ⓝW.V.T))
    [ @cpce_bind [ /2 width=1 by cpce_flat/ ]
    | @(cpms_beta) //
    ]
  | #p #V1 #U1 #W0 #W1 #X0 #T1 #HV01 #HVU1 #HW01 #HT01 #H1 #H2 destruct
    elim (cnv_inv_bind … HT0) -HT0 #HW0 #HT0
    elim (cpce_inv_bind_sn … HT02) -HT02 #W2 #X2 #HW02 #HT02 #H destruct
    elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
    [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
    elim (IH … HW0 … HW01 … HW02 … HL01 … HL02) -HW0
    [| /2 width=1 by fqup_fpbg/ ] #W #HW1 #HW2
    elim (IH … HT0 … HT01 … HT02 … (L1.ⓓW1) … (L2.ⓓW2)) -HT0 -HT01 -HT02
    [|*: /2 width=1 by lpce_pair, fqup_fpbg, lpr_pair/ ] -L0 -V0 -X0 #T #HT1 #HT2
    elim (cpce_lifts_sn … HV1 (Ⓣ) … (L1.ⓓW1) … HVU1) -V1
    [| /3 width=1 by drops_refl, drops_drop/ ] #U #HVU #HU1
    /4 width=9 by cpms_theta, cpce_bind, cpce_flat, ex2_intro/
  ]
| #V0 #T0 #IH #H0 #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
  elim (cnv_inv_cast … H0) -H0 #U0 #HV0 #HT0 #_ #_ -U0
  elim (cpce_inv_flat_sn … HX2) -HX2 #V2 #T2 #HV02 #HT02 #H destruct
  elim (cpm_inv_cast1 … HX1) -HX1 [ * || * ]
  [ #V1 #T1 #HV01 #HT01 #H destruct
    elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
    [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
    elim (IH … HT0 … HT01 … HT02 … HL01 … HL02) -HT0 -HT01 -HT02
    [|*: /2 width=1 by fqup_fpbg/ ] -L0 -V0 -T0 #T #HT1 #HT2
    /3 width=5 by cpce_flat, cpms_cast, ex2_intro/
  | #HT01 -HV0 -HV02
    elim (IH … HT0 … HT01 … HT02 … HL01 … HL02) -HT0 -HT01 -HT02
    [|*: /2 width=1 by fqup_fpbg/ ] -L0 -V0 -T0 #T #HT1 #HT2
    /3 width=3 by cpms_eps, ex2_intro/
  | #m #HV01 #H destruct -HT0 -HT02
    elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
    [| /2 width=1 by fqup_fpbg/ ] -L0 -V0 -T0 #V #HV1 #HV2
    /3 width=3 by cpms_ee, ex2_intro/
  ]
]