matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_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/cpme_aaa.ma".
  16 include "basic_2/rt_computation/cpre_cpre.ma".
  17 include "basic_2/rt_equivalence/cpes.ma".
  18 include "basic_2/dynamic/cnv_cpme.ma".
  19
  20 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
  21
  22 (* Properties with t-bound rt-equivalence for terms *************************)
  23
  24 lemma cnv_cpes_dec (a) (h) (n1) (n2) (G) (L):
  25       ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → ∀T2. ⦃G,L⦄ ⊢ T2 ![a,h] →
  26       Decidable … (⦃G,L⦄ ⊢ T1 ⬌*[h,n1,n2] T2).
  27 #a #h #n1 #n2 #G #L #T1 #HT1 #T2 #HT2
  28 elim (cnv_fwd_aaa … HT1) #A1 #HA1
  29 elim (cnv_fwd_aaa … HT2) #A2 #HA2
  30 elim (cpme_total_aaa h n1 … HA1) -HA1 #U1 #HTU1
  31 elim (cpme_total_aaa h n2 … HA2) -HA2 #U2 #HTU2
  32 elim (eq_term_dec U1 U2) [ #H destruct | #HnU12 ]
  33 [ cases HTU1 -HTU1 #HTU1 #_
  34   cases HTU2 -HTU2 #HTU2 #_
  35   /3 width=3 by cpms_div, or_introl/
  36 | @or_intror * #T0 #HT10 #HT20
  37   lapply (cnv_cpme_cpms_conf … HT1 … HT10 … HTU1) -T1 #H1
  38   lapply (cnv_cpme_cpms_conf … HT2 … HT20 … HTU2) -T2 #H2
  39   /3 width=6 by cpre_mono/
  40 ]
  41 qed-.
  42
  43 (* Advanced inversion lemmas with t-bound rt-equivalence for terms **********)
  44
  45 lemma cnv_inv_appl_SO_cpes (a) (h) (G) (L):
  46       ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] →
  47       ∃∃n,p,W,U. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
  48                  ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U.
  49 #a #h #G #L #V #T #H
  50 elim (cnv_inv_appl_SO … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU
  51 /3 width=7 by cpms_div, ex5_4_intro/
  52 qed-.