matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_scpes.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/computation/scpds_scpds.ma".
  16 include "basic_2/equivalence/scpes.ma".
  17
  18 (* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************)
  19
  20 (* Advanced inversion lemmas ************************************************)
  21
  22 lemma scpes_inv_abst2: ∀h,g,a,G,L,T1,T2,W2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] ⓛ{a}W2.T2 →
  23                        ∃∃W,T. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l1] ⓛ{a}W.T & ⦃G, L⦄ ⊢ W2 ➡* W &
  24                               ⦃G, L.ⓛW2⦄ ⊢ T2 •*➡*[h, g, l2] T.
  25 #h #g #a #G #L #T1 #T2 #W2 #l1 #l2 * #T0 #HT10 #H
  26 elim (scpds_inv_abst1 … H) -H #W #T #HW2 #HT2 #H destruct /2 width=5 by ex3_2_intro/
  27 qed-.
  28
  29 (* Advanced properties ******************************************************)
  30
  31 lemma scpes_refl: ∀h,g,G,L,T,l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T ▪[h, g] l1 →
  32                   ⦃G, L⦄ ⊢ T •*⬌*[h, g, l2, l2] T.
  33 #h #g #G #L #T #l1 #l2 #Hl21 #Hl1
  34 elim (da_inv_sta … Hl1) #U #HTU
  35 elim (lstas_total … HTU l2) -U /3 width=3 by scpds_div, lstas_scpds/
  36 qed.
  37
  38 lemma lstas_scpes_trans: ∀h,g,G,L,T1,l0,l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l0 → l1 ≤ l0 →
  39                          ∀T. ⦃G, L⦄ ⊢ T1 •*[h, l1] T →
  40                          ∀T2,l,l2. ⦃G, L⦄ ⊢ T •*⬌*[h,g,l,l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h,g,l1+l,l2] T2.
  41 #h #g #G #L #T1 #l0 #l1 #Hl0 #Hl10 #T #HT1 #T2 #l #l2 *
  42 /3 width=3 by scpds_div, lstas_scpds_trans/ qed-.
  43
  44 (* Main properties **********************************************************)
  45
  46 theorem scpes_trans: ∀h,g,G,L,T1,T,l1,l. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l] T →
  47                      ∀T2,l2. ⦃G, L⦄ ⊢ T •*⬌*[h, g, l, l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2.
  48 #h #g #G #L #T1 #T #l1 #l * #X1 #HT1X1 #HTX1 #T2 #l2 * #X2 #HTX2 #HT2X2
  49 elim (scpds_conf_eq … HTX1 … HTX2) -T -l /3 width=5 by scpds_cprs_trans, scpds_div/
  50 qed-.
  51
  52 theorem scpes_canc_sn: ∀h,g,G,L,T,T1,l,l1. ⦃G, L⦄ ⊢ T •*⬌*[h, g, l, l1] T1 →
  53                        ∀T2,l2. ⦃G, L⦄ ⊢ T •*⬌*[h, g, l, l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2.
  54 #h #g #G #L #T #T1 #l #l1 #HT1
  55 @scpes_trans /2 width=1 by scpes_sym/ (**) (* full auto raises NTypeChecker failure *)
  56 qed-.
  57
  58 theorem scpes_canc_dx: ∀h,g,G,L,T1,T,l1,l. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l] T →
  59                        ∀T2,l2. ⦃G, L⦄ ⊢ T2 •*⬌*[h, g, l2, l] T → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2.
  60 #h #g #G #L #T1 #T #l1 #l #HT1 #T2 #l2 #HT2
  61 @(scpes_trans … HT1) -T1 -l1 /2 width=1 by scpes_sym/ (**) (* full auto raises NTypeChecker failure *)
  62 qed-.