matita/matita/contribs/lambdadelta/static_2/relocation/lifts_vector.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 "static_2/syntax/term_vector.ma".
  16 include "static_2/relocation/lifts.ma".
  17
  18 (* GENERIC RELOCATION FOR TERM VECTORS *************************************)
  19
  20 (* Basic_2A1: includes: liftv_nil liftv_cons *)
  21 inductive liftsv (f): relation … ≝
  22 | liftsv_nil : liftsv f (Ⓔ) (Ⓔ)
  23 | liftsv_cons: ∀T1s,T2s,T1,T2.
  24                ⇧*[f] T1 ≘ T2 → liftsv f T1s T2s →
  25                liftsv f (T1 ⨮ T1s) (T2 ⨮ T2s)
  26 .
  27
  28 interpretation "generic relocation (term vector)"
  29    'RLiftStar f T1s T2s = (liftsv f T1s T2s).
  30
  31 interpretation "uniform relocation (term vector)"
  32    'RLift i T1s T2s = (liftsv (pr_uni i) T1s T2s).
  33
  34 (* Basic inversion lemmas ***************************************************)
  35
  36 fact liftsv_inv_nil1_aux (f):
  37      ∀X,Y. ⇧*[f] X ≘ Y → X = Ⓔ → Y = Ⓔ.
  38 #f #X #Y * -X -Y //
  39 #T1s #T2s #T1 #T2 #_ #_ #H destruct
  40 qed-.
  41
  42 (* Basic_2A1: includes: liftv_inv_nil1 *)
  43 lemma liftsv_inv_nil1 (f):
  44       ∀Y. ⇧*[f] Ⓔ ≘ Y → Y = Ⓔ.
  45 /2 width=5 by liftsv_inv_nil1_aux/ qed-.
  46
  47 fact liftsv_inv_cons1_aux (f):
  48      ∀X,Y. ⇧*[f] X ≘ Y → ∀T1,T1s. X = T1 ⨮ T1s →
  49      ∃∃T2,T2s. ⇧*[f] T1 ≘ T2 & ⇧*[f] T1s ≘ T2s & Y = T2 ⨮ T2s.
  50 #f #X #Y * -X -Y
  51 [ #U1 #U1s #H destruct
  52 | #T1s #T2s #T1 #T2 #HT12 #HT12s #U1 #U1s #H destruct /2 width=5 by ex3_2_intro/
  53 ]
  54 qed-.
  55
  56 (* Basic_2A1: includes: liftv_inv_cons1 *)
  57 lemma liftsv_inv_cons1 (f):
  58       ∀T1,T1s,Y. ⇧*[f] T1 ⨮ T1s ≘ Y →
  59       ∃∃T2,T2s. ⇧*[f] T1 ≘ T2 & ⇧*[f] T1s ≘ T2s & Y = T2 ⨮ T2s.
  60 /2 width=3 by liftsv_inv_cons1_aux/ qed-.
  61
  62 fact liftsv_inv_nil2_aux (f):
  63      ∀X,Y. ⇧*[f] X ≘ Y → Y = Ⓔ → X = Ⓔ.
  64 #f #X #Y * -X -Y //
  65 #T1s #T2s #T1 #T2 #_ #_ #H destruct
  66 qed-.
  67
  68 lemma liftsv_inv_nil2 (f):
  69       ∀X. ⇧*[f] X ≘ Ⓔ → X = Ⓔ.
  70 /2 width=5 by liftsv_inv_nil2_aux/ qed-.
  71
  72 fact liftsv_inv_cons2_aux (f):
  73      ∀X,Y. ⇧*[f] X ≘ Y → ∀T2,T2s. Y = T2 ⨮ T2s →
  74      ∃∃T1,T1s. ⇧*[f] T1 ≘ T2 & ⇧*[f] T1s ≘ T2s & X = T1 ⨮ T1s.
  75 #f #X #Y * -X -Y
  76 [ #U2 #U2s #H destruct
  77 | #T1s #T2s #T1 #T2 #HT12 #HT12s #U2 #U2s #H destruct /2 width=5 by ex3_2_intro/
  78 ]
  79 qed-.
  80
  81 lemma liftsv_inv_cons2 (f):
  82       ∀X,T2,T2s. ⇧*[f] X ≘ T2 ⨮ T2s →
  83       ∃∃T1,T1s. ⇧*[f] T1 ≘ T2 & ⇧*[f] T1s ≘ T2s & X = T1 ⨮ T1s.
  84 /2 width=3 by liftsv_inv_cons2_aux/ qed-.
  85
  86 (* Basic_1: was: lifts1_flat (left to right) *)
  87 lemma lifts_inv_applv1 (f):
  88       ∀V1s,U1,T2. ⇧*[f] Ⓐ V1s.U1 ≘ T2 →
  89       ∃∃V2s,U2. ⇧*[f] V1s ≘ V2s & ⇧*[f] U1 ≘ U2 & T2 = Ⓐ V2s.U2.
  90 #f #V1s elim V1s -V1s
  91 [ /3 width=5 by ex3_2_intro, liftsv_nil/
  92 | #V1 #V1s #IHV1s #T1 #X #H elim (lifts_inv_flat1 … H) -H
  93   #V2 #Y #HV12 #HY #H destruct elim (IHV1s … HY) -IHV1s -HY
  94   #V2s #T2 #HV12s #HT12 #H destruct /3 width=5 by ex3_2_intro, liftsv_cons/
  95 ]
  96 qed-.
  97
  98 lemma lifts_inv_applv2 (f):
  99       ∀V2s,U2,T1. ⇧*[f] T1 ≘ Ⓐ V2s.U2 →
 100       ∃∃V1s,U1. ⇧*[f] V1s ≘ V2s & ⇧*[f] U1 ≘ U2 & T1 = Ⓐ V1s.U1.
 101 #f #V2s elim V2s -V2s
 102 [ /3 width=5 by ex3_2_intro, liftsv_nil/
 103 | #V2 #V2s #IHV2s #T2 #X #H elim (lifts_inv_flat2 … H) -H
 104   #V1 #Y #HV12 #HY #H destruct elim (IHV2s … HY) -IHV2s -HY
 105   #V1s #T1 #HV12s #HT12 #H destruct /3 width=5 by ex3_2_intro, liftsv_cons/
 106 ]
 107 qed-.
 108
 109 (* Basic properties *********************************************************)
 110
 111 (* Basic_2A1: includes: liftv_total *)
 112 lemma liftsv_total (f):
 113       ∀T1s. ∃T2s. ⇧*[f] T1s ≘ T2s.
 114 #f #T1s elim T1s -T1s
 115 [ /2 width=2 by liftsv_nil, ex_intro/
 116 | #T1 #T1s * #T2s #HT12s
 117   elim (lifts_total T1 f) /3 width=2 by liftsv_cons, ex_intro/
 118 ]
 119 qed-.
 120
 121 (* Basic_1: was: lifts1_flat (right to left) *)
 122 lemma lifts_applv (f):
 123       ∀V1s,V2s. ⇧*[f] V1s ≘ V2s → ∀T1,T2. ⇧*[f] T1 ≘ T2 →
 124       ⇧*[f] Ⓐ V1s.T1 ≘ Ⓐ V2s.T2.
 125 #f #V1s #V2s #H elim H -V1s -V2s /3 width=1 by lifts_flat/
 126 qed.
 127
 128 lemma liftsv_split_trans (f):
 129       ∀T1s,T2s. ⇧*[f] T1s ≘ T2s → ∀f1,f2. f2 ⊚ f1 ≘ f →
 130       ∃∃Ts. ⇧*[f1] T1s ≘ Ts & ⇧*[f2] Ts ≘ T2s.
 131 #f #T1s #T2s #H elim H -T1s -T2s
 132 [ /2 width=3 by liftsv_nil, ex2_intro/
 133 | #T1s #T2s #T1 #T2 #HT12 #_ #IH #f1 #f2 #Hf
 134   elim (IH … Hf) -IH
 135   elim (lifts_split_trans … HT12 … Hf) -HT12 -Hf
 136   /3 width=5 by liftsv_cons, ex2_intro/
 137 ]
 138 qed-.
 139
 140 (* Basic_1: removed theorems 2: lifts1_nil lifts1_cons *)