matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.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/ex_3_2.ma".
  16 include "ground/arith/nat_plus.ma".
  17 include "ground/arith/ynat_succ.ma".
  18
  19 (* ADDITION FOR NON-NEGATIVE INTEGERS WITH INFINITY *************************)
  20
  21 definition yplus_aux (x) (n): ynat ≝
  22            ysucc^n x.
  23
  24 (*** yplus *)
  25 definition yplus (x): ynat → ynat ≝
  26            ynat_bind_nat (yplus_aux x) (∞).
  27
  28 interpretation
  29   "plus (non-negative integers with infinity)"
  30   'plus x y = (yplus x y).
  31
  32 (* Basic constructions ******************************************************)
  33
  34 lemma yplus_inj_dx (x) (n):
  35       ysucc^n x = x + yinj_nat n.
  36 #x @(ynat_bind_nat_inj (yplus_aux x))
  37 qed.
  38
  39 (*** yplus_Y2 *)
  40 lemma yplus_inf_dx (x): ∞ = x + ∞.
  41 // qed.
  42
  43 (*** yplus_O2 *)
  44 lemma yplus_zero_dx (x): x = x + 𝟎.
  45 // qed.
  46
  47 (* Constructions with ysucc *************************************************)
  48
  49 (*** yplus_SO2 *)
  50 lemma yplus_one_dx (x): ↑x = x + 𝟏.
  51 // qed.
  52
  53 (*** yplus_S2 yplus_succ2 *)
  54 lemma yplus_succ_dx (x1) (x2): ↑(x1 + x2) = x1 + ↑x2.
  55 #x1 #x2 @(ynat_split_nat_inf … x2) -x2 //
  56 #n2 <ysucc_inj <yplus_inj_dx <yplus_inj_dx
  57 @niter_succ
  58 qed.
  59
  60 (*** yplus_succ1 *)
  61 lemma yplus_succ_sn (x1) (x2): ↑(x1 + x2) = ↑x1 + x2.
  62 #x1 #x2 @(ynat_split_nat_inf … x2) -x2 //
  63 #n2 <yplus_inj_dx <yplus_inj_dx
  64 @niter_appl
  65 qed.
  66
  67 (*** yplus_succ_swap *)
  68 lemma yplus_succ_shift (x1) (x2): ↑x1 + x2 = x1 + ↑x2.
  69 // qed-.
  70
  71 (* Constructions with nplus *************************************************)
  72
  73 (*** yplus_inj *)
  74 lemma yplus_inj_bi (n) (m):
  75       yinj_nat (m + n) = yinj_nat m + yinj_nat n.
  76 #n @(nat_ind_succ … n) -n //
  77 #n #IH #m
  78 <nplus_succ_dx >ysucc_inj >ysucc_inj <yplus_succ_dx //
  79 qed.
  80
  81 (* Advaced constructions ****************************************************)
  82
  83 (*** ysucc_iter_Y yplus_Y1 *)
  84 lemma yplus_inf_sn (x): ∞ = ∞ + x.
  85 #x @(ynat_ind_succ … x) -x //
  86 #n #IH <yplus_succ_dx //
  87 qed.
  88
  89 (*** yplus_O1 *)
  90 lemma yplus_zero_sn (x): x = 𝟎 + x.
  91 #x @(ynat_split_nat_inf … x) -x //
  92 qed.
  93
  94 (*** yplus_comm *)
  95 lemma yplus_comm: commutative … yplus.
  96 #x1 @(ynat_split_nat_inf … x1) -x1 //
  97 #n1 #x2 @(ynat_split_nat_inf … x2) -x2 //
  98 #n2 <yplus_inj_bi <yplus_inj_bi //
  99 qed.
 100
 101 (*** yplus_assoc *)
 102 lemma yplus_assoc: associative … yplus.
 103 #x1 #x2 @(ynat_split_nat_inf … x2) -x2 //
 104 #n2 #x3 @(ynat_split_nat_inf … x3) -x3 //
 105 #n3 @(ynat_split_nat_inf … x1) -x1 //
 106 <yplus_inf_sn //
 107 qed.
 108
 109 (*** yplus_comm_23 *)
 110 lemma yplus_plus_comm_23 (z) (x) (y):
 111       z + x + y = z + y + x.
 112 #z #x #y >yplus_assoc //
 113 qed.
 114
 115 lemma yplus_plus_comm_13 (x) (y) (z):
 116       x + z + y = y + z + x.
 117 // qed.
 118
 119 (*** yplus_comm_24 *)
 120 lemma yplus_plus_comm_24 (x1) (x4) (x2) (x3):
 121       x1 + x4 + x3 + x2 = x1 + x2 + x3 + x4.
 122 #x1 #x4 #x2 #x3
 123 >yplus_assoc >yplus_assoc >yplus_assoc >yplus_assoc //
 124 qed.
 125
 126 (*** yplus_assoc_23 *)
 127 lemma yplus_plus_assoc_23 (x1) (x4) (x2) (x3):
 128       x1 + (x2 + x3) + x4 = x1 + x2 + (x3 + x4).
 129 #x1 #x4 #x2 #x3
 130 >yplus_assoc >yplus_assoc //
 131 qed.
 132
 133 (* Basic inversions *********************************************************)
 134
 135 (*** yplus_inv_Y1 *)
 136 lemma eq_inv_inf_plus (x) (y):
 137       ∞ = x + y → ∨∨ ∞ = x | ∞ = y.
 138 #x @(ynat_split_nat_inf … x) -x /2 width=1 by or_introl/
 139 #m #y @(ynat_split_nat_inf … y) -y /2 width=1 by or_introl/
 140 #n <yplus_inj_bi #H
 141 elim (eq_inv_inf_yinj_nat … H)
 142 qed-.
 143
 144 (*** yplus_inv_Y2 *)
 145 lemma eq_inv_plus_inf (x) (y):
 146       x + y = ∞ → ∨∨ ∞ = x | ∞ = y.
 147 /2 width=1 by eq_inv_inf_plus/ qed-.
 148
 149 (*** discr_yplus_x_xy discr_yplus_xy_x *)
 150 lemma yplus_refl_sn (x) (y):
 151       x = x + y → ∨∨ ∞ = x | 𝟎 = y.
 152 #x @(ynat_split_nat_inf … x) -x /2 width=1 by or_introl/
 153 #m #y @(ynat_split_nat_inf … y) -y /2 width=1 by or_introl/
 154 #n <yplus_inj_bi #H
 155 lapply (eq_inv_yinj_nat_bi … H) -H #H
 156 <(nplus_refl_sn … H) -n //
 157 qed-.
 158
 159 (*** yplus_inv_monotonic_dx_inj *)
 160 lemma eq_inv_yplus_bi_dx_inj (o) (x) (y):
 161       x + yinj_nat o = y + yinj_nat o → x = y.
 162 #o @(nat_ind_succ … o) -o //
 163 #o #IH #x #y >ysucc_inj <yplus_succ_dx <yplus_succ_dx #H
 164 /3 width=1 by eq_inv_ysucc_bi/
 165 qed-.
 166
 167 lemma eq_inv_yplus_bi_sn_inj (o) (x) (y):
 168       yinj_nat o + x = yinj_nat o + y → x = y.
 169 /2 width=2 by eq_inv_yplus_bi_dx_inj/ qed-.
 170
 171 (* Inversions with nplus ****************************************************)
 172
 173 (*** yplus_inv_inj *)
 174 lemma eq_inv_inj_yplus (o) (x) (y):
 175       yinj_nat o = x + y →
 176       ∃∃m,n. o = m + n & x = yinj_nat m & y = yinj_nat n.
 177 #o #x @(ynat_split_nat_inf … x) -x
 178 [| #y <yplus_inf_sn #H elim (eq_inv_yinj_nat_inf … H) ]
 179 #m #y @(ynat_split_nat_inf … y) -y
 180 [| #H elim (eq_inv_yinj_nat_inf … H) ]
 181 #n <yplus_inj_bi #H
 182 /3 width=5 by eq_inv_yinj_nat_bi, ex3_2_intro/
 183 qed-.
 184
 185 lemma eq_inv_yplus_inj (o) (x) (y):
 186       x + y = yinj_nat o →
 187       ∃∃m,n. o = m + n & x = yinj_nat m & y = yinj_nat n.
 188 #o #x #y <yplus_comm
 189 /2 width=1 by eq_inv_inj_yplus/
 190 qed-.
 191
 192 (* Advanced inversions ******************************************************)
 193
 194 (*** yplus_inv_O *)
 195 lemma eq_inv_zero_yplus (x) (y):
 196       (𝟎) = x + y → ∧∧ 𝟎 = x & 𝟎 = y.
 197 #x #y #H
 198 elim (eq_inv_inj_yplus (𝟎) ?? H) -H #m #n #H #H1 #H2 destruct
 199 elim (eq_inv_zero_nplus … H) -H #H1 #H2 destruct
 200 /2 width=1 by conj/
 201 qed-.