(*** plus *)
definition nplus: nat → nat → nat ≝
- λm,n. nsucc^n m.
+ λm,n. (nsucc^n) m.
interpretation
- "plus (positive integers)"
+ "plus (non-negative integers)"
'plus m n = (nplus m n).
(* Basic constructions ******************************************************)
// qed.
(*** plus_SO_dx *)
-lemma nplus_one_dx (n): ↑n = n + 𝟏.
+lemma nplus_unit_dx (n): ↑n = n + 𝟏.
// qed.
(*** plus_n_Sm *)
(* Constructions with niter *************************************************)
(*** iter_plus *)
-lemma niter_plus (A) (f) (a) (n1) (n2):
- f^n1 (f^n2 a) = f^{A}(n1+n2) a.
-#A #f #a #n1 #n2 @(nat_ind_succ … n2) -n2 //
-#n2 #IH <nplus_succ_dx <niter_succ <niter_succ <niter_appl //
+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.
-(* Advanved constructions (semigroup properties) ****************************)
+(* 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 *)
+(*** plus_O_n *)
lemma nplus_zero_sn (m): m = 𝟎 + m.
#m @(nat_ind_succ … m) -m //
qed.
(*** commutative_plus *)
lemma nplus_comm: commutative … nplus.
#m @(nat_ind_succ … m) -m //
-qed-.
+qed-. (* * gets in the way with auto *)
(*** associative_plus *)
lemma nplus_assoc: associative … nplus.
(* Helper constructions *****************************************************)
(*** plus_SO_sn *)
-lemma nplus_one_sn (n): ↑n = 𝟏 + n.
+lemma nplus_unit_sn (n): ↑n = 𝟏 + n.
#n <nplus_comm // qed.
lemma nplus_succ_shift (m) (n): ↑m + n = m + ↑n.
-// qed-.
+// qed.
(*** assoc_plus1 *)
lemma nplus_plus_comm_12 (o) (m) (n): m + n + o = n + (m + o).
(*** 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.
+(*** 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_nzero_succ … 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_succ … o) -o /3 width=1 by eq_inv_nsucc_bi/
/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 *)