matita/matita/contribs/lambdadelta/basic_2A/etc/cny/cpye.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/psubsteval_6.ma".
  16 include "basic_2/relocation/cny.ma".
  17 include "basic_2/substitution/cpys.ma".
  18
  19 (* EVALUATION FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION ON TERMS **********)
  20
  21 definition cpye: ynat → ynat → relation4 genv lenv term term ≝
  22                  λd,e,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 ∧ ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T2⦄.
  23
  24 interpretation "evaluation for context-sensitive extended substitution (term)"
  25    'PSubstEval G L T1 T2 d e = (cpye d e G L T1 T2).
  26
  27 (* Basic_properties *********************************************************)
  28
  29 (* Note: this should go in subconversion *)
  30 lemma leqy_cpye_trans: ∀G,L2,T1,T2,d,e. ⦃G, L2⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ →
  31                        ∀L1. L1 ⊑×[d, e] L2 → L2 ⊑×[d, e] L1 → ⦃G, L1⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄.
  32 #G #L2 #T1 #T2 #d #e *
  33 /4 width=8 by lsuby_cpys_trans, lsuby_cny_conf, conj/
  34 qed-.
  35
  36 lemma cpye_sort: ∀G,L,d,e,k. ⦃G, L⦄ ⊢ ⋆k ▶*[d, e] 𝐍⦃⋆k⦄.
  37 /3 width=5 by cny_sort, conj/ qed.
  38
  39 lemma cpye_free: ∀G,L,d,e,i. |L| ≤ i → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃#i⦄.
  40 /3 width=6 by cny_lref_free, conj/ qed.
  41
  42 lemma cpye_top: ∀G,L,d,e,i. d + e ≤ yinj i → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃#i⦄.
  43 /3 width=6 by cny_lref_top, conj/ qed.
  44
  45 lemma cpye_skip: ∀G,L,d,e,i. yinj i < d → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃#i⦄.
  46 /3 width=6 by cny_lref_skip, conj/ qed.
  47
  48 lemma cpye_gref: ∀G,L,d,e,p. ⦃G, L⦄ ⊢ §p ▶*[d, e] 𝐍⦃§p⦄.
  49 /3 width=5 by cny_gref, conj/ qed.
  50
  51 lemma cpye_bind: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ →
  52                  ∀I,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*[⫯d, e] 𝐍⦃T2⦄ →
  53                  ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*[d, e] 𝐍⦃ⓑ{a,I}V2.T2⦄.
  54 #G #L #V1 #V2 #d #e * #HV12 #HV2 #I #T1 #T2 *
  55 /5 width=8 by cpys_bind, cny_bind, lsuby_cny_conf, lsuby_succ, conj/
  56 qed.
  57
  58 lemma cpye_flat: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ →
  59                  ∀T1,T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ →
  60                  ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ▶*[d, e] 𝐍⦃ⓕ{I}V2.T2⦄.
  61 #G #L #V1 #V2 #d #e * #HV12 #HV2 #T1 #T2 *
  62 /3 width=7 by cpys_flat, cny_flat, conj/
  63 qed.
  64
  65 (* Basic inversion lemmas ***************************************************)
  66
  67 lemma cpye_inv_sort1: ∀G,L,X,d,e,k. ⦃G, L⦄ ⊢ ⋆k ▶*[d, e] 𝐍⦃X⦄ → X = ⋆k.
  68 #G #L #X #d #e #k * /2 width=5 by cpys_inv_sort1/
  69 qed-.
  70
  71 lemma cpye_inv_gref1: ∀G,L,X,d,e,p. ⦃G, L⦄ ⊢ §p ▶*[d, e] 𝐍⦃X⦄ → X = §p.
  72 #G #L #X #d #e #p * /2 width=5 by cpys_inv_gref1/
  73 qed-.
  74
  75 lemma cpye_inv_bind1: ∀a,I,G,L,V1,T1,X,d,e. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*[d, e] 𝐍⦃X⦄ →
  76                       ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*[⫯d, e] 𝐍⦃T2⦄ &
  77                                X = ⓑ{a,I}V2.T2.
  78 #a #I #G #L #V1 #T1 #X #d #e * #H1 #H2 elim (cpys_inv_bind1 … H1) -H1
  79 #V2 #T2 #HV12 #HT12 #H destruct elim (cny_inv_bind … H2) -H2
  80 /5 width=8 by lsuby_cny_conf, lsuby_succ, ex3_2_intro, conj/
  81 qed-.
  82
  83 lemma cpye_inv_flat1: ∀I,G,L,V1,T1,X,d,e. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ▶*[d, e] 𝐍⦃X⦄ →
  84                       ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ & ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ &
  85                                X = ⓕ{I}V2.T2.
  86 #I #G #L #V1 #T1 #X #d #e * #H1 #H2 elim (cpys_inv_flat1 … H1) -H1
  87 #V2 #T2 #HV12 #HT12 #H destruct elim (cny_inv_flat … H2) -H2
  88 /3 width=5 by ex3_2_intro, conj/
  89 qed-.