matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_drop.ma

   1 definition dropable_dx: predicate (relation lenv) ≝
   2                         λR. ∀L1,L2. R L1 L2 → ∀K2,c,k. ⬇[c, 0, k] L2 ≡ K2 →
   3                         ∃∃K1. ⬇[c, 0, k] L1 ≡ K1 & R K1 K2.
   4
   5 lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (TC … R).
   6 #R #HR #L1 #L2 #H elim H -L2
   7 [ #L2 #HL12 #K2 #c #k #HLK2 elim (HR … HL12 … HLK2) -HR -L2
   8   /3 width=3 by inj, ex2_intro/
   9 | #L #L2 #_ #HL2 #IHL1 #K2 #c #k #HLK2 elim (HR … HL2 … HLK2) -HR -L2
  10   #K #HLK #HK2 elim (IHL1 … HLK) -L
  11   /3 width=5 by step, ex2_intro/
  12 ]
  13 qed-.
  14
  15
  16 fact lpx_sn_dropable_aux: ∀R,L2,K2,c,l,k. ⬇[c, l, k] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 →
  17                           l = 0 → ∃∃K1. ⬇[c, 0, k] L1 ≡ K1 & lpx_sn R K1 K2.
  18 #R #L2 #K2 #c #l #k #H elim H -L2 -K2 -l -k
  19 [ #l #k #Hm #X #H >(lpx_sn_inv_atom2 … H) -H
  20   /4 width=3 by drop_atom, lpx_sn_atom, ex2_intro/
  21 | #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H
  22   #K1 #V1 #HK12 #HV12 #H destruct
  23   /3 width=5 by drop_pair, lpx_sn_pair, ex2_intro/
  24 | #I #L2 #K2 #V2 #k #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H
  25   #L1 #V1 #HL12 #HV12 #H destruct
  26   elim (IHLK2 … HL12) -L2 /3 width=3 by drop_drop, ex2_intro/
  27 | #I #L2 #K2 #V2 #W2 #l #k #_ #_ #_ #L1 #_ #H elim (ysucc_inv_O_dx … H)
  28 ]
  29 qed-.
  30
  31 lemma lpx_sn_dropable: ∀R. dropable_dx (lpx_sn R).
  32 /2 width=5 by lpx_sn_dropable_aux/ qed-.
  33
  34 lemma lpx_sn_drop_trans: ∀R,L1,L2. lpx_sn R L1 L2 →
  35                          ∀I,K2,V2,i. ⬇[i] L2 ≡ K2.ⓑ{I}V2 →
  36                          ∃∃K1,V1. ⬇[i] L1 ≡ K1.ⓑ{I}V1 & lpx_sn R K1 K2 & R K1 V1 V2.
  37 #R #L1 #L2 #H elim H -L1 -L2
  38 [ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct
  39 | #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H
  40   [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/
  41   | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10
  42     /3 width=5 by drop_drop_lt, ex3_2_intro/
  43   ]
  44 ]
  45 qed-.
  46
  47 lemma lpx_sn_drop_conf: ∀R,L1,L2. lpx_sn R L1 L2 →
  48                         ∀I,K1,V1,i. ⬇[i] L1 ≡ K1.ⓑ{I}V1 →
  49                         ∃∃K2,V2. ⬇[i] L2 ≡ K2.ⓑ{I}V2 & lpx_sn R K1 K2 & R K1 V1 V2.
  50 #R #L1 #L2 #H elim H -L1 -L2
  51 [ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct
  52 | #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H
  53   [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/
  54   | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10
  55     /3 width=5 by drop_drop_lt, ex3_2_intro/
  56   ]
  57 ]
  58 qed-.