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/grammar/term_vector.ma".
  16 include "Basic_2/substitution/lift.ma".
  17
  18 (* GENERIC RELOCATION *******************************************************)
  19
  20 let rec ss (des:list2 nat nat) ≝ match des with
  21 [ nil2          ⇒ ⟠
  22 | cons2 d e des ⇒ {d + 1, e} :: ss des
  23 ].
  24
  25 inductive lifts: list2 nat nat → relation term ≝
  26 | lifts_nil : ∀T. lifts ⟠ T T
  27 | lifts_cons: ∀T1,T,T2,des,d,e.
  28               ⇧[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} :: des) T1 T2
  29 .
  30
  31 interpretation "generic relocation"
  32    'RLiftStar des T1 T2 = (lifts des T1 T2).
  33
  34 (* Basic inversion lemmas ***************************************************)
  35
  36 fact lifts_inv_nil_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → des = ⟠ → T1 = T2.
  37 #T1 #T2 #des * -T1 -T2 -des //
  38 #T1 #T #T2 #d #e #des #_ #_ #H destruct
  39 qed.
  40
  41 lemma lifts_inv_nil: ∀T1,T2. ⇧*[⟠] T1 ≡ T2 → T1 = T2.
  42 /2 width=3/ qed-.
  43
  44 fact lifts_inv_cons_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 →
  45                          ∀d,e,tl. des = {d, e} :: tl →
  46                          ∃∃T. ⇧[d, e] T1 ≡ T & ⇧*[tl] T ≡ T2.
  47 #T1 #T2 #des * -T1 -T2 -des
  48 [ #T #d #e #tl #H destruct
  49 | #T1 #T #T2 #des #d #e #HT1 #HT2 #hd #he #tl #H destruct
  50   /2 width=3/
  51 qed.
  52
  53 lemma lifts_inv_cons: ∀T1,T2,d,e,des. ⇧*[{d, e} :: des] T1 ≡ T2 →
  54                       ∃∃T. ⇧[d, e] T1 ≡ T & ⇧*[des] T ≡ T2.
  55 /2 width=3/ qed-.
  56
  57 lemma lifts_inv_bind1: ∀I,T2,des,V1,U1. ⇧*[des] 𝕓{I} V1. U1 ≡ T2 →
  58                        ∃∃V2,U2. ⇧*[des] V1 ≡ V2 & ⇧*[ss des] U1 ≡ U2 &
  59                                 T2 = 𝕓{I} V2. U2.
  60 #I #T2 #des elim des -des
  61 [ #V1 #U1 #H
  62   <(lifts_inv_nil … H) -H /2 width=5/
  63 | #d #e #des #IHdes #V1 #U1 #H
  64   elim (lifts_inv_cons … H) -H #X #H #HT2
  65   elim (lift_inv_bind1 … H) -H #V #U #HV1 #HU1 #H destruct
  66   elim (IHdes … HT2) -IHdes -HT2 #V2 #U2 #HV2 #HU2 #H destruct
  67   /3 width=5/
  68 ]
  69 qed-.
  70
  71 lemma lifts_inv_flat1: ∀I,T2,des,V1,U1. ⇧*[des] 𝕗{I} V1. U1 ≡ T2 →
  72                        ∃∃V2,U2. ⇧*[des] V1 ≡ V2 & ⇧*[des] U1 ≡ U2 &
  73                                 T2 = 𝕗{I} V2. U2.
  74 #I #T2 #des elim des -des
  75 [ #V1 #U1 #H
  76   <(lifts_inv_nil … H) -H /2 width=5/
  77 | #d #e #des #IHdes #V1 #U1 #H
  78   elim (lifts_inv_cons … H) -H #X #H #HT2
  79   elim (lift_inv_flat1 … H) -H #V #U #HV1 #HU1 #H destruct
  80   elim (IHdes … HT2) -IHdes -HT2 #V2 #U2 #HV2 #HU2 #H destruct
  81   /3 width=5/
  82 ]
  83 qed-.
  84
  85 (* Basic forward lemmas *****************************************************)
  86
  87 lemma lifts_simple_dx: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝕊[T1] → 𝕊[T2].
  88 #T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_dx/
  89 qed-.
  90
  91 lemma lifts_simple_sn: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝕊[T2] → 𝕊[T1].
  92 #T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_sn/
  93 qed-.
  94
  95 (* Basic properties *********************************************************)
  96
  97 lemma lifts_bind: ∀I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 →
  98                   ∀T1. ⇧*[ss des] T1 ≡ T2 →
  99                   ⇧*[des] 𝕓{I} V1. T1 ≡ 𝕓{I} V2. T2.
 100 #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
 101 [ #V #T1 #H >(lifts_inv_nil … H) -H //
 102 | #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
 103   elim (lifts_inv_cons … H) -H /3 width=3/
 104 ]
 105 qed.
 106
 107 lemma lifts_flat: ∀I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 →
 108                   ∀T1. ⇧*[des] T1 ≡ T2 →
 109                   ⇧*[des] 𝕗{I} V1. T1 ≡ 𝕗{I} V2. T2.
 110 #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
 111 [ #V #T1 #H >(lifts_inv_nil … H) -H //
 112 | #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
 113   elim (lifts_inv_cons … H) -H /3 width=3/
 114 ]
 115 qed.
 116
 117 lemma lifts_total: ∀des,T1. ∃T2. ⇧*[des] T1 ≡ T2.
 118 #des elim des -des /2 width=2/
 119 #d #e #des #IH #T1
 120 elim (lift_total T1 d e) #T #HT1
 121 elim (IH T) -IH /3 width=4/
 122 qed.