matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_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/relocation/gr_eq.ma".
  16 include "ground/relocation/gr_sor.ma".
  17
  18 (* RELATIONAL UNION FOR GENERIC RELOCATION MAPS *****************************)
  19
  20 (* Main inversions **********************************************************)
  21
  22 (*** sor_mono *)
  23 corec theorem gr_sor_mono:
  24               ∀f1,f2,x,y. f1 ⋓ f2 ≘ x → f1 ⋓ f2 ≘ y → x ≡ y.
  25 #f1 #f2 #x #y * -f1 -f2 -x
  26 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #H
  27 [ cases (gr_sor_inv_push_bi … H … H1 H2)
  28 | cases (gr_sor_inv_next_push … H … H1 H2)
  29 | cases (gr_sor_inv_push_next … H … H1 H2)
  30 | cases (gr_sor_inv_next_bi … H … H1 H2)
  31 ] -g1 -g2
  32 /3 width=5 by gr_eq_push, gr_eq_next/
  33 qed-.
  34
  35 (* Main constructions *******************************************************)
  36
  37 (*** sor_assoc_dx *)
  38 axiom gr_sor_assoc_dx:
  39       ∀f0,f3,f4. f0 ⋓ f3 ≘ f4 →
  40       ∀f1,f2. f1 ⋓ f2 ≘ f0 →
  41       ∀f. f2 ⋓ f3 ≘ f → f1 ⋓ f ≘ f4.
  42
  43 (*** sor_assoc_sn *)
  44 axiom gr_sor_assoc_sn:
  45       ∀f1,f0,f4. f1 ⋓ f0 ≘ f4 →
  46       ∀f2, f3. f2 ⋓ f3 ≘ f0 →
  47       ∀f. f1 ⋓ f2 ≘ f → f ⋓ f3 ≘ f4.
  48
  49 (*** sor_comm_23 *)
  50 lemma gr_sor_comm_23:
  51       ∀f0,f1,f2,f3,f4,f.
  52       f0⋓f4 ≘ f1 → f1⋓f2 ≘ f → f0⋓f2 ≘ f3 → f3⋓f4 ≘ f.
  53 /4 width=6 by gr_sor_comm, gr_sor_assoc_dx/ qed-.
  54
  55 (*** sor_comm_23_idem *)
  56 corec theorem gr_sor_comm_23_idem:
  57               ∀f0,f1,f2. f0 ⋓ f1 ≘ f2 →
  58               ∀f. f1 ⋓ f2 ≘ f → f1 ⋓ f0 ≘ f.
  59 #f0 #f1 #f2 * -f0 -f1 -f2
  60 #f0 #f1 #f2 #g0 #g1 #g2 #Hf2 #H0 #H1 #H2 #g #Hg
  61 [ cases (gr_sor_inv_push_bi … Hg … H1 H2)
  62 | cases (gr_sor_inv_push_next … Hg … H1 H2)
  63 | cases (gr_sor_inv_next_bi … Hg … H1 H2)
  64 | cases (gr_sor_inv_next_bi … Hg … H1 H2)
  65 ] -g2 #f #Hf #H
  66 /3 width=7 by gr_sor_next_bi, gr_sor_next_push, gr_sor_push_next, gr_sor_push_bi/
  67 qed-.
  68
  69 (*** sor_coll_dx *)
  70 corec theorem gr_sor_coll_dx:
  71               ∀f1,f2,f. f1 ⋓ f2 ≘ f → ∀g1,g2,g. g1 ⋓ g2 ≘ g →
  72               ∀g0. g1 ⋓ g0 ≘ f1 → g2 ⋓ g0 ≘ f2 → g ⋓ g0 ≘ f.
  73 #f1 #f2 #f cases (gr_map_split_tl f) #H1 #Hf #g1 #g2 #g #Hg #g0 #Hf1 #Hf2
  74 [ cases (gr_sor_inv_push … Hf … H1) -Hf #x1 #x2 #Hf #Hx1 #Hx2
  75   cases (gr_sor_inv_push … Hf1 … Hx1) -f1 #y1 #y0 #Hf1 #Hy1 #Hy0
  76   cases (gr_sor_inv_push_dx_push … Hf2 … Hy0 … Hx2) -f2 #y2 #Hf2 #Hy2
  77   cases (gr_sor_inv_push_bi … Hg … Hy1 Hy2) -g1 -g2 #y #Hg #Hy
  78   @(gr_sor_push_bi … Hy Hy0 H1) -g -g0 /2 width=8 by/
  79 | cases (gr_map_split_tl g) #H2
  80   [ cases (gr_sor_inv_push … Hg … H2) -Hg #y1 #y2 #Hg #Hy1 #Hy2
  81     cases (gr_sor_next_tl … Hf … H1) * #x1 #x2 #_ #Hx1 #Hx2
  82     [ cases (gr_sor_inv_push_sn_next … Hf1 … Hy1 Hx1) -g1 #y0 #Hf1 #Hy0
  83       cases (gr_sor_inv_push_next … Hf2 … Hy2 Hy0) -g2 -x2 #x2 #Hf2 #Hx2
  84     | cases (gr_sor_inv_push_sn_next … Hf2 … Hy2 Hx2) -g2 #y0 #Hf2 #Hy0
  85       cases (gr_sor_inv_push_next … Hf1 … Hy1 Hy0) -g1 -x1 #x1 #Hf1 #Hx1
  86     ]
  87     lapply (gr_sor_inv_next_bi_next … Hf … Hx1 Hx2 H1) -f1 -f2 #Hf
  88     @(gr_sor_push_next … H2 Hy0 H1) -g0 /2 width=8 by/
  89   | lapply (gr_sor_tl … Hf) -Hf #Hf
  90     lapply (gr_sor_tl … Hg) -Hg #Hg
  91     lapply (gr_sor_tl … Hf1) -Hf1 #Hf1
  92     lapply (gr_sor_tl … Hf2) -Hf2 #Hf2
  93     cases (gr_map_split_tl g0) #H0
  94     [ @(gr_sor_next_push … H2 H0 H1) /2 width=8 by/
  95     | @(gr_sor_next_bi … H2 H0 H1) /2 width=8 by/
  96     ]
  97   ]
  98 ]
  99 qed-.
 100
 101 (*** sor_distr_dx *)
 102 corec theorem gr_sor_distr_dx:
 103               ∀g0,g1,g2,g. g1 ⋓ g2 ≘ g →
 104               ∀f1,f2,f. g1 ⋓ g0 ≘ f1 → g2 ⋓ g0 ≘ f2 → g ⋓ g0 ≘ f →
 105               f1 ⋓ f2 ≘ f.
 106 #g0 cases (gr_map_split_tl g0) #H0 #g1 #g2 #g
 107 [ * -g1 -g2 -g #y1 #y2 #y #g1 #g2 #g #Hy #Hy1 #Hy2 #Hy #f1 #f2 #f #Hf1 #Hf2 #Hf
 108   [ cases (gr_sor_inv_push_bi … Hf1 … Hy1 H0) -g1
 109     cases (gr_sor_inv_push_bi … Hf2 … Hy2 H0) -g2
 110     cases (gr_sor_inv_push_bi … Hf … Hy H0) -g
 111   | cases (gr_sor_inv_next_push … Hf1 … Hy1 H0) -g1
 112     cases (gr_sor_inv_push_bi … Hf2 … Hy2 H0) -g2
 113     cases (gr_sor_inv_next_push … Hf … Hy H0) -g
 114   | cases (gr_sor_inv_push_bi … Hf1 … Hy1 H0) -g1
 115     cases (gr_sor_inv_next_push … Hf2 … Hy2 H0) -g2
 116     cases (gr_sor_inv_next_push … Hf … Hy H0) -g
 117   | cases (gr_sor_inv_next_push … Hf1 … Hy1 H0) -g1
 118     cases (gr_sor_inv_next_push … Hf2 … Hy2 H0) -g2
 119     cases (gr_sor_inv_next_push … Hf … Hy H0) -g
 120   ] #y #Hy #H #y2 #Hy2 #H2 #y1 #Hy1 #H1
 121   /3 width=8 by gr_sor_next_bi, gr_sor_next_push, gr_sor_push_next, gr_sor_push_bi/
 122 | #H #f1 #f2 #f #Hf1 #Hf2 #Hf
 123   cases (gr_sor_next_dx_tl … Hf1 … H0) -Hf1
 124   cases (gr_sor_next_dx_tl … Hf2 … H0) -Hf2
 125   cases (gr_sor_next_dx_tl … Hf … H0) -Hf
 126   #y #x #Hx #Hy #H #y2 #x2 #Hx2 #Hy2 #H2 #y1 #x1 #Hx1 #Hy1 #H1
 127   /4 width=8 by gr_sor_tl, gr_sor_next_bi/
 128 ]
 129 qed-.