matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_drops.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_drops.ma".
  16 include "basic_2/dynamic/cnv.ma".
  17
  18 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
  19
  20 (* Advanced dproperties *****************************************************)
  21
  22 (* Basic_2A1: uses: snv_lref *)
  23 lemma cnv_lref_drops (h) (a) (G):
  24       ∀I,K,V,i,L. ❪G,K❫ ⊢ V ![h,a] →
  25       ⇩[i] L ≘ K.ⓑ[I]V → ❪G,L❫ ⊢ #i ![h,a].
  26 #h #a #G #I #K #V #i elim i -i
  27 [ #L #HV #H
  28   lapply (drops_fwd_isid … H ?) -H // #H destruct
  29   /2 width=1 by cnv_zero/
  30 | #i #IH #L #HV #H
  31   elim (drops_inv_succ … H) -H #J0 #K0 #HK0 #H destruct
  32   /3 width=1 by cnv_lref/
  33 ]
  34 qed.
  35
  36 (* Advanced inversion lemmas ************************************************)
  37
  38 (* Basic_2A1: uses: snv_inv_lref *)
  39 lemma cnv_inv_lref_drops (h) (a) (G):
  40       ∀i,L. ❪G,L❫ ⊢ #i ![h,a] →
  41       ∃∃I,K,V. ⇩[i] L ≘ K.ⓑ[I]V & ❪G,K❫ ⊢ V ![h,a].
  42 #h #a #G #i elim i -i
  43 [ #L #H
  44   elim (cnv_inv_zero … H) -H #I #K #V #HV #H destruct
  45   /3 width=5 by drops_refl, ex2_3_intro/
  46 | #i #IH #X #H
  47   elim (cnv_inv_lref … H) -H #I #L #HL #H destruct
  48   elim (IH … HL) -IH -HL #J #K #V #HLK #HV
  49   /3 width=5 by drops_drop, ex2_3_intro/
  50 ]
  51 qed-.
  52
  53 lemma cnv_inv_lref_pair (h) (a) (G):
  54       ∀i,L. ❪G,L❫ ⊢ #i ![h,a] →
  55       ∀I,K,V. ⇩[i] L ≘ K.ⓑ[I]V → ❪G,K❫ ⊢ V ![h,a].
  56 #h #a #G #i #L #H #I #K #V #HLK
  57 elim (cnv_inv_lref_drops … H) -H #Z #Y #X #HLY #HX
  58 lapply (drops_mono … HLY … HLK) -L #H destruct //
  59 qed-.
  60
  61 lemma cnv_inv_lref_atom (h) (a) (b) (G):
  62       ∀i,L. ❪G,L❫ ⊢ #i ![h,a] → ⇩*[b,𝐔❨i❩] L ≘ ⋆ → ⊥.
  63 #h #a #b #G #i #L #H #Hi
  64 elim (cnv_inv_lref_drops … H) -H #Z #Y #X #HLY #_
  65 lapply (drops_gen b … HLY) -HLY #HLY
  66 lapply (drops_mono … HLY … Hi) -L #H destruct
  67 qed-.
  68
  69 lemma cnv_inv_lref_unit (h) (a) (G):
  70       ∀i,L. ❪G,L❫ ⊢ #i ![h,a] →
  71       ∀I,K. ⇩[i] L ≘ K.ⓤ[I] → ⊥.
  72 #h #a #G #i #L #H #I #K #HLK
  73 elim (cnv_inv_lref_drops … H) -H #Z #Y #X #HLY #_
  74 lapply (drops_mono … HLY … HLK) -L #H destruct
  75 qed-.
  76
  77 (* Properties with generic slicing for local environments *******************)
  78
  79 (* Basic_2A1: uses: snv_lift *)
  80 lemma cnv_lifts (h) (a): ∀G. d_liftable1 (cnv h a G).
  81 #h #a #G #K #T
  82 @(fqup_wf_ind_eq (Ⓣ) … G K T) -G -K -T #G0 #K0 #T0 #IH #G #K * * [|||| * ]
  83 [ #s #HG #HK #HT #_ #b #f #L #_ #X #H2 destruct
  84   >(lifts_inv_sort1 … H2) -X -K -f //
  85 | #i #HG #HK #HT #H1 #b #f #L #HLK #X #H2 destruct
  86   elim (cnv_inv_lref_drops … H1) -H1 #I0 #K0 #V #HK0 #HV
  87   elim (lifts_inv_lref1 … H2) -H2 #j #Hf #H destruct
  88 (**) (* this should be a lemma *)
  89   lapply (drops_trans … HLK … HK0 ??) -HLK [3,6: |*: // ] #H
  90   elim (drops_split_trans … H) -H [1,6: |*: /2 width=6 by after_uni_dx/ ] #Y #HL #HY
  91   lapply (drops_tls_at … Hf … HY) -HY #HY
  92   elim (drops_inv_skip2 … HY) -HY #Z #L0 #HLK0 #HZ #H destruct
  93   elim (liftsb_inv_pair_sn … HZ) -HZ #W #HVW #H destruct
  94 (**) (* end of the lemma *)
  95   /4 width=8 by cnv_lref_drops, fqup_lref, drops_inv_gen/
  96 | #l #HG #HK #HT #H1 #b #f #L #_ #X #_ destruct
  97   elim (cnv_inv_gref … H1)
  98 | #p #I #V #T #HG #HK #HT #H1 #b #f #L #HLK #X #H2 destruct
  99   elim (cnv_inv_bind … H1) -H1 #HV #HT
 100   elim (lifts_inv_bind1 … H2) -H2 #W #U #HVW #HTU #H destruct
 101   /5 width=8 by cnv_bind, drops_skip, ext2_pair/
 102 | #V #T #HG #HK #HT #H1 #b #f #L #HLK #X #H2 destruct
 103   elim (cnv_inv_appl … H1) #n #p #W0 #U0 #Ha #HV #HT #HVW0 #HTW0
 104   elim (lifts_inv_flat1 … H2) -H2 #W #U #HVW #HTU #H destruct
 105   elim (lifts_total W0 f)
 106   elim (lifts_total U0 (⫯f))
 107   /4 width=17 by cnv_appl, cpms_lifts_bi, lifts_bind/
 108 | #V #T #HG #HK #HT #H1 #b #f #L #HLK #X #H2 destruct
 109   elim (cnv_inv_cast … H1) #U0 #HV #HT #HVU0 #HTU0
 110   elim (lifts_inv_flat1 … H2) -H2 #W #U #HVW #HTU #H destruct
 111   elim (lifts_total U0 f)
 112   /3 width=12 by cnv_cast, cpms_lifts_bi/
 113 ]
 114 qed-.
 115
 116 (* Inversion lemmas with generic slicing for local environments *************)
 117
 118 (* Basic_2A1: uses: snv_inv_lift *)
 119 lemma cnv_inv_lifts (h) (a): ∀G. d_deliftable1 (cnv h a G).
 120 #h #a #G #L #U
 121 @(fqup_wf_ind_eq (Ⓣ) … G L U) -G -L -U #G0 #L0 #U0 #IH #G #L * * [|||| * ]
 122 [ #s #HG #HL #HU #H1 #b #f #K #HLK #X #H2 destruct
 123   >(lifts_inv_sort2 … H2) -X -L -f //
 124 | #j #HG #HL #HU #H1 #b #f #K #HLK #X #H2 destruct
 125   elim (cnv_inv_lref_drops … H1) -H1 #I0 #L0 #W #HL0 #HW
 126   elim (lifts_inv_lref2 … H2) -H2 #i #Hf #H destruct
 127 (**) (* this should be a lemma *)
 128   lapply (drops_split_div … HLK (𝐔❨i❩) ???) -HLK [4,8: * |*: // ] #Y0 #HK #HLY0
 129   lapply (drops_conf … HL0 … HLY0 ??) -HLY0 [3,6: |*: /2 width=6 by after_uni_dx/ ] #HLY0
 130   lapply (drops_tls_at … Hf … HLY0) -HLY0 #HLY0
 131   elim (drops_inv_skip1 … HLY0) -HLY0 #Z #K0 #HLK0 #HZ #H destruct
 132   elim (liftsb_inv_pair_dx … HZ) -HZ #V #HVW #H destruct
 133 (**) (* end of the lemma *)
 134   /4 width=8 by cnv_lref_drops, fqup_lref, drops_inv_F/
 135 | #l #HG #HL #HU #H1 #b #f #K #_ #X #_ destruct
 136   elim (cnv_inv_gref … H1)
 137 | #p #I #W #U #HG #HL #HU #H1 #b #f #K #HLK #X #H2 destruct
 138   elim (cnv_inv_bind … H1) -H1 #HW #HU
 139   elim (lifts_inv_bind2 … H2) -H2 #V #T #HVW #HTU #H destruct
 140   /5 width=8 by cnv_bind, drops_skip, ext2_pair/
 141 | #W #U #HG #HL #HU #H1 #b #f #K #HLK #X #H2 destruct
 142   elim (cnv_inv_appl … H1) #n #p #W0 #U0 #Ha #HW #HU #HW0 #HU0
 143   elim (lifts_inv_flat2 … H2) -H2 #V #T #HVW #HTU #H destruct
 144   elim (cpms_inv_lifts_sn … HW0 … HLK … HVW) -HW0 #V0 #HVW0 #HV0
 145   elim (cpms_inv_lifts_sn … HU0 … HLK … HTU) -HU0 #X0 #H #HT0
 146   elim (lifts_inv_bind2 … H) -H #X #T0 #HX #HTU0 #H destruct
 147   lapply (lifts_inj … HX … HVW0) -HX #H destruct
 148   /3 width=8 by cnv_appl/
 149 | #W #U #HG #HL #HU #H1 #b #f #K #HLK #X #H2 destruct
 150   elim (cnv_inv_cast … H1) #U0 #HW #HU #HWU0 #HU0
 151   elim (lifts_inv_flat2 … H2) -H2 #V #T #HVW #HTU #H destruct
 152   elim (cpms_inv_lifts_sn … HWU0 … HLK … HVW) -HWU0 #V0 #HVU0 #HV0
 153   elim (cpms_inv_lifts_sn … HU0 … HLK … HTU) -HU0 #X #HX #HTV0
 154   lapply (lifts_inj … HX … HVU0) -HX #H destruct
 155   /3 width=8 by cnv_cast/
 156 ]
 157 qed-.