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