matita/matita/contribs/lambdadelta/basic_2/relocation/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/notation/relations/rdropstar_4.ma".
  16 include "basic_2/grammar/lenv.ma".
  17 include "basic_2/relocation/lifts.ma".
  18
  19 (* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
  20
  21 (* Basic_1: includes: drop_skip_bind drop1_skip_bind *)
  22 (* Basic_2A1: includes: drop_atom drop_pair drop_drop drop_skip
  23                         drop_refl_atom_O2 drop_drop_lt drop_skip_lt
  24 *)
  25 inductive drops (s:bool): trace → relation lenv ≝
  26 | drops_atom: ∀t. (s = Ⓕ → 𝐈⦃t⦄) → drops s (t) (⋆) (⋆)
  27 | drops_drop: ∀I,L1,L2,V,t. drops s t L1 L2 → drops s (Ⓕ@t) (L1.ⓑ{I}V) L2
  28 | drops_skip: ∀I,L1,L2,V1,V2,t.
  29               drops s t L1 L2 → ⬆*[t] V2 ≡ V1 →
  30               drops s (Ⓣ@t) (L1.ⓑ{I}V1) (L2.ⓑ{I}V2)
  31 .
  32
  33 interpretation "general slicing (local environment)"
  34    'RDropStar s t L1 L2 = (drops s t L1 L2).
  35
  36 definition d_liftable1: relation2 lenv term → predicate bool ≝
  37                         λR,s. ∀L,K,t. ⬇*[s, t] L ≡ K →
  38                         ∀T,U. ⬆*[t] T ≡ U → R K T → R L U.
  39
  40 definition d_liftable2: predicate (lenv → relation term) ≝
  41                         λR. ∀K,T1,T2. R K T1 T2 → ∀L,s,t. ⬇*[s, t] L ≡ K →
  42                         ∀U1. ⬆*[t] T1 ≡ U1 →
  43                         ∃∃U2. ⬆*[t] T2 ≡ U2 & R L U1 U2.
  44
  45 definition d_deliftable2_sn: predicate (lenv → relation term) ≝
  46                              λR. ∀L,U1,U2. R L U1 U2 → ∀K,s,t. ⬇*[s, t] L ≡ K →
  47                              ∀T1. ⬆*[t] T1 ≡ U1 →
  48                              ∃∃T2. ⬆*[t] T2 ≡ U2 & R K T1 T2.
  49
  50 definition dropable_sn: predicate (relation lenv) ≝
  51                         λR. ∀L1,K1,s,t. ⬇*[s, t] L1 ≡ K1 → ∀L2. R L1 L2 →
  52                         ∃∃K2. R K1 K2 & ⬇*[s, t] L2 ≡ K2.
  53 (*
  54 definition dropable_dx: predicate (relation lenv) ≝
  55                         λR. ∀L1,L2. R L1 L2 → ∀K2,s,m. ⬇[s, 0, m] L2 ≡ K2 →
  56                         ∃∃K1. ⬇[s, 0, m] L1 ≡ K1 & R K1 K2.
  57 *)
  58 (* Basic inversion lemmas ***************************************************)
  59
  60 fact drops_inv_atom1_aux: ∀X,Y,s,t. ⬇*[s, t] X ≡ Y → X = ⋆ →
  61                           Y = ⋆ ∧ (s = Ⓕ → 𝐈⦃t⦄).
  62 #X #Y #s #t * -X -Y -t
  63 [ /3 width=1 by conj/
  64 | #I #L1 #L2 #V #t #_ #H destruct
  65 | #I #L1 #L2 #V1 #V2 #t #_ #_ #H destruct
  66 ]
  67 qed-.
  68
  69 (* Basic_1: includes: drop_gen_sort *)
  70 (* Basic_2A1: includes: drop_inv_atom1 *)
  71 lemma drops_inv_atom1: ∀Y,s,t. ⬇*[s, t] ⋆ ≡ Y → Y = ⋆ ∧ (s = Ⓕ → 𝐈⦃t⦄).
  72 /2 width=3 by drops_inv_atom1_aux/ qed-.
  73
  74 fact drops_inv_drop1_aux: ∀X,Y,s,t. ⬇*[s, t] X ≡ Y → ∀I,K,V,tl. X = K.ⓑ{I}V → t = Ⓕ@tl →
  75                           ⬇*[s, tl] K ≡ Y.
  76 #X #Y #s #t * -X -Y -t
  77 [ #t #Ht #J #K #W #tl #H destruct
  78 | #I #L1 #L2 #V #t #HL #J #K #W #tl #H1 #H2 destruct //
  79 | #I #L1 #L2 #V1 #V2 #t #_ #_ #J #K #W #tl #_ #H2 destruct
  80 ]
  81 qed-.
  82
  83 (* Basic_1: includes: drop_gen_drop *)
  84 (* Basic_2A1: includes: drop_inv_drop1_lt drop_inv_drop1 *)
  85 lemma drops_inv_drop1: ∀I,K,Y,V,s,t. ⬇*[s, Ⓕ@t] K.ⓑ{I}V ≡ Y → ⬇*[s, t] K ≡ Y.
  86 /2 width=7 by drops_inv_drop1_aux/ qed-.
  87
  88
  89 fact drops_inv_skip1_aux: ∀X,Y,s,t. ⬇*[s, t] X ≡ Y → ∀I,K1,V1,tl. X = K1.ⓑ{I}V1 → t = Ⓣ@tl →
  90                           ∃∃K2,V2. ⬇*[s, tl] K1 ≡ K2 & ⬆*[tl] V2 ≡ V1 & Y = K2.ⓑ{I}V2.
  91 #X #Y #s #t * -X -Y -t
  92 [ #t #Ht #J #K1 #W1 #tl #H destruct
  93 | #I #L1 #L2 #V #t #_ #J #K1 #W1 #tl #_ #H2 destruct
  94 | #I #L1 #L2 #V1 #V2 #t #HL #HV #J #K1 #W1 #tl #H1 #H2 destruct
  95   /2 width=5 by ex3_2_intro/
  96 ]
  97 qed-.
  98
  99 (* Basic_1: includes: drop_gen_skip_l *)
 100 (* Basic_2A1: includes: drop_inv_skip1 *)
 101 lemma drops_inv_skip1: ∀I,K1,V1,Y,s,t. ⬇*[s, Ⓣ@t] K1.ⓑ{I}V1 ≡ Y →
 102                        ∃∃K2,V2. ⬇*[s, t] K1 ≡ K2 & ⬆*[t] V2 ≡ V1 & Y = K2.ⓑ{I}V2.
 103 /2 width=5 by drops_inv_skip1_aux/ qed-.
 104
 105 fact drops_inv_skip2_aux: ∀X,Y,s,t. ⬇*[s, t] X ≡ Y → ∀I,K2,V2,tl. Y = K2.ⓑ{I}V2 → t = Ⓣ@tl →
 106                           ∃∃K1,V1. ⬇*[s, tl] K1 ≡ K2 & ⬆*[tl] V2 ≡ V1 & X = K1.ⓑ{I}V1.
 107 #X #Y #s #t * -X -Y -t
 108 [ #t #Ht #J #K2 #W2 #tl #H destruct
 109 | #I #L1 #L2 #V #t #_ #J #K2 #W2 #tl #_ #H2 destruct
 110 | #I #L1 #L2 #V1 #V2 #t #HL #HV #J #K2 #W2 #tl #H1 #H2 destruct
 111   /2 width=5 by ex3_2_intro/
 112 ]
 113 qed-.
 114
 115 (* Basic_1: includes: drop_gen_skip_r *)
 116 (* Basic_2A1: includes: drop_inv_skip2 *)
 117 lemma drops_inv_skip2: ∀I,X,K2,V2,s,t. ⬇*[s, Ⓣ@t] X ≡ K2.ⓑ{I}V2 →
 118                        ∃∃K1,V1. ⬇*[s, t] K1 ≡ K2 & ⬆*[t] V2 ≡ V1 & X = K1.ⓑ{I}V1.
 119 /2 width=5 by drops_inv_skip2_aux/ qed-.
 120
 121 (* Basic properties *********************************************************)
 122
 123 (* Basic_2A1: includes: drop_FT *)
 124 lemma drops_FT: ∀L1,L2,t. ⬇*[Ⓕ, t] L1 ≡ L2 → ⬇*[Ⓣ, t] L1 ≡ L2.
 125 #L1 #L2 #t #H elim H -L1 -L2 -t
 126 /3 width=1 by drops_atom, drops_drop, drops_skip/
 127 qed.
 128
 129 (* Basic_2A1: includes: drop_gen *)
 130 lemma drops_gen: ∀L1,L2,s,t. ⬇*[Ⓕ, t] L1 ≡ L2 → ⬇*[s, t] L1 ≡ L2.
 131 #L1 #L2 * /2 width=1 by drops_FT/
 132 qed-.
 133
 134 (* Basic_2A1: includes: drop_T *)
 135 lemma drops_T: ∀L1,L2,s,t. ⬇*[s, t] L1 ≡ L2 → ⬇*[Ⓣ, t] L1 ≡ L2.
 136 #L1 #L2 * /2 width=1 by drops_FT/
 137 qed-.
 138
 139 (* Basic forward lemmas *****************************************************)
 140
 141 fact drops_fwd_drop2_aux: ∀X,Y,s,t2. ⬇*[s, t2] X ≡ Y → ∀I,K,V. Y = K.ⓑ{I}V →
 142                           ∃∃t1,t. 𝐈⦃t1⦄ & t2 ⊚ Ⓕ@t1 ≡ t & ⬇*[s, t] X ≡ K.
 143 #X #Y #s #t2 #H elim H -X -Y -t2
 144 [ #t2 #Ht2 #J #K #W #H destruct
 145 | #I #L1 #L2 #V #t2 #_ #IHL #J #K #W #H elim (IHL … H) -IHL
 146   /3 width=5 by after_false, ex3_2_intro, drops_drop/
 147 | #I #L1 #L2 #V1 #V2 #t2 #HL #_ #_ #J #K #W #H destruct
 148   elim (isid_after_dx t2) /3 width=5 by after_true, ex3_2_intro, drops_drop/
 149 ]
 150 qed-.
 151
 152 (* Basic_1: includes: drop_S *)
 153 (* Basic_2A1: includes: drop_fwd_drop2 *)
 154 lemma drops_fwd_drop2: ∀I,X,K,V,s,t2. ⬇*[s, t2] X ≡ K.ⓑ{I}V →
 155                        ∃∃t1,t. 𝐈⦃t1⦄ & t2 ⊚ Ⓕ@t1 ≡ t & ⬇*[s, t] X ≡ K.
 156 /2 width=5 by drops_fwd_drop2_aux/ qed-.
 157
 158 fact drops_after_fwd_drop2_aux: ∀X,Y,s,t2. ⬇*[s, t2] X ≡ Y → ∀I,K,V. Y = K.ⓑ{I}V →
 159                                 ∀t1,t. 𝐈⦃t1⦄ → t2 ⊚ Ⓕ@t1 ≡ t → ⬇*[s, t] X ≡ K.
 160 #X #Y #s #t2 #H elim H -X -Y -t2
 161 [ #t2 #Ht2 #J #K #W #H destruct
 162 | #I #L1 #L2 #V #t2 #_ #IHL #J #K #W #H #t1 #t #Ht1 #Ht elim (after_inv_false1 … Ht) -Ht
 163   /3 width=3 by drops_drop/
 164 | #I #L1 #L2 #V1 #V2 #t2 #HL #_ #_ #J #K #W #H #t1 #t #Ht1 #Ht elim (after_inv_true1 … Ht) -Ht
 165   #u1 #u #b #H1 #H2 #Hu destruct >(after_isid_inv_dx … Hu) -Hu /2 width=1 by drops_drop/
 166 ]
 167 qed-.
 168
 169 lemma drops_after_fwd_drop2: ∀I,X,K,V,s,t2. ⬇*[s, t2] X ≡ K.ⓑ{I}V →
 170                              ∀t1,t. 𝐈⦃t1⦄ → t2 ⊚ Ⓕ@t1 ≡ t → ⬇*[s, t] X ≡ K.
 171 /2 width=9 by drops_after_fwd_drop2_aux/ qed-.
 172
 173 (* Basic_1: includes: drop_gen_refl *)
 174 (* Basic_2A1: includes: drop_inv_O2 *)
 175 lemma drops_fwd_isid: ∀L1,L2,s,t. ⬇*[s, t] L1 ≡ L2 → 𝐈⦃t⦄ → L1 = L2.
 176 #L1 #L2 #s #t #H elim H -L1 -L2 -t //
 177 [ #I #L1 #L2 #V #t #_ #_ #H elim (isid_inv_false … H)
 178 | /5 width=3 by isid_inv_true, lifts_fwd_isid, eq_f3, sym_eq/
 179 ]
 180 qed-.
 181
 182 (* Basic_2A1: removed theorems 13:
 183               drops_inv_nil drops_inv_cons d1_liftable_liftables
 184               drop_inv_O1_pair1 drop_inv_pair1 drop_inv_O1_pair2
 185               drop_inv_Y1 drop_Y1 drop_O_Y drop_fwd_Y2
 186               drop_fwd_length_minus2 drop_fwd_length_minus4
 187 *)
 188 (* Basic_1: removed theorems 53:
 189             drop1_gen_pnil drop1_gen_pcons drop1_getl_trans
 190             drop_ctail drop_skip_flat
 191             cimp_flat_sx cimp_flat_dx cimp_bind cimp_getl_conf
 192             drop_clear drop_clear_O drop_clear_S
 193             clear_gen_sort clear_gen_bind clear_gen_flat clear_gen_flat_r
 194             clear_gen_all clear_clear clear_mono clear_trans clear_ctail clear_cle
 195             getl_ctail_clen getl_gen_tail clear_getl_trans getl_clear_trans
 196             getl_clear_bind getl_clear_conf getl_dec getl_drop getl_drop_conf_lt
 197             getl_drop_conf_ge getl_conf_ge_drop getl_drop_conf_rev
 198             drop_getl_trans_lt drop_getl_trans_le drop_getl_trans_ge
 199             getl_drop_trans getl_flt getl_gen_all getl_gen_sort getl_gen_O
 200             getl_gen_S getl_gen_2 getl_gen_flat getl_gen_bind getl_conf_le
 201             getl_trans getl_refl getl_head getl_flat getl_ctail getl_mono
 202 *)