matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_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.ma".
  16 include "basic_2/rt_transition/cpg.ma".
  17
  18 (* CONTEXT-SENSITIVE GENERIC PARALLEL RT-TRANSITION FOR TERMS ***************)
  19
  20 (* Properties with generic slicing for local environments *******************)
  21
  22 lemma cpg_delift: ∀h,r,I,G,K,V,T1,L,l. ⬇*[i] L ≡ (K.ⓑ{I}V) →
  23                   ∃∃T2,T. ⦃G, L⦄ ⊢ T1 ➡[h, 𝟘𝟘] T2 & ⬆*[↑1] T ≡ T2.
  24 #h #r #I #G #K #V #T1 elim T1 -T1
  25 [ * #i #L #l /2 width=4 by cpg_atom, lift_sort, lift_gref, ex2_2_intro/
  26   elim (lt_or_eq_or_gt i l) #Hil [1,3: /4 width=4 by cpg_atom, lift_lref_ge_minus, lift_lref_lt, ylt_inj, yle_inj, ex2_2_intro/ ]
  27   destruct
  28   elim (lift_total V 0 (i+1)) #W #HVW
  29   elim (lift_split … HVW i i) /3 width=7 by cpg_delta, ex2_2_intro/
  30 | * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #l #HLK
  31   elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
  32   [ elim (IHU1 (L. ⓑ{I} W1) (l+1)) -IHU1 /3 width=9 by cpg_bind, drop_drop, lift_bind, ex2_2_intro/
  33   | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8 by cpg_flat, lift_flat, ex2_2_intro/
  34   ]
  35 ]
  36 qed-.
  37
  38 lemma cpg_inv_lref1: ∀h,r,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[h, r] T2 →
  39                      T2 = #i ∨
  40                      ∃∃I,K,V,V2. ⬇[i] L ≡ K. ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, r] V2 &
  41                                  ⬆[O, i+1] V2 ≡ T2.
  42 #h #r #G #L #T2 #i #H
  43 elim (cpg_inv_atom1 … H) -H /2 width=1 by or_introl/ *
  44 [ #s #d #_ #_ #H destruct
  45 | #I #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=7 by ex3_4_intro, or_intror/
  46 ]
  47 qed-.