matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.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/unfold/tpss_tpss.ma".
  16 include "basic_2/unfold/ltpss_tpss.ma".
  17
  18 (* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
  19
  20 (* Advanced properties ******************************************************)
  21
  22 (* Main properties **********************************************************)
  23
  24 theorem ltpss_trans_eq: ∀L1,L,L2,d,e.
  25                         L1 [d, e] ▶* L → L [d, e] ▶* L2 → L1 [d, e] ▶* L2.
  26 /2 width=3/ qed.
  27
  28 lemma ltpss_tpss2: ∀L1,L2,I,V1,V2,e.
  29                    L1 [0, e] ▶* L2 → L2 ⊢ V1 [0, e] ▶* V2 →
  30                    L1. ⓑ{I} V1 [0, e + 1] ▶* L2. ⓑ{I} V2.
  31 #L1 #L2 #I #V1 #V2 #e #HL12 #H @(tpss_ind … H) -V2
  32 [ /2 width=1/
  33 | #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2 width=1/
  34 ]
  35 qed.
  36
  37 lemma ltpss_tpss2_lt: ∀L1,L2,I,V1,V2,e.
  38                       L1 [0, e - 1] ▶* L2 → L2 ⊢ V1 [0, e - 1] ▶* V2 →
  39                       0 < e → L1. ⓑ{I} V1 [0, e] ▶* L2. ⓑ{I} V2.
  40 #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
  41 >(plus_minus_m_m e 1) // /2 width=1/
  42 qed.
  43
  44 lemma ltpss_tpss1: ∀L1,L2,I,V1,V2,d,e.
  45                    L1 [d, e] ▶* L2 → L2 ⊢ V1 [d, e] ▶* V2 →
  46                    L1. ⓑ{I} V1 [d + 1, e] ▶* L2. ⓑ{I} V2.
  47 #L1 #L2 #I #V1 #V2 #d #e #HL12 #H @(tpss_ind … H) -V2
  48 [ /2 width=1/
  49 | #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2 width=1/
  50 ]
  51 qed.
  52
  53 lemma ltpss_tpss1_lt: ∀L1,L2,I,V1,V2,d,e.
  54                       L1 [d - 1, e] ▶* L2 → L2 ⊢ V1 [d - 1, e] ▶* V2 →
  55                       0 < d → L1. ⓑ{I} V1 [d, e] ▶* L2. ⓑ{I} V2.
  56 #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
  57 >(plus_minus_m_m d 1) // /2 width=1/
  58 qed.
  59
  60 fact ltps_conf_aux: ∀K,K1,L1,d1,e1. K1 [d1, e1] ▶ L1 →
  61                     ∀K2,L2,d2,e2. K2 [d2, e2] ▶ L2 → K1 = K → K2 = K →
  62                     ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L.
  63 #K @(lw_wf_ind … K) -K #K #IH #K1 #L1 #d1 #e1 * -K1 -L1 -d1 -e1
  64 [ -IH /3 width=3/
  65 | -IH #K1 #I1 #V1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
  66   [ /2 width=3/
  67   | #K2 #I2 #V2 #H1 #H2 destruct /2 width=3/
  68   | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct /4 width=3/
  69   | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct /4 width=3/
  70   ]
  71 | #K1 #L1 #I1 #W1 #V1 #e1 #HKL1 #HWV1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
  72   [ -IH #d2 #e2 #H1 #H2 destruct
  73   | -IH #K2 #I2 #V2 #H1 #H2 destruct
  74     @ex2_1_intro [2,3: @inj ] /3 width=5/ (**) (* /4 width=5/ is too slow *)
  75   | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
  76     elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
  77     elim (ltpss_tps_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
  78     elim (ltpss_tps_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
  79     elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
  80     @(ex2_1_intro … (L.ⓑ{I1}W)) (**) (* explicit constructor *)
  81     [ @(ltpss_trans_eq … (L1.ⓑ{I1}U1)) /2 width=1/
  82     | @(ltpss_trans_eq … (L2.ⓑ{I1}U2)) /2 width=1/
  83     ]
  84   | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
  85     elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
  86     elim (ltpss_tps_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
  87     elim (ltpss_tps_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
  88     elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
  89     @(ex2_1_intro … (L.ⓑ{I1}W)) (**) (* explicit constructor *)
  90     [ @(ltpss_trans_eq … (L1.ⓑ{I1}U1)) /2 width=1/
  91     | @(ltpss_trans_eq … (L2.ⓑ{I1}U2)) /2 width=1/
  92     ]
  93   ]
  94 | #K1 #L1 #I1 #W1 #V1 #d1 #e1 #HKL1 #HWV1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
  95   [ -IH #d2 #e2 #H1 #H2 destruct
  96   | -IH #K2 #I2 #V2 #H1 #H2 destruct
  97     @ex2_1_intro [2,3: @inj ] /3 width=5/ (**) (* /4 width=5/ is too slow *)
  98   | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
  99     elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
 100     elim (ltpss_tps_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
 101     elim (ltpss_tps_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
 102     elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
 103     @(ex2_1_intro … (L.ⓑ{I1}W)) (**) (* explicit constructor *)
 104     [ @(ltpss_trans_eq … (L1.ⓑ{I1}U1)) /2 width=1/
 105     | @(ltpss_trans_eq … (L2.ⓑ{I1}U2)) /2 width=1/
 106     ]
 107   | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
 108     elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
 109     elim (ltpss_tps_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
 110     elim (ltpss_tps_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
 111     elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
 112     @(ex2_1_intro … (L.ⓑ{I1}W)) (**) (* explicit constructor *)
 113     [ @(ltpss_trans_eq … (L1.ⓑ{I1}U1)) /2 width=1/
 114     | @(ltpss_trans_eq … (L2.ⓑ{I1}U2)) /2 width=1/
 115     ]
 116   ]
 117 ]
 118 qed.
 119
 120 lemma ltps_conf: ∀L0,L1,d1,e1. L0 [d1, e1] ▶ L1 →
 121                  ∀L2,d2,e2. L0 [d2, e2] ▶ L2 →
 122                  ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L.
 123 /2 width=7/ qed.
 124
 125 axiom ltpss_conf: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 →
 126                   ∀L2,d2,e2. L0 [d2, e2] ▶* L2 →
 127                   ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L.
 128 (*
 129 fact ltpss_conf_aux: ∀K1,L1,d1,e1. K1 [d1, e1] ▶* L1 →
 130                      ∀K2,L2,d2,e2. K2 [d2, e2] ▶* L2 → K1 = K2 →
 131                      ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L.
 132 #K1 #L1 #d1 #e1 #H @(ltpss_ind_dx … H) -K1 /2 width=3/
 133 #X1 #K1 #HXK1 #HKL1 #IHKL1 #K2 #L2 #d2 #e2 #H @(ltpss_ind_dx … H) -K2
 134 [ -IHKL1 #H destruct
 135   lapply (ltpss_strap … HXK1 HKL1) -K1 /2 width=3/
 136 | #X2 #K2 #HXK2 #HKL2 #_ #H destruct
 137   elim (ltps_conf … HXK1 … HXK2) -X2 #K #HK1 #HK2
 138   elim (IHKL1 … HK1 ?) // -K1 #L #HL1 #HKL
 139   @(ex2_1_intro … K) //
 140 *)