matita/matita/contribs/lambdadelta/basic_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 "basic_2/grammar/term_vector.ma".
  16 include "basic_2/relocation/lifts.ma".
  17
  18 (* GENERIC RELOCATION FOR TERM VECTORS *************************************)
  19
  20 (* Basic_2A1: includes: liftv_nil liftv_cons *)
  21 inductive liftsv (t:trace) : relation (list term) ≝
  22 | liftsv_nil : liftsv t (◊) (◊)
  23 | liftsv_cons: ∀T1s,T2s,T1,T2.
  24                ⬆*[t] T1 ≡ T2 → liftsv t T1s T2s →
  25                liftsv t (T1 @ T1s) (T2 @ T2s)
  26 .
  27
  28 interpretation "generic relocation (vector)"
  29    'RLiftStar t T1s T2s = (liftsv t T1s T2s).
  30
  31 (* Basic inversion lemmas ***************************************************)
  32
  33 fact liftsv_inv_nil1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → X = ◊ → Y = ◊.
  34 #X #Y #t * -X -Y //
  35 #T1s #T2s #T1 #T2 #_ #_ #H destruct
  36 qed-.
  37
  38 (* Basic_2A1: includes: liftv_inv_nil1 *)
  39 lemma liftsv_inv_nil1: ∀Y,t. ⬆*[t] ◊ ≡ Y → Y = ◊.
  40 /2 width=5 by liftsv_inv_nil1_aux/ qed-.
  41
  42 fact liftsv_inv_cons1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y →
  43                            ∀T1,T1s. X = T1 @ T1s →
  44                            ∃∃T2,T2s. ⬆*[t] T1 ≡ T2 & ⬆*[t] T1s ≡ T2s &
  45                                      Y = T2 @ T2s.
  46 #X #Y #t * -X -Y
  47 [ #U1 #U1s #H destruct
  48 | #T1s #T2s #T1 #T2 #HT12 #HT12s #U1 #U1s #H destruct /2 width=5 by ex3_2_intro/
  49 ]
  50 qed-.
  51
  52 (* Basic_2A1: includes: liftv_inv_cons1 *)
  53 lemma liftsv_inv_cons1: ∀T1,T1s,Y,t. ⬆*[t] T1 @ T1s ≡ Y →
  54                         ∃∃T2,T2s. ⬆*[t] T1 ≡ T2 & ⬆*[t] T1s ≡ T2s &
  55                                   Y = T2 @ T2s.
  56 /2 width=3 by liftsv_inv_cons1_aux/ qed-.
  57
  58 fact liftsv_inv_nil2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → Y = ◊ → X = ◊.
  59 #X #Y #t * -X -Y //
  60 #T1s #T2s #T1 #T2 #_ #_ #H destruct
  61 qed-.
  62
  63 lemma liftsv_inv_nil2: ∀X,t. ⬆*[t] X ≡ ◊ → X = ◊.
  64 /2 width=5 by liftsv_inv_nil2_aux/ qed-.
  65
  66 fact liftsv_inv_cons2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y →
  67                            ∀T2,T2s. Y = T2 @ T2s →
  68                            ∃∃T1,T1s. ⬆*[t] T1 ≡ T2 & ⬆*[t] T1s ≡ T2s &
  69                                      X = T1 @ T1s.
  70 #X #Y #t * -X -Y
  71 [ #U2 #U2s #H destruct
  72 | #T1s #T2s #T1 #T2 #HT12 #HT12s #U2 #U2s #H destruct /2 width=5 by ex3_2_intro/
  73 ]
  74 qed-.
  75
  76 lemma liftsv_inv_cons2: ∀X,T2,T2s,t. ⬆*[t] X ≡ T2 @ T2s →
  77                         ∃∃T1,T1s. ⬆*[t] T1 ≡ T2 & ⬆*[t] T1s ≡ T2s &
  78                                   X = T1 @ T1s.
  79 /2 width=3 by liftsv_inv_cons2_aux/ qed-.
  80
  81 (* Basic_1: was: lifts1_flat (left to right) *)
  82 lemma lifts_inv_applv1: ∀V1s,U1,T2,t. ⬆*[t] Ⓐ V1s.U1 ≡ T2 →
  83                         ∃∃V2s,U2. ⬆*[t] V1s ≡ V2s & ⬆*[t] U1 ≡ U2 &
  84                                   T2 = Ⓐ V2s.U2.
  85 #V1s elim V1s -V1s
  86 [ /3 width=5 by ex3_2_intro, liftsv_nil/
  87 | #V1 #V1s #IHV1s #T1 #X #t #H elim (lifts_inv_flat1 … H) -H
  88   #V2 #Y #HV12 #HY #H destruct elim (IHV1s … HY) -IHV1s -HY
  89   #V2s #T2 #HV12s #HT12 #H destruct /3 width=5 by ex3_2_intro, liftsv_cons/
  90 ]
  91 qed-.
  92
  93 lemma lifts_inv_applv2: ∀V2s,U2,T1,t. ⬆*[t] T1 ≡ Ⓐ V2s.U2 →
  94                         ∃∃V1s,U1. ⬆*[t] V1s ≡ V2s & ⬆*[t] U1 ≡ U2 &
  95                                   T1 = Ⓐ V1s.U1.
  96 #V2s elim V2s -V2s
  97 [ /3 width=5 by ex3_2_intro, liftsv_nil/
  98 | #V2 #V2s #IHV2s #T2 #X #t #H elim (lifts_inv_flat2 … H) -H
  99   #V1 #Y #HV12 #HY #H destruct elim (IHV2s … HY) -IHV2s -HY
 100   #V1s #T1 #HV12s #HT12 #H destruct /3 width=5 by ex3_2_intro, liftsv_cons/
 101 ]
 102 qed-.
 103
 104 (* Basic properties *********************************************************)
 105
 106 (* Basic_1: was: lifts1_flat (right to left) *)
 107 lemma lifts_applv: ∀V1s,V2s,t. ⬆*[t] V1s ≡ V2s →
 108                    ∀T1,T2. ⬆*[t] T1 ≡ T2 →
 109                    ⬆*[t] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2.
 110 #V1s #V2s #t #H elim H -V1s -V2s /3 width=1 by lifts_flat/
 111 qed.
 112
 113 (* Basic_2A1: removed theorems 1: liftv_total *)
 114 (* Basic_1: removed theorems 2: lifts1_nil lifts1_cons *)