(* *)
(**************************************************************************)
-include "ground/arith/nat_iter_succ.ma".
+include "ground/arith/nat_succ_iter.ma".
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* ADDITION FOR NON-NEGATIVE INTEGERS ***************************************)
(*** plus *)
definition nplus: nat โ nat โ nat โ
ฮปm,n. nsucc^n m.
interpretation
- "plus (positive integers"
+ "plus (non-negative integers)"
'plus m n = (nplus m n).
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
(*** plus_n_O *)
lemma nplus_zero_dx (m): m = m + ๐.
// qed.
+(*** plus_SO_dx *)
lemma nplus_one_dx (n): โn = n + ๐.
// qed.
-(* Semigroup properties *****************************************************)
-
(*** plus_n_Sm *)
lemma nplus_succ_dx (m) (n): โ(m+n) = m + โn.
#m #n @(niter_succ โฆ nsucc)
qed.
+(* Constructions with niter *************************************************)
+
+(*** iter_plus *)
+lemma niter_plus (A) (f) (n1) (n2):
+ f^n2 โ f^n1 โ f^{A}(n1+n2).
+#A #f #n1 #n2 @(nat_ind_succ โฆ n2) -n2 //
+#n2 #IH <nplus_succ_dx
+@exteq_repl
+/3 width=5 by compose_repl_fwd_sn, compose_repl_fwd_dx/
+qed.
+
+(* Advanced constructions (semigroup properties) ****************************)
+
+(*** plus_S1 *)
lemma nplus_succ_sn (m) (n): โ(m+n) = โm + n.
#m #n @(niter_appl โฆ nsucc)
qed.
(*** plus_O_n.con *)
lemma nplus_zero_sn (m): m = ๐ + m.
-#m @(nat_ind โฆ m) -m //
+#m @(nat_ind_succ โฆ m) -m //
qed.
(*** commutative_plus *)
lemma nplus_comm: commutative โฆ nplus.
-#m @(nat_ind โฆ m) -m //
-qed-.
-
-lemma nplus_one_sn (n): โn = ๐ + n.
-#n <nplus_comm // qed.
+#m @(nat_ind_succ โฆ m) -m //
+qed-. (* * gets in the way with auto *)
(*** associative_plus *)
lemma nplus_assoc: associative โฆ nplus.
-#m #n #o @(nat_ind โฆ o) -o //
+#m #n #o @(nat_ind_succ โฆ o) -o //
#o #IH <nplus_succ_dx <nplus_succ_dx <nplus_succ_dx <IH -IH //
qed.
+(* Helper constructions *****************************************************)
+
+(*** plus_SO_sn *)
+lemma nplus_one_sn (n): โn = ๐ + n.
+#n <nplus_comm // qed.
+
+lemma nplus_succ_shift (m) (n): โm + n = m + โn.
+// qed.
+
(*** assoc_plus1 *)
lemma nplus_plus_comm_12 (o) (m) (n): m + n + o = n + (m + o).
#o #m #n <nplus_comm in โข (??(?%?)?); // qed.
(*** plus_plus_comm_23 *)
lemma nplus_plus_comm_23 (o) (m) (n): o + m + n = o + n + m.
#o #m #n >nplus_assoc >nplus_assoc <nplus_comm in โข (??(??%)?); //
-qed-.
+qed.
(* Basic inversions *********************************************************)
-lemma eq_inv_nzero_plus (m) (n): ๐ = m + n โ โงโง ๐ = m & ๐ = n.
-#m #n @(nat_ind โฆ n) -n /2 width=1 by conj/
-#n #_ <nplus_succ_dx #H
-elim (eq_inv_nzero_succ โฆ H)
+(*** zero_eq_plus *)
+lemma eq_inv_zero_nplus (m) (n): ๐ = m + n โ โงโง ๐ = m & ๐ = n.
+#m #n @(nat_ind_succ โฆ n) -n
+[ /2 width=1 by conj/
+| #n #_ <nplus_succ_dx #H
+ elim (eq_inv_zero_nsucc โฆ H)
+]
qed-.
+(*** plus_inv_O3 *)
+lemma eq_inv_nplus_zero (m) (n):
+ m + n = ๐ โ โงโง ๐ = m & ๐ = n.
+/2 width=1 by eq_inv_zero_nplus/ qed-.
+
(*** injective_plus_l *)
lemma eq_inv_nplus_bi_dx (o) (m) (n): m + o = n + o โ m = n.
-#o @(nat_ind โฆ o) -o /3 width=1 by eq_inv_nsucc_bi/
+#o @(nat_ind_succ โฆ o) -o /3 width=1 by eq_inv_nsucc_bi/
qed-.
(*** injective_plus_r *)
lemma eq_inv_nplus_bi_sn (o) (m) (n): o + m = o + n โ m = n.
#o #m #n <nplus_comm <nplus_comm in โข (???%โ?);
-/2 width=2 by eq_inv_nplus_bi_dx/ qed-.
+/2 width=2 by eq_inv_nplus_bi_dx/
+qed-.
+
+(*** plus_xSy_x_false *)
+lemma succ_nplus_refl_sn (m) (n): m = โ(m + n) โ โฅ.
+#m @(nat_ind_succ โฆ m) -m
+[ /2 width=2 by eq_inv_zero_nsucc/
+| #m #IH #n #H
+ @(IH n) /2 width=1 by eq_inv_nsucc_bi/
+]
+qed-.
+
+(*** discr_plus_xy_y *)
+lemma nplus_refl_dx (m) (n): n = m + n โ ๐ = m.
+#m #n @(nat_ind_succ โฆ n) -n //
+#n #IH /3 width=1 by eq_inv_nsucc_bi/
+qed-.
+
+(*** discr_plus_x_xy *)
+lemma nplus_refl_sn (m) (n): m = m + n โ ๐ = n.
+#m #n <nplus_comm
+/2 width=2 by nplus_refl_dx/
+qed-.
(* Advanced eliminations ****************************************************)
(*** nat_ind_plus *)
lemma nat_ind_plus (Q:predicate โฆ):
Q (๐) โ (โn. Q n โ Q (๐+n)) โ โn. Q n.
-#Q #IH1 #IH2 #n @(nat_ind โฆ n) -n /2 width=1 by/
+#Q #IH1 #IH2 #n @(nat_ind_succ โฆ n) -n /2 width=1 by/
qed-.