matita/matita/contribs/lambdadelta/basic_2A/multiple/frees_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 "ground_2/lib/arith_2a.ma".
  16 include "ground_2/ynat/ynat_minus_sn.ma".
  17 include "basic_2A/substitution/drop_drop.ma".
  18 include "basic_2A/multiple/frees.ma".
  19
  20 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
  21
  22 (* Advanced properties ******************************************************)
  23
  24 lemma frees_dec: ∀L,U,l,i. Decidable (frees l L U i).
  25 #L #U @(f2_ind … rfw … L U) -L -U
  26 #x #IH #L * *
  27 [ -IH /3 width=5 by frees_inv_sort, or_intror/
  28 | #j #Hx #l #i elim (lt_or_eq_or_gt i j) #Hji
  29   [ -x @or_intror #H elim (lt_refl_false i)
  30     lapply (frees_inv_lref_ge … H ?) -L -l /2 width=1 by lt_to_le/
  31   | -x /2 width=1 by or_introl/
  32   | elim (ylt_split j l) #Hli
  33     [ -x @or_intror #H elim (lt_refl_false i)
  34       lapply (frees_inv_lref_skip … H ?) -L //
  35     | elim (lt_or_ge j (|L|)) #Hj
  36       [ elim (drop_O1_lt (Ⓕ) L j) // -Hj #I #K #W #HLK destruct
  37         elim (IH K W … 0 (i-j-1)) -IH [1,3: /3 width=5 by frees_lref_be, drop_fwd_rfw, or_introl/ ] #HnW
  38         @or_intror #H elim (frees_inv_lref_lt … H) // #Z #Y #X #_ #HLY -l
  39         lapply (drop_mono … HLY … HLK) -L #H destruct /2 width=1 by/
  40       | -x @or_intror #H elim (lt_refl_false i)
  41         lapply (frees_inv_lref_free … H ?) -l //
  42       ]
  43     ]
  44   ]
  45 | -IH /3 width=5 by frees_inv_gref, or_intror/
  46 | #a #I #W #U #Hx #l #i destruct
  47   elim (IH L W … l i) [1,3: /3 width=1 by frees_bind_sn, or_introl/ ] #HnW
  48   elim (IH (L.ⓑ{I}W) U … (↑l) (i+1)) -IH [1,3: /3 width=1 by frees_bind_dx, or_introl/ ] #HnU
  49   @or_intror #H elim (frees_inv_bind … H) -H /2 width=1 by/
  50 | #I #W #U #Hx #l #i destruct
  51   elim (IH L W … l i) [1,3: /3 width=1 by frees_flat_sn, or_introl/ ] #HnW
  52   elim (IH L U … l i) -IH [1,3: /3 width=1 by frees_flat_dx, or_introl/ ] #HnU
  53   @or_intror #H elim (frees_inv_flat … H) -H /2 width=1 by/
  54 ]
  55 qed-.
  56
  57 alias symbol "UpArrow" (instance 2) = "ynat successor".
  58 alias symbol "minus" (instance 6) = "natural minus".
  59 alias symbol "minus" (instance 5) = "natural minus".
  60 alias symbol "RDrop" (instance 9) = "basic slicing (local environment) lget".
  61 lemma frees_S: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[yinj l]⦃U⦄ → ∀I,K,W. ⬇[l] L ≡ K.ⓑ{I}W →
  62                (K ⊢ i-l-1 ϵ 𝐅*[0]⦃W⦄ → ⊥) → L ⊢ i ϵ 𝐅*[↑l]⦃U⦄.
  63 #L #U #l #i #H elim (frees_inv … H) -H /3 width=2 by frees_eq/
  64 * #I #K #W #j #Hlj #Hji #HnU #HLK #HW #I0 #K0 #W0 #HLK0 #HnW0
  65 lapply (yle_inv_inj … Hlj) -Hlj #Hlj
  66 elim (le_to_or_lt_eq … Hlj) -Hlj
  67 [ -I0 -K0 -W0 /3 width=9 by frees_be, yle_inj/
  68 | -Hji -HnU #H destruct
  69   lapply (drop_mono … HLK0 … HLK) #H destruct -I
  70   elim HnW0 -L -U -HnW0 //
  71 ]
  72 qed.
  73
  74 (* Note: lemma 1250 *)
  75 lemma frees_bind_dx_O: ∀a,I,L,W,U,i. L.ⓑ{I}W ⊢ i+1 ϵ 𝐅*[0]⦃U⦄ →
  76                        L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄.
  77 #a #I #L #W #U #i #HU elim (frees_dec L W 0 i)
  78 /4 width=5 by frees_S, frees_bind_dx, frees_bind_sn/
  79 qed.
  80
  81 (* Properties on relocation *************************************************)
  82
  83 lemma frees_lift_ge: ∀K,T,l,i. K ⊢ i ϵ𝐅*[l]⦃T⦄ →
  84                      ∀L,s,l0,m0. ⬇[s, l0, m0] L ≡ K →
  85                      ∀U. ⬆[l0, m0] T ≡ U → l0 ≤ i →
  86                      L ⊢ i+m0 ϵ 𝐅*[l]⦃U⦄.
  87 #K #T #l #i #H elim H -K -T -l -i
  88 [ #K #T #l #i #HnT #L #s #l0 #m0 #_ #U #HTU #Hl0i -K -s
  89   @frees_eq #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
  90 | #I #K #K0 #T #V #l #i #j #Hlj #Hji #HnT #HK0 #HV #IHV #L #s #l0 #m0 #HLK #U #HTU #Hl0i
  91   elim (lt_or_ge j l0) #H1
  92   [ elim (drop_trans_lt … HLK … HK0) // -K #L0 #W #HL0 #HLK0 #HVW
  93     @(frees_be … HL0) -HL0 -HV
  94     /3 width=3 by lt_plus_to_minus_r, lt_to_le_to_lt/
  95     [ #X #HXU >(plus_minus_m_m l0 1) in HTU; /2 width=2 by ltn_to_ltO/ #HTU
  96       elim (lift_div_le … HXU … HTU ?) -U /2 width=2 by monotonic_pred/
  97     | >minus_plus <plus_minus // <minus_plus
  98       /3 width=5 by monotonic_le_minus_l2/
  99     ]
 100   | lapply (drop_trans_ge … HLK … HK0 ?) // -K #HLK0
 101     lapply (drop_inv_gen … HLK0) >commutative_plus -HLK0 #HLK0
 102     @(frees_be … HLK0) -HLK0 -IHV
 103     /2 width=1 by yle_plus_dx1_trans, lt_minus_to_plus/
 104     #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
 105   ]
 106 ]
 107 qed.
 108
 109 (* Inversion lemmas on relocation *******************************************)
 110
 111 lemma frees_inv_lift_be: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
 112                          ∀K,s,l0,m0. ⬇[s, l0, m0+1] L ≡ K →
 113                          ∀T. ⬆[l0, m0+1] T ≡ U → l0 ≤ i → i ≤ l0 + m0 → ⊥.
 114 #L #U #l #i #H elim H -L -U -l -i
 115 [ #L #U #l #i #HnU #K #s #l0 #m0 #_ #T #HTU #Hl0i #Hilm0
 116   elim (lift_split … HTU i m0) -HTU /2 width=2 by/
 117 | #I #L #K0 #U #W #l #i #j #Hli #Hij #HnU #HLK0 #_ #IHW #K #s #l0 #m0 #HLK #T #HTU #Hl0i #Hilm0
 118   elim (lt_or_ge j l0) #H1
 119   [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
 120     @(IHW … HKL0 … HVW)
 121     [ /2 width=1 by monotonic_le_minus_l2/
 122     | >minus_plus >minus_plus >plus_minus /2 width=1 by monotonic_le_minus_l/
 123     ]
 124   | elim (lift_split … HTU j m0) -HTU /3 width=3 by lt_to_le_to_lt, lt_to_le/
 125   ]
 126 ]
 127 qed-.
 128
 129 lemma frees_inv_lift_ge: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
 130                          ∀K,s,l0,m0. ⬇[s, l0, m0] L ≡ K →
 131                          ∀T. ⬆[l0, m0] T ≡ U → l0 + m0 ≤ i →
 132                          K ⊢ i-m0 ϵ𝐅*[l-m0]⦃T⦄.
 133 #L #U #l #i #H elim H -L -U -l -i
 134 [ #L #U #l #i #HnU #K #s #l0 #m0 #HLK #T #HTU #Hlm0i -L -s
 135   elim (le_inv_plus_l … Hlm0i) -Hlm0i #Hl0im0 #Hm0i @frees_eq #X #HXT -K
 136   elim (lift_trans_le … HXT … HTU) -T // <plus_minus_m_m /2 width=2 by/
 137 | #I #L #K0 #U #W #l #i #j #Hli #Hij #HnU #HLK0 #_ #IHW #K #s #l0 #m0 #HLK #T #HTU #Hlm0i
 138   elim (lt_or_ge j l0) #H1
 139   [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
 140     elim (le_inv_plus_l … Hlm0i) #H0 #Hm0i
 141     @(frees_be … H) -H
 142     [ /3 width=1 by yle_plus_dx1_trans, monotonic_yle_minus_dx/
 143     | /2 width=3 by lt_to_le_to_lt/
 144     | #X #HXT elim (lift_trans_ge … HXT … HTU) -T /2 width=2 by/
 145     | lapply (IHW … HKL0 … HVW ?) // -I -K -K0 -L0 -V -W -T -U -s
 146       >minus_plus >minus_plus >plus_minus /2 width=1 by monotonic_le_minus_l/
 147     ]
 148   | elim (lt_or_ge j (l0+m0)) [ >commutative_plus |] #H2
 149     [ -L -I -W lapply (lt_plus_to_minus ???? H2) // -H2 #H2
 150       elim (lift_split … HTU j (m0-1)) -HTU //
 151       [ >minus_minus_associative /2 width=2 by ltn_to_ltO/ <minus_n_n
 152         #X #_ #H elim (HnU … H)
 153       | >commutative_plus /3 width=1 by le_minus_to_plus, monotonic_pred/
 154       ]
 155     | lapply (drop_conf_ge … HLK … HLK0 ?) // -L #HK0
 156       elim (le_inv_plus_l … H2) -H2 #H2 #Hm0j
 157       @(frees_be … HK0)
 158       [ /2 width=1 by monotonic_yle_minus_dx/
 159       | /2 width=1 by monotonic_lt_minus_l/
 160       | #X #HXT elim (lift_trans_le … HXT … HTU) -T // <plus_minus_m_m /2 width=2 by/
 161       | >arith_b1 /2 width=5 by/
 162       ]
 163     ]
 164   ]
 165 ]
 166 qed-.