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/relocation/drops_lstar.ma".
  16 include "basic_2/rt_transition/cpx_drops.ma".
  17 include "basic_2/rt_computation/cpxs.ma".
  18
  19 (* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
  20
  21 (* Advanced properties ******************************************************)
  22
  23 lemma cpxs_delta: ∀h,I,G,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 →
  24                   ∀W2. ⬆*[1] V2 ≡ W2 → ⦃G, K.ⓑ{I}V1⦄ ⊢ #0 ⬈*[h] W2.
  25 #h #I #G #K #V1 #V2 #H @(cpxs_ind … H) -V2
  26 [ /3 width=3 by cpx_cpxs, cpx_delta/
  27 | #V #V2 #_ #HV2 #IH #W2 #HVW2
  28   elim (lifts_total V (𝐔❴1❵)) #W #HVW
  29   elim (cpx_lifts … HV2 (Ⓣ) … (K.ⓑ{I}V1) … HVW) -HV2
  30   [ #V0 #HV20 <(lifts_mono … HVW2 … HV20) -V2 -V0 /3 width=3 by cpxs_strap1/
  31   | /3 width=1 by drops_refl, drops_drop/
  32   ]
  33 ]
  34 qed.
  35
  36 lemma cpxs_lref: ∀h,I,G,K,V,T,i. ⦃G, K⦄ ⊢ #i ⬈*[h] T →
  37                  ∀U. ⬆*[1] T ≡ U → ⦃G, K.ⓑ{I}V⦄ ⊢ #⫯i ⬈*[h] U.
  38 #h #I #G #K #V #T #i #H @(cpxs_ind … H) -T
  39 [ /3 width=3 by cpx_cpxs, cpx_lref/
  40 | #T0 #T #_ #HT2 #IH #U #HTU
  41   elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0
  42   elim (cpx_lifts … HT2 (Ⓣ) … (K.ⓑ{I}V) … HTU0) -HT2
  43   [ #X #HTX <(lifts_mono … HTU … HTX) -T -X /3 width=3 by cpxs_strap1/
  44   | /3 width=1 by drops_refl, drops_drop/
  45   ]
  46 ]
  47 qed.
  48
  49 (* Basic_2A1: was: cpxs_delta *)
  50 lemma cpxs_delta_drops: ∀h,I,G,L,K,V1,V2,i.
  51                         ⬇*[i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 →
  52                         ∀W2. ⬆*[⫯i] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ⬈*[h] W2.
  53 #h #I #G #L #K #V1 #V2 #i #HLK #H @(cpxs_ind … H) -V2
  54 [ /3 width=7 by cpx_cpxs, cpx_delta_drops/
  55 | #V #V2 #_ #HV2 #IH #W2 #HVW2
  56   elim (lifts_total V (𝐔❴⫯i❵)) #W #HVW
  57   elim (cpx_lifts … HV2 (Ⓣ) … L … HVW) -HV2
  58   [ #V0 #HV20 <(lifts_mono … HVW2 … HV20) -V2 -V0 /3 width=3 by cpxs_strap1/
  59   | /2 width=3 by drops_isuni_fwd_drop2/
  60   ]
  61 ]
  62 qed.
  63
  64 (* Advanced inversion lemmas ************************************************)
  65
  66 lemma cpxs_inv_zero1: ∀h,G,L,T2. ⦃G, L⦄ ⊢ #0 ⬈*[h] T2 →
  67                       T2 = #0 ∨
  68                       ∃∃I,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 & ⬆*[1] V2 ≡ T2 &
  69                                    L = K.ⓑ{I}V1.
  70 #h #G #L #T2 #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
  71 #T #T2 #_ #HT2 *
  72 [ #H destruct
  73   elim (cpx_inv_zero1 … HT2) -HT2 /2 width=1 by or_introl/
  74   * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/
  75 | * #I #K #V1 #T1 #HVT1 #HT1 #H destruct
  76   elim (cpx_inv_lifts … HT2 (Ⓣ) … K … HT1) -T
  77   /4 width=7 by cpxs_strap1, drops_refl, drops_drop, ex3_4_intro, or_intror/
  78 ]
  79 qed-.
  80
  81 lemma cpxs_inv_lref1: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #⫯i ⬈*[h] T2 →
  82                       T2 = #(⫯i) ∨
  83                       ∃∃I,K,V,T. ⦃G, K⦄ ⊢ #i ⬈*[h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V.
  84 #h #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
  85 #T #T2 #_ #HT2 *
  86 [ #H destruct
  87   elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/
  88   * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/
  89 | * #I #K #V1 #T1 #Hi #HT1 #H destruct
  90   elim (cpx_inv_lifts … HT2 (Ⓣ) … K … HT1) -T
  91   /4 width=7 by cpxs_strap1, drops_refl, drops_drop, ex3_4_intro, or_intror/
  92 ]
  93 qed-.
  94
  95 (* Basic_2A1: was: cpxs_inv_lref1 *)
  96 lemma cpxs_inv_lref1_drops: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #i ⬈*[h] T2 →
  97                             T2 = #i ∨
  98                             ∃∃I,K,V1,T1. ⬇*[i] L ≡ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ⬈*[h] T1 &
  99                                          ⬆*[⫯i] T1 ≡ T2.
 100 #h #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
 101 #T #T2 #_ #HT2 *
 102 [ #H destruct
 103   elim (cpx_inv_lref1_drops … HT2) -HT2 /2 width=1 by or_introl/
 104   * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/
 105 | * #I #K #V1 #T1 #HLK #HVT1 #HT1
 106   lapply (drops_isuni_fwd_drop2 … HLK) // #H0LK
 107   elim (cpx_inv_lifts … HT2 … H0LK … HT1) -H0LK -T
 108   /4 width=7 by cpxs_strap1, ex3_4_intro, or_intror/
 109 ]
 110 qed-.
 111
 112 (* Properties with generic relocation ***************************************)
 113
 114 (* Basic_2A1: includes: cpxs_lift *)
 115 lemma cpxs_lifts: ∀h,G. d_liftable2 (cpxs h G).
 116 /3 width=10 by cpx_lifts, cpxs_strap1, d2_liftable_LTC/ qed-.
 117
 118 (* Inversion lemmas with generic relocation *********************************)
 119
 120 (* Basic_2A1: includes: cpxs_inv_lift1 *)
 121 lemma cpxs_inv_lifts: ∀h,G. d_deliftable2_sn (cpxs h G).
 122 /3 width=6 by d2_deliftable_sn_LTC, cpx_inv_lifts/ qed-.