matita/matita/contribs/lambdadelta/basic_2/computation/csn_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_2/computation/cpxs.ma".
  16 include "basic_2/computation/csn.ma".
  17
  18 (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
  19
  20 (* alternative definition of csn *)
  21 definition csna: ∀h. sd h → lenv → predicate term ≝
  22                  λh,g,L. SN … (cpxs h g L) (eq …).
  23
  24 interpretation
  25    "context-sensitive extended strong normalization (term) alternative"
  26    'SNAlt h g L T = (csna h g L T).
  27
  28 (* Basic eliminators ********************************************************)
  29
  30 lemma csna_ind: ∀h,g,L. ∀R:predicate term.
  31                 (∀T1. ⦃h, L⦄ ⊢ ⬊⬊*[g] T1 →
  32                       (∀T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → (T1 = T2 → ⊥) → R T2) → R T1
  33                 ) →
  34                 ∀T. ⦃h, L⦄ ⊢ ⬊⬊*[g] T → R T.
  35 #h #g #L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1
  36 @H0 -H0 /3 width=1/ -IHT1 /4 width=1/
  37 qed-.
  38
  39 (* Basic properties *********************************************************)
  40
  41 (* Basic_1: was just: sn3_intro *)
  42 lemma csna_intro: ∀h,g,L,T1.
  43                   (∀T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → (T1 = T2 → ⊥) → ⦃h, L⦄ ⊢ ⬊⬊*[g] T2) →
  44                   ⦃h, L⦄ ⊢ ⬊⬊*[g] T1.
  45 /4 width=1/ qed.
  46
  47 fact csna_intro_aux: ∀h,g,L,T1. (
  48                         ∀T,T2. ⦃h, L⦄ ⊢ T ➡*[g] T2 → T1 = T → (T1 = T2 → ⊥) → ⦃h, L⦄ ⊢ ⬊⬊*[g] T2
  49                      ) → ⦃h, L⦄ ⊢ ⬊⬊*[g] T1.
  50 /4 width=3/ qed-.
  51
  52 (* Basic_1: was just: sn3_pr3_trans (old version) *)
  53 lemma csna_cpxs_trans: ∀h,g,L,T1. ⦃h, L⦄ ⊢ ⬊⬊*[g] T1 →
  54                        ∀T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ ⬊⬊*[g] T2.
  55 #h #g #L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12
  56 @csna_intro #T #HLT2 #HT2
  57 elim (term_eq_dec T1 T2) #HT12
  58 [ -IHT1 -HLT12 destruct /3 width=1/
  59 | -HT1 -HT2 /3 width=4/
  60 qed.
  61
  62 (* Basic_1: was just: sn3_pr2_intro (old version) *)
  63 lemma csna_intro_cpx: ∀h,g,L,T1. (
  64                          ∀T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → (T1 = T2 → ⊥) → ⦃h, L⦄ ⊢ ⬊⬊*[g] T2
  65                       ) → ⦃h, L⦄ ⊢ ⬊⬊*[g] T1.
  66 #h #g #L #T1 #H
  67 @csna_intro_aux #T #T2 #H @(cpxs_ind_dx … H) -T
  68 [ -H #H destruct #H
  69   elim (H ?) //
  70 | #T0 #T #HLT1 #HLT2 #IHT #HT10 #HT12 destruct
  71   elim (term_eq_dec T0 T) #HT0
  72   [ -HLT1 -HLT2 -H /3 width=1/
  73   | -IHT -HT12 /4 width=3/
  74   ]
  75 ]
  76 qed.
  77
  78 (* Main properties **********************************************************)
  79
  80 theorem csn_csna: ∀h,g,L,T. ⦃h, L⦄ ⊢ ⬊*[g] T → ⦃h, L⦄ ⊢ ⬊⬊*[g] T.
  81 #h #g #L #T #H @(csn_ind … H) -T /4 width=1/
  82 qed.
  83
  84 theorem csna_csn: ∀h,g,L,T. ⦃h, L⦄ ⊢ ⬊⬊*[g] T → ⦃h, L⦄ ⊢ ⬊*[g] T.
  85 #h #g #L #T #H @(csna_ind … H) -T /4 width=1/
  86 qed.
  87
  88 (* Basic_1: was just: sn3_pr3_trans *)
  89 lemma csn_cpxs_trans: ∀h,g,L,T1. ⦃h, L⦄ ⊢ ⬊*[g] T1 →
  90                       ∀T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ ⬊*[g] T2.
  91 #h #g #L #T1 #HT1 #T2 #H @(cpxs_ind … H) -T2 // /2 width=3 by csn_cpx_trans/
  92 qed-.
  93
  94 (* Main eliminators *********************************************************)
  95
  96 lemma csn_ind_alt: ∀h,g,L. ∀R:predicate term.
  97                    (∀T1. ⦃h, L⦄ ⊢ ⬊*[g] T1 →
  98                          (∀T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → (T1 = T2 → ⊥) → R T2) → R T1
  99                    ) →
 100                    ∀T. ⦃h, L⦄ ⊢ ⬊*[g] T → R T.
 101 #h #g #L #R #H0 #T1 #H @(csna_ind … (csn_csna … H)) -T1 #T1 #HT1 #IHT1
 102 @H0 -H0 /2 width=1/ -HT1 /3 width=1/
 103 qed-.