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