matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter.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/rcoafter_3.ma".
  16 include "ground/xoa/ex_3_2.ma".
  17 include "ground/relocation/gr_tl.ma".
  18
  19 (* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
  20
  21 (*** coafter *)
  22 coinductive gr_coafter: relation3 gr_map gr_map gr_map ≝
  23 (*** coafter_refl *)
  24 | gr_coafter_refl (f1) (f2) (f) (g1) (g2) (g):
  25   gr_coafter f1 f2 f → ⫯f1 = g1 → ⫯f2 = g2 → ⫯f = g → gr_coafter g1 g2 g
  26 (*** coafter_push *)
  27 | gr_coafter_push (f1) (f2) (f) (g1) (g2) (g):
  28   gr_coafter f1 f2 f → ⫯f1 = g1 → ↑f2 = g2 → ↑f = g → gr_coafter g1 g2 g
  29 (*** coafter_next *)
  30 | gr_coafter_next (f1) (f2) (f) (g1) (g):
  31   gr_coafter f1 f2 f → ↑f1 = g1 → ⫯f = g → gr_coafter g1 f2 g
  32 .
  33
  34 interpretation
  35   "relational co-composition (generic relocation maps)"
  36   'RCoAfter f1 f2 f = (gr_coafter f1 f2 f).
  37
  38 (* Basic inversions *********************************************************)
  39
  40 (*** coafter_inv_ppx *)
  41 lemma gr_coafter_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 (*** coafter_inv_pnx *)
  56 lemma gr_coafter_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 (*** coafter_inv_nxx *)
  71 lemma gr_coafter_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 (*** coafter_inv_ppp *)
  88 lemma gr_coafter_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
  92 elim (gr_coafter_inv_push_bi … Hg … H1 H2) -g1 -g2 #x #Hf #Hx destruct
  93 <(eq_inv_gr_push_bi … Hx) -f //
  94 qed-.
  95
  96 (*** coafter_inv_ppn *)
  97 lemma gr_coafter_inv_push_bi_next:
  98       ∀g1,g2,g. g1 ~⊚ g2 ≘ g →
  99       ∀f1,f2,f. ⫯f1 = g1 → ⫯f2 = g2 → ↑f = g → ⊥.
 100 #g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H
 101 elim (gr_coafter_inv_push_bi … Hg … H1 H2) -g1 -g2 #x #Hf #Hx destruct
 102 elim (eq_inv_gr_push_next … Hx)
 103 qed-.
 104
 105 (*** coafter_inv_pnn *)
 106 lemma gr_coafter_inv_push_next_next:
 107       ∀g1,g2,g. g1 ~⊚ g2 ≘ g →
 108       ∀f1,f2,f. ⫯f1 = g1 → ↑f2 = g2 → ↑f = g → f1 ~⊚ f2 ≘ f.
 109 #g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H
 110 elim (gr_coafter_inv_push_next … Hg … H1 H2) -g1 -g2 #x #Hf #Hx destruct
 111 <(eq_inv_gr_next_bi … Hx) -f //
 112 qed-.
 113
 114 (*** coafter_inv_pnp *)
 115 lemma gr_coafter_inv_push_next_push:
 116       ∀g1,g2,g. g1 ~⊚ g2 ≘ g →
 117       ∀f1,f2,f. ⫯f1 = g1 → ↑f2 = g2 → ⫯f = g → ⊥.
 118 #g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H
 119 elim (gr_coafter_inv_push_next … Hg … H1 H2) -g1 -g2 #x #Hf #Hx destruct
 120 elim (eq_inv_gr_next_push … Hx)
 121 qed-.
 122
 123 (*** coafter_inv_nxp *)
 124 lemma gr_coafter_inv_next_sn_push:
 125       ∀g1,f2,g. g1 ~⊚ f2 ≘ g →
 126       ∀f1,f. ↑f1 = g1 → ⫯f = g → f1 ~⊚ f2 ≘ f.
 127 #g1 #f2 #g #Hg #f1 #f #H1 #H
 128 elim (gr_coafter_inv_next_sn … Hg … H1) -g1 #x #Hf #Hx destruct
 129 <(eq_inv_gr_push_bi … Hx) -f //
 130 qed-.
 131
 132 (*** coafter_inv_nxn *)
 133 lemma gr_coafter_inv_next_sn_next:
 134       ∀g1,f2,g. g1 ~⊚ f2 ≘ g →
 135       ∀f1,f. ↑f1 = g1 → ↑f = g → ⊥.
 136 #g1 #f2 #g #Hg #f1 #f #H1 #H
 137 elim (gr_coafter_inv_next_sn … Hg … H1) -g1 #x #Hf #Hx destruct
 138 elim (eq_inv_gr_push_next … Hx)
 139 qed-.
 140
 141 (*** coafter_inv_pxp *)
 142 lemma gr_coafter_inv_push_sn_push:
 143       ∀g1,g2,g. g1 ~⊚ g2 ≘ g →
 144       ∀f1,f. ⫯f1 = g1 → ⫯f = g →
 145       ∃∃f2. f1 ~⊚ f2 ≘ f & ⫯f2 = g2.
 146 #g1 #g2 #g #Hg #f1 #f #H1 #H
 147 elim (gr_map_split_tl g2) #H2
 148 [ lapply (gr_coafter_inv_push_bi_push … Hg … H1 H2 H) -g1 -g
 149   /2 width=3 by ex2_intro/
 150 | elim (gr_coafter_inv_push_next_push … Hg … H1 H2 H)
 151 ]
 152 qed-.
 153
 154 (*** coafter_inv_pxn *)
 155 lemma gr_coafter_inv_push_sn_next:
 156       ∀g1,g2,g. g1 ~⊚ g2 ≘ g →
 157       ∀f1,f. ⫯f1 = g1 → ↑f = g →
 158       ∃∃f2. f1 ~⊚ f2 ≘ f & ↑f2 = g2.
 159 #g1 #g2 #g #Hg #f1 #f #H1 #H
 160 elim (gr_map_split_tl g2) #H2
 161 [ elim (gr_coafter_inv_push_bi_next … Hg … H1 H2 H)
 162 | lapply (gr_coafter_inv_push_next_next … Hg … H1 … H) -g1 -g
 163   /2 width=3 by ex2_intro/
 164 ]
 165 qed-.
 166
 167 (*** coafter_inv_xxn *)
 168 lemma gr_coafter_inv_next:
 169       ∀g1,g2,g. g1 ~⊚ g2 ≘ g → ∀f. ↑f = g →
 170       ∃∃f1,f2. f1 ~⊚ f2 ≘ f & ⫯f1 = g1 & ↑f2 = g2.
 171 #g1 #g2 #g #Hg #f #H
 172 elim (gr_map_split_tl g1) #H1
 173 [ elim (gr_coafter_inv_push_sn_next … Hg … H1 H) -g
 174   /2 width=5 by ex3_2_intro/
 175 | elim (gr_coafter_inv_next_sn_next … Hg … H1 H)
 176 ]
 177 qed-.
 178
 179 (*** coafter_inv_xnn *)
 180 lemma gr_coafter_inv_next_dx_next:
 181       ∀g1,g2,g. g1 ~⊚ g2 ≘ g →
 182       ∀f2,f. ↑f2 = g2 → ↑f = g →
 183       ∃∃f1. f1 ~⊚ f2 ≘ f & ⫯f1 = g1.
 184 #g1 #g2 #g #Hg #f2 #f #H2 destruct #H
 185 elim (gr_coafter_inv_next … Hg … H) -g #z1 #z2 #Hf #H1 #H2 destruct
 186 /2 width=3 by ex2_intro/
 187 qed-.
 188
 189 (*** coafter_inv_xxp *)
 190 lemma gr_coafter_inv_push:
 191       ∀g1,g2,g. g1 ~⊚ g2 ≘ g → ∀f. ⫯f = g →
 192       ∨∨ ∃∃f1,f2. f1 ~⊚ f2 ≘ f & ⫯f1 = g1 & ⫯f2 = g2
 193        | ∃∃f1. f1 ~⊚ g2 ≘ f & ↑f1 = g1.
 194 #g1 #g2 #g #Hg #f #H
 195 elim (gr_map_split_tl g1) #H1
 196 [ elim (gr_coafter_inv_push_sn_push … Hg … H1 H) -g
 197   /3 width=5 by or_introl, ex3_2_intro/
 198 | /4 width=5 by gr_coafter_inv_next_sn_push, or_intror, ex2_intro/
 199 ]
 200 qed-.
 201
 202 (*** coafter_inv_pxx *)
 203 lemma gr_coafter_inv_push_sn:
 204       ∀g1,g2,g. g1 ~⊚ g2 ≘ g → ∀f1. ⫯f1 = g1 →
 205       ∨∨ ∃∃f2,f. f1 ~⊚ f2 ≘ f & ⫯f2 = g2 & ⫯f = g
 206        | ∃∃f2,f. f1 ~⊚ f2 ≘ f & ↑f2 = g2 & ↑f = g.
 207 #g1 #g2 #g #Hg #f1 #H1
 208 elim (gr_map_split_tl g2) #H2
 209 [ elim (gr_coafter_inv_push_bi … Hg … H1 H2) -g1
 210   /3 width=5 by or_introl, ex3_2_intro/
 211 | elim (gr_coafter_inv_push_next … Hg … H1 H2) -g1
 212   /3 width=5 by or_intror, ex3_2_intro/
 213 ]
 214 qed-.
 215
 216 (* Inversions with gr_tl ****************************************************)
 217
 218 (*** coafter_inv_tl1 *)
 219 lemma gr_coafter_inv_tl_dx:
 220       ∀g2,g1,g. g2 ~⊚ ⫱g1 ≘ g →
 221       ∃∃f. ⫯g2 ~⊚ g1 ≘ f & ⫱f = g.
 222 #g2 #g1 #g
 223 elim (gr_map_split_tl g1) #H1 #H2
 224 [ /3 width=7 by gr_coafter_refl, ex2_intro/
 225 | @(ex2_intro … (↑g)) /2 width=7 by gr_coafter_push/ (* * full auto fails *)
 226 ]
 227 qed-.
 228
 229 (*** coafter_inv_tl0 *)
 230 lemma gr_coafter_inv_tl:
 231       ∀g2,g1,g. g2 ~⊚ g1 ≘ ⫱g →
 232       ∃∃f1. ⫯g2 ~⊚ f1 ≘ g & ⫱f1 = g1.
 233 #g2 #g1 #g
 234 elim (gr_map_split_tl g) #H1 #H2
 235 [ /3 width=7 by gr_coafter_refl, ex2_intro/
 236 | @(ex2_intro … (↑g1)) /2 width=7 by gr_coafter_push/ (* * full auto fails *)
 237 ]
 238 qed-.