matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_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/relocation/lpx_sn.ma".
  16 include "basic_2/relocation/drops.ma".
  17
  18 (* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
  19
  20 (* Properties on general slicing for local environments *********************)
  21
  22 lemma lpx_sn_deliftable_dropable: ∀R. (∀b. d_deliftable2_sn (R b)) → dropable_sn (lpx_sn R).
  23 #R #HR #L1 #K1 #c #t #H elim H -L1 -K1 -t
  24 [ #t #Ht #X #u2 #H #u1 #Hu elim (lpx_sn_inv_atom1 … H) -H
  25   #H1 #H2 destruct elim (after_inv_empty3 … Hu) -Hu
  26   #H1 #H2 destruct /3 width=3 by drops_atom, lpx_sn_atom, ex2_intro/
  27 | #I #L1 #K1 #V1 #t #_ #IH #X #u2 #H #u1 #Hu elim (lpx_sn_inv_pair1 … H) -H
  28   #L2 #V2 #y2 #x2 #HL #HV #H1 #H2 destruct elim (after_inv_false1 … Hu) -Hu
  29   #u #H1 #Hu destruct elim (IH … HL … Hu) -L1 /3 width=3 by drops_drop, ex2_intro/
  30 | #I #L1 #K1 #V1 #W1 #t #HLK #HWV #IHLK #X #u2 #H #u1 #Hu elim (lpx_sn_inv_pair1 … H) -H
  31   #L2 #V2 #y2 #x2 #HL #HV #H1 #H2 destruct elim (after_inv_true1 … Hu) -Hu
  32   #y1 #y #x1 #H1 #H2 #Hu destruct elim (HR … HV … HLK … HWV) -V1
  33   elim (IHLK … HL … Hu) -L1 /3 width=5 by drops_skip, lpx_sn_pair, ex2_intro/
  34 ]
  35 qed-.
  36 (*
  37 lemma lpx_sn_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) →
  38                                   d_liftable2 R → dedropable_sn (lpx_sn R).
  39 #R #H1R #H2R #L1 #K1 #s #l #m #H elim H -L1 -K1 -l -m
  40 [ #l #m #Hm #X #H >(lpx_sn_inv_atom1 … H) -H
  41   /4 width=4 by drop_atom, lpx_sn_atom, ex3_intro/
  42 | #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H
  43   #K2 #V2 #HK12 #HV12 #H destruct
  44   lapply (lpx_sn_fwd_length … HK12)
  45   #H @(ex3_intro … (K2.ⓑ{I}V2)) (**) (* explicit constructor *)
  46   /3 width=1 by lpx_sn_pair, lreq_O2/
  47 | #I #L1 #K1 #V1 #m #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1
  48   /3 width=5 by drop_drop, lreq_pair, lpx_sn_pair, ex3_intro/
  49 | #I #L1 #K1 #V1 #W1 #l #m #HLK1 #HWV1 #IHLK1 #X #H
  50   elim (lpx_sn_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
  51   elim (H2R … HW12 … HLK1 … HWV1) -W1
  52   elim (IHLK1 … HK12) -K1
  53   /3 width=6 by drop_skip, lreq_succ, lpx_sn_pair, ex3_intro/
  54 ]
  55 qed-.
  56 *)
  57 include "ground_2/relocation/trace_isun.ma".
  58
  59 lemma lpx_sn_dropable: ∀R,L2,K2,c,t. ⬇*[c, t] L2 ≡ K2 → 𝐔⦃t⦄ →
  60                        ∀L1,u2. lpx_sn R u2 L1 L2 → ∀u1. t ⊚ u1 ≡ u2 →
  61                        ∃∃K1. ⬇*[c, t] L1 ≡ K1 & lpx_sn R u1 K1 K2.
  62 #R #L2 #K2 #c #t #H elim H -L2 -K2 -t
  63 [ #t #Ht #_ #X #u2 #H #u1 #Hu elim (lpx_sn_inv_atom2 … H) -H
  64   #H1 #H2 destruct elim (after_inv_empty3 … Hu) -Hu
  65   /4 width=3 by drops_atom, lpx_sn_atom, ex2_intro/
  66 | #I #L2 #K2 #V2 #t #_ #IH #Ht #X #u2 #H #u1 #Hu elim (lpx_sn_inv_pair2 … H) -H
  67   #L1 #V1 #y2 #x #HL #HV #H1 #H2 destruct elim (after_inv_false1 … Hu) -Hu
  68   #u #H #Hu destruct elim (IH … HL … Hu) -L2 /3 width=3 by drops_drop, isun_inv_false, ex2_intro/
  69 | #I #L2 #K2 #V2 #W2 #t #_ #HWV #IHLK #Ht #X #u2 #H #u1 #Hu elim (lpx_sn_inv_pair2 … H) -H
  70   #L1 #V1 #y2 #x #HL #HV #H1 #H2 destruct elim (after_inv_true1 … Hu) -Hu
  71   #y1 #y #x2 #H1 #H2 #Hu destruct lapply (isun_inv_true … Ht) -Ht
  72   #Ht elim (IHLK … HL … Hu) -L2 -Hu /2 width=1 by isun_id/
  73   #K1 #HLK1 #HK12 lapply (lifts_fwd_isid … HWV ?) // -HWV
  74   #H destruct lapply (drops_fwd_isid … HLK1 ?) //
  75   #H destruct
  76   @ex2_intro
  77   [
  78   | @(drops_skip … HLK1)
  79   | @(lpx_sn_pair … HK12 … HV)
  80
  81
  82    lapply (drops_fwd_isid … HLK1 ?) // -HLK1
  83   2:
  84
  85
  86
  87
  88    elim (HR … HV … HLK … HWV) -V1
  89   elim (IHLK … HL … Hu) -L1 /3 width=5 by drops_skip, lpx_sn_pair, ex2_intro/
  90
  91
  92 ]
  93 qed-.