matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas_sstas.etc

   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/unfold/delift_lift.ma".
  16 include "basic_2/static/ssta_ssta.ma".
  17 include "basic_2/unwind/sstas_lift.ma".
  18
  19 (* ITERATED STRATIFIED STATIC TYPE ASSIGNMENTON TERMS ***********************)
  20
  21 (* Advanced inversion lemmas ************************************************)
  22
  23 lemma sstas_inv_O: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U →
  24                    ∀T0. ⦃h, L⦄ ⊢ T •[g , 0] T0 → U = T.
  25 #h #g #L #T #U #H @(sstas_ind_alt … H) -T //
  26 #T0 #U0 #l0 #HTU0 #_ #_ #T1 #HT01
  27 elim (ssta_mono … HTU0 … HT01) <plus_n_Sm #H destruct
  28 qed-.
  29
  30 lemma sstas_inv_S: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U →
  31                    ∀T0,l. ⦃h, L⦄ ⊢ T •[g , l+1] T0 → ⦃h, L⦄ ⊢ T0 •*[g] U.
  32 #h #g #L #T #U #H @(sstas_ind_alt … H) -T
  33 [ #U0 #HU0 #T #l #HUT
  34   elim (ssta_mono … HUT … HU0) <plus_n_Sm #H destruct
  35 | #T0 #U0 #l0 #HTU0 #HU0 #_ #T #l #HT0
  36   elim (ssta_mono … HT0 … HTU0) -T0 #_ #H destruct -l0 //
  37 ]
  38 qed-.
  39
  40 (* Main properties **********************************************************)
  41
  42 theorem sstas_mono: ∀h,g,L,T,U1. ⦃h, L⦄ ⊢ T •*[g] U1 →
  43                     ∀U2. ⦃h, L⦄ ⊢ T •*[g] U2 → U1 = U2.
  44 #h #g #L #T #U1 #H @(sstas_ind_alt … H) -T
  45 [ #T1 #HUT1 #U2 #HU12
  46   >(sstas_inv_O … HU12 … HUT1) -h -L -T1 -U2 //
  47 | #T0 #U0 #l0 #HTU0 #_ #IHU01 #U2 #HU12
  48   lapply (sstas_inv_S … HU12 … HTU0) -T0 -l0 /2 width=1/
  49 ]
  50 qed-.
  51
  52 (* More advancd inversion lemmas ********************************************)
  53
  54 fact sstas_inv_lref1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → ∀j. T = #j →
  55                           ∃∃I,K,V,W. ⇩[0, j] L ≡ K. ⓑ{I}V & ⦃h, K⦄ ⊢ V •*[g] W &
  56                                      L ⊢ ▼*[0, j + 1] U ≡ W.
  57 #h #g #L #T #U #H @(sstas_ind_alt … H) -T
  58 [ #T #HUT #j #H destruct
  59   elim (ssta_inv_lref1 … HUT) -HUT * #K #V #W [2: #l] #HLK #HVW #HVT
  60   [ <plus_n_Sm #H destruct
  61   | /3 width=12/
  62   ]
  63 | #T0 #U0 #l0 #HTU0 #HU0 #_ #j #H destruct
  64   elim (ssta_inv_lref1 … HTU0) -HTU0 * #K #V #W [2: #l] #HLK #HVW #HVU0
  65   [ #_ -HVW
  66     lapply (ldrop_fwd_ldrop2 … HLK) #H
  67     elim (sstas_inv_lift1 … HU0 … H … HVU0) -HU0 -H -HVU0 /3 width=7/
  68   | elim (sstas_total_S … HVW) -HVW #T #HVT #HWT
  69     lapply (ldrop_fwd_ldrop2 … HLK) #H
  70     elim (sstas_inv_lift1 … HU0 … H … HVU0) -HU0 -H -HVU0 #X #HWX
  71     >(sstas_mono … HWX … HWT) -X -W /3 width=7/
  72   ]
  73 ]
  74 qed-.