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 (f): relation (list term) ≝
  22 | liftsv_nil : liftsv f (◊) (◊)
  23 | liftsv_cons: ∀T1c,T2c,T1,T2.
  24                ⬆*[f] T1 ≡ T2 → liftsv f T1c T2c →
  25                liftsv f (T1 @ T1c) (T2 @ T2c)
  26 .
  27
  28 interpretation "generic relocation (vector)"
  29    'RLiftStar f T1c T2c = (liftsv f T1c T2c).
  30
  31 (* Basic inversion lemmas ***************************************************)
  32
  33 fact liftsv_inv_nil1_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → X = ◊ → Y = ◊.
  34 #X #Y #f * -X -Y //
  35 #T1c #T2c #T1 #T2 #_ #_ #H destruct
  36 qed-.
  37
  38 (* Basic_2A1: includes: liftv_inv_nil1 *)
  39 lemma liftsv_inv_nil1: ∀Y,f. ⬆*[f] ◊ ≡ Y → Y = ◊.
  40 /2 width=5 by liftsv_inv_nil1_aux/ qed-.
  41
  42 fact liftsv_inv_cons1_aux: ∀X,Y,f. ⬆*[f] X ≡ Y →
  43                            ∀T1,T1c. X = T1 @ T1c →
  44                            ∃∃T2,T2c. ⬆*[f] T1 ≡ T2 & ⬆*[f] T1c ≡ T2c &
  45                                      Y = T2 @ T2c.
  46 #X #Y #f * -X -Y
  47 [ #U1 #U1c #H destruct
  48 | #T1c #T2c #T1 #T2 #HT12 #HT12c #U1 #U1c #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,T1c,Y,f. ⬆*[f] T1 @ T1c ≡ Y →
  54                         ∃∃T2,T2c. ⬆*[f] T1 ≡ T2 & ⬆*[f] T1c ≡ T2c &
  55                                   Y = T2 @ T2c.
  56 /2 width=3 by liftsv_inv_cons1_aux/ qed-.
  57
  58 fact liftsv_inv_nil2_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → Y = ◊ → X = ◊.
  59 #X #Y #f * -X -Y //
  60 #T1c #T2c #T1 #T2 #_ #_ #H destruct
  61 qed-.
  62
  63 lemma liftsv_inv_nil2: ∀X,f. ⬆*[f] X ≡ ◊ → X = ◊.
  64 /2 width=5 by liftsv_inv_nil2_aux/ qed-.
  65
  66 fact liftsv_inv_cons2_aux: ∀X,Y,f. ⬆*[f] X ≡ Y →
  67                            ∀T2,T2c. Y = T2 @ T2c →
  68                            ∃∃T1,T1c. ⬆*[f] T1 ≡ T2 & ⬆*[f] T1c ≡ T2c &
  69                                      X = T1 @ T1c.
  70 #X #Y #f * -X -Y
  71 [ #U2 #U2c #H destruct
  72 | #T1c #T2c #T1 #T2 #HT12 #HT12c #U2 #U2c #H destruct /2 width=5 by ex3_2_intro/
  73 ]
  74 qed-.
  75
  76 lemma liftsv_inv_cons2: ∀X,T2,T2c,f. ⬆*[f] X ≡ T2 @ T2c →
  77                         ∃∃T1,T1c. ⬆*[f] T1 ≡ T2 & ⬆*[f] T1c ≡ T2c &
  78                                   X = T1 @ T1c.
  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: ∀V1c,U1,T2,f. ⬆*[f] Ⓐ V1c.U1 ≡ T2 →
  83                         ∃∃V2c,U2. ⬆*[f] V1c ≡ V2c & ⬆*[f] U1 ≡ U2 &
  84                                   T2 = Ⓐ V2c.U2.
  85 #V1c elim V1c -V1c
  86 [ /3 width=5 by ex3_2_intro, liftsv_nil/
  87 | #V1 #V1c #IHV1c #T1 #X #f #H elim (lifts_inv_flat1 … H) -H
  88   #V2 #Y #HV12 #HY #H destruct elim (IHV1c … HY) -IHV1c -HY
  89   #V2c #T2 #HV12c #HT12 #H destruct /3 width=5 by ex3_2_intro, liftsv_cons/
  90 ]
  91 qed-.
  92
  93 lemma lifts_inv_applv2: ∀V2c,U2,T1,f. ⬆*[f] T1 ≡ Ⓐ V2c.U2 →
  94                         ∃∃V1c,U1. ⬆*[f] V1c ≡ V2c & ⬆*[f] U1 ≡ U2 &
  95                                   T1 = Ⓐ V1c.U1.
  96 #V2c elim V2c -V2c
  97 [ /3 width=5 by ex3_2_intro, liftsv_nil/
  98 | #V2 #V2c #IHV2c #T2 #X #f #H elim (lifts_inv_flat2 … H) -H
  99   #V1 #Y #HV12 #HY #H destruct elim (IHV2c … HY) -IHV2c -HY
 100   #V1c #T1 #HV12c #HT12 #H destruct /3 width=5 by ex3_2_intro, liftsv_cons/
 101 ]
 102 qed-.
 103
 104 (* Basic properties *********************************************************)
 105
 106 (* Basic_2A1: includes: liftv_total *)
 107 lemma liftsv_total: ∀f. ∀T1c:list term. ∃T2c. ⬆*[f] T1c ≡ T2c.
 108 #f #T1c elim T1c -T1c
 109 [ /2 width=2 by liftsv_nil, ex_intro/
 110 | #T1 #T1c * #T2c #HT12c
 111   elim (lifts_total T1 f) /3 width=2 by liftsv_cons, ex_intro/
 112 ]
 113 qed-.
 114
 115 (* Basic_1: was: lifts1_flat (right to left) *)
 116 lemma lifts_applv: ∀V1c,V2c,f. ⬆*[f] V1c ≡ V2c →
 117                    ∀T1,T2. ⬆*[f] T1 ≡ T2 →
 118                    ⬆*[f] Ⓐ V1c. T1 ≡ Ⓐ V2c. T2.
 119 #V1c #V2c #f #H elim H -V1c -V2c /3 width=1 by lifts_flat/
 120 qed.
 121
 122 (* Basic_1: removed theorems 2: lifts1_nil lifts1_cons *)