matita/matita/contribs/lambdadelta/basic_2/substitution/frees.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/ynat/ynat_plus.ma".
  16 include "basic_2/notation/relations/freestar_4.ma".
  17 include "basic_2/relocation/lift_neg.ma".
  18 include "basic_2/relocation/ldrop.ma".
  19
  20 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
  21
  22 inductive frees: relation4 ynat lenv term nat ≝
  23 | frees_eq: ∀L,U,d,i. (∀T. ⇧[i, 1] T ≡ U → ⊥) → frees d L U i
  24 | frees_be: ∀I,L,K,U,W,d,i,j. d ≤ yinj j → j < i →
  25             (∀T. ⇧[j, 1] T ≡ U → ⊥) → ⇩[j]L ≡ K.ⓑ{I}W →
  26             frees 0 K W (i-j-1) → frees d L U i.
  27
  28 interpretation
  29    "context-sensitive free variables (term)"
  30    'FreeStar L i d U = (frees d L U i).
  31
  32 (* Basic inversion lemmas ***************************************************)
  33
  34 lemma frees_inv: ∀L,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃U⦄ →
  35                  (∀T. ⇧[i, 1] T ≡ U → ⊥) ∨
  36                  ∃∃I,K,W,j. d ≤ yinj j & j < i & (∀T. ⇧[j, 1] T ≡ U → ⊥) &
  37                             ⇩[j]L ≡ K.ⓑ{I}W & K ⊢ (i-j-1) ϵ 𝐅*[yinj 0]⦃W⦄.
  38 #L #U #d #i * -L -U -d -i /4 width=9 by ex5_4_intro, or_intror, or_introl/
  39 qed-.
  40
  41 lemma frees_inv_sort: ∀L,d,i,k. L ⊢ i ϵ 𝐅*[d]⦃⋆k⦄ → ⊥.
  42 #L #d #i #k #H elim (frees_inv … H) -H [|*] /2 width=2 by/
  43 qed-.
  44
  45 lemma frees_inv_gref: ∀L,d,i,p. L ⊢ i ϵ 𝐅*[d]⦃§p⦄ → ⊥.
  46 #L #d #i #p #H elim (frees_inv … H) -H [|*] /2 width=2 by/
  47 qed-.
  48
  49 lemma frees_inv_lref: ∀L,d,j,i. L ⊢ i ϵ 𝐅*[d]⦃#j⦄ →
  50                       j = i ∨
  51                       ∃∃I,K,W. d ≤ yinj j & j < i & ⇩[j] L ≡ K.ⓑ{I}W & K ⊢ (i-j-1) ϵ 𝐅*[yinj 0]⦃W⦄.
  52 #L #d #x #i #H elim (frees_inv … H) -H
  53 [ /4 width=2 by nlift_inv_lref_be_SO, or_introl/
  54 | * #I #K #W #j #Hdj #Hji #Hnx #HLK #HW
  55   >(nlift_inv_lref_be_SO … Hnx) -x /3 width=5 by ex4_3_intro, or_intror/
  56 ]
  57 qed-.
  58
  59 lemma frees_inv_lref_free: ∀L,d,j,i. L ⊢ i ϵ 𝐅*[d]⦃#j⦄ → |L| ≤ j → j = i.
  60 #L #d #j #i #H #Hj elim (frees_inv_lref … H) -H //
  61 * #I #K #W #_ #_ #HLK lapply (ldrop_fwd_length_lt2 … HLK) -I
  62 #H elim (lt_refl_false j) /2 width=3 by lt_to_le_to_lt/
  63 qed-.
  64
  65 lemma frees_inv_lref_skip: ∀L,d,j,i. L ⊢ i ϵ 𝐅*[d]⦃#j⦄ → yinj j < d → j = i.
  66 #L #d #j #i #H #Hjd elim (frees_inv_lref … H) -H //
  67 * #I #K #W #Hdj elim (ylt_yle_false … Hdj) -Hdj //
  68 qed-.
  69
  70 lemma frees_inv_lref_ge: ∀L,d,j,i. L ⊢ i ϵ 𝐅*[d]⦃#j⦄ → i ≤ j → j = i.
  71 #L #d #j #i #H #Hij elim (frees_inv_lref … H) -H //
  72 * #I #K #W #_ #Hji elim (lt_refl_false j) -I -L -K -W -d /2 width=3 by lt_to_le_to_lt/
  73 qed-.
  74
  75 lemma frees_inv_lref_lt: ∀L,d,j,i.L ⊢ i ϵ 𝐅*[d]⦃#j⦄ → j < i →
  76                          ∃∃I,K,W. d ≤ yinj j & ⇩[j] L ≡ K.ⓑ{I}W & K ⊢ (i-j-1) ϵ 𝐅*[yinj 0]⦃W⦄.
  77 #L #d #j #i #H #Hji elim (frees_inv_lref … H) -H
  78 [ #H elim (lt_refl_false j) //
  79 | * /2 width=5 by ex3_3_intro/
  80 ]
  81 qed-.
  82
  83 lemma frees_inv_bind: ∀a,I,L,W,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃ⓑ{a,I}W.U⦄ →
  84                       L ⊢ i ϵ 𝐅*[d]⦃W⦄ ∨ L.ⓑ{I}W ⊢ i+1 ϵ 𝐅*[⫯d]⦃U⦄ .
  85 #a #J #L #V #U #d #i #H elim (frees_inv … H) -H
  86 [ #HnX elim (nlift_inv_bind … HnX) -HnX
  87   /4 width=2 by frees_eq, or_intror, or_introl/
  88 | * #I #K #W #j #Hdj #Hji #HnX #HLK #HW elim (nlift_inv_bind … HnX) -HnX
  89   [ /4 width=9 by frees_be, or_introl/
  90   | #HnT @or_intror @(frees_be … HnT) -HnT
  91     [4,5,6: /2 width=1 by ldrop_drop, yle_succ, lt_minus_to_plus/
  92     |7: >minus_plus_plus_l //
  93     |*: skip
  94     ]
  95   ]
  96 ]
  97 qed-.
  98
  99 lemma frees_inv_flat: ∀I,L,W,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃ⓕ{I}W.U⦄ →
 100                       L ⊢ i ϵ 𝐅*[d]⦃W⦄ ∨ L ⊢ i ϵ 𝐅*[d]⦃U⦄ .
 101 #J #L #V #U #d #i #H elim (frees_inv … H) -H
 102 [ #HnX elim (nlift_inv_flat … HnX) -HnX
 103   /4 width=2 by frees_eq, or_intror, or_introl/
 104 | * #I #K #W #j #Hdj #Hji #HnX #HLK #HW elim (nlift_inv_flat … HnX) -HnX
 105   /4 width=9 by frees_be, or_intror, or_introl/
 106 ]
 107 qed-.
 108
 109 (* Basic properties *********************************************************)
 110
 111 lemma frees_lref_eq: ∀L,d,i. L ⊢ i ϵ 𝐅*[d]⦃#i⦄.
 112 /3 width=7 by frees_eq, lift_inv_lref2_be/ qed.
 113
 114 lemma frees_lref_be: ∀I,L,K,W,d,i,j. d ≤ yinj j → j < i → ⇩[j]L ≡ K.ⓑ{I}W →
 115                      K ⊢ i-j-1 ϵ 𝐅*[0]⦃W⦄ → L ⊢ i ϵ 𝐅*[d]⦃#j⦄.
 116 /3 width=9 by frees_be, lift_inv_lref2_be/ qed.
 117
 118 lemma frees_bind_sn: ∀a,I,L,W,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃W⦄ →
 119                      L ⊢ i ϵ 𝐅*[d]⦃ⓑ{a,I}W.U⦄.
 120 #a #I #L #W #U #d #i #H elim (frees_inv … H) -H [|*]
 121 /4 width=9 by frees_be, frees_eq, nlift_bind_sn/
 122 qed.
 123
 124 lemma frees_bind_dx: ∀a,I,L,W,U,d,i. L.ⓑ{I}W ⊢ i+1 ϵ 𝐅*[⫯d]⦃U⦄ →
 125                      L ⊢ i ϵ 𝐅*[d]⦃ⓑ{a,I}W.U⦄.
 126 #a #J #L #V #U #d #i #H elim (frees_inv … H) -H
 127 [ /4 width=9 by frees_eq, nlift_bind_dx/
 128 | * #I #K #W #j #Hdj #Hji #HnU #HLK #HW
 129   elim (yle_inv_succ1 … Hdj) -Hdj <yminus_SO2 #Hyj #H
 130   lapply (ylt_O … H) -H #Hj
 131   >(plus_minus_m_m j 1) in HnU; // <minus_le_minus_minus_comm in HW;
 132   /4 width=9 by frees_be, nlift_bind_dx, ldrop_inv_drop1_lt, lt_plus_to_minus/
 133 ]
 134 qed.
 135
 136 lemma frees_flat_sn: ∀I,L,W,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃W⦄ →
 137                      L ⊢ i ϵ 𝐅*[d]⦃ⓕ{I}W.U⦄.
 138 #I #L #W #U #d #i #H elim (frees_inv … H) -H [|*]
 139 /4 width=9 by frees_be, frees_eq, nlift_flat_sn/
 140 qed.
 141
 142 lemma frees_flat_dx: ∀I,L,W,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃U⦄ →
 143                      L ⊢ i ϵ 𝐅*[d]⦃ⓕ{I}W.U⦄.
 144 #I #L #W #U #d #i #H elim (frees_inv … H) -H [|*]
 145 /4 width=9 by frees_be, frees_eq, nlift_flat_dx/
 146 qed.
 147
 148 lemma frees_weak: ∀L,U,d1,i. L ⊢ i ϵ 𝐅*[d1]⦃U⦄ →
 149                   ∀d2. d2 ≤ d1 → L ⊢ i ϵ 𝐅*[d2]⦃U⦄.
 150 #L #U #d1 #i #H elim H -L -U -d1 -i
 151 /3 width=9 by frees_be, frees_eq, yle_trans/
 152 qed-.
 153
 154 (* Advanced inversion lemmas ************************************************)
 155
 156 lemma frees_inv_bind_O: ∀a,I,L,W,U,i. L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄ →
 157                         L ⊢ i ϵ 𝐅*[0]⦃W⦄ ∨ L.ⓑ{I}W ⊢ i+1 ϵ 𝐅*[0]⦃U⦄ .
 158 #a #I #L #W #U #i #H elim (frees_inv_bind … H) -H
 159 /3 width=3 by frees_weak, or_intror, or_introl/
 160 qed-.