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 (* EXTENDED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS *************)
  20
  21 (* Advanced properties ******************************************************)
  22
  23 lemma cpxs_delta (G) (K):
  24       ∀I,V1,V2. ❪G,K❫ ⊢ V1 ⬈* V2 →
  25       ∀W2. ⇧[1] V2 ≘ W2 → ❪G,K.ⓑ[I]V1❫ ⊢ #0 ⬈* W2.
  26 #G #K #I #V1 #V2 #H @(cpxs_ind … H) -V2
  27 [ /3 width=3 by cpx_cpxs, cpx_delta/
  28 | #V #V2 #_ #HV2 #IH #W2 #HVW2
  29   elim (lifts_total V (𝐔❨1❩))
  30   /5 width=11 by cpxs_strap1, cpx_lifts_bi, drops_refl, drops_drop/
  31 ]
  32 qed.
  33
  34 lemma cpxs_lref (G) (K):
  35       ∀I,T,i. ❪G,K❫ ⊢ #i ⬈* T →
  36       ∀U. ⇧[1] T ≘ U → ❪G,K.ⓘ[I]❫ ⊢ #↑i ⬈* U.
  37 #G #K #I #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❩))
  41   /5 width=11 by cpxs_strap1, cpx_lifts_bi, drops_refl, drops_drop/
  42 ]
  43 qed.
  44
  45 (* Basic_2A1: was: cpxs_delta *)
  46 lemma cpxs_delta_drops (G) (L):
  47       ∀I,K,V1,V2,i. ⇩[i] L ≘ K.ⓑ[I]V1 → ❪G,K❫ ⊢ V1 ⬈* V2 →
  48       ∀W2. ⇧[↑i] V2 ≘ W2 → ❪G,L❫ ⊢ #i ⬈* W2.
  49 #G #L #I #K #V1 #V2 #i #HLK #H @(cpxs_ind … H) -V2
  50 [ /3 width=7 by cpx_cpxs, cpx_delta_drops/
  51 | #V #V2 #_ #HV2 #IH #W2 #HVW2
  52   elim (lifts_total V (𝐔❨↑i❩))
  53   /4 width=11 by cpxs_strap1, cpx_lifts_bi, drops_isuni_fwd_drop2/
  54 ]
  55 qed.
  56
  57 (* Advanced inversion lemmas ************************************************)
  58
  59 lemma cpxs_inv_zero1 (G) (L):
  60       ∀T2. ❪G,L❫ ⊢ #0 ⬈* T2 →
  61       ∨∨ T2 = #0
  62        | ∃∃I,K,V1,V2. ❪G,K❫ ⊢ V1 ⬈* V2 & ⇧[1] V2 ≘ T2 & L = K.ⓑ[I]V1.
  63 #G #L #T2 #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
  64 #T #T2 #_ #HT2 *
  65 [ #H destruct
  66   elim (cpx_inv_zero1 … HT2) -HT2 /2 width=1 by or_introl/
  67   * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/
  68 | * #I #K #V1 #T1 #HVT1 #HT1 #H destruct
  69   elim (cpx_inv_lifts_sn … HT2 (Ⓣ) … K … HT1) -T
  70   /4 width=7 by cpxs_strap1, drops_refl, drops_drop, ex3_4_intro, or_intror/
  71 ]
  72 qed-.
  73
  74 lemma cpxs_inv_lref1 (G) (L):
  75       ∀T2,i. ❪G,L❫ ⊢ #↑i ⬈* T2 →
  76       ∨∨ T2 = #(↑i)
  77        | ∃∃I,K,T. ❪G,K❫ ⊢ #i ⬈* T & ⇧[1] T ≘ T2 & L = K.ⓘ[I].
  78 #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
  79 #T #T2 #_ #HT2 *
  80 [ #H destruct
  81   elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/
  82   * /4 width=6 by cpx_cpxs, ex3_3_intro, or_intror/
  83 | * #I #K #T1 #Hi #HT1 #H destruct
  84   elim (cpx_inv_lifts_sn … HT2 (Ⓣ) … K … HT1) -T
  85   /4 width=6 by cpxs_strap1, drops_refl, drops_drop, ex3_3_intro, or_intror/
  86 ]
  87 qed-.
  88
  89 (* Basic_2A1: was: cpxs_inv_lref1 *)
  90 lemma cpxs_inv_lref1_drops (G) (L):
  91       ∀T2,i. ❪G,L❫ ⊢ #i ⬈* T2 →
  92       ∨∨ T2 = #i
  93        | ∃∃I,K,V1,T1. ⇩[i] L ≘ K.ⓑ[I]V1 & ❪G,K❫ ⊢ V1 ⬈* T1 & ⇧[↑i] T1 ≘ T2.
  94 #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
  95 #T #T2 #_ #HT2 *
  96 [ #H destruct
  97   elim (cpx_inv_lref1_drops … HT2) -HT2 /2 width=1 by or_introl/
  98   * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/
  99 | * #I #K #V1 #T1 #HLK #HVT1 #HT1
 100   lapply (drops_isuni_fwd_drop2 … HLK) // #H0LK
 101   elim (cpx_inv_lifts_sn … HT2 … H0LK … HT1) -H0LK -T
 102   /4 width=7 by cpxs_strap1, ex3_4_intro, or_intror/
 103 ]
 104 qed-.
 105
 106 (* Properties with generic relocation ***************************************)
 107
 108 (* Basic_2A1: includes: cpxs_lift *)
 109 lemma cpxs_lifts_sn (G):
 110       d_liftable2_sn … lifts (cpxs G).
 111 /3 width=10 by cpx_lifts_sn, cpxs_strap1, d2_liftable_sn_CTC/ qed-.
 112
 113 lemma cpxs_lifts_bi (G):
 114       d_liftable2_bi … lifts (cpxs G).
 115 /3 width=12 by cpxs_lifts_sn, d_liftable2_sn_bi, lifts_mono/ qed-.
 116
 117 (* Inversion lemmas with generic relocation *********************************)
 118
 119 (* Basic_2A1: includes: cpxs_inv_lift1 *)
 120 lemma cpxs_inv_lifts_sn (G):
 121       d_deliftable2_sn … lifts (cpxs G).
 122 /3 width=6 by d2_deliftable_sn_CTC, cpx_inv_lifts_sn/ qed-.
 123
 124 lemma cpxs_inv_lifts_bi (G):
 125       d_deliftable2_bi … lifts (cpxs G).
 126 /3 width=12 by cpxs_inv_lifts_sn, d_deliftable2_sn_bi, lifts_inj/ qed-.