matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_lift.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/cny_lift.ma".
  16 include "basic_2/substitution/fqup.ma".
  17 include "basic_2/substitution/cpys_lift.ma".
  18 include "basic_2/substitution/cpye.ma".
  19
  20 (* EVALUATION FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION ON TERMS **********)
  21
  22 (* Advanced properties ******************************************************)
  23
  24 lemma cpye_subst: ∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → i < d + e →
  25                   ⇩[i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ▶*[O, ⫰(d+e-i)] 𝐍⦃V2⦄ →
  26                   ⇧[O, i+1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃W2⦄.
  27 #I #G #L #K #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK *
  28 /4 width=13 by cpys_subst, cny_subst_aux, ldrop_fwd_drop2, conj/
  29 qed.
  30
  31 lemma cpys_total: ∀G,L,T1,d,e. ∃T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄.
  32 #G #L #T1 @(fqup_wf_ind_eq … G L T1) -G -L -T1
  33 #Z #Y #X #IH #G #L * *
  34 [ #k #HG #HL #HT #d #e destruct -IH /2 width=2 by ex_intro/
  35 | #i #HG #HL #HT #d #e destruct
  36   elim (ylt_split i d) /3 width=2 by cpye_skip, ex_intro/
  37   elim (ylt_split i (d+e)) /3 width=2 by cpye_top, ex_intro/
  38   elim (lt_or_ge i (|L|)) /3 width=2 by cpye_free, ex_intro/
  39   #Hi #Hide #Hdi elim (ldrop_O1_lt L i) // -Hi
  40   #I #K #V1 #HLK elim (IH G K V1 … 0 (⫰(d+e-i))) -IH /2 width=2 by fqup_lref/
  41   #V2 elim (lift_total V2 0 (i+1)) /3 width=8 by ex_intro, cpye_subst/
  42 | #p #HG #HL #HT #d #e destruct -IH /2 width=2 by ex_intro/
  43 | #a #I #V1 #T1 #HG #HL #HT #d #e destruct
  44   elim (IH G L V1 … d e) // elim (IH G (L.ⓑ{I}V1) T1 … (⫯d) e) //
  45   /3 width=2 by cpye_bind, ex_intro/
  46 | #I #V1 #T1 #HG #HL #HT #d #e destruct
  47   elim (IH G L V1 … d e) // elim (IH G L T1 … d e) //
  48   /3 width=2 by cpye_flat, ex_intro/
  49 ]
  50 qed-.
  51
  52 (* Advanced inversion lemmas ************************************************)
  53
  54 lemma cpye_inv_lref1: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ →
  55                       ∨∨ |L| ≤ i ∧ T2 = #i
  56                        | d + e ≤ yinj i ∧ T2 = #i
  57                        | yinj i < d ∧ T2 = #i
  58                        | ∃∃I,K,V1,V2. d ≤ yinj i & yinj i < d + e &
  59                                       ⇩[i] L ≡ K.ⓑ{I}V1 &
  60                                       ⦃G, K⦄ ⊢ V1 ▶*[yinj 0, ⫰(d+e-yinj i)]  𝐍⦃V2⦄ &
  61                                       ⇧[O, i+1] V2 ≡ T2.
  62 #G #L #T2 #i #d #e * #H1 #H2 elim (cpys_inv_lref1 … H1) -H1
  63 [ #H destruct elim (cny_inv_lref … H2) -H2
  64   /3 width=1 by or4_intro0, or4_intro1, or4_intro2, conj/
  65 | * #I #K #V1 #V2 #Hdi #Hide #HLK #HV12 #HVT2
  66     @or4_intro3 @(ex5_4_intro … HLK … HVT2) (**) (* explicit constructor *)
  67     /4 width=13 by cny_inv_subst_aux, ldrop_fwd_drop2, conj/
  68 ]
  69 qed-.
  70
  71 lemma cpye_inv_lref1_free: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ →
  72                            (∨∨ |L| ≤ i | d + e ≤ yinj i | yinj i < d) → T2 = #i.
  73 #G #L #T2 #d #e #i #H * elim (cpye_inv_lref1 … H) -H * //
  74 #I #K #V1 #V2 #Hdi #Hide #HLK #_ #_ #H
  75 [ elim (lt_refl_false i) -d
  76   @(lt_to_le_to_lt … H) -H /2 width=5 by ldrop_fwd_length_lt2/ (**) (* full auto slow: 19s *)
  77 ]
  78 elim (ylt_yle_false … H) //
  79 qed-.
  80
  81 lemma cpye_inv_lref1_subst: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ →
  82                             ∀I,K,V1,V2. d ≤ yinj i → yinj i < d + e →
  83                             ⇩[i] L ≡ K.ⓑ{I}V1 → ⇧[O, i+1] V2 ≡ T2 →
  84                             ⦃G, K⦄ ⊢ V1 ▶*[yinj 0, ⫰(d+e-yinj i)]  𝐍⦃V2⦄.
  85 #G #L #T2 #d #e #i #H #I #K #V1 #V2 #Hdi #Hide #HLK #HVT2 elim (cpye_inv_lref1 … H) -H *
  86 [ #H elim (lt_refl_false i) -V2 -T2 -d
  87   @(lt_to_le_to_lt … H) -H /2 width=5 by ldrop_fwd_length_lt2/
  88 |2,3: #H elim (ylt_yle_false … H) //
  89 | #Z #Y #X1 #X2 #_ #_ #HLY #HX12 #HXT2
  90   lapply (ldrop_mono … HLY … HLK) -HLY -HLK #H destruct
  91   lapply (lift_inj … HXT2 … HVT2) -HXT2 -HVT2 #H destruct //
  92 ]
  93 qed-.