matita/matita/contribs/lambdadelta/basic_2/etc/lstas/lstas_cpxs.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 (* Advanced properties ******************************************************)
  16
  17 lemma lstas_cpxs: ∀h,o,G,L,T1,T2,d2. ⦃G, L⦄ ⊢ T1 •*[h, d2] T2 →
  18                   ∀d1. ⦃G, L⦄ ⊢ T1 ▪[h, o] d1 → d2 ≤ d1 → ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2.
  19 #h #o #G #L #T1 #T2 #d2 #H elim H -G -L -T1 -T2 -d2 //
  20 [ /3 width=3 by cpxs_sort, da_inv_sort/
  21 | #G #L #K #V1 #V2 #W2 #i #d2 #HLK #_ #HVW2 #IHV12 #d1 #H #Hd21
  22   elim (da_inv_lref … H) -H * #K0 #V0 [| #d0 ] #HLK0
  23   lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct /3 width=7 by cpxs_delta/
  24 | #G #L #K #V1 #V2 #W2 #i #d2 #HLK #_ #HVW2 #IHV12 #d1 #H #Hd21
  25   elim (da_inv_lref … H) -H * #K0 #V0 [| #d0 ] #HLK0
  26   lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct
  27   #HV1 #H destruct lapply (le_plus_to_le_c … Hd21) -Hd21
  28   /3 width=7 by cpxs_delta/
  29 | /4 width=3 by cpxs_bind_dx, da_inv_bind/
  30 | /4 width=3 by cpxs_flat_dx, da_inv_flat/
  31 | /4 width=3 by cpxs_eps, da_inv_flat/
  32 ]
  33 qed.
  34
  35 lemma fquq_lstas_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
  36                         ∀U2,d1. ⦃G2, L2⦄ ⊢ T2 •*[h, d1] U2 →
  37                         ∀d2. ⦃G2, L2⦄ ⊢ T2 ▪[h, o] d2 → d1 ≤ d2 →
  38                         ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
  39 /3 width=5 by fquq_cpxs_trans, lstas_cpxs/ qed-.
  40
  41 lemma fqus_lstas_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
  42                         ∀U2,d1. ⦃G2, L2⦄ ⊢ T2 •*[h, d1] U2 →
  43                         ∀d2. ⦃G2, L2⦄ ⊢ T2 ▪[h, o] d2 → d1 ≤ d2 →
  44                         ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄.
  45 /3 width=6 by fqus_cpxs_trans, lstas_cpxs/ qed-.