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