matita/matita/contribs/lambdadelta/basic_2/static/frees_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 "ground_2/relocation/rtmap_pushs.ma".
  16 include "basic_2/relocation/drops.ma".
  17 include "basic_2/static/frees.ma".
  18
  19 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
  20
  21 (* Advanced properties ******************************************************)
  22
  23 lemma drops_atom_F: ∀f. ⬇*[Ⓕ, f] ⋆ ≡ ⋆.
  24 #f @drops_atom #H destruct
  25 qed.
  26
  27 lemma frees_inv_lref_drops: ∀i,f,L. L ⊢ 𝐅*⦃#i⦄ ≡ f →
  28                             (⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ ∧ 𝐈⦃f⦄) ∨
  29                             ∃∃g,I,K,V. K ⊢ 𝐅*⦃V⦄ ≡ g &
  30                                        ⬇*[i] L ≡ K.ⓑ{I}V & f = ↑*[i] ⫯g.
  31 #i elim i -i
  32 [ #f #L #H elim (frees_inv_zero … H) -H *
  33   /4 width=7 by ex3_4_intro, or_introl, or_intror, conj, drops_refl/
  34 | #i #IH #f #L #H elim (frees_inv_lref … H) -H * /3 width=1 by or_introl, conj/
  35   #g #I #K #V #Hg #H1 #H2 destruct
  36   elim (IH … Hg) -IH -Hg *
  37   [ /4 width=3 by or_introl, conj, isid_push, drops_drop/
  38   | /4 width=7 by drops_drop, ex3_4_intro, or_intror/
  39   ]
  40 ]
  41 qed-.
  42
  43
  44
  45 lemma frees_dec: ∀L,U,l,i. Decidable (frees l L U i).
  46 #L #U @(f2_ind … rfw … L U) -L -U
  47 #x #IH #L * *
  48 [ -IH /3 width=5 by frees_inv_sort, or_intror/
  49 | #j #Hx #l #i elim (ylt_split_eq i j) #Hji
  50   [ -x @or_intror #H elim (ylt_yle_false … Hji)
  51     lapply (frees_inv_lref_ge … H ?) -L -l /2 width=1 by ylt_fwd_le/
  52   | -x /2 width=1 by or_introl/
  53   | elim (ylt_split j l) #Hli
  54     [ -x @or_intror #H elim (ylt_yle_false … Hji)
  55       lapply (frees_inv_lref_skip … H ?) -L //
  56     | elim (lt_or_ge j (|L|)) #Hj
  57       [ elim (drop_O1_lt (Ⓕ) L j) // -Hj #I #K #W #HLK destruct
  58         elim (IH K W … 0 (i-j-1)) -IH [1,3: /3 width=5 by frees_lref_be, drop_fwd_rfw, or_introl/ ] #HnW
  59         @or_intror #H elim (frees_inv_lref_lt … H) // #Z #Y #X #_ #HLY -l
  60         lapply (drop_mono … HLY … HLK) -L #H destruct /2 width=1 by/
  61       | -x @or_intror #H elim (ylt_yle_false … Hji)
  62         lapply (frees_inv_lref_free … H ?) -l //
  63       ]
  64     ]
  65   ]
  66 | -IH /3 width=5 by frees_inv_gref, or_intror/
  67 | #a #I #W #U #Hx #l #i destruct
  68   elim (IH L W … l i) [1,3: /3 width=1 by frees_bind_sn, or_introl/ ] #HnW
  69   elim (IH (L.ⓑ{I}W) U … (⫯l) (i+1)) -IH [1,3: /3 width=1 by frees_bind_dx, or_introl/ ] #HnU
  70   @or_intror #H elim (frees_inv_bind … H) -H /2 width=1 by/
  71 | #I #W #U #Hx #l #i destruct
  72   elim (IH L W … l i) [1,3: /3 width=1 by frees_flat_sn, or_introl/ ] #HnW
  73   elim (IH L U … l i) -IH [1,3: /3 width=1 by frees_flat_dx, or_introl/ ] #HnU
  74   @or_intror #H elim (frees_inv_flat … H) -H /2 width=1 by/
  75 ]
  76 qed-.
  77
  78 lemma frees_S: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[yinj l]⦃U⦄ → ∀I,K,W. ⬇[l] L ≡ K.ⓑ{I}W →
  79                (K ⊢ ⫰(i-l) ϵ 𝐅*[0]⦃W⦄ → ⊥) → L ⊢ i ϵ 𝐅*[⫯l]⦃U⦄.
  80 #L #U #l #i #H elim (frees_inv … H) -H /3 width=2 by frees_eq/
  81 * #I #K #W #j #Hlj #Hji #HnU #HLK #HW #I0 #K0 #W0 #HLK0 #HnW0
  82 lapply (yle_inv_inj … Hlj) -Hlj #Hlj
  83 elim (le_to_or_lt_eq … Hlj) -Hlj
  84 [ -I0 -K0 -W0 /3 width=9 by frees_be, yle_inj/
  85 | -Hji -HnU #H destruct
  86   lapply (drop_mono … HLK0 … HLK) #H destruct -I
  87   elim HnW0 -L -U -HnW0 //
  88 ]
  89 qed.
  90
  91 (* Note: lemma 1250 *)
  92 lemma frees_bind_dx_O: ∀a,I,L,W,U,i. L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[0]⦃U⦄ →
  93                        L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄.
  94 #a #I #L #W #U #i #HU elim (frees_dec L W 0 i)
  95 /4 width=5 by frees_S, frees_bind_dx, frees_bind_sn/
  96 qed.
  97
  98 (* Properties on relocation *************************************************)
  99
 100 lemma frees_lift_ge: ∀K,T,l,i. K ⊢ i ϵ𝐅*[l]⦃T⦄ →
 101                      ∀L,s,l0,m0. ⬇[s, l0, m0] L ≡ K →
 102                      ∀U. ⬆[l0, m0] T ≡ U → l0 ≤ i →
 103                      L ⊢ i+m0 ϵ 𝐅*[l]⦃U⦄.
 104 #K #T #l #i #H elim H -K -T -l -i
 105 [ #K #T #l #i #HnT #L #s #l0 #m0 #_ #U #HTU #Hl0i -K -s
 106   @frees_eq #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
 107 | #I #K #K0 #T #V #l #i #j #Hlj #Hji #HnT #HK0 #HV #IHV #L #s #l0 #m0 #HLK #U #HTU #Hl0i
 108   elim (ylt_split j l0) #H0
 109   [ elim (drop_trans_lt … HLK … HK0) // -K #L0 #W #HL0 >yminus_SO2 #HLK0 #HVW
 110     @(frees_be … HL0) -HL0 -HV /3 width=3 by ylt_plus_dx2_trans/
 111     [ lapply (ylt_fwd_lt_O1 … H0) #H1
 112       #X #HXU <(ymax_pre_sn l0 1) in HTU; /2 width=1 by ylt_fwd_le_succ1/ #HTU
 113       <(ylt_inv_O1 l0) in H0; // -H1 #H0
 114       elim (lift_div_le … HXU … HTU ?) -U /2 width=2 by ylt_fwd_succ2/
 115     | >yplus_minus_comm_inj /2 width=1 by ylt_fwd_le/
 116       <yplus_pred1 /4 width=5 by monotonic_yle_minus_dx, yle_pred, ylt_to_minus/
 117     ]
 118   | lapply (drop_trans_ge … HLK … HK0 ?) // -K #HLK0
 119     lapply (drop_inv_gen … HLK0) >commutative_plus -HLK0 #HLK0
 120     @(frees_be … HLK0) -HLK0 -IHV
 121     /2 width=1 by monotonic_ylt_plus_dx, yle_plus_dx1_trans/
 122     [ #X <yplus_inj #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
 123     | <yplus_minus_assoc_comm_inj //
 124     ]
 125   ]
 126 ]
 127 qed.
 128
 129 (* Inversion lemmas on relocation *******************************************)
 130
 131 lemma frees_inv_lift_be: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
 132                          ∀K,s,l0,m0. ⬇[s, l0, m0+1] L ≡ K →
 133                          ∀T. ⬆[l0, m0+1] T ≡ U → l0 ≤ i → i ≤ l0 + m0 → ⊥.
 134 #L #U #l #i #H elim H -L -U -l -i
 135 [ #L #U #l #i #HnU #K #s #l0 #m0 #_ #T #HTU #Hl0i #Hilm0
 136   elim (lift_split … HTU i m0) -HTU /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 #Hl0i #Hilm0
 138   elim (ylt_split j l0) #H1
 139   [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
 140     @(IHW … HKL0 … HVW)
 141     [ /3 width=1 by monotonic_yle_minus_dx, yle_pred/
 142     | >yplus_pred1 /2 width=1 by ylt_to_minus/
 143       <yplus_minus_comm_inj /3 width=1 by monotonic_yle_minus_dx, yle_pred, ylt_fwd_le/
 144     ]
 145   | elim (lift_split … HTU j m0) -HTU /3 width=3 by ylt_yle_trans, ylt_fwd_le/
 146   ]
 147 ]
 148 qed-.
 149
 150 lemma frees_inv_lift_ge: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
 151                          ∀K,s,l0,m0. ⬇[s, l0, m0] L ≡ K →
 152                          ∀T. ⬆[l0, m0] T ≡ U → l0 + m0 ≤ i →
 153                          K ⊢ i-m0 ϵ𝐅*[l-yinj m0]⦃T⦄.
 154 #L #U #l #i #H elim H -L -U -l -i
 155 [ #L #U #l #i #HnU #K #s #l0 #m0 #HLK #T #HTU #Hlm0i -L -s
 156   elim (yle_inv_plus_inj2 … Hlm0i) -Hlm0i #Hl0im0 #Hm0i @frees_eq #X #HXT -K
 157   elim (lift_trans_le … HXT … HTU) -T // >ymax_pre_sn /2 width=2 by/
 158 | #I #L #K0 #U #W #l #i #j #Hli #Hij #HnU #HLK0 #_ #IHW #K #s #l0 #m0 #HLK #T #HTU #Hlm0i
 159   elim (ylt_split j l0) #H1
 160   [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
 161     elim (yle_inv_plus_inj2 … Hlm0i) #H0 #Hm0i
 162     @(frees_be … H) -H
 163     [ /3 width=1 by yle_plus_dx1_trans, monotonic_yle_minus_dx/
 164     | /2 width=3 by ylt_yle_trans/
 165     | #X #HXT elim (lift_trans_ge … HXT … HTU) -T /2 width=2 by ylt_fwd_le_succ1/
 166     | lapply (IHW … HKL0 … HVW ?) // -I -K -K0 -L0 -V -W -T -U -s
 167       >yplus_pred1 /2 width=1 by ylt_to_minus/
 168       <yplus_minus_comm_inj /3 width=1 by monotonic_yle_minus_dx, yle_pred, ylt_fwd_le/
 169     ]
 170   | elim (ylt_split j (l0+m0)) #H2
 171     [ -L -I -W elim (yle_inv_inj2 … H1) -H1 #x #H1 #H destruct
 172       lapply (ylt_plus2_to_minus_inj1 … H2) /2 width=1 by yle_inj/ #H3
 173       lapply (ylt_fwd_lt_O1 … H3) -H3 #H3
 174       elim (lift_split … HTU j (m0-1)) -HTU /2 width=1 by yle_inj/
 175       [ >minus_minus_associative /2 width=1 by ylt_inv_inj/ <minus_n_n
 176         -H2 #X #_ #H elim (HnU … H)
 177       | <yminus_inj >yminus_SO2 >yplus_pred2 /2 width=1 by ylt_fwd_le_pred2/
 178       ]
 179     | lapply (drop_conf_ge … HLK … HLK0 ?) // -L #HK0
 180       elim ( yle_inv_plus_inj2 … H2) -H2 #H2 #Hm0j
 181       @(frees_be … HK0)
 182       [ /2 width=1 by monotonic_yle_minus_dx/
 183       | /2 width=1 by monotonic_ylt_minus_dx/
 184       | #X #HXT elim (lift_trans_le … HXT … HTU) -T //
 185         <yminus_inj >ymax_pre_sn /2 width=2 by/
 186       | <yminus_inj >yplus_minus_assoc_comm_inj //
 187         >ymax_pre_sn /3 width=5 by yle_trans, ylt_fwd_le/
 188       ]
 189     ]
 190   ]
 191 ]
 192 qed-.