matita/matita/contribs/lambdadelta/basic_2/etc_2A1/cny/cny.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 include "basic_2/notation/relations/psubstnormal_5.ma".
  16 include "basic_2/relocation/cpy.ma".
  17
  18 (* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION *****************)
  19
  20 definition cny: ∀d,e. relation3 genv lenv term ≝
  21                 λd,e,G,L. NF … (cpy d e G L) (eq …).
  22
  23 interpretation
  24    "normality for context-sensitive extended substitution (term)"
  25    'PSubstNormal G L T d e = (cny d e G L T).
  26
  27 (* Basic inversion lemmas ***************************************************)
  28
  29 lemma cny_inv_lref: ∀G,L,d,e,i. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄ →
  30                     ∨∨ yinj i < d | d + e ≤ yinj i | |L| ≤ i.
  31 #G #L #d #e #i #H elim (ylt_split i d) /2 width=1 by or3_intro0/
  32 #Hdi elim (ylt_split i (d+e)) /2 width=1 by or3_intro1/
  33 #Hide elim (lt_or_ge i (|L|)) /2 width=1 by or3_intro2/
  34 #Hi elim (ldrop_O1_lt L i) //
  35 #I #K #V #HLK elim (lift_total V 0 (i+1))
  36 #W #HVW lapply (H W ?) -H /2 width=5 by cpy_subst/ -HLK
  37 #H destruct elim (lift_inv_lref2_be … HVW) -L -d -e //
  38 qed-.
  39
  40 lemma cny_inv_bind: ∀a,I,G,L,V,T,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓑ{a,I}V.T⦄ →
  41                     ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ ▶[⫯d, e] 𝐍⦃T⦄.
  42 #a #I #G #L #V1 #T1 #d #e #HVT1 @conj
  43 [ #V2 #HV2 lapply (HVT1 (ⓑ{a,I}V2.T1) ?) -HVT1
  44 | #T2 #HT2 lapply (HVT1 (ⓑ{a,I}V1.T2) ?) -HVT1
  45 ]
  46 /2 width=1 by cpy_bind/ #H destruct //
  47 qed-.
  48
  49 lemma cny_inv_flat: ∀I,G,L,V,T,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓕ{I}V.T⦄ →
  50                     ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ ∧ ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T⦄.
  51 #I #G #L #V1 #T1 #d #e #HVT1 @conj
  52 [ #V2 #HV2 lapply (HVT1 (ⓕ{I}V2.T1) ?) -HVT1
  53 | #T2 #HT2 lapply (HVT1 (ⓕ{I}V1.T2) ?) -HVT1
  54 ]
  55 /2 width=1 by cpy_flat/ #H destruct //
  56 qed-.
  57
  58 (* Basic properties *********************************************************)
  59
  60 lemma lsuby_cny_conf: ∀G,d,e.
  61                       ∀L1,T. ⦃G, L1⦄ ⊢ ▶[d, e] 𝐍⦃T⦄ →
  62                       ∀L2. L1 ⊑×[d, e] L2 → ⦃G, L2⦄ ⊢ ▶[d, e] 𝐍⦃T⦄.
  63 #G #d #e #L1 #T1 #HT1 #L2 #HL12 #T2 #HT12
  64 @HT1 /3 width=3 by lsuby_cpy_trans/
  65 qed-.
  66
  67 lemma cny_sort: ∀G,L,d,e,k. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃⋆k⦄.
  68 #G #L #d #e #k #X #H elim (cpy_inv_sort1 … H) -H //
  69 qed.
  70
  71 lemma cny_lref_free: ∀G,L,d,e,i. |L| ≤ i → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
  72 #G #L #d #e #i #Hi #X #H elim (cpy_inv_lref1 … H) -H // *
  73 #I #K #V #_ #_ #HLK #_ lapply (ldrop_fwd_length_lt2 … HLK) -HLK
  74 #H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/
  75 qed.
  76
  77 lemma cny_lref_atom: ∀G,L,d,e,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
  78 #G #L #d #e #i #HL @cny_lref_free >(ldrop_fwd_length … HL) -HL //
  79 qed.
  80
  81 lemma cny_lref_top: ∀G,L,d,e,i. d+e ≤ yinj i → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
  82 #G #L #d #e #i #Hdei #X #H elim (cpy_inv_lref1 … H) -H // *
  83 #I #K #V #_ #H elim (ylt_yle_false … H) //
  84 qed.
  85
  86 lemma cny_lref_skip: ∀G,L,d,e,i. yinj i < d → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
  87 #G #L #d #e #i #Hid #X #H elim (cpy_inv_lref1 … H) -H // *
  88 #I #K #V #H elim (ylt_yle_false … H) //
  89 qed.
  90
  91 lemma cny_gref: ∀G,L,d,e,p. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃§p⦄.
  92 #G #L #d #e #p #X #H elim (cpy_inv_gref1 … H) -H //
  93 qed.
  94
  95 lemma cny_bind: ∀G,L,V,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ →
  96                 ∀I,T. ⦃G, L.ⓑ{I}V⦄ ⊢ ▶[⫯d, e] 𝐍⦃T⦄ →
  97                 ∀a. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓑ{a,I}V.T⦄.
  98 #G #L #V1 #d #e #HV1 #I #T1 #HT1 #a #X #H
  99 elim (cpy_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
 100 >(HV1 … HV12) -V2 >(HT1 … HT12) -T2 //
 101 qed.
 102
 103 lemma cny_flat: ∀G,L,V,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ →
 104                 ∀T. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T⦄ →
 105                 ∀I. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓕ{I}V.T⦄.
 106 #G #L #V1 #d #e #HV1 #T1 #HT1 #I #X #H
 107 elim (cpy_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
 108 >(HV1 … HV12) -V2 >(HT1 … HT12) -T2 //
 109 qed.
 110
 111 lemma cny_narrow: ∀G,L,T,d1,e1. ⦃G, L⦄ ⊢ ▶[d1, e1] 𝐍⦃T⦄ →
 112                   ∀d2,e2. d1 ≤ d2 → d2 + e2 ≤ d1 + e1 → ⦃G, L⦄ ⊢ ▶[d2, e2] 𝐍⦃T⦄.
 113 #G #L #T1 #d1 #e1 #HT1 #d2 #e2 #Hd12 #Hde21 #T2 #HT12
 114 @HT1 /2 width=5 by cpy_weak/ qed-.