matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees_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/substitution/cpys_lift.ma".
  16 include "basic_2/substitution/cofrees.ma".
  17
  18 (* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************)
  19
  20 (* Advanced properties ******************************************************)
  21
  22 lemma cofrees_lref_skip: ∀L,d,i,j. j < i → yinj j < d → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄.
  23 #L #d #i #j #Hji #Hjd #X #H elim (cpys_inv_lref1_Y2 … H) -H
  24 [ #H destruct /3 width=2 by lift_lref_lt, ex_intro/
  25 | * #I #K #W1 #W2 #Hdj elim (ylt_yle_false … Hdj) -i -I -L -K -W1 -W2 -X //
  26 ]
  27 qed.
  28
  29 lemma cofrees_lref_lt: ∀L,d,i,j. i < j → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄.
  30 #L #d #i #j #Hij #X #H elim (cpys_inv_lref1_Y2 … H) -H
  31 [ #H destruct /3 width=2 by lift_lref_ge_minus, ex_intro/
  32 | * #I #K #V1 #V2 #_ #_ #_ #H -I -L -K -V1 -d
  33   elim (lift_split … H i j) /2 width=2 by lt_to_le, ex_intro/
  34 ]
  35 qed.
  36
  37 lemma cofrees_lref_gt: ∀I,L,K,W,d,i,j. j < i → ⇩[j] L ≡ K.ⓑ{I}W →
  38                        K ⊢ (i-j-1) ~ϵ 𝐅*[O]⦃W⦄ → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄.
  39 #I #L #K #W1 #d #i #j #Hji #HLK #HW1 #X #H elim (cpys_inv_lref1_Y2 … H) -H
  40 [ #H destruct /3 width=2 by lift_lref_lt, ex_intro/
  41 | * #I0 #K0 #W0 #W2 #Hdj #HLK0 #HW12 #HW2 lapply (ldrop_mono … HLK0 … HLK) -L
  42   #H destruct elim (HW1 … HW12) -I -K -W1 -d
  43   #V2 #HVW2 elim (lift_trans_le … HVW2 … HW2) -W2 //
  44   >minus_plus <plus_minus_m_m /2 width=2 by ex_intro/
  45 ]
  46 qed.
  47
  48 lemma cofrees_lref_free: ∀L,d,i,j. |L| ≤ j → j < i → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄.
  49 #L #d #i #j #Hj #Hji #X #H elim (cpys_inv_lref1_Y2 … H) -H
  50 [ #H destruct /3 width=2 by lift_lref_lt, ex_intro/
  51 | * #I #K #W1 #W2 #_ #HLK lapply (ldrop_fwd_length_lt2 … HLK) -I
  52   #H elim (lt_refl_false j) -d -i -K -W1 -W2 -X /2 width=3 by lt_to_le_to_lt/
  53 ]
  54 qed.
  55
  56 (* Advanced negated inversion lemmas ****************************************)
  57
  58 lemma frees_inv_lref_gt: ∀L,d,i,j. j < i → (L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄ → ⊥) →
  59                          ∃∃I,K,W. ⇩[j] L ≡ K.ⓑ{I}W & (K ⊢ (i-j-1) ~ϵ 𝐅*[0]⦃W⦄ → ⊥) & d ≤ yinj j.
  60 #L #d #i #j #Hji #H elim (ylt_split j d) #Hjd
  61 [ elim H -H /2 width=6 by cofrees_lref_skip/
  62 | elim (lt_or_ge j (|L|)) #Hj
  63   [ elim (ldrop_O1_lt … Hj) -Hj /4 width=10 by cofrees_lref_gt, ex3_3_intro/
  64   | elim H -H /2 width=6 by cofrees_lref_free/
  65   ]
  66 ]
  67 qed-.
  68
  69 lemma frees_inv_lref_free: ∀L,d,i,j. (L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄  → ⊥) → |L| ≤ j → j = i.
  70 #L #d #i #j #H #Hj elim (lt_or_eq_or_gt i j) //
  71 #Hij elim H -H /2 width=6 by cofrees_lref_lt, cofrees_lref_free/
  72 qed-.
  73
  74 lemma frees_inv_gen: ∀L,U,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) →
  75                      ∃∃U0.  ⦃⋆, L⦄ ⊢ U ▶*[d, ∞] U0 & (∀T. ⇧[i, 1] T ≡ U0 → ⊥).
  76 #L #U @(f2_ind … rfw … L U) -L -U
  77 #n #IH #L * *
  78 [ -IH #k #_ #d #i #H elim H -H //
  79 | #j #Hn #d #i #H elim (lt_or_eq_or_gt i j)
  80   [ -n #Hij elim H -H /2 width=5 by cofrees_lref_lt/
  81   | -H -n #H destruct /3 width=7 by lift_inv_lref2_be, ex2_intro/
  82   | #Hji elim (frees_inv_lref_gt … H) // -H
  83     #I #K #W1 #HLK #H #Hdj elim (IH … H) /2 width=2 by ldrop_fwd_rfw/ -H -n
  84     #W2 #HW12 #HnW2 elim (lift_total W2 0 (j+1))
  85     #U2 #HWU2 @(ex2_intro … U2) /2 width=7 by cpys_subst_Y2/ -I -L -K -W1 -d
  86     #T2 #HTU2 elim (lift_div_le … HWU2 (i-j-1) 1 T2) /2 width=2 by/ -W2
  87     >minus_plus <plus_minus_m_m //
  88   ]
  89 | -IH #p #_ #d #i #H elim H -H //
  90 | #a #I #W #U #Hn #d #i #H elim (frees_inv_bind … H) -H
  91   #H elim (IH … H) // -H -n
  92   /4 width=9 by cpys_bind, nlift_bind_dx, nlift_bind_sn, ex2_intro/
  93 | #I #W #U #Hn #d #i #H elim (frees_inv_flat … H) -H
  94   #H elim (IH … H) // -H -n
  95   /4 width=9 by cpys_flat, nlift_flat_dx, nlift_flat_sn, ex2_intro/
  96 ]
  97 qed-.