matita/matita/contribs/lambdadelta/basic_2/unfold/sstas.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 "basic_2/notation/relations/statictypestar_5.ma".
  16 include "basic_2/static/ssta.ma".
  17
  18 (* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************)
  19
  20 (* Note: includes: stass_refl *)
  21 definition sstas: ∀h. sd h → lenv → relation term ≝
  22                   λh,g,L. star … (ssta_step h g L).
  23
  24 interpretation "iterated stratified static type assignment (term)"
  25    'StaticTypeStar h g L T U = (sstas h g L T U).
  26
  27 (* Basic eliminators ********************************************************)
  28
  29 lemma sstas_ind: ∀h,g,L,T. ∀R:predicate term.
  30                  R T → (
  31                     ∀U1,U2,l. ⦃h, L⦄ ⊢ T •* [g] U1 →  ⦃h, L⦄ ⊢ U1 •[g] ⦃l+1, U2⦄ →
  32                     R U1 → R U2
  33                  ) →
  34                  ∀U. ⦃h, L⦄ ⊢ T •*[g] U → R U.
  35 #h #g #L #T #R #IH1 #IH2 #U #H elim H -U //
  36 #U1 #U2 #H * /2 width=5/
  37 qed-.
  38
  39 lemma sstas_ind_dx: ∀h,g,L,U2. ∀R:predicate term.
  40                     R U2 → (
  41                        ∀T,U1,l. ⦃h, L⦄ ⊢ T •[g] ⦃l+1, U1⦄ → ⦃h, L⦄ ⊢ U1 •* [g] U2 →
  42                        R U1 → R T
  43                     ) →
  44                     ∀T. ⦃h, L⦄ ⊢ T •*[g] U2 → R T.
  45 #h #g #L #U2 #R #IH1 #IH2 #T #H @(star_ind_l … T H) -T //
  46 #T #T0 * /2 width=5/
  47 qed-.
  48
  49 (* Basic properties *********************************************************)
  50
  51 lemma sstas_refl: ∀h,g,L. reflexive … (sstas h g L).
  52 // qed.
  53
  54 lemma ssta_sstas: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l+1, U⦄ → ⦃h, L⦄ ⊢ T •*[g] U.
  55 /3 width=2 by R_to_star, ex_intro/ qed. (**) (* auto fails without trace *)
  56
  57 lemma sstas_strap1: ∀h,g,L,T1,T2,U2,l. ⦃h, L⦄ ⊢ T1 •*[g] T2 → ⦃h, L⦄ ⊢ T2 •[g] ⦃l+1, U2⦄ →
  58                     ⦃h, L⦄ ⊢ T1 •*[g] U2.
  59 /3 width=4 by sstep, ex_intro/ (**) (* auto fails without trace *)
  60 qed.
  61
  62 lemma sstas_strap2: ∀h,g,L,T1,U1,U2,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ⦃h, L⦄ ⊢ U1 •*[g] U2 →
  63                     ⦃h, L⦄ ⊢ T1 •*[g] U2.
  64 /3 width=3 by star_compl, ex_intro/ (**) (* auto fails without trace *)
  65 qed.
  66
  67 (* Basic inversion lemmas ***************************************************)
  68
  69 lemma sstas_inv_bind1: ∀h,g,a,I,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{a,I}Y.X •*[g] U →
  70                        ∃∃Z. ⦃h, L.ⓑ{I}Y⦄ ⊢ X •*[g] Z & U = ⓑ{a,I}Y.Z.
  71 #h #g #a #I #L #Y #X #U #H @(sstas_ind … H) -U /2 width=3/
  72 #T #U #l #_ #HTU * #Z #HXZ #H destruct
  73 elim (ssta_inv_bind1 … HTU) -HTU #Z0 #HZ0 #H destruct /3 width=4/
  74 qed-.
  75
  76 lemma sstas_inv_appl1: ∀h,g,L,Y,X,U. ⦃h, L⦄ ⊢ ⓐY.X •*[g] U →
  77                        ∃∃Z. ⦃h, L⦄ ⊢ X •*[g] Z & U = ⓐY.Z.
  78 #h #g #L #Y #X #U #H @(sstas_ind … H) -U /2 width=3/
  79 #T #U #l #_ #HTU * #Z #HXZ #H destruct
  80 elim (ssta_inv_appl1 … HTU) -HTU #Z0 #HZ0 #H destruct /3 width=4/
  81 qed-.