matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fsle.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/static/fsle_drops.ma".
  16 include "basic_2/static/lfxs_fsle.ma".
  17 include "basic_2/rt_transition/lfpx_length.ma".
  18 include "basic_2/rt_transition/lfpx_fqup.ma".
  19
  20 (* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
  21
  22 (* Forward lemmas with free variables inclusion for restricted closures *****)
  23
  24 (* Note: "⦃L2, T1⦄ ⊆ ⦃L2, T0⦄" does not hold *)
  25 (* Note: Take L0 = K0.ⓓ(ⓝW.V), L2 = K0.ⓓW, T0 = #0, T1 = ⬆*[1]V *)
  26 (* Note: This invalidates lfpxs_cpx_conf: "∀h,G. s_r_confluent1 … (cpx h G) (lfpxs h G)" *)
  27 (* Basic_2A1: uses: lpx_cpx_frees_trans *)
  28 lemma lfpx_cpx_conf_fsge: ∀h,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 →
  29                           ∀L2. ⦃G, L0⦄ ⊢⬈[h, T0] L2 → ⦃L2, T1⦄ ⊆ ⦃L0, T0⦄.
  30 #h #G0 #L0 #T0 @(fqup_wf_ind_eq (Ⓕ) … G0 L0 T0) -G0 -L0 -T0
  31 #G #L #T #IH #G0 #L0 * *
  32 [ #s #HG #HL #HT #X #HX #Y #HY destruct -IH
  33   elim (cpx_inv_sort1 … HX) -HX #H destruct
  34   lapply (lfpx_fwd_length … HY) -HY #H0
  35   /2 width=1 by fsle_sort_bi/
  36 | * [| #i ] #HG #HL #HT #X #HX #Y #HY destruct
  37   [ elim (cpx_inv_zero1 … HX) -HX
  38     [ #H destruct
  39       elim (lfpx_inv_zero_length … HY) -HY *
  40       [ #H1 #H2 destruct -IH //
  41       | #I #K0 #K2 #V0 #V2 #HK02 #HV02 #H1 #H2 destruct
  42         lapply (lfpx_fwd_length … HK02) #H0
  43         /4 width=4 by fsle_pair_bi, fqu_fqup, fqu_lref_O/
  44       | #I #K0 #K2 #HK02 #H1 #H2 destruct -IH
  45         /2 width=1 by fsle_unit_bi/
  46       ]
  47     | * #I0 #K0 #V0 #V1 #HV01 #HV1X #H destruct
  48       elim (lfpx_inv_zero_pair_sn … HY) -HY #K2 #V2 #HK02 #HV02 #H destruct
  49       lapply (lfpx_fwd_length … HK02) #H0
  50       /4 width=4 by fsle_lifts_SO_sn, fqu_fqup, fqu_lref_O/
  51     ]
  52   | elim (cpx_inv_lref1 … HX) -HX
  53     [ #H destruct
  54       elim (lfpx_inv_lref … HY) -HY *
  55       [ #H0 #H1 destruct //
  56       | #I0 #I2 #K0 #K2 #HK02 #H1 #H2 destruct
  57         lapply (lfpx_fwd_length … HK02) #H0
  58         /4 width=5 by fsle_lifts_SO, fqu_fqup/
  59       ]
  60     | * #I0 #K0 #V1 #HV1 #HV1X #H0 destruct
  61       elim (lfpx_inv_lref_bind_sn … HY) -HY #I2 #K2 #HK02 #H destruct
  62       lapply (lfpx_fwd_length … HK02) #H0
  63       /4 width=5 by fsle_lifts_SO, fqu_fqup/
  64     ]
  65   ]
  66 | #l #HG #HL #HT #X #HX #Y #HY destruct -IH
  67   >(cpx_inv_gref1 … HX) -X
  68   lapply (lfpx_fwd_length … HY) -HY #H0
  69   /2 width=1 by fsle_gref_bi/
  70 | #p #I #V0 #T0 #HG #HL #HT #X #HX #Y #HY destruct
  71   elim (lfpx_inv_bind … V0 ? HY) -HY #HV0 #HT0
  72   elim (cpx_inv_bind1 … HX) -HX *
  73   [ #V1 #T1 #HV01 #HT01 #H destruct
  74     lapply (lfpx_fwd_length … HV0) #H0
  75     /4 width=6 by fsle_bind_eq, fsle_fwd_pair_sn/
  76   | #T #HT #HXT #H1 #H2 destruct
  77     lapply (lfpx_fwd_length … HV0) #H0
  78     /3 width=8 by fsle_inv_lifts_sn/
  79   ]
  80 | #I #V0 #X0 #HG #HL #HT #X #HX #Y #HY destruct
  81   elim (lfxs_inv_flat … HY) -HY #HV0 #HX0
  82   elim (cpx_inv_flat1 … HX) -HX *
  83   [ #V1 #T1 #HV01 #HT01 #H destruct
  84     /3 width=4 by fsle_flat/
  85   | #HX #H destruct
  86     /4 width=4 by fsle_flat_dx_dx/
  87   | #HX #H destruct
  88     /4 width=4 by fsle_flat_dx_sn/
  89   | #p #V1 #W0 #W1 #T0 #T1 #HV01 #HW01 #HT01 #H1 #H2 #H3 destruct
  90     elim (lfpx_inv_bind … W0 ? HX0) -HX0 #HW0 #HT0
  91     lapply (lfpx_fwd_length … HV0) #H0
  92     lapply (IH … HV01 … HV0) -HV01 -HV0 // #HV
  93     lapply (IH … HW01 … HW0) -HW01 -HW0 // #HW
  94     lapply (IH … HT01 … HT0) -HT01 -HT0 -IH // #HT
  95     lapply (fsle_fwd_pair_sn … HT) -HT #HT
  96     @fsle_bind_sn_ge //
  97     [ /4 width=1 by fsle_flat_sn, fsle_flat_dx_dx, fsle_flat_dx_sn, fsle_bind_dx_sn/
  98     | /3 width=1 by fsle_flat_dx_dx, fsle_shift/
  99     ]
 100   | #p #V1 #X1 #W0 #W1 #T0 #T1 #HV01 #HVX1 #HW01 #HT01 #H1 #H2 #H3 destruct
 101     elim (lfpx_inv_bind … W0 ? HX0) -HX0 #HW0 #HT0
 102     lapply (lfpx_fwd_length … HV0) #H0
 103     lapply (IH … HV01 … HV0) -HV01 -HV0 // #HV
 104     lapply (IH … HW01 … HW0) -HW01 -HW0 // #HW
 105     lapply (IH … HT01 … HT0) -HT01 -HT0 -IH // #HT
 106     lapply (fsle_fwd_pair_sn … HT) -HT #HT
 107     @fsle_bind_sn_ge //
 108     [ /3 width=1 by fsle_flat_dx_dx, fsle_bind_dx_sn/
 109     | /4 width=3 by fsle_flat_sn, fsle_flat_dx_sn, fsle_flat_dx_dx, fsle_shift, fsle_lifts_sn/
 110     ]
 111   ]
 112 ]
 113 qed.
 114
 115 (* Basic_2A1: uses: cpx_frees_trans *)
 116 lemma cpx_fsge_comp: ∀h,G. R_fsge_compatible (cpx h G).
 117 /2 width=4 by lfpx_cpx_conf_fsge/ qed-.
 118
 119 (* Basic_2A1: uses: lpx_frees_trans *)
 120 lemma lfpx_fsge_comp: ∀h,G. lfxs_fsge_compatible (cpx h G).
 121 /2 width=4 by lfpx_cpx_conf_fsge/ qed-.
 122
 123 (* Properties with generic extension on referred entries ********************)
 124
 125 (* Note: lemma 1000 *)
 126 (* Basic_2A1: uses: cpx_llpx_sn_conf *)
 127 lemma cpx_lfxs_conf: ∀R,h,G. s_r_confluent1 … (cpx h G) (lfxs R).
 128 /3 width=3 by fsge_lfxs_trans, cpx_fsge_comp/ qed-.
 129
 130 (* Advanced properties ******************************************************)
 131
 132 lemma lfpx_cpx_conf: ∀h,G. s_r_confluent1 … (cpx h G) (lfpx h G).
 133 /2 width=5 by cpx_lfxs_conf/ qed-.
 134
 135 lemma lfpx_cpx_conf_fsge_dx: ∀h,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 →
 136                              ∀L2. ⦃G, L0⦄ ⊢⬈[h, T0] L2 → ⦃L2, T1⦄ ⊆ ⦃L0, T1⦄.
 137 /3 width=5 by lfpx_cpx_conf, lfpx_fsge_comp/ qed-.