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