(* *)
(**************************************************************************)
-include "basic_2/rt_computation/fpbg_fqus.ma".
include "basic_2/rt_computation/fpbs_cpxs.ma".
-include "basic_2/rt_computation/fpbg_fpbs.ma".
+include "basic_2/rt_computation/fpbg_fqus.ma".
(* EXAMPLES *****************************************************************)
"cic:/matita/arithmetics/nat/monotonic_pred.con"
#
"cic:/matita/arithmetics/nat/S_pred.con"
-
-####################################
-
-"cic:/matita/arithmetics/nat/discr_minus_x_xy.con"
-"cic:/matita/arithmetics/nat/discr_plus_xy_minus_xz.con"
-"cic:/matita/arithmetics/nat/eq_minus_O.con"
+#
+"cic:/matita/arithmetics/nat/minus.con"
+"cic:/matita/arithmetics/nat/minus_n_O.con"
"cic:/matita/arithmetics/nat/eq_minus_S_pred.con"
+"cic:/matita/arithmetics/nat/minus_O_n.con"
+"cic:/matita/arithmetics/nat/minus_S_S.con"
+"cic:/matita/arithmetics/nat/minus_n_n.con"
+"cic:/matita/arithmetics/nat/minus_Sn_n.con"
+"cic:/matita/arithmetics/nat/minus_minus_comm.con"
+#
+"cic:/matita/arithmetics/nat/minus_plus_m_m.con"
+"cic:/matita/arithmetics/nat/minus_plus.con"
+"cic:/matita/arithmetics/nat/minus_plus_plus_l.con"
+"cic:/matita/arithmetics/nat/plus_minus_plus_plus_l.con"
+"cic:/matita/arithmetics/nat/plus_to_minus.con"
+"cic:/matita/arithmetics/nat/discr_plus_xy_minus_xz.con"
+"cic:/matita/arithmetics/nat/discr_minus_x_xy.con"
+#
+"cic:/matita/arithmetics/nat/minus_le.con"
"cic:/matita/arithmetics/nat/inv_eq_minus_O.con"
-"cic:/matita/arithmetics/nat/le_minus_to_plus.con"
-"cic:/matita/arithmetics/nat/le_minus_to_plus_r.con"
+"cic:/matita/arithmetics/nat/monotonic_le_minus_l.con"
+"cic:/matita/arithmetics/nat/monotonic_le_minus_r.con"
+"cic:/matita/arithmetics/nat/eq_minus_O.con"
+"cic:/matita/arithmetics/nat/minus_Sn_m.con"
+"cic:/matita/arithmetics/nat/minus_minus_m_m.con"
+#
"cic:/matita/arithmetics/nat/le_plus_minus_m_m.con"
"cic:/matita/arithmetics/nat/le_plus_to_minus.con"
"cic:/matita/arithmetics/nat/le_plus_to_minus_r.con"
-"cic:/matita/arithmetics/nat/lt_minus_to_plus.con"
-"cic:/matita/arithmetics/nat/lt_minus_to_plus_r.con"
-"cic:/matita/arithmetics/nat/lt_plus_to_minus.con"
-"cic:/matita/arithmetics/nat/lt_plus_to_minus_r.con"
-"cic:/matita/arithmetics/nat/minus.con"
-"cic:/matita/arithmetics/nat/minus_le.con"
-"cic:/matita/arithmetics/nat/minus_le_minus_minus_comm.con"
+"cic:/matita/arithmetics/nat/le_inv_plus_l.con"
+"cic:/matita/arithmetics/nat/plus_minus_m_m.con"
+"cic:/matita/arithmetics/nat/le_minus_to_plus.con"
+"cic:/matita/arithmetics/nat/le_minus_to_plus_r.con"
+"cic:/matita/arithmetics/nat/plus_minus.con"
+"cic:/matita/arithmetics/nat/plus_minus_associative.con"
"cic:/matita/arithmetics/nat/minus_minus_associative.con"
-"cic:/matita/arithmetics/nat/minus_minus_comm.con"
"cic:/matita/arithmetics/nat/minus_minus.con"
-"cic:/matita/arithmetics/nat/minus_minus_m_m.con"
-"cic:/matita/arithmetics/nat/minus_n_n.con"
-"cic:/matita/arithmetics/nat/minus_n_O.con"
-"cic:/matita/arithmetics/nat/minus_O_n.con"
-"cic:/matita/arithmetics/nat/minus_plus.con"
-"cic:/matita/arithmetics/nat/minus_plus_m_m.con"
-"cic:/matita/arithmetics/nat/minus_plus_plus_l.con"
+"cic:/matita/arithmetics/nat/minus_le_minus_minus_comm.con"
+#
"cic:/matita/arithmetics/nat/minus_pred_pred.con"
-"cic:/matita/arithmetics/nat/minus_Sn_m.con"
-"cic:/matita/arithmetics/nat/minus_Sn_n.con"
-"cic:/matita/arithmetics/nat/minus_S_S.con"
-"cic:/matita/arithmetics/nat/monotonic_le_minus_l.con"
-"cic:/matita/arithmetics/nat/monotonic_le_minus_r.con"
"cic:/matita/arithmetics/nat/monotonic_lt_minus_l.con"
-"cic:/matita/arithmetics/nat/plus_minus_associative.con"
-"cic:/matita/arithmetics/nat/plus_minus.con"
-"cic:/matita/arithmetics/nat/plus_minus_m_m.con"
-"cic:/matita/arithmetics/nat/plus_minus_plus_plus_l.con"
-"cic:/matita/arithmetics/nat/plus_to_minus.con"
-"cic:/matita/arithmetics/nat/le_inv_plus_l.con"
+
+"cic:/matita/arithmetics/nat/lt_minus_to_plus.con"
+"cic:/matita/arithmetics/nat/lt_minus_to_plus_r.con"
+"cic:/matita/arithmetics/nat/lt_plus_to_minus.con"
+"cic:/matita/arithmetics/nat/lt_plus_to_minus_r.con"
"cic:/matita/arithmetics/nat/lt_inv_plus_l.con"
+####################################
+
"cic:/matita/arithmetics/nat/to_max.con"
"cic:/matita/arithmetics/nat/commutative_max.con"
"cic:/matita/arithmetics/nat/leb.con"
include "ground/arith/pnat_iter.ma".
include "ground/arith/nat.ma".
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* ITERATED FUNCTION FOR NON-NEGATIVE INTEGERS ******************************)
definition niter (n:nat) (A:Type[0]) (f:A→A) (a:A) ≝
match n with
include "ground/insert_eq/insert_eq_0.ma".
include "ground/arith/nat_succ.ma".
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* ORDER FOR NON-NEGATIVE INTEGERS ******************************************)
(*** le *)
(*** le_ind *)
]
qed-.
+(* Advanced inversions ******************************************************)
+
+lemma nle_inv_succ_zero (m): ↑m ≤ 𝟎 → ⊥.
+/3 width=2 by nle_inv_zero_dx, eq_inv_nzero_succ/ qed-.
+
lemma nle_inv_succ_sn_refl (m): ↑m ≤ m → ⊥.
#m @(nat_ind … m) -m [| #m #IH ] #H
[ /3 width=2 by nle_inv_zero_dx, eq_inv_nzero_succ/
]
qed-.
-(* Order properties *********************************************************)
-
(*** le_to_le_to_eq *)
theorem nle_antisym (m) (n): m ≤ n → n ≤ m → m = n.
#m #n #H elim H -n //
elim (nle_inv_succ_sn_refl … Hn)
qed-.
+(* Advanced eliminations ****************************************************)
+
+lemma nle_ind_alt (Q: relation2 nat nat):
+ (∀n. Q (𝟎) (n)) →
+ (∀m,n. m ≤ n → Q m n → Q (↑m) (↑n)) →
+ ∀m,n. m ≤ n → Q m n.
+#Q #IH1 #IH2 #m #n @(nat_ind_2 … m n) -m -n //
+[ #m #H elim (nle_inv_succ_zero … H)
+| /4 width=1 by nle_inv_succ_bi/
+]
+qed-.
+
+(* Advanced constructions ***************************************************)
+
(*** transitive_le *)
theorem nle_trans: Transitive … nle.
#m #n #H elim H -n /3 width=1 by nle_inv_succ_sn/
qed-.
-(* Advanced constructions ***************************************************)
-
(*** decidable_le *)
lemma nle_dec (m) (n): Decidable … (m ≤ n).
#m #n elim (nle_ge_e m n) [ /2 width=1 by or_introl/ ]
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_minus.ma".
+include "ground/arith/nat_le_pred.ma".
+
+(* ORDER FOR NON-NEGATIVE INTEGERS ******************************************)
+
+(* Constructions with nminus ************************************************)
+
+(*** minus_le *)
+lemma nle_minus_sn_refl_sn (m) (n): m - n ≤ m.
+#m #n elim n -n //
+#n #IH /2 width=3 by nle_trans/
+qed.
+
+(*** inv_eq_minus_O *)
+lemma nle_eq_minus_O (m) (n): 𝟎 = m - n → m ≤ n.
+#m #n @(nat_ind_2 … m n) //
+/3 width=1 by nle_succ_bi/
+qed.
+
+(*** monotonic_le_minus_l *)
+lemma nle_minus_sn_bi (m) (n) (o): m ≤ n → m-o ≤ n-o.
+#m #n #o elim o -o //
+#o #IH #Hmn /3 width=1 by nle_pred_bi/
+qed.
+
+(*** monotonic_le_minus_r *)
+lemma nle_minus_dx_bi (m) (n) (o): m ≤ n → o-n ≤ o-m.
+#m #n #o #H elim H -n //
+#n #_ #IH /2 width=3 by nle_trans/
+qed.
+
+(* Inversions with nminus ***************************************************)
+
+(*** eq_minus_O *)
+lemma nle_inv_eq_minus_O (m) (n): m ≤ n → 𝟎 = m - n.
+#m #n #H elim H -n //
+qed-.
+
+(* Destructions with nminus *************************************************)
+
+(*** minus_Sn_m *)
+lemma nminus_succ_sn (m) (n): m ≤ n → ↑(n-m) = ↑n - m.
+#m #n #H @(nle_ind_alt … H) -m -n //
+qed-.
+
+(*** minus_minus_m_m *)
+lemma nminus_minus_dx_refl_sn (m) (n): m ≤ n → m = n - (n - m).
+#m #n #H elim H -n //
+#n #Hmn #IH <(nminus_succ_sn … Hmn) -Hmn //
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_minus_plus.ma".
+include "ground/arith/nat_le_plus.ma".
+include "ground/arith/nat_le_minus.ma".
+
+(* ORDER FOR NON-NEGATIVE INTEGERS ******************************************)
+
+(* Constructions with nminus and nplus **************************************)
+
+(*** le_plus_minus_m_m *)
+lemma nle_plus_minus_sn_refl_sn (n) (m): m ≤ m - n + n.
+#n elim n -n //
+#n #IH #m <nminus_succ_dx_pred_sn <nplus_succ_dx
+/2 width=1 by nle_inv_pred_sn/
+qed.
+
+lemma plus_minus_sn_refl_sn_nle (m) (n): n = n - m + m → m ≤ n.
+// qed.
+
+(*** le_plus_to_minus *)
+lemma nle_minus_sn (o) (m) (n): m ≤ n + o → m - o ≤ n.
+/2 width=1 by nle_minus_sn_bi/ qed.
+
+(*** le_plus_to_minus_r *)
+lemma nle_minus_dx (o) (m) (n): m + o ≤ n → m ≤ n - o.
+#o #m #n #H >(nminus_plus_sn_refl_sn m o)
+/2 width=1 by nle_minus_sn_bi/
+qed.
+
+(*** le_inv_plus_l *)
+lemma nle_minus_dx_full (o) (m) (n): m + o ≤ n → ∧∧ m ≤ n - o & o ≤ n.
+/3 width=3 by nle_minus_dx, nle_trans, conj/ qed-.
+
+(* Inversions with nminus and nplus *****************************************)
+
+(*** plus_minus_m_m *)
+lemma nplus_minus_sn_refl_sn (m) (n): m ≤ n → n = n - m + m.
+#m #n #H elim H -n //
+#n #Hn #IH <(nminus_succ_sn … Hn) -Hn
+<nplus_succ_sn //
+qed-.
+
+lemma nplus_minus_dx_refl_sn (m) (n): m ≤ n → n = m + (n - m).
+#m #n <nplus_comm
+/2 width=1 by nplus_minus_sn_refl_sn/
+qed-.
+
+(*** le_minus_to_plus *)
+lemma nle_inv_minus_sn (o) (m) (n): m - o ≤ n → m ≤ n + o.
+/3 width=3 by nle_plus_bi_dx, nle_trans/ qed-.
+
+(*** le_minus_to_plus_r *)
+lemma nle_inv_minus_dx (o) (m) (n): o ≤ n → m ≤ n - o → m + o ≤ n.
+#o #m #n #Hon #Hm
+>(nplus_minus_sn_refl_sn … Hon)
+/2 width=1 by nle_plus_bi_dx/
+qed-.
+
+(* Destructions with nminus and nplus ***************************************)
+
+(*** plus_minus *)
+lemma nminus_plus_comm_23 (o) (m) (n):
+ m ≤ n → n - m + o = n + o - m.
+#o #m #n #H elim H -n //
+#n #Hn #IH <(nminus_succ_sn … Hn)
+<nplus_succ_sn <nplus_succ_sn <nminus_succ_sn //
+/2 width=3 by nle_trans/
+qed-.
+
+(*** plus_minus_associative *)
+lemma nplus_minus_assoc (m1) (m2) (n):
+ n ≤ m2 → m1 + m2 - n = m1 + (m2 - n).
+/2 width=1 by nminus_plus_comm_23/ qed-.
+
+(*** minus_minus_associative *)
+theorem nminus_assoc (m1) (m2) (m3):
+ m3 ≤ m2 → m2 ≤ m1 → m1 - m2 + m3 = m1 - (m2 - m3).
+#m1 #m2 #m3 #Hm32 #Hm21
+@nminus_plus_sn >nplus_assoc
+<nplus_minus_dx_refl_sn //
+/2 width=1 by nplus_minus_sn_refl_sn/
+qed-.
+
+(*** minus_minus *)
+theorem nminus_assoc_comm (m1) (m2) (m3):
+ m3 ≤ m2 → m2 ≤ m1 → m3 + (m1 - m2) = m1 - (m2 - m3).
+#m1 #m2 #m3 #Hm32 #Hm21 <nplus_comm
+/2 width=1 by nminus_assoc/
+qed-.
+
+(*** minus_le_minus_minus_comm *)
+theorem minus_assoc_comm_23 (m1) (m2) (m3):
+ m3 ≤ m2 → m1 + m3 - m2 = m1 - (m2 - m3).
+#m1 #m2 #m3 #Hm
+>(nplus_minus_sn_refl_sn … Hm) in ⊢ (??%?); //
+qed-.
include "ground/arith/nat_plus.ma".
include "ground/arith/nat_le.ma".
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* ORDER FOR NON-NEGATIVE INTEGERS ****************************************************)
-(* Basic constructions with plus ********************************************)
+(* Constructions with nplus ***********************************************************)
(*** monotonic_le_plus_l *)
lemma nle_plus_bi_dx (m) (n1) (n2): n1 ≤ n2 → n1 + m ≤ n2 + m.
lemma nle_plus_dx_sn (m) (n) (o): n ≤ m → n ≤ o + m.
/2 width=3 by nle_trans/ qed.
-(* Main constructions with plus *********************************************)
+(* Main constructions with nplus ********************************************)
(*** le_plus *)
theorem nle_plus_bi (m1) (m2) (n1) (n2):
m1 ≤ m2 → n1 ≤ n2 → m1 + n1 ≤ m2 + n2.
/3 width=3 by nle_plus_bi_dx, nle_plus_bi_sn, nle_trans/ qed.
-(* Basic inversions with plus ***********************************************)
+(* Inversions with nplus ****************************************************)
(*** plus_le_0 *)
lemma nle_inv_plus_zero (m) (n): m + n ≤ 𝟎 → ∧∧ 𝟎 = m & 𝟎 = n.
(*** le_plus_to_le *)
lemma nle_inv_plus_bi_sn (o) (m) (n): o + n ≤ o + m → n ≤ m.
/2 width=2 by nle_inv_plus_bi_dx/ qed-.
-
include "ground/arith/nat_pred_succ.ma".
include "ground/arith/nat_le.ma".
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* ORDER FOR NON-NEGATIVE INTEGERS ******************************************)
-(* Basic constructions with pred ********************************************)
+(* Constructions with npred *************************************************)
(*** le_pred_n *)
lemma nle_pred_sn_refl (m): ↓m ≤ m.
(*** monotonic_pred *)
lemma nle_pred_bi (m) (n): m ≤ n → ↓m ≤ ↓n.
-#m #n #H elim H -n
+#m #n #H elim H -n //
/2 width=3 by nle_trans/
qed.
+
+lemma nle_pred_sn (m) (n): m ≤ ↑n → ↓m ≤ n.
+#m #n elim m -m //
+/2 width=1 by nle_pred_bi/
+qed-.
+
+(* Destructions with npred **************************************************)
+
+lemma nle_inv_pred_sn (m) (n): ↓m ≤ n → m ≤ ↑n.
+#m #n elim m -m
+/2 width=1 by nle_succ_bi/
+qed-.
include "ground/arith/nat_le.ma".
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS ***********************************)
(*** lt *)
definition nlt: relation2 nat nat ≝
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_le_minus.ma".
+include "ground/arith/nat_lt_pred.ma".
+
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS ***********************************)
+
+(* Rewrites with nminus *****************************************************)
+
+(*** minus_pred_pred *)
+lemma nminus_pred_bi (m) (n): 𝟎 < m → 𝟎 < n → n - m = ↓n - ↓m.
+#m #n #Hm #Hn
+>(nlt_inv_zero_sn … Hm) in ⊢ (??%?); -Hm
+>(nlt_inv_zero_sn … Hn) in ⊢ (??%?); -Hn
+//
+qed-.
+
+(* Constructions with nminus ************************************************)
+
+(*** monotonic_lt_minus_l *)
+lemma nlt_minus_sn_bi (o) (m) (n): o ≤ m → m < n → m - o < n - o.
+#o #m #n #Hom #Hmn
+lapply (nle_minus_sn_bi … o Hmn) -Hmn
+<(nminus_succ_sn … Hom) //
+qed.
include "ground/arith/nat_le_plus.ma".
include "ground/arith/nat_lt.ma".
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS ***********************************)
-(* Basic constructions with plus ********************************************)
+(* Constructions with nplus *************************************************)
(*** monotonic_lt_plus_l *)
lemma nlt_plus_bi_dx (m) (n1) (n2): n1 < n2 → n1 + m < n2 + m.
lemma lt_plus_Sn_r: ∀a,x,n. a < a + x + ↑n.
/2 width=1/ qed-.
-(* Basic inversions with plus ***********************************************)
+(* Inversions with nplus ****************************************************)
(*** lt_plus_to_lt_l *)
lemma nlt_inv_plus_bi_dx (m) (n1) (n2): n1 + m < n2 + m → n1 < n2.
include "ground/arith/nat_pred_succ.ma".
include "ground/arith/nat_lt.ma".
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS ***********************************)
-(* Basic constructions with pred ********************************************)
+(* Constructions with npred *************************************************)
lemma nlt_zero_sn (m): m = ↑↓m → 𝟎 < m.
// qed.
-(* Basic inversions with pred ***********************************************)
+(* Inversions with npred ****************************************************)
(*** S_pred *)
lemma nlt_inv_zero_sn (m): 𝟎 < m → m = ↑↓m.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_succ_iter.ma".
+include "ground/arith/nat_pred_succ.ma".
+
+(* SUBTRACTION FOR NON-NEGATIVE INTEGERS ************************************)
+
+(*** minus *)
+definition nminus: nat → nat → nat ≝
+ λm,n. npred^n m.
+
+interpretation
+ "minus (positive integers"
+ 'minus m n = (nminus m n).
+
+(* Basic rewrites ***********************************************************)
+
+(*** minus_n_O *)
+lemma nminus_zero_dx (m): m = m - 𝟎.
+// qed.
+
+lemma nminus_pred_sn (m) (n): ↓(m - n) = ↓m - n.
+#m #n @(niter_appl … npred)
+qed.
+
+(*** eq_minus_S_pred *)
+lemma nminus_succ_dx (m) (n): ↓(m - n) = m - ↑n.
+#m #n @(niter_succ … npred)
+qed.
+
+(*** minus_O_n *)
+lemma nminus_zero_sn (n): 𝟎 = 𝟎 - n.
+#n elim n -n //
+qed.
+
+(*** minus_S_S *)
+lemma nminus_succ_bi (m) (n): m - n = ↑m - ↑n.
+#m #n elim n -n //
+qed.
+
+(* Advanced rewrites ********************************************************)
+
+lemma nminus_succ_dx_pred_sn (m) (n): ↓m - n = m - ↑n.
+// qed-.
+
+(*** minus_n_n *)
+lemma nminus_refl (m): 𝟎 = m - m.
+#m elim m -m //
+qed.
+
+(*** minus_Sn_n *)
+lemma nminus_succ_sn_refl (m): ninj (𝟏) = ↑m - m.
+#m elim m -m //
+qed.
+
+(*** minus_minus_comm *)
+lemma nminus_minus_comm (o) (m) (n): o - m - n = o - n - m.
+#o #m #n elim n -n //
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_plus.ma".
+include "ground/arith/nat_minus.ma".
+
+(* SUBTRACTION FOR NON-NEGATIVE INTEGERS ************************************)
+
+(* Rewrites with nplus ******************************************************)
+
+(*** minus_plus_m_m *)
+lemma nminus_plus_sn_refl_sn (m) (n): m = m + n - n.
+#m #n elim n -n //
+#n #IH <nplus_succ_dx <nminus_succ_bi //
+qed.
+
+lemma nminus_plus_sn_refl_dx (m) (n): m = n + m - n.
+#m #n <nplus_comm //
+qed.
+
+(*** minus_plus *)
+theorem nminus_assoc (o) (m) (n): o-m-n = o-(m+n).
+#o #m #n elim n -n //
+#n #IH <nplus_succ_dx <nminus_succ_dx <nminus_succ_dx //
+qed-.
+
+(*** minus_plus_plus_l *)
+lemma nminus_plus_dx_bi (m) (n) (o): m - n = (m + o) - (n + o).
+#m #n #o <nminus_assoc <nminus_minus_comm //
+qed.
+
+(*** plus_minus_plus_plus_l *) (**)
+lemma plus_minus_plus_plus_l: ∀z,x,y,h. z + (x + h) - (y + h) = z + x - y.
+// qed-.
+
+(* Helper constructions with nplus ******************************************)
+
+(*** plus_to_minus *)
+lemma nminus_plus_dx (o) (m) (n): o = m+n → n = o-m.
+#o #m #n #H destruct //
+qed-.
+
+lemma nminus_plus_sn (o) (m) (n): o = m+n → m = o-n.
+#o #m #n #H destruct //
+qed-.
+
+(* Inversions with nplus ****************************************************)
+
+(*** discr_plus_xy_minus_xz *)
+lemma eq_inv_plus_nminus_refl_sn (m) (n) (o):
+ m + o = m - n →
+ ∨∨ ∧∧ 𝟎 = m & 𝟎 = o
+ | ∧∧ 𝟎 = n & 𝟎 = o.
+#m elim m -m
+[ /3 width=1 by or_introl, conj/
+| #m #IH #n @(nat_ind … n) -n
+ [ #o #Ho
+ lapply (eq_inv_nplus_bi_sn … (𝟎) Ho) -Ho
+ /3 width=1 by or_intror, conj/
+ | #n #_ #o
+ <nminus_succ_bi >nplus_succ_shift #Ho
+ elim (IH … Ho) -IH -Ho * #_ #H
+ elim (eq_inv_nzero_succ … H)
+ ]
+]
+qed-.
+
+(*** discr_minus_x_xy *)
+lemma eq_inv_nminus_refl_sn (m) (n): m = m - n → ∨∨ 𝟎 = m | 𝟎 = n.
+#m #n #Hmn
+elim (eq_inv_plus_nminus_refl_sn … (𝟎) Hmn) -Hmn * #H1 #H2
+/2 width=1 by or_introl, or_intror/
+qed-.
include "ground/arith/nat_succ_iter.ma".
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* ADDITION FOR NON-NEGATIVE INTEGERS ***************************************)
(*** plus *)
definition nplus: nat → nat → nat ≝
lemma nplus_one_dx (n): ↑n = n + 𝟏.
// qed.
-(* Semigroup properties *****************************************************)
+(* Advanved rewrites (semigroup properties) *********************************)
(*** plus_n_Sm *)
lemma nplus_succ_dx (m) (n): ↑(m+n) = m + ↑n.
#m @(nat_ind … m) -m //
qed-.
-lemma nplus_one_sn (n): ↑n = 𝟏 + n.
-#n <nplus_comm // qed.
-
(*** associative_plus *)
lemma nplus_assoc: associative … nplus.
#m #n #o @(nat_ind … o) -o //
#o #IH <nplus_succ_dx <nplus_succ_dx <nplus_succ_dx <IH -IH //
qed.
+(* Advanced constructions ***************************************************)
+
+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.
(*** 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-.
(* Advanced eliminations ****************************************************)
include "ground/arith/pnat_dis.ma".
include "ground/arith/nat.ma".
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* PREDECESSOR FOR NON-NEGATIVE INTEGERS ************************************)
(*** pred *)
definition npred (m): nat ≝ match m with
include "ground/arith/nat_succ.ma".
include "ground/arith/nat_pred.ma".
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* PREDECESSOR FOR NON-NEGATIVE INTEGERS ************************************)
-(* Basic rewrites with succ *************************************************)
+(* Rewrites with nsucc ******************************************************)
(*** pred_Sn *)
lemma npred_succ (n): n = ↓↑n.
include "ground/arith/nat.ma".
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* SUCCESSOR FOR NON-NEGATIVE INTEGERS **************************************)
definition nsucc: nat → nat ≝ λm. match m with
[ nzero ⇒ ninj (𝟏)
#m #IH #n elim n -n /2 width=1 by/
qed-.
-(* Basic inversions *********************************************************)
+(* Basic inversions ***************************************************************)
(*** injective_S *)
lemma eq_inv_nsucc_bi: injective … nsucc.
include "ground/arith/nat_iter.ma".
include "ground/arith/nat_succ.ma".
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* SUCCESSOR FOR NON-NEGATIVE INTEGERS **************************************)
(* Rewrites with niter ******************************************************)
include "ground/arith/pnat.ma".
-(* POSITIVE INTEGERS ********************************************************)
+(* DISCRIMINATOR FOR POSITIVE INTEGERS **************************************)
definition pdis (A:Type[0]) (a) (f) (p): A ≝
match p with
include "ground/notation/functions/exp_3.ma".
include "ground/arith/pnat.ma".
-(* POSITIVE INTEGERS ********************************************************)
+(* ITERATED FUNCTION FOR POSITIVE INTEGERS **********************************)
rec definition piter (p:pnat) (A:Type[0]) (f:A→A) (a:A) ≝
match p with
include "ground/arith/pnat_iter.ma".
-(* POSITIVE INTEGERS ********************************************************)
+(* ADDITION FOR POSITIVE INTEGERS *******************************************)
definition pplus: pnat → pnat → pnat ≝
λp,q. psucc^q p.
lemma pplus_succ_dx (p) (q): ↑(p+q) = p + ↑q.
// qed.
-(* Semigroup properties *****************************************************)
+(* Advanced reweites (semigroup properties) *********************************)
lemma pplus_succ_sn (p) (q): ↑(p+q) = ↑p + q.
#p #q @(piter_appl … psucc)
class "grass"
[ { "arithmetics" * } {
[ { "non-negative integers" * } {
- [ "nat_lt ( ?<? )" "nat_lt_pred" "nat_lt_plus" * ]
- [ "nat_le ( ?≤? )" "nat_le_pred" "nat_le_plus" * ]
+ [ "nat_lt ( ?<? )" "nat_lt_pred" "nat_lt_plus" "nat_lt_minus" "nat_lt_minus_plus" * ]
+ [ "nat_le ( ?≤? )" "nat_le_pred" "nat_le_plus" "nat_le_minus" "nat_le_minus_plus" * ]
+ [ "nat_minus ( ?-? )" "nat_minus_plus" * ]
[ "nat_plus ( ?+? )" * ]
[ "nat_pred ( ↓? )" "nat_pred_succ" * ]
[ "nat_succ ( ↑? )" "nat_succ_iter" * ]
]
class "orange"
[ { "generated library" * } {
+ [ { "well-founded induction" * } {
+ [ "wf1_ind_nlt" "wf2_ind_nlt" "wf3_ind_nlt.ma" * ]
+ }
+ ]
[ { "generalization with equality" * } {
[ "insert_eq" * ]
}
projects / helm.git / commitdiff
