matita/matita/contribs/lambdadelta/basic_2A/computation/csx_alt.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_2A/notation/relations/snalt_5.ma".
  16 include "basic_2A/computation/cpxs.ma".
  17 include "basic_2A/computation/csx.ma".
  18
  19 (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
  20
  21 (* alternative definition of csx *)
  22 definition csxa: ∀h. sd h → relation3 genv lenv term ≝
  23                  λh,g,G,L. SN … (cpxs h g G L) (eq …).
  24
  25 interpretation
  26    "context-sensitive extended strong normalization (term) alternative"
  27    'SNAlt h g G L T = (csxa h g G L T).
  28
  29 (* Basic eliminators ********************************************************)
  30
  31 lemma csxa_ind: ∀h,g,G,L. ∀R:predicate term.
  32                 (∀T1. ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T1 →
  33                       (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → R T2) → R T1
  34                 ) →
  35                 ∀T. ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T → R T.
  36 #h #g #G #L #R #H0 #T1 #H elim H -T1 /5 width=1 by SN_intro/
  37 qed-.
  38
  39 (* Basic properties *********************************************************)
  40
  41 lemma csx_intro_cpxs: ∀h,g,G,L,T1.
  42                          (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] T2) →
  43                       ⦃G, L⦄ ⊢ ⬊*[h, g] T1.
  44 /4 width=1 by cpx_cpxs, csx_intro/ qed.
  45
  46 (* Basic_1: was just: sn3_intro *)
  47 lemma csxa_intro: ∀h,g,G,L,T1.
  48                   (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T2) →
  49                   ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T1.
  50 /4 width=1 by SN_intro/ qed.
  51
  52 fact csxa_intro_aux: ∀h,g,G,L,T1. (
  53                         ∀T,T2. ⦃G, L⦄ ⊢ T ➡*[h, g] T2 → T1 = T → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T2
  54                      ) → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T1.
  55 /4 width=3 by csxa_intro/ qed-.
  56
  57 (* Basic_1: was just: sn3_pr3_trans (old version) *)
  58 lemma csxa_cpxs_trans: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T1 →
  59                        ∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T2.
  60 #h #g #G #L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12
  61 @csxa_intro #T #HLT2 #HT2
  62 elim (eq_term_dec T1 T2) #HT12
  63 [ -IHT1 -HLT12 destruct /3 width=1 by/
  64 | -HT1 -HT2 /3 width=4 by/
  65 qed.
  66
  67 (* Basic_1: was just: sn3_pr2_intro (old version) *)
  68 lemma csxa_intro_cpx: ∀h,g,G,L,T1. (
  69                          ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T2
  70                       ) → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T1.
  71 #h #g #G #L #T1 #H
  72 @csxa_intro_aux #T #T2 #H @(cpxs_ind_dx … H) -T
  73 [ -H #H destruct #H
  74   elim H //
  75 | #T0 #T #HLT1 #HLT2 #IHT #HT10 #HT12 destruct
  76   elim (eq_term_dec T0 T) #HT0
  77   [ -HLT1 -HLT2 -H /3 width=1 by/
  78   | -IHT -HT12 /4 width=3 by csxa_cpxs_trans/
  79   ]
  80 ]
  81 qed.
  82
  83 (* Main properties **********************************************************)
  84
  85 theorem csx_csxa: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T.
  86 #h #g #G #L #T #H @(csx_ind … H) -T /4 width=1 by csxa_intro_cpx/
  87 qed.
  88
  89 theorem csxa_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
  90 #h #g #G #L #T #H @(csxa_ind … H) -T /4 width=1 by cpx_cpxs, csx_intro/
  91 qed.
  92
  93 (* Basic_1: was just: sn3_pr3_trans *)
  94 lemma csx_cpxs_trans: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 →
  95                       ∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ ⬊*[h, g] T2.
  96 #h #g #G #L #T1 #HT1 #T2 #H @(cpxs_ind … H) -T2 /2 width=3 by csx_cpx_trans/
  97 qed-.
  98
  99 (* Main eliminators *********************************************************)
 100
 101 lemma csx_ind_alt: ∀h,g,G,L. ∀R:predicate term.
 102                    (∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 →
 103                          (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → R T2) → R T1
 104                    ) →
 105                    ∀T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R T.
 106 #h #g #G #L #R #H0 #T1 #H @(csxa_ind … (csx_csxa … H)) -T1 /4 width=1 by csxa_csx/
 107 qed-.