matita/matita/contribs/lambdadelta/ground/relocation/rtmap_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/xoa/or_3.ma".
  16 include "ground/xoa/ex_3_1.ma".
  17 include "ground/xoa/ex_4_2.ma".
  18 include "ground/notation/relations/runion_3.ma".
  19 include "ground/arith/nat_plus.ma".
  20 include "ground/arith/nat_le_max.ma".
  21 include "ground/relocation/rtmap_isfin.ma".
  22 include "ground/relocation/rtmap_sle.ma".
  23
  24 coinductive sor: relation3 rtmap rtmap rtmap ≝
  25 | sor_pp: ∀f1,f2,f,g1,g2,g. sor f1 f2 f → ⫯f1 = g1 → ⫯f2 = g2 → ⫯f = g → sor g1 g2 g
  26 | sor_np: ∀f1,f2,f,g1,g2,g. sor f1 f2 f → ↑f1 = g1 → ⫯f2 = g2 → ↑f = g → sor g1 g2 g
  27 | sor_pn: ∀f1,f2,f,g1,g2,g. sor f1 f2 f → ⫯f1 = g1 → ↑f2 = g2 → ↑f = g → sor g1 g2 g
  28 | sor_nn: ∀f1,f2,f,g1,g2,g. sor f1 f2 f → ↑f1 = g1 → ↑f2 = g2 → ↑f = g → sor g1 g2 g
  29 .
  30
  31 interpretation "union (rtmap)"
  32    'RUnion f1 f2 f = (sor f1 f2 f).
  33
  34 (* Basic inversion lemmas ***************************************************)
  35
  36 lemma sor_inv_ppx: ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 →
  37                    ∃∃f. f1 ⋓ f2 ≘ f & ⫯f = g.
  38 #g1 #g2 #g * -g1 -g2 -g
  39 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct
  40 try (>(injective_push … Hx1) -x1) try (>(injective_next … Hx1) -x1)
  41 try elim (discr_push_next … Hx1) try elim (discr_next_push … Hx1)
  42 try (>(injective_push … Hx2) -x2) try (>(injective_next … Hx2) -x2)
  43 try elim (discr_push_next … Hx2) try elim (discr_next_push … Hx2)
  44 /2 width=3 by ex2_intro/
  45 qed-.
  46
  47 lemma sor_inv_npx: ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 →
  48                    ∃∃f. f1 ⋓ f2 ≘ f & ↑f = g.
  49 #g1 #g2 #g * -g1 -g2 -g
  50 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct
  51 try (>(injective_push … Hx1) -x1) try (>(injective_next … Hx1) -x1)
  52 try elim (discr_push_next … Hx1) try elim (discr_next_push … Hx1)
  53 try (>(injective_push … Hx2) -x2) try (>(injective_next … Hx2) -x2)
  54 try elim (discr_push_next … Hx2) try elim (discr_next_push … Hx2)
  55 /2 width=3 by ex2_intro/
  56 qed-.
  57
  58 lemma sor_inv_pnx: ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 →
  59                    ∃∃f. f1 ⋓ f2 ≘ f & ↑f = g.
  60 #g1 #g2 #g * -g1 -g2 -g
  61 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct
  62 try (>(injective_push … Hx1) -x1) try (>(injective_next … Hx1) -x1)
  63 try elim (discr_push_next … Hx1) try elim (discr_next_push … Hx1)
  64 try (>(injective_push … Hx2) -x2) try (>(injective_next … Hx2) -x2)
  65 try elim (discr_push_next … Hx2) try elim (discr_next_push … Hx2)
  66 /2 width=3 by ex2_intro/
  67 qed-.
  68
  69 lemma sor_inv_nnx: ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 →
  70                    ∃∃f. f1 ⋓ f2 ≘ f & ↑f = g.
  71 #g1 #g2 #g * -g1 -g2 -g
  72 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct
  73 try (>(injective_push … Hx1) -x1) try (>(injective_next … Hx1) -x1)
  74 try elim (discr_push_next … Hx1) try elim (discr_next_push … Hx1)
  75 try (>(injective_push … Hx2) -x2) try (>(injective_next … Hx2) -x2)
  76 try elim (discr_push_next … Hx2) try elim (discr_next_push … Hx2)
  77 /2 width=3 by ex2_intro/
  78 qed-.
  79
  80 (* Advanced inversion lemmas ************************************************)
  81
  82 lemma sor_inv_ppn: ∀g1,g2,g. g1 ⋓ g2 ≘ g →
  83                    ∀f1,f2,f. ⫯f1 = g1 → ⫯f2 = g2 → ↑f = g → ⊥.
  84 #g1 #g2 #g #H #f1 #f2 #f #H1 #H2 #H0
  85 elim (sor_inv_ppx … H … H1 H2) -g1 -g2 #x #_ #H destruct
  86 /2 width=3 by discr_push_next/
  87 qed-.
  88
  89 lemma sor_inv_nxp: ∀g1,g2,g. g1 ⋓ g2 ≘ g →
  90                    ∀f1,f. ↑f1 = g1 → ⫯f = g → ⊥.
  91 #g1 #g2 #g #H #f1 #f #H1 #H0
  92 elim (pn_split g2) * #f2 #H2
  93 [ elim (sor_inv_npx … H … H1 H2)
  94 | elim (sor_inv_nnx … H … H1 H2)
  95 ] -g1 -g2 #x #_ #H destruct
  96 /2 width=3 by discr_next_push/
  97 qed-.
  98
  99 lemma sor_inv_xnp: ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 100                    ∀f2,f. ↑f2 = g2 → ⫯f = g → ⊥.
 101 #g1 #g2 #g #H #f2 #f #H2 #H0
 102 elim (pn_split g1) * #f1 #H1
 103 [ elim (sor_inv_pnx … H … H1 H2)
 104 | elim (sor_inv_nnx … H … H1 H2)
 105 ] -g1 -g2 #x #_ #H destruct
 106 /2 width=3 by discr_next_push/
 107 qed-.
 108
 109 lemma sor_inv_ppp: ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 110                    ∀f1,f2,f. ⫯f1 = g1 → ⫯f2 = g2 → ⫯f = g → f1 ⋓ f2 ≘ f.
 111 #g1 #g2 #g #H #f1 #f2 #f #H1 #H2 #H0
 112 elim (sor_inv_ppx … H … H1 H2) -g1 -g2 #x #Hx #H destruct
 113 <(injective_push … H) -f //
 114 qed-.
 115
 116 lemma sor_inv_npn: ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 117                    ∀f1,f2,f. ↑f1 = g1 → ⫯f2 = g2 → ↑f = g → f1 ⋓ f2 ≘ f.
 118 #g1 #g2 #g #H #f1 #f2 #f #H1 #H2 #H0
 119 elim (sor_inv_npx … H … H1 H2) -g1 -g2 #x #Hx #H destruct
 120 <(injective_next … H) -f //
 121 qed-.
 122
 123 lemma sor_inv_pnn: ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 124                    ∀f1,f2,f. ⫯f1 = g1 → ↑f2 = g2 → ↑f = g → f1 ⋓ f2 ≘ f.
 125 #g1 #g2 #g #H #f1 #f2 #f #H1 #H2 #H0
 126 elim (sor_inv_pnx … H … H1 H2) -g1 -g2 #x #Hx #H destruct
 127 <(injective_next … H) -f //
 128 qed-.
 129
 130 lemma sor_inv_nnn: ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 131                    ∀f1,f2,f. ↑f1 = g1 → ↑f2 = g2 → ↑f = g → f1 ⋓ f2 ≘ f.
 132 #g1 #g2 #g #H #f1 #f2 #f #H1 #H2 #H0
 133 elim (sor_inv_nnx … H … H1 H2) -g1 -g2 #x #Hx #H destruct
 134 <(injective_next … H) -f //
 135 qed-.
 136
 137 lemma sor_inv_pxp: ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 138                    ∀f1,f. ⫯f1 = g1 → ⫯f = g →
 139                    ∃∃f2. f1 ⋓ f2 ≘ f & ⫯f2 = g2.
 140 #g1 #g2 #g #H #f1 #f #H1 #H0
 141 elim (pn_split g2) * #f2 #H2
 142 [ /3 width=7 by sor_inv_ppp, ex2_intro/
 143 | elim (sor_inv_xnp … H … H2 H0)
 144 ]
 145 qed-.
 146
 147 lemma sor_inv_xpp: ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 148                    ∀f2,f. ⫯f2 = g2 → ⫯f = g →
 149                    ∃∃f1. f1 ⋓ f2 ≘ f & ⫯f1 = g1.
 150 #g1 #g2 #g #H #f2 #f #H2 #H0
 151 elim (pn_split g1) * #f1 #H1
 152 [ /3 width=7 by sor_inv_ppp, ex2_intro/
 153 | elim (sor_inv_nxp … H … H1 H0)
 154 ]
 155 qed-.
 156
 157 lemma sor_inv_pxn: ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 158                    ∀f1,f. ⫯f1 = g1 → ↑f = g →
 159                    ∃∃f2. f1 ⋓ f2 ≘ f & ↑f2 = g2.
 160 #g1 #g2 #g #H #f1 #f #H1 #H0
 161 elim (pn_split g2) * #f2 #H2
 162 [ elim (sor_inv_ppn … H … H1 H2 H0)
 163 | /3 width=7 by sor_inv_pnn, ex2_intro/
 164 ]
 165 qed-.
 166
 167 lemma sor_inv_xpn: ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 168                    ∀f2,f. ⫯f2 = g2 → ↑f = g →
 169                    ∃∃f1. f1 ⋓ f2 ≘ f & ↑f1 = g1.
 170 #g1 #g2 #g #H #f2 #f #H2 #H0
 171 elim (pn_split g1) * #f1 #H1
 172 [ elim (sor_inv_ppn … H … H1 H2 H0)
 173 | /3 width=7 by sor_inv_npn, ex2_intro/
 174 ]
 175 qed-.
 176
 177 lemma sor_inv_xxp: ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f. ⫯f = g →
 178                    ∃∃f1,f2. f1 ⋓ f2 ≘ f & ⫯f1 = g1 & ⫯f2 = g2.
 179 #g1 #g2 #g #H #f #H0
 180 elim (pn_split g1) * #f1 #H1
 181 [ elim (sor_inv_pxp … H … H1 H0) -g /2 width=5 by ex3_2_intro/
 182 | elim (sor_inv_nxp … H … H1 H0)
 183 ]
 184 qed-.
 185
 186 lemma sor_inv_nxn: ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 187                    ∀f1,f. ↑f1 = g1 → ↑f = g →
 188                    (∃∃f2. f1 ⋓ f2 ≘ f & ⫯f2 = g2) ∨
 189                    ∃∃f2. f1 ⋓ f2 ≘ f & ↑f2 = g2.
 190 #g1 #g2 elim (pn_split g2) *
 191 /4 width=7 by sor_inv_npn, sor_inv_nnn, ex2_intro, or_intror, or_introl/
 192 qed-.
 193
 194 lemma sor_inv_xnn: ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 195                    ∀f2,f. ↑f2 = g2 → ↑f = g →
 196                    (∃∃f1. f1 ⋓ f2 ≘ f & ⫯f1 = g1) ∨
 197                    ∃∃f1. f1 ⋓ f2 ≘ f & ↑f1 = g1.
 198 #g1 elim (pn_split g1) *
 199 /4 width=7 by sor_inv_pnn, sor_inv_nnn, ex2_intro, or_intror, or_introl/
 200 qed-.
 201
 202 lemma sor_inv_xxn: ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f. ↑f = g →
 203                    ∨∨ ∃∃f1,f2. f1 ⋓ f2 ≘ f & ↑f1 = g1 & ⫯f2 = g2
 204                     | ∃∃f1,f2. f1 ⋓ f2 ≘ f & ⫯f1 = g1 & ↑f2 = g2
 205                     | ∃∃f1,f2. f1 ⋓ f2 ≘ f & ↑f1 = g1 & ↑f2 = g2.
 206 #g1 #g2 #g #H #f #H0
 207 elim (pn_split g1) * #f1 #H1
 208 [ elim (sor_inv_pxn … H … H1 H0) -g
 209   /3 width=5 by or3_intro1, ex3_2_intro/
 210 | elim (sor_inv_nxn … H … H1 H0) -g *
 211   /3 width=5 by or3_intro0, or3_intro2, ex3_2_intro/
 212 ]
 213 qed-.
 214
 215 (* Main inversion lemmas ****************************************************)
 216
 217 corec theorem sor_mono: ∀f1,f2,x,y. f1 ⋓ f2 ≘ x → f1 ⋓ f2 ≘ y → x ≡ y.
 218 #f1 #f2 #x #y * -f1 -f2 -x
 219 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #H
 220 [ cases (sor_inv_ppx … H … H1 H2)
 221 | cases (sor_inv_npx … H … H1 H2)
 222 | cases (sor_inv_pnx … H … H1 H2)
 223 | cases (sor_inv_nnx … H … H1 H2)
 224 ] -g1 -g2
 225 /3 width=5 by eq_push, eq_next/
 226 qed-.
 227
 228 (* Basic properties *********************************************************)
 229
 230 corec lemma sor_eq_repl_back1: ∀f2,f. eq_repl_back … (λf1. f1 ⋓ f2 ≘ f).
 231 #f2 #f #f1 * -f1 -f2 -f
 232 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #x #Hx
 233 try cases (eq_inv_px … Hx … H1) try cases (eq_inv_nx … Hx … H1) -g1
 234 /3 width=7 by sor_pp, sor_np, sor_pn, sor_nn/
 235 qed-.
 236
 237 lemma sor_eq_repl_fwd1: ∀f2,f. eq_repl_fwd … (λf1. f1 ⋓ f2 ≘ f).
 238 #f2 #f @eq_repl_sym /2 width=3 by sor_eq_repl_back1/
 239 qed-.
 240
 241 corec lemma sor_eq_repl_back2: ∀f1,f. eq_repl_back … (λf2. f1 ⋓ f2 ≘ f).
 242 #f1 #f #f2 * -f1 -f2 -f
 243 #f1 #f2 #f #g1 #g2 #g #Hf #H #H2 #H0 #x #Hx
 244 try cases (eq_inv_px … Hx … H2) try cases (eq_inv_nx … Hx … H2) -g2
 245 /3 width=7 by sor_pp, sor_np, sor_pn, sor_nn/
 246 qed-.
 247
 248 lemma sor_eq_repl_fwd2: ∀f1,f. eq_repl_fwd … (λf2. f1 ⋓ f2 ≘ f).
 249 #f1 #f @eq_repl_sym /2 width=3 by sor_eq_repl_back2/
 250 qed-.
 251
 252 corec lemma sor_eq_repl_back3: ∀f1,f2. eq_repl_back … (λf. f1 ⋓ f2 ≘ f).
 253 #f1 #f2 #f * -f1 -f2 -f
 254 #f1 #f2 #f #g1 #g2 #g #Hf #H #H2 #H0 #x #Hx
 255 try cases (eq_inv_px … Hx … H0) try cases (eq_inv_nx … Hx … H0) -g
 256 /3 width=7 by sor_pp, sor_np, sor_pn, sor_nn/
 257 qed-.
 258
 259 lemma sor_eq_repl_fwd3: ∀f1,f2. eq_repl_fwd … (λf. f1 ⋓ f2 ≘ f).
 260 #f1 #f2 @eq_repl_sym /2 width=3 by sor_eq_repl_back3/
 261 qed-.
 262
 263 corec lemma sor_idem: ∀f. f ⋓ f ≘ f.
 264 #f cases (pn_split f) * #g #H
 265 [ @(sor_pp … H H H) | @(sor_nn … H H H) ] -H //
 266 qed.
 267
 268 corec lemma sor_comm: ∀f1,f2,f. f1 ⋓ f2 ≘ f → f2 ⋓ f1 ≘ f.
 269 #f1 #f2 #f * -f1 -f2 -f
 270 #f1 #f2 #f #g1 #g2 #g #Hf * * * -g1 -g2 -g
 271 [ @sor_pp | @sor_pn | @sor_np | @sor_nn ] /2 width=7 by/
 272 qed-.
 273
 274 (* Properties with tail *****************************************************)
 275
 276 lemma sor_tl: ∀f1,f2,f. f1 ⋓ f2 ≘ f → ⫱f1 ⋓ ⫱f2 ≘ ⫱f.
 277 #f1 cases (pn_split f1) * #g1 #H1
 278 #f2 cases (pn_split f2) * #g2 #H2
 279 #f #Hf
 280 [ cases (sor_inv_ppx … Hf … H1 H2)
 281 | cases (sor_inv_pnx … Hf … H1 H2)
 282 | cases (sor_inv_npx … Hf … H1 H2)
 283 | cases (sor_inv_nnx … Hf … H1 H2)
 284 ] -Hf #g #Hg #H destruct //
 285 qed.
 286
 287 lemma sor_xxn_tl: ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f. ↑f = g →
 288                   (∃∃f1,f2. f1 ⋓ f2 ≘ f & ↑f1 = g1 & ⫱g2 = f2) ∨
 289                   (∃∃f1,f2. f1 ⋓ f2 ≘ f & ⫱g1 = f1 & ↑f2 = g2).
 290 #g1 #g2 #g #H #f #H0 elim (sor_inv_xxn … H … H0) -H -H0 *
 291 /3 width=5 by ex3_2_intro, or_introl, or_intror/
 292 qed-.
 293
 294 lemma sor_xnx_tl: ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f2. ↑f2 = g2 →
 295                   ∃∃f1,f. f1 ⋓ f2 ≘ f & ⫱g1 = f1 & ↑f = g.
 296 #g1 elim (pn_split g1) * #f1 #H1 #g2 #g #H #f2 #H2
 297 [ elim (sor_inv_pnx … H … H1 H2) | elim (sor_inv_nnx … H … H1 H2) ] -g2
 298 /3 width=5 by ex3_2_intro/
 299 qed-.
 300
 301 lemma sor_nxx_tl: ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f1. ↑f1 = g1 →
 302                   ∃∃f2,f. f1 ⋓ f2 ≘ f & ⫱g2 = f2 & ↑f = g.
 303 #g1 #g2 elim (pn_split g2) * #f2 #H2 #g #H #f1 #H1
 304 [ elim (sor_inv_npx … H … H1 H2) | elim (sor_inv_nnx … H … H1 H2) ] -g1
 305 /3 width=5 by ex3_2_intro/
 306 qed-.
 307
 308 (* Properties with iterated tail ********************************************)
 309
 310 lemma sor_tls: ∀f1,f2,f. f1 ⋓ f2 ≘ f →
 311                ∀n. ⫱*[n]f1 ⋓ ⫱*[n]f2 ≘ ⫱*[n]f.
 312 #f1 #f2 #f #Hf #n @(nat_ind_succ … n) -n
 313 /2 width=1 by sor_tl/
 314 qed.
 315
 316 (* Properies with test for identity *****************************************)
 317
 318 corec lemma sor_isid_sn: ∀f1. 𝐈❪f1❫ → ∀f2. f1 ⋓ f2 ≘ f2.
 319 #f1 * -f1
 320 #f1 #g1 #Hf1 #H1 #f2 cases (pn_split f2) *
 321 /3 width=7 by sor_pp, sor_pn/
 322 qed.
 323
 324 corec lemma sor_isid_dx: ∀f2. 𝐈❪f2❫ → ∀f1. f1 ⋓ f2 ≘ f1.
 325 #f2 * -f2
 326 #f2 #g2 #Hf2 #H2 #f1 cases (pn_split f1) *
 327 /3 width=7 by sor_pp, sor_np/
 328 qed.
 329
 330 lemma sor_isid: ∀f1,f2,f. 𝐈❪f1❫ → 𝐈❪f2❫ → 𝐈❪f❫ → f1 ⋓ f2 ≘ f.
 331 /4 width=3 by sor_eq_repl_back2, sor_eq_repl_back1, isid_inv_eq_repl/ qed.
 332
 333 (* Inversion lemmas with tail ***********************************************)
 334
 335 lemma sor_inv_tl_sn: ∀f1,f2,f. ⫱f1 ⋓ f2 ≘ f → f1 ⋓ ↑f2 ≘ ↑f.
 336 #f1 #f2 #f elim (pn_split f1) *
 337 #g1 #H destruct /2 width=7 by sor_pn, sor_nn/
 338 qed-.
 339
 340 lemma sor_inv_tl_dx: ∀f1,f2,f. f1 ⋓ ⫱f2 ≘ f → ↑f1 ⋓ f2 ≘ ↑f.
 341 #f1 #f2 #f elim (pn_split f2) *
 342 #g2 #H destruct /2 width=7 by sor_np, sor_nn/
 343 qed-.
 344
 345 (* Inversion lemmas with test for identity **********************************)
 346
 347 lemma sor_isid_inv_sn: ∀f1,f2,f. f1 ⋓ f2 ≘ f → 𝐈❪f1❫ → f2 ≡ f.
 348 /3 width=4 by sor_isid_sn, sor_mono/
 349 qed-.
 350
 351 lemma sor_isid_inv_dx: ∀f1,f2,f. f1 ⋓ f2 ≘ f → 𝐈❪f2❫ → f1 ≡ f.
 352 /3 width=4 by sor_isid_dx, sor_mono/
 353 qed-.
 354
 355 corec lemma sor_fwd_isid1: ∀f1,f2,f. f1 ⋓ f2 ≘ f → 𝐈❪f❫ → 𝐈❪f1❫.
 356 #f1 #f2 #f * -f1 -f2 -f
 357 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H #Hg
 358 [ /4 width=6 by isid_inv_push, isid_push/ ]
 359 cases (isid_inv_next … Hg … H)
 360 qed-.
 361
 362 corec lemma sor_fwd_isid2: ∀f1,f2,f. f1 ⋓ f2 ≘ f → 𝐈❪f❫ → 𝐈❪f2❫.
 363 #f1 #f2 #f * -f1 -f2 -f
 364 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H #Hg
 365 [ /4 width=6 by isid_inv_push, isid_push/ ]
 366 cases (isid_inv_next … Hg … H)
 367 qed-.
 368
 369 lemma sor_inv_isid3: ∀f1,f2,f. f1 ⋓ f2 ≘ f → 𝐈❪f❫ → 𝐈❪f1❫ ∧ 𝐈❪f2❫.
 370 /3 width=4 by sor_fwd_isid2, sor_fwd_isid1, conj/ qed-.
 371
 372 (* Properties with finite colength assignment *******************************)
 373
 374 lemma sor_fcla_ex: ∀f1,n1. 𝐂❪f1❫ ≘ n1 → ∀f2,n2. 𝐂❪f2❫ ≘ n2 →
 375                    ∃∃f,n. f1 ⋓ f2 ≘ f & 𝐂❪f❫ ≘ n & (n1 ∨ n2) ≤ n & n ≤ n1 + n2.
 376 #f1 #n1 #Hf1 elim Hf1 -f1 -n1 /3 width=6 by sor_isid_sn, ex4_2_intro/
 377 #f1 #n1 #Hf1 #IH #f2 #n2 * -f2 -n2 /3 width=6 by fcla_push, fcla_next, ex4_2_intro, sor_isid_dx/
 378 #f2 #n2 #Hf2 elim (IH … Hf2) -IH -Hf2 -Hf1 [2,4: #f #n <nplus_succ_dx ] (**) (* full auto fails *)
 379 [ /3 width=7 by fcla_next, sor_pn, nle_max_sn_succ_dx, nle_succ_bi, ex4_2_intro/
 380 | /4 width=7 by fcla_next, sor_nn, nle_succ_dx, nle_succ_bi, ex4_2_intro/
 381 | /3 width=7 by fcla_push, sor_pp, ex4_2_intro/
 382 | /3 width=7 by fcla_next, sor_np, nle_max_sn_succ_sn, nle_succ_bi, ex4_2_intro/
 383 ]
 384 qed-.
 385
 386 lemma sor_fcla: ∀f1,n1. 𝐂❪f1❫ ≘ n1 → ∀f2,n2. 𝐂❪f2❫ ≘ n2 → ∀f. f1 ⋓ f2 ≘ f →
 387                 ∃∃n. 𝐂❪f❫ ≘ n & (n1 ∨ n2) ≤ n & n ≤ n1 + n2.
 388 #f1 #n1 #Hf1 #f2 #n2 #Hf2 #f #Hf elim (sor_fcla_ex … Hf1 … Hf2) -Hf1 -Hf2
 389 /4 width=6 by sor_mono, fcla_eq_repl_back, ex3_intro/
 390 qed-.
 391
 392 (* Forward lemmas with finite colength **************************************)
 393
 394 lemma sor_fwd_fcla_sn_ex: ∀f,n. 𝐂❪f❫ ≘ n → ∀f1,f2. f1 ⋓ f2 ≘ f →
 395                           ∃∃n1.  𝐂❪f1❫ ≘ n1 & n1 ≤ n.
 396 #f #n #H elim H -f -n
 397 [ /4 width=4 by sor_fwd_isid1, fcla_isid, ex2_intro/
 398 | #f #n #_ #IH #f1 #f2 #H
 399   elim (sor_inv_xxp … H) -H [ |*: // ] #g1 #g2 #Hf #H1 #H2 destruct
 400   elim (IH … Hf) -f /3 width=3 by fcla_push, ex2_intro/
 401 | #f #n #_ #IH #f1 #f2 #H
 402   elim (sor_inv_xxn … H) -H [1,3,4: * |*: // ] #g1 #g2 #Hf #H1 #H2 destruct
 403   elim (IH … Hf) -f /3 width=3 by fcla_push, fcla_next, nle_succ_bi, nle_succ_dx, ex2_intro/
 404 ]
 405 qed-.
 406
 407 lemma sor_fwd_fcla_dx_ex: ∀f,n. 𝐂❪f❫ ≘ n → ∀f1,f2. f1 ⋓ f2 ≘ f →
 408                           ∃∃n2.  𝐂❪f2❫ ≘ n2 & n2 ≤ n.
 409 /3 width=4 by sor_fwd_fcla_sn_ex, sor_comm/ qed-.
 410
 411 (* Properties with test for finite colength *********************************)
 412
 413 lemma sor_isfin_ex: ∀f1,f2. 𝐅❪f1❫ → 𝐅❪f2❫ → ∃∃f. f1 ⋓ f2 ≘ f & 𝐅❪f❫.
 414 #f1 #f2 * #n1 #H1 * #n2 #H2 elim (sor_fcla_ex … H1 … H2) -H1 -H2
 415 /3 width=4 by ex2_intro, ex_intro/
 416 qed-.
 417
 418 lemma sor_isfin: ∀f1,f2. 𝐅❪f1❫ → 𝐅❪f2❫ → ∀f. f1 ⋓ f2 ≘ f → 𝐅❪f❫.
 419 #f1 #f2 #Hf1 #Hf2 #f #Hf elim (sor_isfin_ex … Hf1 … Hf2) -Hf1 -Hf2
 420 /3 width=6 by sor_mono, isfin_eq_repl_back/
 421 qed-.
 422
 423 (* Forward lemmas with test for finite colength *****************************)
 424
 425 lemma sor_fwd_isfin_sn: ∀f. 𝐅❪f❫ → ∀f1,f2. f1 ⋓ f2 ≘ f → 𝐅❪f1❫.
 426 #f * #n #Hf #f1 #f2 #H
 427 elim (sor_fwd_fcla_sn_ex … Hf … H) -f -f2 /2 width=2 by ex_intro/
 428 qed-.
 429
 430 lemma sor_fwd_isfin_dx: ∀f. 𝐅❪f❫ → ∀f1,f2. f1 ⋓ f2 ≘ f → 𝐅❪f2❫.
 431 #f * #n #Hf #f1 #f2 #H
 432 elim (sor_fwd_fcla_dx_ex … Hf … H) -f -f1 /2 width=2 by ex_intro/
 433 qed-.
 434
 435 (* Inversion lemmas with test for finite colength ***************************)
 436
 437 lemma sor_inv_isfin3: ∀f1,f2,f. f1 ⋓ f2 ≘ f → 𝐅❪f❫ → 𝐅❪f1❫ ∧ 𝐅❪f2❫.
 438 /3 width=4 by sor_fwd_isfin_dx, sor_fwd_isfin_sn, conj/ qed-.
 439
 440 (* Inversion lemmas with inclusion ******************************************)
 441
 442 corec lemma sor_inv_sle_sn: ∀f1,f2,f. f1 ⋓ f2 ≘ f → f1 ⊆ f.
 443 #f1 #f2 #f * -f1 -f2 -f
 444 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0
 445 /3 width=5 by sle_push, sle_next, sle_weak/
 446 qed-.
 447
 448 corec lemma sor_inv_sle_dx: ∀f1,f2,f. f1 ⋓ f2 ≘ f → f2 ⊆ f.
 449 #f1 #f2 #f * -f1 -f2 -f
 450 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0
 451 /3 width=5 by sle_push, sle_next, sle_weak/
 452 qed-.
 453
 454 lemma sor_inv_sle_sn_trans: ∀f1,f2,f. f1 ⋓ f2 ≘ f → ∀g. g ⊆ f1 → g ⊆ f.
 455 /3 width=4 by sor_inv_sle_sn, sle_trans/ qed-.
 456
 457 lemma sor_inv_sle_dx_trans: ∀f1,f2,f. f1 ⋓ f2 ≘ f → ∀g. g ⊆ f2 → g ⊆ f.
 458 /3 width=4 by sor_inv_sle_dx, sle_trans/ qed-.
 459
 460 axiom sor_inv_sle: ∀f1,f2,f. f1 ⋓ f2 ≘ f → ∀g. f1 ⊆ g → f2 ⊆ g → f ⊆ g.
 461
 462 (* Properties with inclusion ************************************************)
 463
 464 corec lemma sor_sle_dx: ∀f1,f2. f1 ⊆ f2 → f1 ⋓ f2 ≘ f2.
 465 #f1 #f2 * -f1 -f2 /3 width=7 by sor_pp, sor_nn, sor_pn/
 466 qed.
 467
 468 corec lemma sor_sle_sn: ∀f1,f2. f1 ⊆ f2 → f2 ⋓ f1 ≘ f2.
 469 #f1 #f2 * -f1 -f2 /3 width=7 by sor_pp, sor_nn, sor_np/
 470 qed.
 471
 472 (* Main properties **********************************************************)
 473
 474 axiom monotonic_sle_sor: ∀f1,g1. f1 ⊆ g1 → ∀f2,g2. f2 ⊆ g2 →
 475                          ∀f. f1 ⋓ f2 ≘ f → ∀g. g1 ⋓ g2 ≘ g → f ⊆ g.
 476
 477 axiom sor_assoc_dx: ∀f0,f3,f4. f0 ⋓ f3 ≘ f4 →
 478                     ∀f1,f2. f1 ⋓ f2 ≘ f0 →
 479                     ∀f. f2 ⋓ f3 ≘ f → f1 ⋓ f ≘ f4.
 480
 481 axiom sor_assoc_sn: ∀f1,f0,f4. f1 ⋓ f0 ≘ f4 →
 482                     ∀f2, f3. f2 ⋓ f3 ≘ f0 →
 483                     ∀f. f1 ⋓ f2 ≘ f → f ⋓ f3 ≘ f4.
 484
 485 lemma sor_comm_23: ∀f0,f1,f2,f3,f4,f.
 486                    f0⋓f4 ≘ f1 → f1⋓f2 ≘ f → f0⋓f2 ≘ f3 → f3⋓f4 ≘ f.
 487 /4 width=6 by sor_comm, sor_assoc_dx/ qed-.
 488
 489 corec theorem sor_comm_23_idem: ∀f0,f1,f2. f0 ⋓ f1 ≘ f2 →
 490                                 ∀f. f1 ⋓ f2 ≘ f → f1 ⋓ f0 ≘ f.
 491 #f0 #f1 #f2 * -f0 -f1 -f2
 492 #f0 #f1 #f2 #g0 #g1 #g2 #Hf2 #H0 #H1 #H2 #g #Hg
 493 [ cases (sor_inv_ppx … Hg … H1 H2)
 494 | cases (sor_inv_pnx … Hg … H1 H2)
 495 | cases (sor_inv_nnx … Hg … H1 H2)
 496 | cases (sor_inv_nnx … Hg … H1 H2)
 497 ] -g2 #f #Hf #H
 498 /3 width=7 by sor_nn, sor_np, sor_pn, sor_pp/
 499 qed-.
 500
 501 corec theorem sor_coll_dx: ∀f1,f2,f. f1 ⋓ f2 ≘ f → ∀g1,g2,g. g1 ⋓ g2 ≘ g →
 502                            ∀g0. g1 ⋓ g0 ≘ f1 → g2 ⋓ g0 ≘ f2 → g ⋓ g0 ≘ f.
 503 #f1 #f2 #f cases (pn_split f) * #x #Hx #Hf #g1 #g2 #g #Hg #g0 #Hf1 #Hf2
 504 [ cases (sor_inv_xxp … Hf … Hx) -Hf #x1 #x2 #Hf #Hx1 #Hx2
 505   cases (sor_inv_xxp … Hf1 … Hx1) -f1 #y1 #y0 #Hf1 #Hy1 #Hy0
 506   cases (sor_inv_xpp … Hf2 … Hy0 … Hx2) -f2 #y2 #Hf2 #Hy2
 507   cases (sor_inv_ppx … Hg … Hy1 Hy2) -g1 -g2 #y #Hg #Hy
 508   @(sor_pp … Hy Hy0 Hx) -g -g0 -f /2 width=8 by/
 509 | cases (pn_split g) * #y #Hy
 510   [ cases (sor_inv_xxp … Hg … Hy) -Hg #y1 #y2 #Hg #Hy1 #Hy2
 511     cases (sor_xxn_tl … Hf … Hx) * #x1 #x2 #_ #Hx1 #Hx2
 512     [ cases (sor_inv_pxn … Hf1 … Hy1 Hx1) -g1 #y0 #Hf1 #Hy0
 513       cases (sor_inv_pnx … Hf2 … Hy2 Hy0) -g2 -x2 #x2 #Hf2 #Hx2
 514     | cases (sor_inv_pxn … Hf2 … Hy2 Hx2) -g2 #y0 #Hf2 #Hy0
 515       cases (sor_inv_pnx … Hf1 … Hy1 Hy0) -g1 -x1 #x1 #Hf1 #Hx1
 516     ]
 517     lapply (sor_inv_nnn … Hf … Hx1 Hx2 Hx) -f1 -f2 #Hf
 518     @(sor_pn … Hy Hy0 Hx) -g -g0 -f /2 width=8 by/
 519   | lapply (sor_tl … Hf) -Hf #Hf
 520     lapply (sor_tl … Hg) -Hg #Hg
 521     lapply (sor_tl … Hf1) -Hf1 #Hf1
 522     lapply (sor_tl … Hf2) -Hf2 #Hf2
 523     cases (pn_split g0) * #y0 #Hy0
 524     [ @(sor_np … Hy Hy0 Hx) /2 width=8 by/
 525     | @(sor_nn … Hy Hy0 Hx) /2 width=8 by/
 526     ]
 527   ]
 528 ]
 529 qed-.
 530
 531 corec theorem sor_distr_dx: ∀g0,g1,g2,g. g1 ⋓ g2 ≘ g →
 532                             ∀f1,f2,f. g1 ⋓ g0 ≘ f1 → g2 ⋓ g0 ≘ f2 → g ⋓ g0 ≘ f →
 533                             f1 ⋓ f2 ≘ f.
 534 #g0 cases (pn_split g0) * #y0 #H0 #g1 #g2 #g
 535 [ * -g1 -g2 -g #y1 #y2 #y #g1 #g2 #g #Hy #Hy1 #Hy2 #Hy #f1 #f2 #f #Hf1 #Hf2 #Hf
 536   [ cases (sor_inv_ppx … Hf1 … Hy1 H0) -g1
 537     cases (sor_inv_ppx … Hf2 … Hy2 H0) -g2
 538     cases (sor_inv_ppx … Hf … Hy H0) -g
 539   | cases (sor_inv_npx … Hf1 … Hy1 H0) -g1
 540     cases (sor_inv_ppx … Hf2 … Hy2 H0) -g2
 541     cases (sor_inv_npx … Hf … Hy H0) -g
 542   | cases (sor_inv_ppx … Hf1 … Hy1 H0) -g1
 543     cases (sor_inv_npx … Hf2 … Hy2 H0) -g2
 544     cases (sor_inv_npx … Hf … Hy H0) -g
 545   | cases (sor_inv_npx … Hf1 … Hy1 H0) -g1
 546     cases (sor_inv_npx … Hf2 … Hy2 H0) -g2
 547     cases (sor_inv_npx … Hf … Hy H0) -g
 548   ] -g0 #y #Hy #H #y2 #Hy2 #H2 #y1 #Hy1 #H1
 549   /3 width=8 by sor_nn, sor_np, sor_pn, sor_pp/
 550 | #H #f1 #f2 #f #Hf1 #Hf2 #Hf
 551   cases (sor_xnx_tl … Hf1 … H0) -Hf1
 552   cases (sor_xnx_tl … Hf2 … H0) -Hf2
 553   cases (sor_xnx_tl … Hf … H0) -Hf
 554   -g0 #y #x #Hx #Hy #H #y2 #x2 #Hx2 #Hy2 #H2 #y1 #x1 #Hx1 #Hy1 #H1
 555   /4 width=8 by sor_tl, sor_nn/
 556 ]
 557 qed-.