matita/matita/contribs/lambdadelta/basic_2/relocation/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/grammar/lenv.ma".
  18
  19 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
  20
  21 inductive frees: relation3 lenv term rtmap ≝
  22 | frees_atom: ∀I,f. 𝐈⦃f⦄ → frees (⋆) (⓪{I}) f
  23 | frees_sort: ∀I,L,V,s,f. frees L (⋆s) f →
  24               frees (L.ⓑ{I}V) (⋆s) (↑f)
  25 | frees_zero: ∀I,L,V,f. frees L V f →
  26               frees (L.ⓑ{I}V) (#0) (⫯f)
  27 | frees_lref: ∀I,L,V,i,f. frees L (#i) f →
  28               frees (L.ⓑ{I}V) (#⫯i) (↑f)
  29 | frees_gref: ∀I,L,V,p,f. frees L (§p) f →
  30               frees (L.ⓑ{I}V) (§p) (↑f)
  31 | frees_bind: ∀I,L,V,T,a,f1,f2,f. frees L V f1 → frees (L.ⓑ{I}V) T f2 →
  32               f1 ⋓ ⫱f2 ≡ f → frees L (ⓑ{a,I}V.T) f
  33 | frees_flat: ∀I,L,V,T,f1,f2,f. 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_sort_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀x. X = ⋆x → 𝐈⦃f⦄.
  44 #L #X #f #H elim H -L -X -f /3 width=3 by isid_push/
  45 [ #_ #L #V #f #_ #_ #x #H destruct
  46 | #_ #L #_ #i #f #_ #_ #x #H destruct
  47 | #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct
  48 | #I #L #V #T #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct
  49 ]
  50 qed-.
  51
  52 lemma frees_inv_sort: ∀L,s,f. L ⊢ 𝐅*⦃⋆s⦄ ≡ f → 𝐈⦃f⦄.
  53 /2 width=5 by frees_inv_sort_aux/ qed-.
  54
  55 fact frees_inv_gref_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀x. X = §x → 𝐈⦃f⦄.
  56 #L #X #f #H elim H -L -X -f /3 width=3 by isid_push/
  57 [ #_ #L #V #f #_ #_ #x #H destruct
  58 | #_ #L #_ #i #f #_ #_ #x #H destruct
  59 | #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct
  60 | #I #L #V #T #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct
  61 ]
  62 qed-.
  63
  64 lemma frees_inv_gref: ∀L,p,f. L ⊢ 𝐅*⦃§p⦄ ≡ f → 𝐈⦃f⦄.
  65 /2 width=5 by frees_inv_gref_aux/ qed-.
  66
  67 fact frees_inv_zero_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → X = #0 →
  68                          (L = ⋆ ∧ 𝐈⦃f⦄) ∨
  69                          ∃∃I,K,V,g. K ⊢ 𝐅*⦃V⦄ ≡ g & L = K.ⓑ{I}V & f = ⫯g.
  70 #L #X #f * -L -X -f
  71 [ /3 width=1 by or_introl, conj/
  72 | #I #L #V #s #f #_ #H destruct
  73 | /3 width=7 by ex3_4_intro, or_intror/
  74 | #I #L #V #i #f #_ #H destruct
  75 | #I #L #V #p #f #_ #H destruct
  76 | #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #H destruct
  77 | #I #L #V #T #f1 #f2 #f #_ #_ #_ #H destruct
  78 ]
  79 qed-.
  80
  81 lemma frees_inv_zero: ∀L,f. L ⊢ 𝐅*⦃#0⦄ ≡ f →
  82                       (L = ⋆ ∧ 𝐈⦃f⦄) ∨
  83                       ∃∃I,K,V,g. K ⊢ 𝐅*⦃V⦄ ≡ g & L = K.ⓑ{I}V & f = ⫯g.
  84 /2 width=3 by frees_inv_zero_aux/ qed-.
  85
  86 fact frees_inv_lref_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀j. X = #(⫯j) →
  87                          (L = ⋆ ∧ 𝐈⦃f⦄) ∨
  88                          ∃∃I,K,V,g. K ⊢ 𝐅*⦃#j⦄ ≡ g & L = K.ⓑ{I}V & f = ↑g.
  89 #L #X #f * -L -X -f
  90 [ /3 width=1 by or_introl, conj/
  91 | #I #L #V #s #f #_ #j #H destruct
  92 | #I #L #V #f #_ #j #H destruct
  93 | #I #L #V #i #f #Ht #j #H destruct /3 width=7 by ex3_4_intro, or_intror/
  94 | #I #L #V #p #f #_ #j #H destruct
  95 | #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #j #H destruct
  96 | #I #L #V #T #f1 #f2 #f #_ #_ #_ #j #H destruct
  97 ]
  98 qed-.
  99
 100 lemma frees_inv_lref: ∀L,i,f. L ⊢ 𝐅*⦃#(⫯i)⦄ ≡ f →
 101                       (L = ⋆ ∧ 𝐈⦃f⦄) ∨
 102                       ∃∃I,K,V,g. K ⊢ 𝐅*⦃#i⦄ ≡ g & L = K.ⓑ{I}V & f = ↑g.
 103 /2 width=3 by frees_inv_lref_aux/ qed-.
 104
 105 fact frees_inv_bind_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,V,T,a. X = ⓑ{a,I}V.T →
 106                          ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L.ⓑ{I}V ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ ⫱f2 ≡ f.
 107 #L #X #f * -L -X -f
 108 [ #I #f #_ #J #W #U #b #H destruct
 109 | #I #L #V #s #f #_ #J #W #U #b #H destruct
 110 | #I #L #V #f #_ #J #W #U #b #H destruct
 111 | #I #L #V #i #f #_ #J #W #U #b #H destruct
 112 | #I #L #V #p #f #_ #J #W #U #b #H destruct
 113 | #I #L #V #T #a #f1 #f2 #f #HV #HT #Hf #J #W #U #b #H destruct /2 width=5 by ex3_2_intro/
 114 | #I #L #V #T #f1 #f2 #f #_ #_ #_ #J #W #U #b #H destruct
 115 ]
 116 qed-.
 117
 118 lemma frees_inv_bind: ∀I,L,V,T,a,f. L ⊢ 𝐅*⦃ⓑ{a,I}V.T⦄ ≡ f →
 119                       ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L.ⓑ{I}V ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ ⫱f2 ≡ f.
 120 /2 width=4 by frees_inv_bind_aux/ qed-.
 121
 122 fact frees_inv_flat_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,V,T. X = ⓕ{I}V.T →
 123                          ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ f2 ≡ f.
 124 #L #X #f * -L -X -f
 125 [ #I #f #_ #J #W #U #H destruct
 126 | #I #L #V #s #f #_ #J #W #U #H destruct
 127 | #I #L #V #f #_ #J #W #U #H destruct
 128 | #I #L #V #i #f #_ #J #W #U #H destruct
 129 | #I #L #V #p #f #_ #J #W #U #H destruct
 130 | #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #J #W #U #H destruct
 131 | #I #L #V #T #f1 #f2 #f #HV #HT #Hf #J #W #U #H destruct /2 width=5 by ex3_2_intro/
 132 ]
 133 qed-.
 134
 135 lemma frees_inv_flat: ∀I,L,V,T,f. L ⊢ 𝐅*⦃ⓕ{I}V.T⦄ ≡ f →
 136                       ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ f2 ≡ f.
 137 /2 width=4 by frees_inv_flat_aux/ qed-.
 138
 139 (* Basic properties ********************************************************)
 140
 141 lemma frees_eq_repl_back: ∀L,T. eq_repl_back … (λf. L ⊢ 𝐅*⦃T⦄ ≡ f).
 142 #L #T #f1 #H elim H -L -T -f1
 143 [ /3 width=3 by frees_atom, isid_eq_repl_back/
 144 | #I #L #V #s #f1 #_ #IH #f2 #Hf12
 145   elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_sort/
 146 | #I #L #V #f1 #_ #IH #f2 #Hf12
 147   elim (eq_inv_nx … Hf12) -Hf12 /3 width=3 by frees_zero/
 148 | #I #L #V #i #f1 #_ #IH #f2 #Hf12
 149   elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_lref/
 150 | #I #L #V #p #f1 #_ #IH #f2 #Hf12
 151   elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_gref/
 152 | /3 width=7 by frees_bind, sor_eq_repl_back3/
 153 | /3 width=7 by frees_flat, sor_eq_repl_back3/
 154 ]
 155 qed-.
 156
 157 lemma frees_eq_repl_fwd: ∀L,T. eq_repl_fwd … (λf. L ⊢ 𝐅*⦃T⦄ ≡ f).
 158 #L #T @eq_repl_sym /2 width=3 by frees_eq_repl_back/
 159 qed-.
 160
 161 lemma frees_sort_gen: ∀L,s,f. 𝐈⦃f⦄ → L ⊢ 𝐅*⦃⋆s⦄ ≡ f.
 162 #L elim L -L
 163 /4 width=3 by frees_eq_repl_back, frees_sort, frees_atom, eq_push_inv_isid/
 164 qed.
 165
 166 lemma frees_gref_gen: ∀L,p,f. 𝐈⦃f⦄ → L ⊢ 𝐅*⦃§p⦄ ≡ f.
 167 #L elim L -L
 168 /4 width=3 by frees_eq_repl_back, frees_gref, frees_atom, eq_push_inv_isid/
 169 qed.