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/arith/nat_succ_iter.ma".
17 (* ADDITION FOR NON-NEGATIVE INTEGERS ***************************************)
20 definition nplus: nat → nat → nat ≝
24 "plus (positive integers"
25 'plus m n = (nplus m n).
27 (* Basic rewrites ***********************************************************)
30 lemma nplus_zero_dx (m): m = m + 𝟎.
33 lemma nplus_one_dx (n): ↑n = n + 𝟏.
36 (* Advanved rewrites (semigroup properties) *********************************)
39 lemma nplus_succ_dx (m) (n): ↑(m+n) = m + ↑n.
40 #m #n @(niter_succ … nsucc)
43 lemma nplus_succ_sn (m) (n): ↑(m+n) = ↑m + n.
44 #m #n @(niter_appl … nsucc)
48 lemma nplus_zero_sn (m): m = 𝟎 + m.
49 #m @(nat_ind … m) -m //
52 (*** commutative_plus *)
53 lemma nplus_comm: commutative … nplus.
54 #m @(nat_ind … m) -m //
57 (*** associative_plus *)
58 lemma nplus_assoc: associative … nplus.
59 #m #n #o @(nat_ind … o) -o //
60 #o #IH <nplus_succ_dx <nplus_succ_dx <nplus_succ_dx <IH -IH //
63 (* Advanced constructions ***************************************************)
65 lemma nplus_one_sn (n): ↑n = 𝟏 + n.
66 #n <nplus_comm // qed.
68 lemma nplus_succ_shift (m) (n): ↑m + n = m + ↑n.
72 lemma nplus_plus_comm_12 (o) (m) (n): m + n + o = n + (m + o).
73 #o #m #n <nplus_comm in ⊢ (??(?%?)?); // qed.
75 (*** plus_plus_comm_23 *)
76 lemma nplus_plus_comm_23 (o) (m) (n): o + m + n = o + n + m.
77 #o #m #n >nplus_assoc >nplus_assoc <nplus_comm in ⊢ (??(??%)?); //
80 (* Basic inversions *********************************************************)
82 lemma eq_inv_nzero_plus (m) (n): 𝟎 = m + n → ∧∧ 𝟎 = m & 𝟎 = n.
83 #m #n @(nat_ind … n) -n /2 width=1 by conj/
84 #n #_ <nplus_succ_dx #H
85 elim (eq_inv_nzero_succ … H)
88 (*** injective_plus_l *)
89 lemma eq_inv_nplus_bi_dx (o) (m) (n): m + o = n + o → m = n.
90 #o @(nat_ind … o) -o /3 width=1 by eq_inv_nsucc_bi/
93 (*** injective_plus_r *)
94 lemma eq_inv_nplus_bi_sn (o) (m) (n): o + m = o + n → m = n.
95 #o #m #n <nplus_comm <nplus_comm in ⊢ (???%→?);
96 /2 width=2 by eq_inv_nplus_bi_dx/
99 (* Advanced eliminations ****************************************************)
102 lemma nat_ind_plus (Q:predicate …):
103 Q (𝟎) → (∀n. Q n → Q (𝟏+n)) → ∀n. Q n.
104 #Q #IH1 #IH2 #n @(nat_ind … n) -n /2 width=1 by/