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" 'RLift des T1 T2 = (lifts des T1 T2).
  32
  33 (* Basic inversion lemmas ***************************************************)
  34
  35 fact lifts_inv_nil_aux: ∀T1,T2,des. ⇑[des] T1 ≡ T2 → des = ⟠ → T1 = T2.
  36 #T1 #T2 #des * -T1 -T2 -des //
  37 #T1 #T #T2 #d #e #des #_ #_ #H destruct
  38 qed.
  39
  40 lemma lifts_inv_nil: ∀T1,T2. ⇑[⟠] T1 ≡ T2 → T1 = T2.
  41 /2 width=3/ qed-.
  42
  43 fact lifts_inv_cons_aux: ∀T1,T2,des. ⇑[des] T1 ≡ T2 →
  44                          ∀d,e,tl. des = {d, e} :: tl →
  45                          ∃∃T. ⇑[d, e] T1 ≡ T & ⇑[tl] T ≡ T2.
  46 #T1 #T2 #des * -T1 -T2 -des
  47 [ #T #d #e #tl #H destruct
  48 | #T1 #T #T2 #des #d #e #HT1 #HT2 #hd #he #tl #H destruct
  49   /2 width=3/
  50 qed.
  51
  52 lemma lifts_inv_cons: ∀T1,T2,d,e,des. ⇑[{d, e} :: des] T1 ≡ T2 →
  53                       ∃∃T. ⇑[d, e] T1 ≡ T & ⇑[des] T ≡ T2.
  54 /2 width=3/ qed-.
  55
  56 lemma lifts_inv_bind1: ∀I,T2,des,V1,U1. ⇑[des] 𝕓{I} V1. U1 ≡ T2 →
  57                        ∃∃V2,U2. ⇑[des] V1 ≡ V2 & ⇑[ss des] U1 ≡ U2 &
  58                                 T2 = 𝕓{I} V2. U2.
  59 #I #T2 #des elim des -des
  60 [ #V1 #U1 #H
  61   <(lifts_inv_nil … H) -H /2 width=5/
  62 | #d #e #des #IHdes #V1 #U1 #H
  63   elim (lifts_inv_cons … H) -H #X #H #HT2
  64   elim (lift_inv_bind1 … H) -H #V #U #HV1 #HU1 #H destruct
  65   elim (IHdes … HT2) -IHdes -HT2 #V2 #U2 #HV2 #HU2 #H destruct
  66   /3 width=5/
  67 ]
  68 qed-.
  69
  70 lemma lifts_inv_flat1: ∀I,T2,des,V1,U1. ⇑[des] 𝕗{I} V1. U1 ≡ T2 →
  71                        ∃∃V2,U2. ⇑[des] V1 ≡ V2 & ⇑[des] U1 ≡ U2 &
  72                                 T2 = 𝕗{I} V2. U2.
  73 #I #T2 #des elim des -des
  74 [ #V1 #U1 #H
  75   <(lifts_inv_nil … H) -H /2 width=5/
  76 | #d #e #des #IHdes #V1 #U1 #H
  77   elim (lifts_inv_cons … H) -H #X #H #HT2
  78   elim (lift_inv_flat1 … H) -H #V #U #HV1 #HU1 #H destruct
  79   elim (IHdes … HT2) -IHdes -HT2 #V2 #U2 #HV2 #HU2 #H destruct
  80   /3 width=5/
  81 ]
  82 qed-.
  83
  84 (* Basic forward lemmas *****************************************************)
  85
  86 lemma lifts_simple_dx: ∀T1,T2,des. ⇑[des] T1 ≡ T2 → 𝕊[T1] → 𝕊[T2].
  87 #T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_dx/
  88 qed-.
  89
  90 lemma lifts_simple_sn: ∀T1,T2,des. ⇑[des] T1 ≡ T2 → 𝕊[T2] → 𝕊[T1].
  91 #T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_sn/
  92 qed-.
  93
  94 (* Basic properties *********************************************************)
  95
  96 lemma lifts_bind: ∀I,T2,V1,V2,des. ⇑[des] V1 ≡ V2 →
  97                   ∀T1. ⇑[ss des] T1 ≡ T2 →
  98                   ⇑[des] 𝕓{I} V1. T1 ≡ 𝕓{I} V2. T2.
  99 #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
 100 [ #V #T1 #H >(lifts_inv_nil … H) -H //
 101 | #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
 102   elim (lifts_inv_cons … H) -H /3 width=3/
 103 ]
 104 qed.
 105
 106 lemma lifts_flat: ∀I,T2,V1,V2,des. ⇑[des] V1 ≡ V2 →
 107                   ∀T1. ⇑[des] T1 ≡ T2 →
 108                   ⇑[des] 𝕗{I} V1. T1 ≡ 𝕗{I} V2. T2.
 109 #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
 110 [ #V #T1 #H >(lifts_inv_nil … H) -H //
 111 | #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
 112   elim (lifts_inv_cons … H) -H /3 width=3/
 113 ]
 114 qed.
 115
 116 lemma lifts_total: ∀des,T1. ∃T2. ⇑[des] T1 ≡ T2.
 117 #des elim des -des /2 width=2/
 118 #d #e #des #IH #T1
 119 elim (lift_total T1 d e) #T #HT1
 120 elim (IH T) -IH /3 width=4/
 121 qed.