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 (non-negative integers)"
25 'plus m n = (nplus m n).
27 (* Basic constructions ******************************************************)
30 lemma nplus_zero_dx (m): m = m + ๐.
34 lemma nplus_unit_dx (n): โn = n + ๐.
38 lemma nplus_succ_dx (m) (n): โ(m+n) = m + โn.
39 #m #n @(niter_succ โฆ nsucc)
42 (* Constructions with niter *************************************************)
45 lemma niter_plus (A) (f) (n1) (n2):
46 f^n2 โ f^n1 โ f^{A}(n1+n2).
47 #A #f #n1 #n2 @(nat_ind_succ โฆ n2) -n2 //
48 #n2 #IH <nplus_succ_dx
50 /3 width=5 by compose_repl_fwd_sn, compose_repl_fwd_dx/
53 (* Advanced constructions (semigroup properties) ****************************)
56 lemma nplus_succ_sn (m) (n): โ(m+n) = โm + n.
57 #m #n @(niter_appl โฆ nsucc)
61 lemma nplus_zero_sn (m): m = ๐ + m.
62 #m @(nat_ind_succ โฆ m) -m //
65 (*** commutative_plus *)
66 lemma nplus_comm: commutative โฆ nplus.
67 #m @(nat_ind_succ โฆ m) -m //
68 qed-. (* * gets in the way with auto *)
70 (*** associative_plus *)
71 lemma nplus_assoc: associative โฆ nplus.
72 #m #n #o @(nat_ind_succ โฆ o) -o //
73 #o #IH <nplus_succ_dx <nplus_succ_dx <nplus_succ_dx <IH -IH //
76 (* Helper constructions *****************************************************)
79 lemma nplus_unit_sn (n): โn = ๐ + n.
80 #n <nplus_comm // qed.
82 lemma nplus_succ_shift (m) (n): โm + n = m + โn.
86 lemma nplus_plus_comm_12 (o) (m) (n): m + n + o = n + (m + o).
87 #o #m #n <nplus_comm in โข (??(?%?)?); // qed.
89 (*** plus_plus_comm_23 *)
90 lemma nplus_plus_comm_23 (o) (m) (n): o + m + n = o + n + m.
91 #o #m #n >nplus_assoc >nplus_assoc <nplus_comm in โข (??(??%)?); //
94 (* Basic inversions *********************************************************)
97 lemma eq_inv_zero_nplus (m) (n): ๐ = m + n โ โงโง ๐ = m & ๐ = n.
98 #m #n @(nat_ind_succ โฆ n) -n
100 | #n #_ <nplus_succ_dx #H
101 elim (eq_inv_zero_nsucc โฆ H)
106 lemma eq_inv_nplus_zero (m) (n):
107 m + n = ๐ โ โงโง ๐ = m & ๐ = n.
108 /2 width=1 by eq_inv_zero_nplus/ qed-.
110 (*** injective_plus_l *)
111 lemma eq_inv_nplus_bi_dx (o) (m) (n): m + o = n + o โ m = n.
112 #o @(nat_ind_succ โฆ o) -o /3 width=1 by eq_inv_nsucc_bi/
115 (*** injective_plus_r *)
116 lemma eq_inv_nplus_bi_sn (o) (m) (n): o + m = o + n โ m = n.
117 #o #m #n <nplus_comm <nplus_comm in โข (???%โ?);
118 /2 width=2 by eq_inv_nplus_bi_dx/
121 (*** plus_xSy_x_false *)
122 lemma succ_nplus_refl_sn (m) (n): m = โ(m + n) โ โฅ.
123 #m @(nat_ind_succ โฆ m) -m
124 [ /2 width=2 by eq_inv_zero_nsucc/
126 @(IH n) /2 width=1 by eq_inv_nsucc_bi/
130 (*** discr_plus_xy_y *)
131 lemma nplus_refl_dx (m) (n): n = m + n โ ๐ = m.
132 #m #n @(nat_ind_succ โฆ n) -n //
133 #n #IH /3 width=1 by eq_inv_nsucc_bi/
136 (*** discr_plus_x_xy *)
137 lemma nplus_refl_sn (m) (n): m = m + n โ ๐ = n.
139 /2 width=2 by nplus_refl_dx/
142 (* Advanced eliminations ****************************************************)
145 lemma nat_ind_plus (Q:predicate โฆ):
146 Q (๐) โ (โn. Q n โ Q (๐+n)) โ โn. Q n.
147 #Q #IH1 #IH2 #n @(nat_ind_succ โฆ n) -n /2 width=1 by/