matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.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_pushs.ma".
  16 include "ground_2/relocation/rtmap_coafter.ma".
  17 include "basic_2/relocation/lifts_lifts.ma".
  18 include "basic_2/relocation/drops.ma".
  19 include "basic_2/static/frees.ma".
  20
  21 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
  22
  23 (* Advanced properties ******************************************************)
  24
  25 lemma frees_lref_atom: ∀L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ → L ⊢ 𝐅*⦃#i⦄ ≡ 𝐈𝐝.
  26 #L elim L -L /2 width=1 by frees_atom/
  27 #L #I #V #IH *
  28 [ #H lapply (drops_fwd_isid … H ?) -H // #H destruct
  29 | /4 width=3 by frees_lref, drops_inv_drop1/
  30 ]
  31 qed.
  32
  33 lemma frees_lref_pair: ∀f,K,V. K ⊢ 𝐅*⦃V⦄ ≡ f →
  34                        ∀i,I,L. ⬇*[i] L ≡ K.ⓑ{I}V → L ⊢ 𝐅*⦃#i⦄ ≡ ↑*[i] ⫯f.
  35 #f #K #V #Hf #i elim i -i
  36 [ #I #L #H lapply (drops_fwd_isid … H ?) -H /2 width=1 by frees_zero/
  37 | #i #IH #I #L #H elim (drops_inv_succ … H) -H /3 width=2 by frees_lref/
  38 ]
  39 qed.
  40
  41 (* Advanced inversion lemmas ************************************************)
  42
  43 lemma frees_inv_lref_drops: ∀i,f,L. L ⊢ 𝐅*⦃#i⦄ ≡ f →
  44                             (⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ ∧ 𝐈⦃f⦄) ∨
  45                             ∃∃g,I,K,V. K ⊢ 𝐅*⦃V⦄ ≡ g &
  46                                        ⬇*[i] L ≡ K.ⓑ{I}V & f = ↑*[i] ⫯g.
  47 #i elim i -i
  48 [ #f #L #H elim (frees_inv_zero … H) -H *
  49   /4 width=7 by ex3_4_intro, or_introl, or_intror, conj, drops_refl/
  50 | #i #IH #f #L #H elim (frees_inv_lref … H) -H * /3 width=1 by or_introl, conj/
  51   #g #I #K #V #Hg #H1 #H2 destruct
  52   elim (IH … Hg) -IH -Hg *
  53   [ /4 width=3 by or_introl, conj, isid_push, drops_drop/
  54   | /4 width=7 by drops_drop, ex3_4_intro, or_intror/
  55   ]
  56 ]
  57 qed-.
  58
  59 (* Properties with generic slicing for local environments *******************)
  60
  61 (* Inversion lemmas with generic slicing for local environments *************)
  62
  63 lemma frees_inv_lifts: ∀b,f2,L,U. L ⊢ 𝐅*⦃U⦄ ≡ f2 →
  64                        ∀f,K. ⬇*[b, f] L ≡ K → ∀T. ⬆*[f] T ≡ U →
  65                        ∀f1. f ~⊚ f1 ≡ f2 → K ⊢ 𝐅*⦃T⦄ ≡ f1.
  66 #b #f2 #L #U #H lapply (frees_fwd_isfin … H) elim H -f2 -L -U
  67 [ #f2 #I #Hf2 #_ #f #K #H1 #T #H2 #f1 #H3
  68   lapply (coafter_fwd_isid2 … H3 … Hf2) -H3 // -Hf2 #Hf1
  69   elim (drops_inv_atom1 … H1) -H1 #H #_ destruct
  70   elim (lifts_fwd_atom2 … H2) -H2
  71   /2 width=3 by frees_atom/
  72 | #f2 #I #L #W #s #_ #IH #Hf2 #f #Y #H1 #T #H2 #f1 #H3
  73   lapply (isfin_fwd_push … Hf2 ??) -Hf2 [3: |*: // ] #Hf2
  74   lapply (lifts_inv_sort2 … H2) -H2 #H destruct
  75   elim (coafter_inv_xxp … H3) -H3 [1,3: * |*: // ]
  76   [ #g #g1 #Hf2 #H #H0 destruct
  77     elim (drops_inv_skip1 … H1) -H1 #K #V #HLK #_ #H destruct
  78   | #g #Hf2 #H destruct
  79     lapply (drops_inv_drop1 … H1) -H1
  80   ] /3 width=4 by frees_sort/
  81 | #f2 #I #L #W #_ #IH #Hf2 #f #Y #H1 #T #H2 #f1 #H3
  82   lapply (isfin_inv_next … Hf2 ??) -Hf2 [3: |*: // ] #Hf2
  83   elim (lifts_inv_lref2 … H2) -H2 #i #H2 #H destruct
  84   lapply (at_inv_xxp … H2 ?) -H2 // * #g #H #H0 destruct
  85   elim (drops_inv_skip1 … H1) -H1 #K #V #HLK #HVW #H destruct
  86   elim (coafter_inv_pxn … H3) -H3 [ |*: // ] #g1 #Hf2 #H destruct
  87   /3 width=4 by frees_zero/
  88 | #f2 #I #L #W #j #_ #IH #Hf2 #f #Y #H1 #T #H2 #f1 #H3
  89   lapply (isfin_fwd_push … Hf2 ??) -Hf2 [3: |*: // ] #Hf2
  90   elim (lifts_inv_lref2 … H2) -H2 #x #H2 #H destruct
  91   elim (coafter_inv_xxp … H3) -H3 [1,3: * |*: // ]
  92   [ #g #g1 #Hf2 #H #H0 destruct
  93     elim (drops_inv_skip1 … H1) -H1 #K #V #HLK #HVW #H destruct
  94     elim (at_inv_xpn … H2) -H2 [ |*: // ] #j #Hg #H destruct
  95   | #g #Hf2 #H destruct
  96     lapply (drops_inv_drop1 … H1) -H1
  97     lapply (at_inv_xnn … H2 ????) -H2 [5: |*: // ]
  98   ] /4 width=4 by lifts_lref, frees_lref/
  99 | #f2 #I #L #W #l #_ #IH #Hf2 #f #Y #H1 #T #H2 #f1 #H3
 100   lapply (isfin_fwd_push … Hf2 ??) -Hf2 [3: |*: // ] #Hf2
 101   lapply (lifts_inv_gref2 … H2) -H2 #H destruct
 102   elim (coafter_inv_xxp … H3) -H3 [1,3: * |*: // ]
 103   [ #g #g1 #Hf2 #H #H0 destruct
 104     elim (drops_inv_skip1 … H1) -H1 #K #V #HLK #_ #H destruct
 105   | #g #Hf2 #H destruct
 106     lapply (drops_inv_drop1 … H1) -H1
 107   ] /3 width=4 by frees_gref/
 108 | #f2W #f2U #f2 #p #I #L #W #U #_ #_ #H1f2 #IHW #IHU #H2f2 #f #K #H1 #X #H2 #f1 #H3
 109   elim (sor_inv_isfin3 … H1f2) // #H1f2W #H
 110   lapply (isfin_inv_tl … H) -H
 111   elim (lifts_inv_bind2 … H2) -H2 #V #T #HVW #HTU #H destruct
 112   elim (coafter_inv_sor … H3 … H1f2) -H3 -H1f2 // #f1W #f1U #H2f2W #H
 113   elim (coafter_inv_tl0 … H) -H /4 width=5 by frees_bind, drops_skip/
 114 | #f2W #f2U #f2 #I #L #W #U #_ #_ #H1f2 #IHW #IHU #H2f2 #f #K #H1 #X #H2 #f1 #H3
 115   elim (sor_inv_isfin3 … H1f2) //
 116   elim (lifts_inv_flat2 … H2) -H2 #V #T #HVW #HTU #H destruct
 117   elim (coafter_inv_sor … H3 … H1f2) -H3 -H1f2 /3 width=5 by frees_flat/
 118 ]
 119 qed-.