matita/matita/contribs/lambdadelta/ground/relocation/gr_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/notation/relations/rafter_3.ma".
  16 include "ground/xoa/ex_3_2.ma".
  17 include "ground/relocation/gr_tl.ma".
  18
  19 (* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
  20
  21 (*** after *)
  22 coinductive gr_after: relation3 gr_map gr_map gr_map ≝
  23 (*** after_refl *)
  24 | gr_after_refl (f1) (f2) (f) (g1) (g2) (g):
  25   gr_after f1 f2 f → ⫯f1 = g1 → ⫯f2 = g2 → ⫯f = g → gr_after g1 g2 g
  26 (*** after_push *)
  27 | gr_after_push (f1) (f2) (f) (g1) (g2) (g):
  28   gr_after f1 f2 f → ⫯f1 = g1 → ↑f2 = g2 → ↑f = g → gr_after g1 g2 g
  29 (*** after_next *)
  30 | gr_after_next (f1) (f2) (f) (g1) (g):
  31   gr_after f1 f2 f → ↑f1 = g1 → ↑f = g → gr_after g1 f2 g
  32 .
  33
  34 interpretation
  35   "relational composition (generic relocation maps)"
  36   'RAfter f1 f2 f = (gr_after f1 f2 f).
  37
  38 (* Basic inversions *********************************************************)
  39
  40 (*** after_inv_ppx *)
  41 lemma gr_after_inv_push_bi:
  42       ∀g1,g2,g. g1 ⊚ g2 ≘ g → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 →
  43       ∃∃f. f1 ⊚ f2 ≘ f & ⫯f = g.
  44 #g1 #g2 #g * -g1 -g2 -g #f1 #f2 #f #g1
  45 [ #g2 #g #Hf #H1 #H2 #H #x1 #x2 #Hx1 #Hx2 destruct
  46   >(eq_inv_gr_push_bi … Hx1) >(eq_inv_gr_push_bi … Hx2) -x2 -x1
  47   /2 width=3 by ex2_intro/
  48 | #g2 #g #_ #_ #H2 #_ #x1 #x2 #_ #Hx2 destruct
  49   elim (eq_inv_gr_push_next … Hx2)
  50 | #g #_ #H1 #_ #x1 #x2 #Hx1 #_ destruct
  51   elim (eq_inv_gr_push_next … Hx1)
  52 ]
  53 qed-.
  54
  55 (*** after_inv_pnx *)
  56 lemma gr_after_inv_push_next:
  57       ∀g1,g2,g. g1 ⊚ g2 ≘ g → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 →
  58       ∃∃f. f1 ⊚ f2 ≘ f & ↑f = g.
  59 #g1 #g2 #g * -g1 -g2 -g #f1 #f2 #f #g1
  60 [ #g2 #g #_ #_ #H2 #_ #x1 #x2 #_ #Hx2 destruct
  61   elim (eq_inv_gr_next_push … Hx2)
  62 | #g2 #g #Hf #H1 #H2 #H3 #x1 #x2 #Hx1 #Hx2 destruct
  63   >(eq_inv_gr_push_bi … Hx1) >(eq_inv_gr_next_bi … Hx2) -x2 -x1
  64   /2 width=3 by ex2_intro/
  65 | #g #_ #H1 #_ #x1 #x2 #Hx1 #_ destruct
  66   elim (eq_inv_gr_push_next … Hx1)
  67 ]
  68 qed-.
  69
  70 (*** after_inv_nxx *)
  71 lemma gr_after_inv_next_sn:
  72       ∀g1,f2,g. g1 ⊚ f2 ≘ g → ∀f1. ↑f1 = g1 →
  73       ∃∃f. f1 ⊚ f2 ≘ f & ↑f = g.
  74 #g1 #f2 #g * -g1 -f2 -g #f1 #f2 #f #g1
  75 [ #g2 #g #_ #H1 #_ #_ #x1 #Hx1 destruct
  76   elim (eq_inv_gr_next_push … Hx1)
  77 | #g2 #g #_ #H1 #_ #_ #x1 #Hx1 destruct
  78   elim (eq_inv_gr_next_push … Hx1)
  79 | #g #Hf #H1 #H #x1 #Hx1 destruct
  80   >(eq_inv_gr_next_bi … Hx1) -x1
  81   /2 width=3 by ex2_intro/
  82 ]
  83 qed-.
  84
  85 (* Advanced inversions ******************************************************)
  86
  87 (*** after_inv_ppp *)
  88 lemma gr_after_inv_push_bi_push:
  89       ∀g1,g2,g. g1 ⊚ g2 ≘ g →
  90       ∀f1,f2,f. ⫯f1 = g1 → ⫯f2 = g2 → ⫯f = g → f1 ⊚ f2 ≘ f.
  91 #g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (gr_after_inv_push_bi … Hg … H1 H2) -g1 -g2
  92 #x #Hf #Hx destruct <(eq_inv_gr_push_bi … Hx) -f //
  93 qed-.
  94
  95 (*** after_inv_ppn *)
  96 lemma gr_after_inv_push_bi_next:
  97       ∀g1,g2,g. g1 ⊚ g2 ≘ g →
  98       ∀f1,f2,f. ⫯f1 = g1 → ⫯f2 = g2 → ↑f = g → ⊥.
  99 #g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (gr_after_inv_push_bi … Hg … H1 H2) -g1 -g2
 100 #x #Hf #Hx destruct elim (eq_inv_gr_push_next … Hx)
 101 qed-.
 102
 103 (*** after_inv_pnn *)
 104 lemma gr_after_inv_push_next_next:
 105       ∀g1,g2,g. g1 ⊚ g2 ≘ g →
 106       ∀f1,f2,f. ⫯f1 = g1 → ↑f2 = g2 → ↑f = g → f1 ⊚ f2 ≘ f.
 107 #g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (gr_after_inv_push_next … Hg … H1 H2) -g1 -g2
 108 #x #Hf #Hx destruct <(eq_inv_gr_next_bi … Hx) -f //
 109 qed-.
 110
 111 (*** after_inv_pnp *)
 112 lemma gr_after_inv_push_next_push:
 113       ∀g1,g2,g. g1 ⊚ g2 ≘ g →
 114       ∀f1,f2,f. ⫯f1 = g1 → ↑f2 = g2 → ⫯f = g → ⊥.
 115 #g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (gr_after_inv_push_next … Hg … H1 H2) -g1 -g2
 116 #x #Hf #Hx destruct elim (eq_inv_gr_next_push … Hx)
 117 qed-.
 118
 119 (*** after_inv_nxn *)
 120 lemma gr_after_inv_next_sn_next:
 121       ∀g1,f2,g. g1 ⊚ f2 ≘ g →
 122       ∀f1,f. ↑f1 = g1 → ↑f = g → f1 ⊚ f2 ≘ f.
 123 #g1 #f2 #g #Hg #f1 #f #H1 #H elim (gr_after_inv_next_sn … Hg … H1) -g1
 124 #x #Hf #Hx destruct <(eq_inv_gr_next_bi … Hx) -f //
 125 qed-.
 126
 127 (*** after_inv_nxp *)
 128 lemma gr_after_inv_next_sn_push:
 129       ∀g1,f2,g. g1 ⊚ f2 ≘ g →
 130       ∀f1,f. ↑f1 = g1 → ⫯f = g → ⊥.
 131 #g1 #f2 #g #Hg #f1 #f #H1 #H elim (gr_after_inv_next_sn … Hg … H1) -g1
 132 #x #Hf #Hx destruct elim (eq_inv_gr_next_push … Hx)
 133 qed-.
 134
 135 (*** after_inv_pxp *)
 136 lemma gr_after_inv_push_sn_push:
 137       ∀g1,g2,g. g1 ⊚ g2 ≘ g →
 138       ∀f1,f. ⫯f1 = g1 → ⫯f = g →
 139       ∃∃f2. f1 ⊚ f2 ≘ f & ⫯f2 = g2.
 140 #g1 #g2 elim (gr_map_split_tl g2)
 141 #Hg2 #g #Hg #f1 #f #H1 #H
 142 [ lapply (gr_after_inv_push_bi_push … Hg … H1 … H) -g1 -g
 143   /2 width=3 by ex2_intro/
 144 | elim (gr_after_inv_push_next_push … Hg … H1 … H) -g1 -g -f1 -f //
 145 ]
 146 qed-.
 147
 148 (*** after_inv_pxn *)
 149 lemma gr_after_inv_push_sn_next:
 150       ∀g1,g2,g. g1 ⊚ g2 ≘ g →
 151       ∀f1,f. ⫯f1 = g1 → ↑f = g →
 152       ∃∃f2. f1 ⊚ f2 ≘ f & ↑f2 = g2.
 153 #g1 #g2 elim (gr_map_split_tl g2)
 154 #Hg2 #g #Hg #f1 #f #H1 #H
 155 [ elim (gr_after_inv_push_bi_next … Hg … H1 … H) -g1 -g -f1 -f //
 156 | lapply (gr_after_inv_push_next_next … Hg … H1 … H) -g1 -g
 157   /2 width=3 by ex2_intro/
 158 ]
 159 qed-.
 160
 161 (*** after_inv_xxp *)
 162 lemma gr_after_inv_push:
 163       ∀g1,g2,g. g1 ⊚ g2 ≘ g → ∀f. ⫯f = g →
 164       ∃∃f1,f2. f1 ⊚ f2 ≘ f & ⫯f1 = g1 & ⫯f2 = g2.
 165 #g1 elim (gr_map_split_tl g1)
 166 #Hg1 #g2 #g #Hg #f #H
 167 [ elim (gr_after_inv_push_sn_push … Hg … H) -g /2 width=5 by ex3_2_intro/
 168 | elim (gr_after_inv_next_sn_push … Hg … H) -g2 -g -f //
 169 ]
 170 qed-.
 171
 172 (*** after_inv_xxn *)
 173 lemma gr_after_inv_next:
 174       ∀g1,g2,g. g1 ⊚ g2 ≘ g → ∀f. ↑f = g →
 175       ∨∨ ∃∃f1,f2. f1 ⊚ f2 ≘ f & ⫯f1 = g1 & ↑f2 = g2
 176        | ∃∃f1. f1 ⊚ g2 ≘ f & ↑f1 = g1.
 177 #g1 elim (gr_map_split_tl g1)
 178 #Hg1 #g2 #g #Hg #f #H
 179 [ elim (gr_after_inv_push_sn_next … Hg … H) -g
 180   /3 width=5 by or_introl, ex3_2_intro/
 181 | /4 width=5 by gr_after_inv_next_sn_next, or_intror, ex2_intro/
 182 ]
 183 qed-.
 184
 185 (*** after_inv_pxx *)
 186 lemma gr_after_inv_push_sn:
 187       ∀g1,g2,g. g1 ⊚ g2 ≘ g → ∀f1. ⫯f1 = g1 →
 188       ∨∨ ∃∃f2,f. f1 ⊚ f2 ≘ f & ⫯f2 = g2 & ⫯f = g
 189        | ∃∃f2,f. f1 ⊚ f2 ≘ f & ↑f2 = g2 & ↑f = g.
 190 #g1 #g2 elim (gr_map_split_tl g2)
 191 #Hg2 #g #Hg #f1 #H
 192 [ elim (gr_after_inv_push_bi … Hg … H) -g1
 193   /3 width=5 by or_introl, ex3_2_intro/
 194 | elim (gr_after_inv_push_next … Hg … H) -g1
 195   /3 width=5 by or_intror, ex3_2_intro/
 196 ]
 197 qed-.