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 "static_2/relocation/drops_ctc.ma".
  16 include "basic_2/rt_transition/cpx_drops.ma".
  17 include "basic_2/rt_computation/cpxs.ma".
  18
  19 (* UNBOUND 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❵))
  29   /5 width=11 by cpxs_strap1, cpx_lifts_bi, drops_refl, drops_drop/
  30 ]
  31 qed.
  32
  33 lemma cpxs_lref: ∀h,I,G,K,T,i. ⦃G, K⦄ ⊢ #i ⬈*[h] T →
  34                  ∀U. ⬆*[1] T ≘ U → ⦃G, K.ⓘ{I}⦄ ⊢ #↑i ⬈*[h] U.
  35 #h #I #G #K #T #i #H @(cpxs_ind … H) -T
  36 [ /3 width=3 by cpx_cpxs, cpx_lref/
  37 | #T0 #T #_ #HT2 #IH #U #HTU
  38   elim (lifts_total T0 (𝐔❴1❵))
  39   /5 width=11 by cpxs_strap1, cpx_lifts_bi, drops_refl, drops_drop/
  40 ]
  41 qed.
  42
  43 (* Basic_2A1: was: cpxs_delta *)
  44 lemma cpxs_delta_drops: ∀h,I,G,L,K,V1,V2,i.
  45                         ⬇*[i] L ≘ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 →
  46                         ∀W2. ⬆*[↑i] V2 ≘ W2 → ⦃G, L⦄ ⊢ #i ⬈*[h] W2.
  47 #h #I #G #L #K #V1 #V2 #i #HLK #H @(cpxs_ind … H) -V2
  48 [ /3 width=7 by cpx_cpxs, cpx_delta_drops/
  49 | #V #V2 #_ #HV2 #IH #W2 #HVW2
  50   elim (lifts_total V (𝐔❴↑i❵))
  51   /4 width=11 by cpxs_strap1, cpx_lifts_bi, drops_isuni_fwd_drop2/
  52 ]
  53 qed.
  54
  55 (* Advanced inversion lemmas ************************************************)
  56
  57 lemma cpxs_inv_zero1: ∀h,G,L,T2. ⦃G, L⦄ ⊢ #0 ⬈*[h] T2 →
  58                       T2 = #0 ∨
  59                       ∃∃I,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 & ⬆*[1] V2 ≘ T2 &
  60                                    L = K.ⓑ{I}V1.
  61 #h #G #L #T2 #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
  62 #T #T2 #_ #HT2 *
  63 [ #H destruct
  64   elim (cpx_inv_zero1 … HT2) -HT2 /2 width=1 by or_introl/
  65   * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/
  66 | * #I #K #V1 #T1 #HVT1 #HT1 #H destruct
  67   elim (cpx_inv_lifts_sn … HT2 (Ⓣ) … K … HT1) -T
  68   /4 width=7 by cpxs_strap1, drops_refl, drops_drop, ex3_4_intro, or_intror/
  69 ]
  70 qed-.
  71
  72 lemma cpxs_inv_lref1: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #↑i ⬈*[h] T2 →
  73                       T2 = #(↑i) ∨
  74                       ∃∃I,K,T. ⦃G, K⦄ ⊢ #i ⬈*[h] T & ⬆*[1] T ≘ T2 & L = K.ⓘ{I}.
  75 #h #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
  76 #T #T2 #_ #HT2 *
  77 [ #H destruct
  78   elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/
  79   * /4 width=6 by cpx_cpxs, ex3_3_intro, or_intror/
  80 | * #I #K #T1 #Hi #HT1 #H destruct
  81   elim (cpx_inv_lifts_sn … HT2 (Ⓣ) … K … HT1) -T
  82   /4 width=6 by cpxs_strap1, drops_refl, drops_drop, ex3_3_intro, or_intror/
  83 ]
  84 qed-.
  85
  86 (* Basic_2A1: was: cpxs_inv_lref1 *)
  87 lemma cpxs_inv_lref1_drops: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #i ⬈*[h] T2 →
  88                             T2 = #i ∨
  89                             ∃∃I,K,V1,T1. ⬇*[i] L ≘ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ⬈*[h] T1 &
  90                                          ⬆*[↑i] T1 ≘ T2.
  91 #h #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
  92 #T #T2 #_ #HT2 *
  93 [ #H destruct
  94   elim (cpx_inv_lref1_drops … HT2) -HT2 /2 width=1 by or_introl/
  95   * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/
  96 | * #I #K #V1 #T1 #HLK #HVT1 #HT1
  97   lapply (drops_isuni_fwd_drop2 … HLK) // #H0LK
  98   elim (cpx_inv_lifts_sn … HT2 … H0LK … HT1) -H0LK -T
  99   /4 width=7 by cpxs_strap1, ex3_4_intro, or_intror/
 100 ]
 101 qed-.
 102
 103 (* Properties with generic relocation ***************************************)
 104
 105 (* Basic_2A1: includes: cpxs_lift *)
 106 lemma cpxs_lifts_sn: ∀h,G. d_liftable2_sn … lifts (cpxs h G).
 107 /3 width=10 by cpx_lifts_sn, cpxs_strap1, d2_liftable_sn_CTC/ qed-.
 108
 109 lemma cpxs_lifts_bi: ∀h,G. d_liftable2_bi … lifts (cpxs h G).
 110 /3 width=12 by cpxs_lifts_sn, d_liftable2_sn_bi, lifts_mono/ qed-.
 111
 112 (* Inversion lemmas with generic relocation *********************************)
 113
 114 (* Basic_2A1: includes: cpxs_inv_lift1 *)
 115 lemma cpxs_inv_lifts_sn: ∀h,G. d_deliftable2_sn … lifts (cpxs h G).
 116 /3 width=6 by d2_deliftable_sn_CTC, cpx_inv_lifts_sn/ qed-.
 117
 118 lemma cpxs_inv_lifts_bi: ∀h,G. d_deliftable2_bi … lifts (cpxs h G).
 119 /3 width=12 by cpxs_inv_lifts_sn, d_deliftable2_sn_bi, lifts_inj/ qed-.