matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_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 "static_2/relocation/drops.ma".
  16 include "basic_2/rt_computation/jsx.ma".
  17
  18 (* COMPATIBILITY OF STRONG NORMALIZATION FOR UNBOUND RT-TRANSITION **********)
  19
  20 (* Forward lemmas with uniform slicing for local environments ***************)
  21
  22 lemma jsx_fwd_drops_atom_sn (h) (b) (G):
  23       ∀L1,L2. G ⊢ L1 ⊒[h] L2 →
  24       ∀f. 𝐔❪f❫ → ⇩*[b,f]L1 ≘ ⋆ → ⇩*[b,f]L2 ≘ ⋆.
  25 #h #b #G #L1 #L2 #H elim H -L1 -L2
  26 [ #f #_ #H //
  27 | #I #K1 #K2 #_ #IH #f #Hf #H
  28 | #I #K1 #K2 #V #_ #HV #IH #f #Hf #H
  29 ]
  30 elim (drops_inv_bind1_isuni … H) -H [3,6: // |*: * -Hf ]
  31 [1,3: #_ #H destruct
  32 |2,4: #g #Hg #HK1 #H destruct /3 width=1 by drops_drop/
  33 ]
  34 qed-.
  35
  36 lemma jsx_fwd_drops_unit_sn (h) (b) (G):
  37       ∀L1,L2. G ⊢ L1 ⊒[h] L2 →
  38       ∀f. 𝐔❪f❫ → ∀I,K1. ⇩*[b,f]L1 ≘ K1.ⓤ[I] →
  39       ∃∃K2. G ⊢ K1 ⊒[h] K2 & ⇩*[b,f]L2 ≘ K2.ⓤ[I].
  40 #h #b #G #L1 #L2 #H elim H -L1 -L2
  41 [ #f #_ #J #Y1 #H
  42   lapply (drops_inv_atom1 … H) -H * #H #_ destruct
  43 | #I #K1 #K2 #HK12 #IH #f #Hf #J #Y1 #H
  44 | #I #K1 #K2 #V #HK12 #HV #IH #f #Hf #J #Y1 #H
  45 ]
  46 elim (drops_inv_bind1_isuni … H) -H [3,6: // |*: * -Hf ]
  47 [1,3: #Hf #H destruct -IH /3 width=3 by drops_refl, ex2_intro/
  48 |2,4:
  49   #g #Hg #HK1 #H destruct
  50   elim (IH … Hg … HK1) -K1 -Hg #Y2 #HY12 #HKY2
  51   /3 width=3 by drops_drop, ex2_intro/
  52 ]
  53 qed-.
  54
  55 lemma jsx_fwd_drops_pair_sn (h) (b) (G):
  56       ∀L1,L2. G ⊢ L1 ⊒[h] L2 →
  57       ∀f. 𝐔❪f❫ → ∀I,K1,V. ⇩*[b,f]L1 ≘ K1.ⓑ[I]V →
  58       ∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & ⇩*[b,f]L2 ≘ K2.ⓑ[I]V
  59        | ∃∃K2. G ⊢ K1 ⊒[h] K2 & ⇩*[b,f]L2 ≘ K2.ⓧ & G ⊢ ⬈*𝐒[h,V] K2.
  60 #h #b #G #L1 #L2 #H elim H -L1 -L2
  61 [ #f #_ #J #Y1 #X1 #H
  62   lapply (drops_inv_atom1 … H) -H * #H #_ destruct
  63 | #I #K1 #K2 #HK12 #IH #f #Hf #J #Y1 #X1 #H
  64 | #I #K1 #K2 #V #HK12 #HV #IH #f #Hf #J #Y1 #X1 #H
  65 ]
  66 elim (drops_inv_bind1_isuni … H) -H [3,6: // |*: * -Hf ]
  67 [1,3:
  68   #Hf #H destruct -IH
  69   /4 width=4 by drops_refl, ex3_intro, ex2_intro, or_introl, or_intror/
  70 |2,4:
  71   #g #Hg #HK1 #H destruct
  72   elim (IH … Hg … HK1) -K1 -Hg * #Y2 #HY12 #HKY2 [2,4: #HX1 ]
  73   /4 width=4 by drops_drop, ex3_intro, ex2_intro, or_introl, or_intror/
  74 ]
  75 qed-.