1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground/xoa/ex_3_2.ma".
16 include "ground/arith/nat_plus.ma".
17 include "ground/arith/ynat_succ.ma".
19 (* ADDITION FOR NON-NEGATIVE INTEGERS WITH INFINITY *************************)
21 definition yplus_aux (x) (n): ynat ≝
25 definition yplus (x): ynat → ynat ≝
26 ynat_bind_nat (yplus_aux x) (∞).
29 "plus (non-negative integers with infinity)"
30 'plus x y = (yplus x y).
32 (* Basic constructions ******************************************************)
34 lemma yplus_inj_dx (x) (n):
35 (ysucc^n) x = x + yinj_nat n.
36 #x @(ynat_bind_nat_inj (yplus_aux x))
40 lemma yplus_inf_dx (x): ∞ = x + ∞.
44 lemma yplus_zero_dx (x): x = x + 𝟎.
47 (* Constructions with ysucc *************************************************)
50 lemma yplus_unit_dx (x): ↑x = x + 𝟏.
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
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
67 (*** yplus_succ_swap *)
68 lemma yplus_succ_shift (x1) (x2): ↑x1 + x2 = x1 + ↑x2.
71 (* Constructions with nplus *************************************************)
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 //
78 <nplus_succ_dx >ysucc_inj >ysucc_inj <yplus_succ_dx //
81 (* Advanced constructions ***************************************************)
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 //
90 lemma yplus_zero_sn (x): x = 𝟎 + x.
91 #x @(ynat_split_nat_inf … x) -x //
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 //
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 //
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 //
115 lemma yplus_plus_comm_13 (x) (y) (z):
116 x + z + y = y + z + x.
119 (*** yplus_comm_24 *)
120 lemma yplus_plus_comm_24 (x1) (x4) (x2) (x3):
121 x1 + x4 + x3 + x2 = x1 + x2 + x3 + x4.
123 >yplus_assoc >yplus_assoc >yplus_assoc >yplus_assoc //
126 (*** yplus_assoc_23 *)
127 lemma yplus_plus_assoc_23 (x1) (x4) (x2) (x3):
128 x1 + (x2 + x3) + x4 = x1 + x2 + (x3 + x4).
130 >yplus_assoc >yplus_assoc //
133 (* Basic inversions *********************************************************)
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/
141 elim (eq_inv_inf_yinj_nat … H)
145 lemma eq_inv_plus_inf (x) (y):
146 x + y = ∞ → ∨∨ ∞ = x | ∞ = y.
147 /2 width=1 by eq_inv_inf_plus/ qed-.
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/
155 lapply (eq_inv_yinj_nat_bi … H) -H #H
156 <(nplus_refl_sn … H) -n //
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/
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-.
171 (* Inversions with nplus ****************************************************)
173 (*** yplus_inv_inj *)
174 lemma eq_inv_inj_yplus (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) ]
182 /3 width=5 by eq_inv_yinj_nat_bi, ex3_2_intro/
185 lemma eq_inv_yplus_inj (o) (x) (y):
187 ∃∃m,n. o = m + n & x = yinj_nat m & y = yinj_nat n.
189 /2 width=1 by eq_inv_inj_yplus/
192 (* Advanced inversions ******************************************************)
195 lemma eq_inv_zero_yplus (x) (y):
196 (𝟎) = x + y → ∧∧ 𝟎 = x & 𝟎 = y.
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