matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.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/rliftstar_3.ma".
  16 include "basic_2/substitution/lift.ma".
  17 include "basic_2/multiple/mr2_plus.ma".
  18
  19 (* GENERIC TERM RELOCATION **************************************************)
  20
  21 inductive lifts: list2 nat nat → relation term ≝
  22 | lifts_nil : ∀T. lifts (◊) T T
  23 | lifts_cons: ∀T1,T,T2,des,d,e.
  24               ⬆[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} @ des) T1 T2
  25 .
  26
  27 interpretation "generic relocation (term)"
  28    'RLiftStar des T1 T2 = (lifts des T1 T2).
  29
  30 (* Basic inversion lemmas ***************************************************)
  31
  32 fact lifts_inv_nil_aux: ∀T1,T2,des. ⬆*[des] T1 ≡ T2 → des = ◊ → T1 = T2.
  33 #T1 #T2 #des * -T1 -T2 -des //
  34 #T1 #T #T2 #d #e #des #_ #_ #H destruct
  35 qed-.
  36
  37 lemma lifts_inv_nil: ∀T1,T2. ⬆*[◊] T1 ≡ T2 → T1 = T2.
  38 /2 width=3 by lifts_inv_nil_aux/ qed-.
  39
  40 fact lifts_inv_cons_aux: ∀T1,T2,des. ⬆*[des] T1 ≡ T2 →
  41                          ∀d,e,tl. des = {d, e} @ tl →
  42                          ∃∃T. ⬆[d, e] T1 ≡ T & ⬆*[tl] T ≡ T2.
  43 #T1 #T2 #des * -T1 -T2 -des
  44 [ #T #d #e #tl #H destruct
  45 | #T1 #T #T2 #des #d #e #HT1 #HT2 #hd #he #tl #H destruct
  46   /2 width=3 by ex2_intro/
  47 qed-.
  48
  49 lemma lifts_inv_cons: ∀T1,T2,d,e,des. ⬆*[{d, e} @ des] T1 ≡ T2 →
  50                       ∃∃T. ⬆[d, e] T1 ≡ T & ⬆*[des] T ≡ T2.
  51 /2 width=3 by lifts_inv_cons_aux/ qed-.
  52
  53 (* Basic_1: was: lift1_sort *)
  54 lemma lifts_inv_sort1: ∀T2,k,des. ⬆*[des] ⋆k ≡ T2 → T2 = ⋆k.
  55 #T2 #k #des elim des -des
  56 [ #H <(lifts_inv_nil … H) -H //
  57 | #d #e #des #IH #H
  58   elim (lifts_inv_cons … H) -H #X #H
  59   >(lift_inv_sort1 … H) -H /2 width=1 by/
  60 ]
  61 qed-.
  62
  63 (* Basic_1: was: lift1_lref *)
  64 lemma lifts_inv_lref1: ∀T2,des,i1. ⬆*[des] #i1 ≡ T2 →
  65                        ∃∃i2. @⦃i1, des⦄ ≡ i2 & T2 = #i2.
  66 #T2 #des elim des -des
  67 [ #i1 #H <(lifts_inv_nil … H) -H /2 width=3 by at_nil, ex2_intro/
  68 | #d #e #des #IH #i1 #H
  69   elim (lifts_inv_cons … H) -H #X #H1 #H2
  70   elim (lift_inv_lref1 … H1) -H1 * #Hdi1 #H destruct
  71   elim (IH … H2) -IH -H2 /3 width=3 by at_lt, at_ge, ex2_intro/
  72 ]
  73 qed-.
  74
  75 lemma lifts_inv_gref1: ∀T2,p,des. ⬆*[des] §p ≡ T2 → T2 = §p.
  76 #T2 #p #des elim des -des
  77 [ #H <(lifts_inv_nil … H) -H //
  78 | #d #e #des #IH #H
  79   elim (lifts_inv_cons … H) -H #X #H
  80   >(lift_inv_gref1 … H) -H /2 width=1 by/
  81 ]
  82 qed-.
  83
  84 (* Basic_1: was: lift1_bind *)
  85 lemma lifts_inv_bind1: ∀a,I,T2,des,V1,U1. ⬆*[des] ⓑ{a,I} V1. U1 ≡ T2 →
  86                        ∃∃V2,U2. ⬆*[des] V1 ≡ V2 & ⬆*[des + 1] U1 ≡ U2 &
  87                                 T2 = ⓑ{a,I} V2. U2.
  88 #a #I #T2 #des elim des -des
  89 [ #V1 #U1 #H
  90   <(lifts_inv_nil … H) -H /2 width=5 by ex3_2_intro, lifts_nil/
  91 | #d #e #des #IHdes #V1 #U1 #H
  92   elim (lifts_inv_cons … H) -H #X #H #HT2
  93   elim (lift_inv_bind1 … H) -H #V #U #HV1 #HU1 #H destruct
  94   elim (IHdes … HT2) -IHdes -HT2 #V2 #U2 #HV2 #HU2 #H destruct
  95   /3 width=5 by ex3_2_intro, lifts_cons/
  96 ]
  97 qed-.
  98
  99 (* Basic_1: was: lift1_flat *)
 100 lemma lifts_inv_flat1: ∀I,T2,des,V1,U1. ⬆*[des] ⓕ{I} V1. U1 ≡ T2 →
 101                        ∃∃V2,U2. ⬆*[des] V1 ≡ V2 & ⬆*[des] U1 ≡ U2 &
 102                                 T2 = ⓕ{I} V2. U2.
 103 #I #T2 #des elim des -des
 104 [ #V1 #U1 #H
 105   <(lifts_inv_nil … H) -H /2 width=5 by ex3_2_intro, lifts_nil/
 106 | #d #e #des #IHdes #V1 #U1 #H
 107   elim (lifts_inv_cons … H) -H #X #H #HT2
 108   elim (lift_inv_flat1 … H) -H #V #U #HV1 #HU1 #H destruct
 109   elim (IHdes … HT2) -IHdes -HT2 #V2 #U2 #HV2 #HU2 #H destruct
 110   /3 width=5 by ex3_2_intro, lifts_cons/
 111 ]
 112 qed-.
 113
 114 (* Basic forward lemmas *****************************************************)
 115
 116 lemma lifts_simple_dx: ∀T1,T2,des. ⬆*[des] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
 117 #T1 #T2 #des #H elim H -T1 -T2 -des /3 width=5 by lift_simple_dx/
 118 qed-.
 119
 120 lemma lifts_simple_sn: ∀T1,T2,des. ⬆*[des] T1 ≡ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
 121 #T1 #T2 #des #H elim H -T1 -T2 -des /3 width=5 by lift_simple_sn/
 122 qed-.
 123
 124 (* Basic properties *********************************************************)
 125
 126 lemma lifts_bind: ∀a,I,T2,V1,V2,des. ⬆*[des] V1 ≡ V2 →
 127                   ∀T1. ⬆*[des + 1] T1 ≡ T2 →
 128                   ⬆*[des] ⓑ{a,I} V1. T1 ≡ ⓑ{a,I} V2. T2.
 129 #a #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
 130 [ #V #T1 #H >(lifts_inv_nil … H) -H //
 131 | #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
 132   elim (lifts_inv_cons … H) -H /3 width=3 by lift_bind, lifts_cons/
 133 ]
 134 qed.
 135
 136 lemma lifts_flat: ∀I,T2,V1,V2,des. ⬆*[des] V1 ≡ V2 →
 137                   ∀T1. ⬆*[des] T1 ≡ T2 →
 138                   ⬆*[des] ⓕ{I} V1. T1 ≡ ⓕ{I} V2. T2.
 139 #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
 140 [ #V #T1 #H >(lifts_inv_nil … H) -H //
 141 | #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
 142   elim (lifts_inv_cons … H) -H /3 width=3 by lift_flat, lifts_cons/
 143 ]
 144 qed.
 145
 146 lemma lifts_total: ∀des,T1. ∃T2. ⬆*[des] T1 ≡ T2.
 147 #des elim des -des /2 width=2 by lifts_nil, ex_intro/
 148 #d #e #des #IH #T1 elim (lift_total T1 d e)
 149 #T #HT1 elim (IH T) -IH /3 width=4 by lifts_cons, ex_intro/
 150 qed.