matita/matita/contribs/lambdadelta/basic_2/static/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/relocation/rtmap_sor.ma".
  16 include "basic_2/notation/relations/freestar_3.ma".
  17 include "basic_2/syntax/lenv.ma".
  18
  19 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
  20
  21 inductive frees: relation3 lenv term rtmap ≝
  22 | frees_atom: ∀f,I. 𝐈⦃f⦄ → frees (⋆) (⓪{I}) f
  23 | frees_sort: ∀f,I,L,V,s. frees L (⋆s) f →
  24               frees (L.ⓑ{I}V) (⋆s) (↑f)
  25 | frees_zero: ∀f,I,L,V. frees L V f →
  26               frees (L.ⓑ{I}V) (#0) (⫯f)
  27 | frees_lref: ∀f,I,L,V,i. frees L (#i) f →
  28               frees (L.ⓑ{I}V) (#⫯i) (↑f)
  29 | frees_gref: ∀f,I,L,V,l. frees L (§l) f →
  30               frees (L.ⓑ{I}V) (§l) (↑f)
  31 | frees_bind: ∀f1,f2,f,p,I,L,V,T. frees L V f1 → frees (L.ⓑ{I}V) T f2 →
  32               f1 ⋓ ⫱f2 ≡ f → frees L (ⓑ{p,I}V.T) f
  33 | frees_flat: ∀f1,f2,f,I,L,V,T. frees L V f1 → frees L T f2 →
  34               f1 ⋓ f2 ≡ f → frees L (ⓕ{I}V.T) f
  35 .
  36
  37 interpretation
  38    "context-sensitive free variables (term)"
  39    'FreeStar L T t = (frees L T t).
  40
  41 (* Basic inversion lemmas ***************************************************)
  42
  43 fact frees_inv_atom_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀J. L = ⋆ → X = ⓪{J} → 𝐈⦃f⦄.
  44 #f #L #X #H elim H -f -L -X /3 width=3 by isid_push/
  45 [5,6: #f1 #f2 #f [ #p ] #I #L #V #T #_ #_ #_ #_ #_ #J #_ #H destruct
  46 |*: #f #I #L #V [1,3,4: #x ] #_ #_ #J #H destruct
  47 ]
  48 qed-.
  49
  50 lemma frees_inv_atom: ∀f,I. ⋆ ⊢ 𝐅*⦃⓪{I}⦄ ≡ f → 𝐈⦃f⦄.
  51 /2 width=6 by frees_inv_atom_aux/ qed-.
  52
  53 fact frees_inv_sort_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀x. X = ⋆x → 𝐈⦃f⦄.
  54 #L #X #f #H elim H -f -L -X /3 width=3 by isid_push/
  55 [ #f #_ #L #V #_ #_ #x #H destruct
  56 | #f #_ #L #_ #i #_ #_ #x #H destruct
  57 | #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #_ #_ #x #H destruct
  58 | #f1 #f2 #f #I #L #V #T #_ #_ #_ #_ #_ #x #H destruct
  59 ]
  60 qed-.
  61
  62 lemma frees_inv_sort: ∀f,L,s. L ⊢ 𝐅*⦃⋆s⦄ ≡ f → 𝐈⦃f⦄.
  63 /2 width=5 by frees_inv_sort_aux/ qed-.
  64
  65 fact frees_inv_gref_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀x. X = §x → 𝐈⦃f⦄.
  66 #f #L #X #H elim H -f -L -X /3 width=3 by isid_push/
  67 [ #f #_ #L #V #_ #_ #x #H destruct
  68 | #f #_ #L #_ #i #_ #_ #x #H destruct
  69 | #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #_ #_ #x #H destruct
  70 | #f1 #f2 #f #I #L #V #T #_ #_ #_ #_ #_ #x #H destruct
  71 ]
  72 qed-.
  73
  74 lemma frees_inv_gref: ∀f,L,l. L ⊢ 𝐅*⦃§l⦄ ≡ f → 𝐈⦃f⦄.
  75 /2 width=5 by frees_inv_gref_aux/ qed-.
  76
  77 fact frees_inv_zero_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → X = #0 →
  78                          (L = ⋆ ∧ 𝐈⦃f⦄) ∨
  79                          ∃∃g,I,K,V. K ⊢ 𝐅*⦃V⦄ ≡ g & L = K.ⓑ{I}V & f = ⫯g.
  80 #f #L #X * -f -L -X
  81 [ /3 width=1 by or_introl, conj/
  82 | #f #I #L #V #s #_ #H destruct
  83 | /3 width=7 by ex3_4_intro, or_intror/
  84 | #f #I #L #V #i #_ #H destruct
  85 | #f #I #L #V #l #_ #H destruct
  86 | #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #H destruct
  87 | #f1 #f2 #f #I #L #V #T #_ #_ #_ #H destruct
  88 ]
  89 qed-.
  90
  91 lemma frees_inv_zero: ∀f,L. L ⊢ 𝐅*⦃#0⦄ ≡ f →
  92                       (L = ⋆ ∧ 𝐈⦃f⦄) ∨
  93                       ∃∃g,I,K,V. K ⊢ 𝐅*⦃V⦄ ≡ g & L = K.ⓑ{I}V & f = ⫯g.
  94 /2 width=3 by frees_inv_zero_aux/ qed-.
  95
  96 fact frees_inv_lref_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀j. X = #(⫯j) →
  97                          (L = ⋆ ∧ 𝐈⦃f⦄) ∨
  98                          ∃∃g,I,K,V. K ⊢ 𝐅*⦃#j⦄ ≡ g & L = K.ⓑ{I}V & f = ↑g.
  99 #f #L #X * -f -L -X
 100 [ /3 width=1 by or_introl, conj/
 101 | #f #I #L #V #s #_ #j #H destruct
 102 | #f #I #L #V #_ #j #H destruct
 103 | #f #I #L #V #i #Hf #j #H destruct /3 width=7 by ex3_4_intro, or_intror/
 104 | #f #I #L #V #l #_ #j #H destruct
 105 | #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #j #H destruct
 106 | #f1 #f2 #f #I #L #V #T #_ #_ #_ #j #H destruct
 107 ]
 108 qed-.
 109
 110 lemma frees_inv_lref: ∀f,L,i. L ⊢ 𝐅*⦃#(⫯i)⦄ ≡ f →
 111                       (L = ⋆ ∧ 𝐈⦃f⦄) ∨
 112                       ∃∃g,I,K,V. K ⊢ 𝐅*⦃#i⦄ ≡ g & L = K.ⓑ{I}V & f = ↑g.
 113 /2 width=3 by frees_inv_lref_aux/ qed-.
 114
 115 fact frees_inv_bind_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀p,I,V,T. X = ⓑ{p,I}V.T →
 116                          ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L.ⓑ{I}V ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ ⫱f2 ≡ f.
 117 #f #L #X * -f -L -X
 118 [ #f #I #_ #q #J #W #U #H destruct
 119 | #f #I #L #V #s #_ #q #J #W #U #H destruct
 120 | #f #I #L #V #_ #q #J #W #U #H destruct
 121 | #f #I #L #V #i #_ #q #J #W #U #H destruct
 122 | #f #I #L #V #l #_ #q #J #W #U #H destruct
 123 | #f1 #f2 #f #p #I #L #V #T #HV #HT #Hf #q #J #W #U #H destruct /2 width=5 by ex3_2_intro/
 124 | #f1 #f2 #f #I #L #V #T #_ #_ #_ #q #J #W #U #H destruct
 125 ]
 126 qed-.
 127
 128 lemma frees_inv_bind: ∀f,p,I,L,V,T. L ⊢ 𝐅*⦃ⓑ{p,I}V.T⦄ ≡ f →
 129                       ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L.ⓑ{I}V ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ ⫱f2 ≡ f.
 130 /2 width=4 by frees_inv_bind_aux/ qed-.
 131
 132 fact frees_inv_flat_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,V,T. X = ⓕ{I}V.T →
 133                          ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ f2 ≡ f.
 134 #f #L #X * -f -L -X
 135 [ #f #I #_ #J #W #U #H destruct
 136 | #f #I #L #V #s #_ #J #W #U #H destruct
 137 | #f #I #L #V #_ #J #W #U #H destruct
 138 | #f #I #L #V #i #_ #J #W #U #H destruct
 139 | #f #I #L #V #l #_ #J #W #U #H destruct
 140 | #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #J #W #U #H destruct
 141 | #f1 #f2 #f #I #L #V #T #HV #HT #Hf #J #W #U #H destruct /2 width=5 by ex3_2_intro/
 142 ]
 143 qed-.
 144
 145 lemma frees_inv_flat: ∀f,I,L,V,T. L ⊢ 𝐅*⦃ⓕ{I}V.T⦄ ≡ f →
 146                       ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ f2 ≡ f.
 147 /2 width=4 by frees_inv_flat_aux/ qed-.
 148
 149 (* Advanced inversion lemmas ***********************************************)
 150
 151 lemma frees_inv_zero_pair: ∀f,I,K,V. K.ⓑ{I}V ⊢ 𝐅*⦃#0⦄ ≡ f →
 152                            ∃∃g. K ⊢ 𝐅*⦃V⦄ ≡ g & f = ⫯g.
 153 #f #I #K #V #H elim (frees_inv_zero … H) -H *
 154 [ #H destruct
 155 | #g #Z #Y #X #Hg #H1 #H2 destruct /3 width=3 by ex2_intro/
 156 ]
 157 qed-.
 158
 159 lemma frees_inv_lref_pair: ∀f,I,K,V,i. K.ⓑ{I}V ⊢ 𝐅*⦃#(⫯i)⦄ ≡ f →
 160                            ∃∃g. K ⊢ 𝐅*⦃#i⦄ ≡ g & f = ↑g.
 161 #f #I #K #V #i #H elim (frees_inv_lref … H) -H *
 162 [ #H destruct
 163 | #g #Z #Y #X #Hg #H1 #H2 destruct /3 width=3 by ex2_intro/
 164 ]
 165 qed-.
 166
 167 (* Basic forward lemmas ****************************************************)
 168
 169 lemma frees_fwd_isfin: ∀f,L,T. L ⊢ 𝐅*⦃T⦄ ≡ f → 𝐅⦃f⦄.
 170 #f #L #T #H elim H -f -L -T
 171 /3 width=5 by sor_isfin, isfin_isid, isfin_tl, isfin_push, isfin_next/
 172 qed-.
 173
 174 (* Basic properties ********************************************************)
 175
 176 lemma frees_eq_repl_back: ∀L,T. eq_repl_back … (λf. L ⊢ 𝐅*⦃T⦄ ≡ f).
 177 #L #T #f1 #H elim H -f1 -L -T
 178 [ /3 width=3 by frees_atom, isid_eq_repl_back/
 179 | #f1 #I #L #V #s #_ #IH #f2 #Hf12
 180   elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_sort/
 181 | #f1 #I #L #V #_ #IH #f2 #Hf12
 182   elim (eq_inv_nx … Hf12) -Hf12 /3 width=3 by frees_zero/
 183 | #f1 #I #L #V #i #_ #IH #f2 #Hf12
 184   elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_lref/
 185 | #f1 #I #L #V #l #_ #IH #f2 #Hf12
 186   elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_gref/
 187 | /3 width=7 by frees_bind, sor_eq_repl_back3/
 188 | /3 width=7 by frees_flat, sor_eq_repl_back3/
 189 ]
 190 qed-.
 191
 192 lemma frees_eq_repl_fwd: ∀L,T. eq_repl_fwd … (λf. L ⊢ 𝐅*⦃T⦄ ≡ f).
 193 #L #T @eq_repl_sym /2 width=3 by frees_eq_repl_back/
 194 qed-.
 195
 196 lemma frees_sort_gen: ∀f,L,s. 𝐈⦃f⦄ → L ⊢ 𝐅*⦃⋆s⦄ ≡ f.
 197 #f #L elim L -L
 198 /4 width=3 by frees_eq_repl_back, frees_sort, frees_atom, eq_push_inv_isid/
 199 qed.
 200
 201 lemma frees_gref_gen: ∀f,L,p. 𝐈⦃f⦄ → L ⊢ 𝐅*⦃§p⦄ ≡ f.
 202 #f #L elim L -L
 203 /4 width=3 by frees_eq_repl_back, frees_gref, frees_atom, eq_push_inv_isid/
 204 qed.
 205
 206 (* Basic_2A1: removed theorems 30:
 207               frees_eq frees_be frees_inv
 208               frees_inv_sort frees_inv_gref frees_inv_lref frees_inv_lref_free
 209               frees_inv_lref_skip frees_inv_lref_ge frees_inv_lref_lt
 210               frees_inv_bind frees_inv_flat frees_inv_bind_O
 211               frees_lref_eq frees_lref_be frees_weak
 212               frees_bind_sn frees_bind_dx frees_flat_sn frees_flat_dx
 213               frees_lift_ge frees_inv_lift_be frees_inv_lift_ge
 214               lreq_frees_trans frees_lreq_conf
 215               llor_atom llor_skip llor_total
 216               llor_tail_frees llor_tail_cofrees
 217 *)