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/trace_sor.ma".
  16 include "ground_2/relocation/trace_isun.ma".
  17 include "basic_2/notation/relations/freestar_3.ma".
  18 include "basic_2/grammar/lenv.ma".
  19
  20 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
  21
  22 inductive frees: relation3 lenv term trace ≝
  23 | frees_atom: ∀I. frees (⋆) (⓪{I}) (◊)
  24 | frees_sort: ∀I,L,V,s,t. frees L (⋆s) t →
  25               frees (L.ⓑ{I}V) (⋆s) (Ⓕ @ t)
  26 | frees_zero: ∀I,L,V,t. frees L V t →
  27               frees (L.ⓑ{I}V) (#0) (Ⓣ @ t)
  28 | frees_lref: ∀I,L,V,i,t. frees L (#i) t →
  29               frees (L.ⓑ{I}V) (#⫯i) (Ⓕ @ t)
  30 | frees_gref: ∀I,L,V,p,t. frees L (§p) t →
  31               frees (L.ⓑ{I}V) (§p) (Ⓕ @ t)
  32 | frees_bind: ∀I,L,V,T,t1,t2,t,b,a. frees L V t1 → frees (L.ⓑ{I}V) T (b @ t2) →
  33               t1 ⋓ t2 ≡ t → frees L (ⓑ{a,I}V.T) t
  34 | frees_flat: ∀I,L,V,T,t1,t2,t. frees L V t1 → frees L T t2 →
  35               t1 ⋓ t2 ≡ t → frees L (ⓕ{I}V.T) t
  36 .
  37
  38 interpretation
  39    "context-sensitive free variables (term)"
  40    'FreeStar L T t = (frees L T t).
  41
  42 (* Basic forward lemmas *****************************************************)
  43
  44 fact frees_fwd_sort_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → ∀x. X = ⋆x → 𝐔⦃t⦄.
  45 #L #X #t #H elim H -L -X -t /3 width=2 by isun_id, isun_false/
  46 [ #_ #L #V #t #_ #_ #x #H destruct
  47 | #_ #L #_ #i #t #_ #_ #x #H destruct
  48 | #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #_ #_ #x #H destruct
  49 | #I #L #V #T #t1 #t2 #t #_ #_ #_ #_ #_ #x #H destruct
  50 ]
  51 qed-.
  52
  53 lemma frees_fwd_sort: ∀L,t,s. L ⊢ 𝐅*⦃⋆s⦄ ≡ t → 𝐔⦃t⦄.
  54 /2 width=5 by frees_fwd_sort_aux/ qed-.
  55
  56 fact frees_fwd_gref_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → ∀x. X = §x → 𝐔⦃t⦄.
  57 #L #X #t #H elim H -L -X -t /3 width=2 by isun_id, isun_false/
  58 [ #_ #L #V #t #_ #_ #x #H destruct
  59 | #_ #L #_ #i #t #_ #_ #x #H destruct
  60 | #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #_ #_ #x #H destruct
  61 | #I #L #V #T #t1 #t2 #t #_ #_ #_ #_ #_ #x #H destruct
  62 ]
  63 qed-.
  64
  65 lemma frees_fwd_gref: ∀L,t,p. L ⊢ 𝐅*⦃§p⦄ ≡ t → 𝐔⦃t⦄.
  66 /2 width=5 by frees_fwd_gref_aux/ qed-.
  67
  68 (* Basic inversion lemmas ***************************************************)
  69
  70 fact frees_inv_zero_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → X = #0 →
  71                          (L = ⋆ ∧ t = ◊) ∨
  72                          ∃∃I,K,V,u. K ⊢ 𝐅*⦃V⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓣ@u.
  73 #L #X #t * -L -X -t
  74 [ /3 width=1 by or_introl, conj/
  75 | #I #L #V #s #t #_ #H destruct
  76 | /3 width=7 by ex3_4_intro, or_intror/
  77 | #I #L #V #i #t #_ #H destruct
  78 | #I #L #V #p #t #_ #H destruct
  79 | #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #H destruct
  80 | #I #L #V #T #t1 #t2 #t #_ #_ #_ #H destruct
  81 ]
  82 qed-.
  83
  84 lemma frees_inv_zero: ∀L,t. L ⊢ 𝐅*⦃#0⦄ ≡ t →
  85                       (L = ⋆ ∧ t = ◊) ∨
  86                       ∃∃I,K,V,u. K ⊢ 𝐅*⦃V⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓣ@u.
  87 /2 width=3 by frees_inv_zero_aux/ qed-.
  88
  89 fact frees_inv_lref_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → ∀j. X = #(⫯j) →
  90                          (L = ⋆ ∧ t = ◊) ∨
  91                          ∃∃I,K,V,u. K ⊢ 𝐅*⦃#j⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓕ@u.
  92 #L #X #t * -L -X -t
  93 [ /3 width=1 by or_introl, conj/
  94 | #I #L #V #s #t #_ #j #H destruct
  95 | #I #L #V #t #_ #j #H destruct
  96 | #I #L #V #i #t #Ht #j #H destruct /3 width=7 by ex3_4_intro, or_intror/
  97 | #I #L #V #p #t #_ #j #H destruct
  98 | #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #j #H destruct
  99 | #I #L #V #T #t1 #t2 #t #_ #_ #_ #j #H destruct
 100 ]
 101 qed-.
 102
 103 lemma frees_inv_lref: ∀L,i,t. L ⊢ 𝐅*⦃#(⫯i)⦄ ≡ t →
 104                       (L = ⋆ ∧ t = ◊) ∨
 105                       ∃∃I,K,V,u. K ⊢ 𝐅*⦃#i⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓕ@u.
 106 /2 width=3 by frees_inv_lref_aux/ qed-.