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