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