matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.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/rt_transition/cpx_drops.ma".
  16 include "basic_2/rt_computation/cpxs.ma".
  17
  18 (* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
  19
  20 (* Advanced properties ******************************************************)
  21
  22 lemma cpxs_delta: ∀h,I,G,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 →
  23                   ∀W2. ⬆*[1] V2 ≡ W2 → ⦃G, K.ⓑ{I}V1⦄ ⊢ #0 ⬈*[h] W2.
  24 #h #I #G #K #V1 #V2 #H @(cpxs_ind … H) -V2
  25 [ /3 width=3 by cpx_cpxs, cpx_delta/
  26 | #V #V2 #_ #HV2 #IH #W2 #HVW2
  27   elim (lifts_total V (𝐔❴1❵)) #W #HVW
  28   elim (cpx_lifts … HV2 (Ⓣ) … (K.ⓑ{I}V1) … HVW) -HV2
  29   [ #V0 #HV20 <(lifts_mono … HVW2 … HV20) -V2 -V0 /3 width=3 by cpxs_strap1/
  30   | /3 width=1 by drops_refl, drops_drop/
  31   ]
  32 ]
  33 qed.
  34
  35 lemma cpxs_lref: ∀h,I,G,K,V,T,i. ⦃G, K⦄ ⊢ #i ⬈*[h] T →
  36                  ∀U. ⬆*[1] T ≡ U → ⦃G, K.ⓑ{I}V⦄ ⊢ #⫯i ⬈*[h] U.
  37 #h #I #G #K #V #T #i #H @(cpxs_ind … H) -T
  38 [ /3 width=3 by cpx_cpxs, cpx_lref/
  39 | #T0 #T #_ #HT2 #IH #U #HTU
  40   elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0
  41   elim (cpx_lifts … HT2 (Ⓣ) … (K.ⓑ{I}V) … HTU0) -HT2
  42   [ #X #HTX <(lifts_mono … HTU … HTX) -T -X /3 width=3 by cpxs_strap1/
  43   | /3 width=1 by drops_refl, drops_drop/
  44   ]
  45 ]
  46 qed.
  47
  48 (* Basic_2A1: was: cpxs_delta *)
  49 lemma cpxs_delta_drops: ∀h,I,G,L,K,V1,V2,i.
  50                         ⬇*[i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 →
  51                         ∀W2. ⬆*[⫯i] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ⬈*[h] W2.
  52 #h #I #G #L #K #V1 #V2 #i #HLK #H @(cpxs_ind … H) -V2
  53 [ /3 width=7 by cpx_cpxs, cpx_delta_drops/
  54 | #V #V2 #_ #HV2 #IH #W2 #HVW2
  55   elim (lifts_total V (𝐔❴⫯i❵)) #W #HVW
  56   elim (cpx_lifts … HV2 (Ⓣ) … L … HVW) -HV2
  57   [ #V0 #HV20 <(lifts_mono … HVW2 … HV20) -V2 -V0 /3 width=3 by cpxs_strap1/
  58   | /2 width=3 by drops_isuni_fwd_drop2/
  59   ]
  60 ]
  61 qed.
  62 (*
  63 (* Advanced inversion lemmas ************************************************)
  64
  65 lemma cpxs_inv_lref1: ∀h,o,G,L,T2,i. ⦃G, L⦄ ⊢ #i ⬈*[h, o] T2 →
  66                       T2 = #i ∨
  67                       ∃∃I,K,V1,T1. ⬇[i] L ≡ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ⬈*[h, o] T1 &
  68                                    ⬆[0, i+1] T1 ≡ T2.
  69 #h #o #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
  70 #T #T2 #_ #HT2 *
  71 [ #H destruct
  72   elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/
  73   * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/
  74 | * #I #K #V1 #T1 #HLK #HVT1 #HT1
  75   lapply (drop_fwd_drop2 … HLK) #H0LK
  76   elim (cpx_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T
  77   /4 width=7 by cpxs_strap1, ex3_4_intro, or_intror/
  78 ]
  79 qed-.
  80
  81 (* Relocation properties ****************************************************)
  82
  83 lemma cpxs_lift: ∀h,o,G. d_liftable (cpxs h o G).
  84 /3 width=10 by cpx_lift, cpxs_strap1, d_liftable_LTC/ qed.
  85
  86 lemma cpxs_inv_lift1: ∀h,o,G. d_deliftable_sn (cpxs h o G).
  87 /3 width=6 by d_deliftable_sn_LTC, cpx_inv_lift1/
  88 qed-.
  89 *)