matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_etc.ma

   1 (*
   2 (* Advanced inversion lemmas ************************************************)
   3
   4
   5 (* Basic_1: was ty3_gen_lref *)
   6 lemma nta_inv_lref1: ∀h,L,U,i. ⦃h, L⦄ ⊢ #i : U →
   7                      (∃∃K,V,W,U0. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W &
   8                                   ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
   9                      ) ∨
  10                      (∃∃K,W,V,U0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V &
  11                                   ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
  12                      ).
  13 /2 width=3/ qed-.
  14
  15 (* Advanced forvard lemmas **************************************************)
  16
  17 lemma nta_fwd_pure1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓐY.X : U →
  18                      ∃∃V,W. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V & L ⊢ ⓐY.V ⬌* U.
  19 /2 width=3/ qed-.
  20
  21 lemma nta_ind_alt: ∀h. ∀R:lenv→relation term.
  22    (∀L,k. R L ⋆k ⋆(next h k)) →
  23    (∀L,K,V,W,U,i.
  24       ⇩[O, i] L ≡ K.ⓓV → ⦃h, K⦄ ⊢ V : W → ⇧[O, i + 1] W ≡ U →
  25       R K V W → R L (#i) U
  26    ) →
  27    (∀L,K,W,V,U,i.
  28       ⇩[O, i] L ≡ K.ⓛW → ⦃h, K⦄ ⊢ W : V → ⇧[O, i + 1] W ≡ U →
  29       R K W V → R L (#i) U
  30    ) →
  31    (∀I,L,V,W,T,U.
  32       ⦃h, L⦄ ⊢ V : W → ⦃h, L.ⓑ{I}V⦄ ⊢ T : U →
  33       R L V W → R (L.ⓑ{I}V) T U → R L (ⓑ{I}V.T) (ⓑ{I}V.U)
  34    ) →
  35    (∀L,V,W,T,U.
  36       ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ (ⓛW.T):(ⓛW.U) →
  37       R L V W →R L (ⓛW.T) (ⓛW.U) →R L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U)
  38    ) →
  39    (∀L,V,W,T,U.
  40       ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ (ⓐV.U) : W →
  41       R L T U → R L (ⓐV.U) W → R L (ⓐV.T) (ⓐV.U)
  42    ) →
  43    (∀L,T,U,W.
  44       ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W →
  45       R L T U → R L U W → R L (ⓝU.T) U
  46    ) →
  47    (∀L,T,U1,U2,V2.
  48       ⦃h, L⦄ ⊢ T : U1 → L ⊢ U1 ⬌* U2 → ⦃h, L⦄ ⊢ U2 : V2 →
  49       R L T U1 →R L U2 V2 →R L T U2
  50    ) →
  51    ∀L,T,U. ⦃h, L⦄ ⊢ T : U → R L T U.
  52 #h #R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #L #T #U #H elim (nta_ntaa … H) -L -T -U
  53 // /3 width=1 by ntaa_nta/ /3 width=3 by ntaa_nta/ /3 width=4 by ntaa_nta/
  54 /3 width=7 by ntaa_nta/
  55 qed-.
  56
  57 *)