matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_trans.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_trans.ma".
  16 include "basic_2/dynamic/cnv_cpm_tdeq.ma".
  17
  18 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
  19
  20 definition IH_cnv_cpm_tdeq_cpm_trans (a) (h) (o): relation3 genv lenv term ≝
  21            λG,L,T1. ⦃G, L⦄ ⊢ T1 ![a,h] →
  22            ∀n1,T.  ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → T1 ≛[h,o] T →
  23            ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
  24            ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡[n1,h] T2 & T0 ≛[h,o] T2.
  25
  26 (* Transitive properties restricted rt-transition for terms *****************)
  27
  28 fact cnv_cpm_tdeq_cpm_trans_sub (a) (h) (o) (G0) (L0) (T0):
  29      (∀G,L,T. ⦃G0, L0, T0⦄ >[h,o] ⦃G, L, T⦄ → IH_cnv_cpm_trans_lpr a h G L T) →
  30      (∀G,L,T. ⦃G0,L0,T0⦄ ⊐+ ⦃G,L,T⦄ → IH_cnv_cpm_tdeq_cpm_trans a h o G L T) →
  31      ∀G,L,T1. G0 = G → L0 = L → T0 = T1 → IH_cnv_cpm_tdeq_cpm_trans a h o G L T1.
  32 #a #h #o #G0 #L0 #T0 #IH2 #IH1 #G #L * [| * [| * ]]
  33 [ #I #_ #_ #_ #_ #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct -G0 -L0 -T0
  34   elim (cpm_tdeq_inv_atom_sn … H1X H2X) -H1X -H2X *
  35   [ #H1 #H2 destruct /2 width=4 by ex3_intro/
  36   | #s #H1 #H2 #H3 #Hs destruct
  37     elim (cpm_inv_sort1 … HX2) -HX2 #H #Hn2 destruct >iter_n_Sm
  38     /5 width=6 by cpm_sort_iter, tdeq_sort, deg_iter, deg_next, ex3_intro/
  39   ]
  40 | #p #I #V1 #T1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct
  41   elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T #_ #H0T1 #H1T1 #H2T1 #H destruct
  42   elim (cpm_inv_bind1 … HX2) -HX2 *
  43   [ #V2 #T2 #HV12 #HT2 #H destruct
  44     elim (IH1 … H0T1 … H1T1 H2T1 … HT2) -T -IH1 [| // ] #T0 #HT10 #H1T02 #H2T02
  45     lapply (IH2 … H0T1 … HT10 (L.ⓑ{I}V1) ?) -IH2 -H0T1 [3:|*: /2 width=1 by fqup_fpbg/ ] #HT0
  46     lapply (cpm_tdeq_free … HT0 … H1T02 H2T02 G (L.ⓑ{I}V2)) -H1T02 #H1T02
  47     /3 width=6 by cpm_bind, tdeq_pair, ex3_intro/
  48   | #T2 #HT2 #HTX2 #H1 #H2 destruct -IH2
  49     elim (tdeq_inv_lifts_dx … H2T1 … HT2) -H2T1 #XT #HXT1 #H2XT2
  50     lapply (cpm_inv_lifts_bi … H1T1 (Ⓣ) … HXT1 … HT2) -T [3:|*: /3 width=2 by drops_refl, drops_drop/ ] #H1XT2
  51     lapply (cnv_inv_lifts … H0T1 (Ⓣ) … HXT1) -H0T1 [3:|*: /3 width=2 by drops_refl, drops_drop/ ] #H0XT2
  52     elim (IH1 … H0XT2 … H1XT2 H2XT2 … HTX2) -T2 -IH1 -H0XT2 [| /2 width=1 by fqup_zeta/ ] #T2 #HXT2 #H1TX2 #H2XT2
  53     /3 width=4 by cpm_zeta, ex3_intro/
  54   ]
  55 | #V1 #XT1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct
  56   elim (cpm_tdeq_inv_appl_sn … H0 … H1X H2X) -H0 -H1X -H2X #m #q #W1 #U1 #XT #_ #_ #_ #_ #H0T1 #H1T1 #H2T1 #H destruct -m -q -W1 -U1
  57   elim (cpm_inv_appl1 … HX2) -HX2 *
  58   [ #V2 #T2 #HV12 #HT2 #H destruct -IH2
  59     elim (IH1 … H0T1 … H1T1 H2T1 … HT2) -XT -IH1 -H0T1 [| // ] #T0 #HT10 #H1T02 #H2T02
  60     /3 width=6 by cpm_appl, tdeq_pair, ex3_intro/
  61   | #p #V2 #W1 #W2 #T #T2 #HV12 #HW12 #HT2 #H1 #H2 destruct
  62     elim (cpm_tdeq_inv_bind_dx … H0T1 … H1T1 H2T1) -H0T1 -H1T1 -H2T1 #T1 #_ #H0T1 #H1T1 #H2T1 #H destruct
  63     elim (IH1 … H0T1 … H1T1 H2T1 … HT2) -T -IH1 [| // ] #T0 #HT10 #H1T02 #H2T02
  64     lapply (IH2 … H0T1 … HT10 (L.ⓛW1) ?) -IH2 -H0T1 [3:|*: /2 width=1 by fqup_fpbg/ ] #HT0
  65     lapply (cpm_tdeq_free … HT0 … H1T02 H2T02 G (L.ⓓⓝW2.V2)) -H1T02 #H1T02
  66     /3 width=6 by cpm_beta, cpm_bind, tdeq_pair, ex3_intro/
  67   | #p #V2 #V0 #W1 #W2 #T #T2 #HV12 #HV20 #HW12 #HT2 #H1 #H2 destruct
  68     elim (cpm_tdeq_inv_bind_dx … H0T1 … H1T1 H2T1) -H0T1 -H1T1 -H2T1 #T1 #_ #H0T1 #H1T1 #H2T1 #H destruct
  69     elim (IH1 … H0T1 … H1T1 H2T1 … HT2) -T -IH1 [| // ] #T0 #HT10 #H1T02 #H2T02
  70     lapply (IH2 … H0T1 … HT10 (L.ⓓW1) ?) -IH2 -H0T1 [3:|*: /2 width=1 by fqup_fpbg/ ] #HT0
  71     lapply (cpm_tdeq_free … HT0 … H1T02 H2T02 G (L.ⓓW2)) -H1T02
  72     /4 width=8 by cpm_theta, cpm_appl, cpm_bind, tdeq_pair, ex3_intro/
  73   ]
  74 | #U1 #T1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct -IH2
  75   elim (cpm_tdeq_inv_cast_sn … H0 … H1X H2X) -H0 -H1X -H2X #U0 #U #T #_ #_ #H0U1 #H1U1 #H2U1 #H0T1 #H1T1 #H2T1 #H destruct -U0
  76   elim (cpm_inv_cast1 … HX2) -HX2 [ * || * ]
  77   [ #U2 #T2 #HU2 #HT2 #H destruct
  78     elim (IH1 … H0U1 … H1U1 H2U1 … HU2) -U -H0U1 [| // ] #U0 #HU10 #H1U02 #H2U02
  79     elim (IH1 … H0T1 … H1T1 H2T1 … HT2) -T -IH1 -H0T1 [| // ] #T0 #HT10 #H1T02 #H2T02
  80     /3 width=6 by cpm_cast, tdeq_pair, ex3_intro/
  81   | #HTX2 -U -H0U1
  82     elim (IH1 … H0T1 … H1T1 H2T1 … HTX2) -T -IH1 -H0T1 [| // ] #T0 #HT10 #H1T02 #H2T02
  83     /3 width=4 by cpm_eps, ex3_intro/
  84   | #m2 #HUX2 #H destruct -T -H0T1
  85     elim (IH1 … H0U1 … H1U1 H2U1 … HUX2) -U -H0U1 [| // ] #U0 #HU10 #H1U02 #H2U02
  86     /3 width=4 by cpm_ee, ex3_intro/
  87   ]
  88 ]
  89 qed-.
  90
  91 fact cnv_cpm_tdeq_cpm_trans_aux (a) (h) (o) (G0) (L0) (T0):
  92      (∀G,L,T. ⦃G0, L0, T0⦄ >[h, o] ⦃G, L, T⦄ → IH_cnv_cpm_trans_lpr a h G L T) →
  93      IH_cnv_cpm_tdeq_cpm_trans a h o G0 L0 T0.
  94 #a #h #o #G0 #L0 #T0
  95 @(fqup_wf_ind (Ⓣ) … G0 L0 T0) -G0 -L0 -T0 #G0 #L0 #T0 #IH #IH0
  96 /5 width=10 by cnv_cpm_tdeq_cpm_trans_sub, fqup_fpbg_trans/
  97 qed-.