matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.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/rt_computation/cpms_cpms.ma".
  16 include "basic_2/rt_equivalence/cpes.ma".
  17 include "basic_2/dynamic/cnv_aaa.ma".
  18
  19 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
  20
  21 (* Properties with t-bound rt-equivalence for terms *************************)
  22
  23 lemma cnv_appl_cpes (a) (h) (G) (L):
  24       ∀n. (a = Ⓣ → n ≤ 1) →
  25       ∀V. ⦃G, L⦄ ⊢ V ![a, h] → ∀T. ⦃G, L⦄ ⊢ T ![a, h] →
  26       ∀W. ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W →
  27       ∀p,U. ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U → ⦃G, L⦄ ⊢ ⓐV.T ![a, h].
  28 #a #h #G #L #n #Hn #V #HV #T #HT #W *
  29 /4 width=11 by cnv_appl, cpms_cprs_trans, cpms_bind/
  30 qed.
  31
  32 lemma cnv_cast_cpes (a) (h) (G) (L):
  33       ∀U. ⦃G, L⦄ ⊢ U ![a, h] →
  34       ∀T. ⦃G, L⦄ ⊢ T ![a, h] → ⦃G, L⦄ ⊢ U ⬌*[h,0,1] T → ⦃G, L⦄ ⊢ ⓝU.T ![a, h].
  35 #a #h #G #L #U #HU #T #HT * /2 width=3 by cnv_cast/
  36 qed.
  37
  38 (* Inversion lemmas with t-bound rt-equivalence for terms *******************)
  39
  40 lemma cnv_inv_appl_cpes (a) (h) (G) (L):
  41       ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] →
  42       ∃∃n,p,W,U. a = Ⓣ → n ≤ 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
  43                  ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U.
  44 #a #h #G #L #V #T #H
  45 elim (cnv_inv_appl … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU
  46 /3 width=7 by cpms_div, ex5_4_intro/
  47 qed-.
  48
  49 lemma cnv_inv_appl_SO_cpes (a) (h) (G) (L):
  50       ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] →
  51       ∃∃n,p,W,U. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
  52                  ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U.
  53 #a #h #G #L #V #T #H
  54 elim (cnv_inv_appl_SO … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU
  55 /3 width=7 by cpms_div, ex5_4_intro/
  56 qed-.
  57
  58 lemma cnv_inv_appl_true_cpes (h) (G) (L):
  59       ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![h] →
  60       ∃∃p,W,U. ⦃G,L⦄ ⊢ V ![h] & ⦃G,L⦄ ⊢ T ![h] &
  61                  ⦃G,L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G,L⦄ ⊢ T ➡*[1,h] ⓛ{p}W.U.
  62 #h #G #L #V #T #H
  63 elim (cnv_inv_appl_SO_cpes … H) -H #n #p #W #U #Hn
  64 >Hn -n [| // ] #HV #HT #HVW #HTU
  65 /2 width=5 by ex4_3_intro/
  66 qed-.
  67
  68 lemma cnv_inv_cast_cpes (a) (h) (G) (L):
  69       ∀U,T. ⦃G, L⦄ ⊢ ⓝU.T ![a, h] →
  70       ∧∧ ⦃G, L⦄ ⊢ U ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & ⦃G, L⦄ ⊢ U ⬌*[h,0,1] T.
  71 #a #h #G #L #U #T #H
  72 elim (cnv_inv_cast … H) -H
  73 /3 width=3 by cpms_div, and3_intro/
  74 qed-.
  75
  76 (* Eliminators with t-bound rt-equivalence for terms ************************)
  77
  78 lemma cnv_ind_cpes (a) (h) (Q:relation3 genv lenv term):
  79       (∀G,L,s. Q G L (⋆s)) →
  80       (∀I,G,K,V. ⦃G,K⦄ ⊢ V![a,h] → Q G K V → Q G (K.ⓑ{I}V) (#O)) →
  81       (∀I,G,K,i. ⦃G,K⦄ ⊢ #i![a,h] → Q G K (#i) → Q G (K.ⓘ{I}) (#(↑i))) →
  82       (∀p,I,G,L,V,T. ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L.ⓑ{I}V⦄⊢T![a,h] →
  83                      Q G L V →Q G (L.ⓑ{I}V) T →Q G L (ⓑ{p,I}V.T)
  84       ) →
  85       (∀n,p,G,L,V,W,T,U. (a = Ⓣ → n ≤ 1) → ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L⦄ ⊢ T![a,h] →
  86                          ⦃G,L⦄ ⊢ V ⬌*[h,1,0]W → ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W.U →
  87                          Q G L V → Q G L T → Q G L (ⓐV.T)
  88       ) →
  89       (∀G,L,U,T. ⦃G,L⦄⊢ U![a,h] → ⦃G,L⦄ ⊢ T![a,h] → ⦃G,L⦄ ⊢ U ⬌*[h,0,1] T →
  90                  Q G L U → Q G L T → Q G L (ⓝU.T)
  91       ) →
  92       ∀G,L,T. ⦃G,L⦄⊢ T![a,h] → Q G L T.
  93 #a #h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #G #L #T #H
  94 elim H -G -L -T [5,6: /3 width=7 by cpms_div/ |*: /2 width=1 by/ ]
  95 qed-.