matita/matita/contribs/lambdadelta/ground/relocation/pr_sor.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/runion_3.ma".
  16 include "ground/xoa/or_3.ma".
  17 include "ground/xoa/ex_3_2.ma".
  18 include "ground/relocation/pr_tl.ma".
  19
  20 (* RELATIONAL UNION FOR PARTIAL RELOCATION MAPS *****************************)
  21
  22 (*** sor *)
  23 coinductive pr_sor: relation3 pr_map pr_map pr_map ≝
  24 (*** sor_pp *)
  25 | pr_sor_push_bi (f1) (f2) (f) (g1) (g2) (g):
  26   pr_sor f1 f2 f → ⫯f1 = g1 → ⫯f2 = g2 → ⫯f = g → pr_sor g1 g2 g
  27 (*** sor_np *)
  28 | pr_sor_next_push (f1) (f2) (f) (g1) (g2) (g):
  29   pr_sor f1 f2 f → ↑f1 = g1 → ⫯f2 = g2 → ↑f = g → pr_sor g1 g2 g
  30 (*** sor_pn *)
  31 | pr_sor_push_next (f1) (f2) (f) (g1) (g2) (g):
  32   pr_sor f1 f2 f → ⫯f1 = g1 → ↑f2 = g2 → ↑f = g → pr_sor g1 g2 g
  33 (*** sor_nn *)
  34 | pr_sor_next_bi (f1) (f2) (f) (g1) (g2) (g):
  35   pr_sor f1 f2 f → ↑f1 = g1 → ↑f2 = g2 → ↑f = g → pr_sor g1 g2 g
  36 .
  37
  38 interpretation
  39   "relational union (partial relocation maps)"
  40   'RUnion f1 f2 f = (pr_sor f1 f2 f).
  41
  42 (* Basic constructions ******************************************************)
  43
  44 (*** sor_idem *)
  45 corec lemma pr_sor_idem:
  46             ∀f. f ⋓ f ≘ f.
  47 #f cases (pr_map_split_tl f) #H
  48 [ @(pr_sor_push_bi … H H H)
  49 | @(pr_sor_next_bi … H H H)
  50 ] -H //
  51 qed.
  52
  53 (*** sor_comm *)
  54 corec lemma pr_sor_comm:
  55             ∀f1,f2,f. f1 ⋓ f2 ≘ f → f2 ⋓ f1 ≘ f.
  56 #f1 #f2 #f * -f1 -f2 -f
  57 #f1 #f2 #f #g1 #g2 #g #Hf * * * -g1 -g2 -g
  58 [ @pr_sor_push_bi | @pr_sor_push_next | @pr_sor_next_push | @pr_sor_next_bi ] /2 width=7 by/
  59 qed-.
  60
  61 (* Basic inversions *********************************************************)
  62
  63 (*** sor_inv_ppx *)
  64 lemma pr_sor_inv_push_bi:
  65       ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 →
  66       ∃∃f. f1 ⋓ f2 ≘ f & ⫯f = g.
  67 #g1 #g2 #g * -g1 -g2 -g
  68 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct
  69 try (>(eq_inv_pr_push_bi … Hx1) -x1) try (>(eq_inv_pr_next_bi … Hx1) -x1)
  70 try elim (eq_inv_pr_push_next … Hx1) try elim (eq_inv_pr_next_push … Hx1)
  71 try (>(eq_inv_pr_push_bi … Hx2) -x2) try (>(eq_inv_pr_next_bi … Hx2) -x2)
  72 try elim (eq_inv_pr_push_next … Hx2) try elim (eq_inv_pr_next_push … Hx2)
  73 /2 width=3 by ex2_intro/
  74 qed-.
  75
  76 (*** sor_inv_npx *)
  77 lemma pr_sor_inv_next_push:
  78       ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 →
  79       ∃∃f. f1 ⋓ f2 ≘ f & ↑f = g.
  80 #g1 #g2 #g * -g1 -g2 -g
  81 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct
  82 try (>(eq_inv_pr_push_bi … Hx1) -x1) try (>(eq_inv_pr_next_bi … Hx1) -x1)
  83 try elim (eq_inv_pr_push_next … Hx1) try elim (eq_inv_pr_next_push … Hx1)
  84 try (>(eq_inv_pr_push_bi … Hx2) -x2) try (>(eq_inv_pr_next_bi … Hx2) -x2)
  85 try elim (eq_inv_pr_push_next … Hx2) try elim (eq_inv_pr_next_push … Hx2)
  86 /2 width=3 by ex2_intro/
  87 qed-.
  88
  89 (*** sor_inv_pnx *)
  90 lemma pr_sor_inv_push_next:
  91       ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 →
  92       ∃∃f. f1 ⋓ f2 ≘ f & ↑f = g.
  93 #g1 #g2 #g * -g1 -g2 -g
  94 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct
  95 try (>(eq_inv_pr_push_bi … Hx1) -x1) try (>(eq_inv_pr_next_bi … Hx1) -x1)
  96 try elim (eq_inv_pr_push_next … Hx1) try elim (eq_inv_pr_next_push … Hx1)
  97 try (>(eq_inv_pr_push_bi … Hx2) -x2) try (>(eq_inv_pr_next_bi … Hx2) -x2)
  98 try elim (eq_inv_pr_push_next … Hx2) try elim (eq_inv_pr_next_push … Hx2)
  99 /2 width=3 by ex2_intro/
 100 qed-.
 101
 102 (*** sor_inv_nnx *)
 103 lemma pr_sor_inv_next_bi:
 104       ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 →
 105       ∃∃f. f1 ⋓ f2 ≘ f & ↑f = g.
 106 #g1 #g2 #g * -g1 -g2 -g
 107 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct
 108 try (>(eq_inv_pr_push_bi … Hx1) -x1) try (>(eq_inv_pr_next_bi … Hx1) -x1)
 109 try elim (eq_inv_pr_push_next … Hx1) try elim (eq_inv_pr_next_push … Hx1)
 110 try (>(eq_inv_pr_push_bi … Hx2) -x2) try (>(eq_inv_pr_next_bi … Hx2) -x2)
 111 try elim (eq_inv_pr_push_next … Hx2) try elim (eq_inv_pr_next_push … Hx2)
 112 /2 width=3 by ex2_intro/
 113 qed-.
 114
 115 (* Advanced inversions ******************************************************)
 116
 117 (*** sor_inv_ppn *)
 118 lemma pr_sor_inv_push_bi_next:
 119       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 120       ∀f1,f2,f. ⫯f1 = g1 → ⫯f2 = g2 → ↑f = g → ⊥.
 121 #g1 #g2 #g #H #f1 #f2 #f #H1 #H2 #H0
 122 elim (pr_sor_inv_push_bi … H … H1 H2) -g1 -g2 #x #_ #H destruct
 123 /2 width=3 by eq_inv_pr_push_next/
 124 qed-.
 125
 126 (*** sor_inv_nxp *)
 127 lemma pr_sor_inv_next_sn_push:
 128       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 129       ∀f1,f. ↑f1 = g1 → ⫯f = g → ⊥.
 130 #g1 #g2 #g #H #f1 #f #H1 #H0
 131 elim (pr_map_split_tl g2) #H2
 132 [ elim (pr_sor_inv_next_push … H … H1 H2)
 133 | elim (pr_sor_inv_next_bi … H … H1 H2)
 134 ] -g1 #x #H
 135 /2 width=3 by eq_inv_pr_next_push/
 136 qed-.
 137
 138 (*** sor_inv_xnp *)
 139 lemma pr_sor_inv_next_dx_push:
 140       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 141       ∀f2,f. ↑f2 = g2 → ⫯f = g → ⊥.
 142 #g1 #g2 #g #H #f2 #f #H2 #H0
 143 elim (pr_map_split_tl g1) #H1
 144 [ elim (pr_sor_inv_push_next … H … H1 H2)
 145 | elim (pr_sor_inv_next_bi … H … H1 H2)
 146 ] -g2 #x #H
 147 /2 width=3 by eq_inv_pr_next_push/
 148 qed-.
 149
 150 (*** sor_inv_ppp *)
 151 lemma pr_sor_inv_push_bi_push:
 152       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 153       ∀f1,f2,f. ⫯f1 = g1 → ⫯f2 = g2 → ⫯f = g → f1 ⋓ f2 ≘ f.
 154 #g1 #g2 #g #H #f1 #f2 #f #H1 #H2 #H0
 155 elim (pr_sor_inv_push_bi … H … H1 H2) -g1 -g2 #x #Hx #H destruct
 156 <(eq_inv_pr_push_bi … H) -f //
 157 qed-.
 158
 159 (*** sor_inv_npn *)
 160 lemma pr_sor_inv_next_push_next:
 161       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 162       ∀f1,f2,f. ↑f1 = g1 → ⫯f2 = g2 → ↑f = g → f1 ⋓ f2 ≘ f.
 163 #g1 #g2 #g #H #f1 #f2 #f #H1 #H2 #H0
 164 elim (pr_sor_inv_next_push … H … H1 H2) -g1 -g2 #x #Hx #H destruct
 165 <(eq_inv_pr_next_bi … H) -f //
 166 qed-.
 167
 168 (*** sor_inv_pnn *)
 169 lemma pr_sor_inv_push_next_next:
 170       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 171       ∀f1,f2,f. ⫯f1 = g1 → ↑f2 = g2 → ↑f = g → f1 ⋓ f2 ≘ f.
 172 #g1 #g2 #g #H #f1 #f2 #f #H1 #H2 #H0
 173 elim (pr_sor_inv_push_next … H … H1 H2) -g1 -g2 #x #Hx #H destruct
 174 <(eq_inv_pr_next_bi … H) -f //
 175 qed-.
 176
 177 (*** sor_inv_nnn *)
 178 lemma pr_sor_inv_next_bi_next:
 179       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 180       ∀f1,f2,f. ↑f1 = g1 → ↑f2 = g2 → ↑f = g → f1 ⋓ f2 ≘ f.
 181 #g1 #g2 #g #H #f1 #f2 #f #H1 #H2 #H0
 182 elim (pr_sor_inv_next_bi … H … H1 H2) -g1 -g2 #x #Hx #H destruct
 183 <(eq_inv_pr_next_bi … H) -f //
 184 qed-.
 185
 186 (*** sor_inv_pxp *)
 187 lemma pr_sor_inv_push_sn_push:
 188       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 189       ∀f1,f. ⫯f1 = g1 → ⫯f = g →
 190       ∃∃f2. f1 ⋓ f2 ≘ f & ⫯f2 = g2.
 191 #g1 #g2 #g #H #f1 #f #H1 #H0
 192 elim (pr_map_split_tl g2) #H2
 193 [ /3 width=7 by pr_sor_inv_push_bi_push, ex2_intro/
 194 | elim (pr_sor_inv_next_dx_push … H … H2 H0)
 195 ]
 196 qed-.
 197
 198 (*** sor_inv_xpp *)
 199 lemma pr_sor_inv_push_dx_push:
 200       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 201       ∀f2,f. ⫯f2 = g2 → ⫯f = g →
 202       ∃∃f1. f1 ⋓ f2 ≘ f & ⫯f1 = g1.
 203 #g1 #g2 #g #H #f2 #f #H2 #H0
 204 elim (pr_map_split_tl g1) #H1
 205 [ /3 width=7 by pr_sor_inv_push_bi_push, ex2_intro/
 206 | elim (pr_sor_inv_next_sn_push … H … H1 H0)
 207 ]
 208 qed-.
 209
 210 (*** sor_inv_pxn *)
 211 lemma pr_sor_inv_push_sn_next:
 212       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 213       ∀f1,f. ⫯f1 = g1 → ↑f = g →
 214       ∃∃f2. f1 ⋓ f2 ≘ f & ↑f2 = g2.
 215 #g1 #g2 #g #H #f1 #f #H1 #H0
 216 elim (pr_map_split_tl g2) #H2
 217 [ elim (pr_sor_inv_push_bi_next … H … H1 H2 H0)
 218 | /3 width=7 by pr_sor_inv_push_next_next, ex2_intro/
 219 ]
 220 qed-.
 221
 222 (*** sor_inv_xpn *)
 223 lemma pr_sor_inv_push_dx_next:
 224       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 225       ∀f2,f. ⫯f2 = g2 → ↑f = g →
 226       ∃∃f1. f1 ⋓ f2 ≘ f & ↑f1 = g1.
 227 #g1 #g2 #g #H #f2 #f #H2 #H0
 228 elim (pr_map_split_tl g1) #H1
 229 [ elim (pr_sor_inv_push_bi_next … H … H1 H2 H0)
 230 | /3 width=7 by pr_sor_inv_next_push_next, ex2_intro/
 231 ]
 232 qed-.
 233
 234 (*** sor_inv_xxp *)
 235 lemma pr_sor_inv_push:
 236       ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f. ⫯f = g →
 237       ∃∃f1,f2. f1 ⋓ f2 ≘ f & ⫯f1 = g1 & ⫯f2 = g2.
 238 #g1 #g2 #g #H #f #H0
 239 elim (pr_map_split_tl g1) #H1
 240 [ elim (pr_sor_inv_push_sn_push … H … H1 H0) -g /2 width=5 by ex3_2_intro/
 241 | elim (pr_sor_inv_next_sn_push … H … H1 H0)
 242 ]
 243 qed-.
 244
 245 (*** sor_inv_nxn *)
 246 lemma pr_sor_inv_next_sn_next:
 247       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 248       ∀f1,f. ↑f1 = g1 → ↑f = g →
 249       ∨∨ ∃∃f2. f1 ⋓ f2 ≘ f & ⫯f2 = g2
 250        | ∃∃f2. f1 ⋓ f2 ≘ f & ↑f2 = g2.
 251 #g1 #g2 elim (pr_map_split_tl g2)
 252 /4 width=7 by pr_sor_inv_next_push_next, pr_sor_inv_next_bi_next, ex2_intro, or_intror, or_introl/
 253 qed-.
 254
 255 (*** sor_inv_xnn *)
 256 lemma pr_sor_inv_next_dx_next:
 257       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 258       ∀f2,f. ↑f2 = g2 → ↑f = g →
 259       ∨∨ ∃∃f1. f1 ⋓ f2 ≘ f & ⫯f1 = g1
 260        | ∃∃f1. f1 ⋓ f2 ≘ f & ↑f1 = g1.
 261 #g1 elim (pr_map_split_tl g1)
 262 /4 width=7 by pr_sor_inv_push_next_next, pr_sor_inv_next_bi_next, ex2_intro, or_intror, or_introl/
 263 qed-.
 264
 265 (*** sor_inv_xxn *)
 266 lemma pr_sor_inv_next:
 267       ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f. ↑f = g →
 268       ∨∨ ∃∃f1,f2. f1 ⋓ f2 ≘ f & ↑f1 = g1 & ⫯f2 = g2
 269        | ∃∃f1,f2. f1 ⋓ f2 ≘ f & ⫯f1 = g1 & ↑f2 = g2
 270        | ∃∃f1,f2. f1 ⋓ f2 ≘ f & ↑f1 = g1 & ↑f2 = g2.
 271 #g1 #g2 #g #H #f #H0
 272 elim (pr_map_split_tl g1) #H1
 273 [ elim (pr_sor_inv_push_sn_next … H … H1 H0) -g
 274   /3 width=5 by or3_intro1, ex3_2_intro/
 275 | elim (pr_sor_inv_next_sn_next … H … H1 H0) -g *
 276   /3 width=5 by or3_intro0, or3_intro2, ex3_2_intro/
 277 ]
 278 qed-.
 279
 280 (* Constructions with pr_tl *************************************************)
 281
 282 (*** sor_tl *)
 283 lemma pr_sor_tl:
 284       ∀f1,f2,f. f1 ⋓ f2 ≘ f → ⫰f1 ⋓ ⫰f2 ≘ ⫰f.
 285 #f1 cases (pr_map_split_tl f1) #H1
 286 #f2 cases (pr_map_split_tl f2) #H2
 287 #f #Hf
 288 [ cases (pr_sor_inv_push_bi … Hf … H1 H2)
 289 | cases (pr_sor_inv_push_next … Hf … H1 H2)
 290 | cases (pr_sor_inv_next_push … Hf … H1 H2)
 291 | cases (pr_sor_inv_next_bi … Hf … H1 H2)
 292 ] -Hf #g #Hg #H destruct //
 293 qed.
 294
 295 (*** sor_xxn_tl *)
 296 lemma pr_sor_next_tl:
 297       ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f. ↑f = g →
 298       (∃∃f1,f2. f1 ⋓ f2 ≘ f & ↑f1 = g1 & ⫰g2 = f2) ∨
 299       (∃∃f1,f2. f1 ⋓ f2 ≘ f & ⫰g1 = f1 & ↑f2 = g2).
 300 #g1 #g2 #g #H #f #H0 elim (pr_sor_inv_next … H … H0) -H -H0 *
 301 /3 width=5 by ex3_2_intro, or_introl, or_intror/
 302 qed-.
 303
 304 (*** sor_xnx_tl *)
 305 lemma pr_sor_next_dx_tl:
 306       ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f2. ↑f2 = g2 →
 307       ∃∃f1,f. f1 ⋓ f2 ≘ f & ⫰g1 = f1 & ↑f = g.
 308 #g1 elim (pr_map_split_tl g1) #H1 #g2 #g #H #f2 #H2
 309 [ elim (pr_sor_inv_push_next … H … H1 H2)
 310 | elim (pr_sor_inv_next_bi … H … H1 H2)
 311 ] -g2
 312 /3 width=5 by ex3_2_intro/
 313 qed-.
 314
 315 (*** sor_nxx_tl *)
 316 lemma pr_sor_next_sn_tl:
 317       ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f1. ↑f1 = g1 →
 318       ∃∃f2,f. f1 ⋓ f2 ≘ f & ⫰g2 = f2 & ↑f = g.
 319 #g1 #g2 elim (pr_map_split_tl g2) #H2 #g #H #f1 #H1
 320 [ elim (pr_sor_inv_next_push … H … H1 H2)
 321 | elim (pr_sor_inv_next_bi … H … H1 H2)
 322 ] -g1
 323 /3 width=5 by ex3_2_intro/
 324 qed-.
 325
 326 (* Inversions with pr_tl ****************************************************)
 327
 328 (*** sor_inv_tl_sn *)
 329 lemma pr_sor_inv_tl_sn:
 330       ∀f1,f2,f. ⫰f1 ⋓ f2 ≘ f → f1 ⋓ ↑f2 ≘ ↑f.
 331 #f1 #f2 #f elim (pr_map_split_tl f1)
 332 /2 width=7 by pr_sor_push_next, pr_sor_next_bi/
 333 qed-.
 334
 335 (*** sor_inv_tl_dx *)
 336 lemma pr_sor_inv_tl_dx:
 337       ∀f1,f2,f. f1 ⋓ ⫰f2 ≘ f → ↑f1 ⋓ f2 ≘ ↑f.
 338 #f1 #f2 #f elim (pr_map_split_tl f2)
 339 /2 width=7 by pr_sor_next_push, pr_sor_next_bi/
 340 qed-.