matita/matita/contribs/lambdadelta/ground_2/relocation/trace_after.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 "ground_2/notation/relations/rafter_3.ma".
  16 include "ground_2/relocation/trace_at.ma".
  17
  18 (* RELOCATION TRACE *********************************************************)
  19
  20 inductive after: relation3 trace trace trace ≝
  21    | after_empty: after (◊) (◊) (◊)
  22    | after_true : ∀cs1,cs2,cs. after cs1 cs2 cs →
  23                   ∀b. after (Ⓣ @ cs1) (b @ cs2) (b @ cs)
  24    | after_false: ∀cs1,cs2,cs. after cs1 cs2 cs →
  25                   after (Ⓕ @ cs1) cs2 (Ⓕ @ cs).
  26
  27 interpretation "composition (trace)"
  28    'RAfter cs1 cs2 cs = (after cs1 cs2 cs).
  29
  30 (* Basic inversion lemmas ***************************************************)
  31
  32 fact after_inv_empty1_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → cs1 = ◊ →
  33                            cs2 = ◊ ∧ cs = ◊.
  34 #cs1 #cs2 #cs * -cs1 -cs2 -cs
  35 [ /2 width=1 by conj/
  36 | #cs1 #cs2 #cs #_ #b #H destruct
  37 | #cs1 #cs2 #cs #_ #H destruct
  38 ]
  39 qed-.
  40
  41 lemma after_inv_empty1: ∀cs2,cs. ◊ ⊚ cs2 ≡ cs → cs2 = ◊ ∧ cs = ◊.
  42 /2 width=3 by after_inv_empty1_aux/ qed-.
  43
  44 fact after_inv_true1_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → ∀tl1. cs1 = Ⓣ @ tl1 →
  45                           ∃∃tl2,tl,b. cs2 = b @ tl2 & cs = b @ tl & tl1 ⊚ tl2 ≡ tl.
  46 #cs1 #cs2 #cs * -cs1 -cs2 -cs
  47 [ #tl1 #H destruct
  48 | #cs1 #cs2 #cs #H12 #b #tl1 #H destruct
  49   /2 width=6 by ex3_3_intro/
  50 | #cs1 #cs2 #cs #_ #tl1 #H destruct
  51 ]
  52 qed-.
  53
  54 lemma after_inv_true1: ∀tl1,cs2,cs. (Ⓣ @ tl1) ⊚ cs2 ≡ cs →
  55                        ∃∃tl2,tl,b. cs2 = b @ tl2 & cs = b @ tl & tl1 ⊚ tl2 ≡ tl.
  56 /2 width=3 by after_inv_true1_aux/ qed-.
  57
  58 fact after_inv_false1_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → ∀tl1. cs1 = Ⓕ @ tl1 →
  59                            ∃∃tl. cs = Ⓕ @ tl & tl1 ⊚ cs2 ≡ tl.
  60 #cs1 #cs2 #cs * -cs1 -cs2 -cs
  61 [ #tl1 #H destruct
  62 | #cs1 #cs2 #cs #_ #b #tl1 #H destruct
  63 | #cs1 #cs2 #cs #H12 #tl1 #H destruct
  64   /2 width=3 by ex2_intro/
  65 ]
  66 qed-.
  67
  68 lemma after_inv_false1: ∀tl1,cs2,cs. (Ⓕ @ tl1) ⊚ cs2 ≡ cs →
  69                         ∃∃tl. cs = Ⓕ @ tl & tl1 ⊚ cs2 ≡ tl.
  70 /2 width=3 by after_inv_false1_aux/ qed-.
  71
  72 fact after_inv_empty3_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → cs = ◊ →
  73                            cs1 = ◊ ∧ cs2 = ◊.
  74 #cs1 #cs2 #cs * -cs1 -cs2 -cs
  75 [ /2 width=1 by conj/
  76 | #cs1 #cs2 #cs #_ #b #H destruct
  77 | #cs1 #cs2 #cs #_ #H destruct
  78 ]
  79 qed-.
  80
  81 lemma after_inv_empty3: ∀cs1,cs2. cs1 ⊚ cs2 ≡ ◊ → cs1 = ◊ ∧ cs2 = ◊.
  82 /2 width=3 by after_inv_empty3_aux/ qed-.
  83
  84 fact after_inv_inh3_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → ∀tl,b. cs = b @ tl →
  85                          (∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = b @ tl2 & tl1 ⊚ tl2 ≡ tl) ∨
  86                          ∃∃tl1.  cs1 = Ⓕ @ tl1 & b = Ⓕ & tl1 ⊚ cs2 ≡ tl.
  87 #cs1 #cs2 #cs * -cs1 -cs2 -cs
  88 [ #tl #b #H destruct
  89 | #cs1 #cs2 #cs #H12 #b0 #tl #b #H destruct
  90   /3 width=5 by ex3_2_intro, or_introl/
  91 | #cs1 #cs2 #cs #H12 #tl #b #H destruct
  92   /3 width=3 by ex3_intro, or_intror/
  93 ]
  94 qed-.
  95
  96 lemma after_inv_inh3: ∀cs1,cs2,tl,b. cs1 ⊚ cs2 ≡ b @ tl →
  97                       (∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = b @ tl2 & tl1 ⊚ tl2 ≡ tl) ∨
  98                       ∃∃tl1.  cs1 = Ⓕ @ tl1 & b = Ⓕ & tl1 ⊚ cs2 ≡ tl.
  99 /2 width=3 by after_inv_inh3_aux/ qed-.
 100
 101 (* Basic forward lemmas *****************************************************)
 102
 103 lemma after_at_fwd: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → ∀i1,i. @⦃i1, cs⦄ ≡ i →
 104                     ∃∃i2. @⦃i1, cs1⦄ ≡ i2 & @⦃i2, cs2⦄ ≡ i.
 105 #cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs
 106 [ #i1 #i #H elim (at_inv_empty … H)
 107 | #cs1 #cs2 #cs #_ * #IH #i1 #i #H
 108   [ elim (at_inv_true … H) -H *
 109     [ -IH #H1 #H2 destruct /2 width=3 by at_zero, ex2_intro/
 110     | #j1 #j #H1 #H2 #Hj1 destruct
 111       elim (IH … Hj1) -IH -Hj1 /3 width=3 by at_succ, ex2_intro/
 112     ]
 113   | elim (at_inv_false … H) -H
 114     #j #H #Hj destruct
 115     elim (IH … Hj) -IH -Hj /3 width=3 by at_succ, at_false, ex2_intro/
 116   ]
 117 | #cs1 #cs2 #cs #_ #IH #i1 #i #H elim (at_inv_false … H) -H
 118   #j #H #Hj destruct
 119   elim (IH … Hj) -IH -Hj /3 width=3 by at_false, ex2_intro/
 120 ]
 121 qed-.
 122
 123 lemma after_fwd_at: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → ∀i1,i2. @⦃i1, cs1⦄ ≡ i2 →
 124                     ∃∃i. @⦃i2, cs2⦄ ≡ i & @⦃i1, cs⦄ ≡ i.
 125 #cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs
 126 [ #i1 #i2 #H elim (at_inv_empty … H)
 127 | #cs1 #cs2 #cs #_ * #IH #i1 #i2 #H
 128   [ elim (at_inv_true … H) -H *
 129     [ -IH #H1 #H2 destruct /2 width=3 by at_zero, ex2_intro/
 130     | #j1 #j2 #H1 #H2 #Hj12 destruct
 131       elim (IH … Hj12) -IH -Hj12 /3 width=3 by at_succ, ex2_intro/
 132     ]
 133   | elim (at_inv_false … H) -H
 134     #j2 #H #Hj2 destruct
 135     elim (IH … Hj2) -IH -Hj2 /3 width=3 by at_succ, at_false, ex2_intro/
 136   ]
 137 | #cs1 #cs2 #cs #_ #IH #i1 #i2 #H elim (IH … H) -IH -H
 138   /3 width=3 by at_false, ex2_intro/
 139 ]
 140 qed-.
 141
 142 (* Main properties **********************************************************)
 143
 144 theorem after_trans1: ∀cs1,cs2,cs0. cs1 ⊚ cs2 ≡ cs0 →
 145                       ∀cs3, cs4. cs0 ⊚ cs3 ≡ cs4 →
 146                       ∃∃cs. cs2 ⊚ cs3 ≡ cs & cs1 ⊚ cs ≡ cs4.
 147 #cs1 #cs2 #cs0 #H elim H -cs1 -cs2 -cs0
 148 [ #cs3 #cs4 #H elim (after_inv_empty1 … H) -H
 149   #H1 #H2 destruct /2 width=3 by ex2_intro, after_empty/
 150 | #cs1 #cs2 #cs0 #_ * #IH #cs3 #cs4 #H
 151   [ elim (after_inv_true1 … H) -H
 152     #tl3 #tl4 #b #H1 #H2 #Htl destruct
 153     elim (IH … Htl) -cs0
 154     /3 width=3 by ex2_intro, after_true/
 155   | elim (after_inv_false1 … H) -H
 156     #tl4 #H #Htl destruct
 157     elim (IH … Htl) -cs0
 158     /3 width=3 by ex2_intro, after_true, after_false/
 159   ]
 160 | #cs1 #cs2 #cs0 #_ #IH #cs3 #cs4 #H
 161   elim (after_inv_false1 … H) -H
 162   #tl4 #H #Htl destruct
 163   elim (IH … Htl) -cs0
 164   /3 width=3 by ex2_intro, after_false/
 165 ]
 166 qed-.
 167
 168 theorem after_trans2: ∀cs1,cs0,cs4. cs1 ⊚ cs0 ≡ cs4 →
 169                       ∀cs2, cs3. cs2 ⊚ cs3 ≡ cs0 →
 170                       ∃∃cs. cs1 ⊚ cs2 ≡ cs & cs ⊚ cs3 ≡ cs4.
 171 #cs1 #cs0 #cs4 #H elim H -cs1 -cs0 -cs4
 172 [ #cs2 #cs3 #H elim (after_inv_empty3 … H) -H
 173   #H1 #H2 destruct /2 width=3 by ex2_intro, after_empty/
 174 | #cs1 #cs0 #cs4 #_ #b #IH #cs2 #cs3 #H elim (after_inv_inh3 … H) -H *
 175   [ #tl2 #tl3 #H1 #H2 #Htl destruct
 176     elim (IH … Htl) -cs0
 177     /3 width=3 by ex2_intro, after_true/
 178   | #tl2 #H1 #H2 #Htl destruct
 179     elim (IH … Htl) -cs0
 180     /3 width=3 by ex2_intro, after_true, after_false/
 181   ]
 182 | #cs1 #cs0 #cs4 #_ #IH #cs2 #cs3 #H elim (IH … H) -cs0
 183   /3 width=3 by ex2_intro, after_false/
 184 ]
 185 qed-.
 186
 187 theorem after_mono: ∀cs1,cs2,x. cs1 ⊚ cs2 ≡ x → ∀y. cs1 ⊚ cs2 ≡ y → x = y.
 188 #cs1 #cs2 #x #H elim H -cs1 -cs2 -x
 189 [ #y #H elim (after_inv_empty1 … H) -H //
 190 | #cs1 #cs #x #_ #b #IH #y #H elim (after_inv_true1 … H) -H
 191   #tl #tly #b0 #H1 #H2 #Htl destruct >(IH … Htl) -tl -cs1 -x //
 192 | #cs1 #cs2 #x #_ #IH #y #H elim (after_inv_false1 … H) -H
 193   #tly #H #Htl destruct >(IH … Htl) -cs1 -cs2 -x //
 194 ]
 195 qed-.
 196
 197 theorem after_inj: ∀cs1,x,cs. cs1 ⊚ x ≡ cs → ∀y. cs1 ⊚ y ≡ cs → x = y.
 198 #cs1 #x #cs #H elim H -cs1 -x -cs
 199 [ #y #H elim (after_inv_empty1 … H) -H //
 200 | #cs1 #x #cs #_ #b #IH #y #H elim (after_inv_true1 … H) -H
 201   #tly #tl #b0 #H1 #H2 #Htl destruct >(IH … Htl) -tl -cs1 -x //
 202 | #cs1 #x #cs #_ #IH #y #H elim (after_inv_false1 … H) -H
 203   #tl #H #Htl destruct >(IH … Htl) -tl -cs1 -x //
 204 ]
 205 qed-.