--- /dev/null
+(* Equalities ***************************************************************)
+
+lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m.
+// qed-.
+
+lemma plus_minus_m_m_commutative (n) (m): m ≤ n → n = m+(n-m).
+/2 width=1 by plus_minus_associative/ qed-.
+
+lemma plus_to_minus_2: ∀m1,m2,n1,n2. n1 ≤ m1 → n2 ≤ m2 →
+ m1+n2 = m2+n1 → m1-n1 = m2-n2.
+#m1 #m2 #n1 #n2 #H1 #H2 #H
+@plus_to_minus >plus_minus_associative //
+qed-.
+
+(* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *)
+lemma plus_minus_minus_be: ∀x,y,z. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y.
+#x #z #y #Hzy #Hyx >plus_minus // >commutative_plus >plus_minus //
+qed-.
+
+lemma lt_succ_pred: ∀m,n. n < m → m = ↑↓m.
+#m #n #Hm >S_pred /2 width=2 by ltn_to_ltO/
+qed-.
+
+fact plus_minus_minus_be_aux: ∀i,x,y,z. y ≤ z → z ≤ x → i = z - y → x - z + i = x - y.
+/2 width=1 by plus_minus_minus_be/ qed-.
+
+lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p).
+/2 by plus_minus/ qed-.
+
+lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n.
+/2 by plus_minus/ qed-.
+
+lemma minus_minus_comm3: ∀n,x,y,z. n-x-y-z = n-y-z-x.
+// qed.
+
+(* Properties ***************************************************************)
+
+lemma eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2).
+#n1 elim n1 -n1 [| #n1 #IHn1 ] * [2,4: #n2 ]
+[1,4: @or_intror #H destruct
+| elim (IHn1 n2) -IHn1 /3 width=1 by or_intror, or_introl/
+| /2 width=1 by or_introl/
+]
+qed-.
+
+lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m.
+#m #n elim (lt_or_ge m n) /2 width=1 by or3_intro0/
+#H elim H -m /2 width=1 by or3_intro1/
+#m #Hm * /3 width=1 by not_le_to_lt, le_S_S, or3_intro2/
+qed-.
+
+lemma monotonic_le_minus_l2: ∀x1,x2,y,z. x1 ≤ x2 → x1 - y - z ≤ x2 - y - z.
+/3 width=1 by monotonic_le_minus_l/ qed.
+
+lemma minus_le_trans_sn: ∀x1,x2. x1 ≤ x2 → ∀x. x1-x ≤ x2.
+/2 width=3 by transitive_le/ qed.
+
+lemma le_plus_to_minus_l: ∀a,b,c. a + b ≤ c → b ≤ c-a.
+/2 width=1 by le_plus_to_minus_r/
+qed-.
+
+lemma le_plus_to_minus_comm: ∀n,m,p. n ≤ p+m → n-p ≤ m.
+/2 width=1 by le_plus_to_minus/ qed-.
+
+lemma le_inv_S1: ∀m,n. ↑m ≤ n → ∃∃p. m ≤ p & ↑p = n.
+#m *
+[ #H lapply (le_n_O_to_eq … H) -H
+ #H destruct
+| /3 width=3 by monotonic_pred, ex2_intro/
+]
+qed-.
+
+(* Note: this might interfere with nat.ma *)
+lemma monotonic_lt_pred: ∀m,n. m < n → 0 < m → pred m < pred n.
+#m #n #Hmn #Hm whd >(S_pred … Hm)
+@le_S_S_to_le >S_pred /2 width=3 by transitive_lt/
+qed.
+
+lemma lt_S_S: ∀x,y. x < y → ↑x < ↑y.
+/2 width=1 by le_S_S/ qed.
+
+lemma lt_S: ∀n,m. n < m → n < ↑m.
+/2 width=1 by le_S/ qed.
+
+lemma monotonic_lt_minus_r:
+∀p,q,n. q < n -> q < p → n-p < n-q.
+#p #q #n #Hn #H
+lapply (monotonic_le_minus_r … n H) -H #H
+@(le_to_lt_to_lt … H) -H
+/2 width=1 by lt_plus_to_minus/
+qed.
+
+(* Inversion & forward lemmas ***********************************************)
+
+lemma lt_refl_false: ∀n. n < n → ⊥.
+#n #H elim (lt_to_not_eq … H) -H /2 width=1 by/
+qed-.
+
+lemma lt_zero_false: ∀n. n < 0 → ⊥.
+#n #H elim (lt_to_not_le … H) -H /2 width=1 by/
+qed-.
+
+lemma lt_le_false: ∀x,y. x < y → y ≤ x → ⊥.
+/3 width=4 by lt_refl_false, lt_to_le_to_lt/ qed-.
+
+lemma le_dec (n) (m): Decidable (n≤m).
+#n elim n -n [ /2 width=1 by or_introl/ ]
+#n #IH * [ /3 width=2 by lt_zero_false, or_intror/ ]
+#m elim (IH m) -IH
+[ /3 width=1 by or_introl, le_S_S/
+| /4 width=1 by or_intror, le_S_S_to_le/
+]
+qed-.
+
+lemma succ_inv_refl_sn: ∀x. ↑x = x → ⊥.
+#x #H @(lt_le_false x (↑x)) //
+qed-.
+
+lemma le_plus_xSy_O_false: ∀x,y. x + S y ≤ 0 → ⊥.
+#x #y #H lapply (le_n_O_to_eq … H) -H <plus_n_Sm #H destruct
+qed-.
+
+lemma le_plus_xySz_x_false: ∀y,z,x. x + y + S z ≤ x → ⊥.
+#y #z #x elim x -x /3 width=1 by le_S_S_to_le/
+#H elim (le_plus_xSy_O_false … H)
+qed-.
+
+lemma plus_xySz_x_false: ∀z,x,y. x + y + S z = x → ⊥.
+/2 width=4 by le_plus_xySz_x_false/ qed-.
+
+lemma plus_xSy_x_false: ∀y,x. x + S y = x → ⊥.
+/2 width=4 by plus_xySz_x_false/ qed-.
+
+lemma pred_inv_fix_sn: ∀x. ↓x = x → 0 = x.
+* // #x <pred_Sn #H
+elim (succ_inv_refl_sn x) //
+qed-.
+
+lemma discr_plus_xy_y: ∀x,y. x + y = y → x = 0.
+// qed-.
+
+lemma discr_plus_x_xy: ∀x,y. x = x + y → y = 0.
+/2 width=2 by le_plus_minus_comm/ qed-.
+
+lemma plus2_le_sn_sn: ∀m1,m2,n1,n2. m1 + n1 = m2 + n2 → m1 ≤ m2 → n2 ≤ n1.
+#m1 #m2 #n1 #n2 #H #Hm
+lapply (monotonic_le_plus_l n1 … Hm) -Hm >H -H
+/2 width=2 by le_plus_to_le/
+qed-.
+
+lemma plus2_le_sn_dx: ∀m1,m2,n1,n2. m1 + n1 = n2 + m2 → m1 ≤ m2 → n2 ≤ n1.
+/2 width=4 by plus2_le_sn_sn/ qed-.
+
+lemma plus2_le_dx_sn: ∀m1,m2,n1,n2. n1 + m1 = m2 + n2 → m1 ≤ m2 → n2 ≤ n1.
+/2 width=4 by plus2_le_sn_sn/ qed-.
+
+lemma plus2_le_dx_dx: ∀m1,m2,n1,n2. n1 + m1 = n2 + m2 → m1 ≤ m2 → n2 ≤ n1.
+/2 width=4 by plus2_le_sn_sn/ qed-.
+
+lemma lt_S_S_to_lt: ∀x,y. ↑x < ↑y → x < y.
+/2 width=1 by le_S_S_to_le/ qed-.
+
+(* Note this should go in nat.ma *)
+lemma discr_x_minus_xy: ∀x,y. x = x - y → x = 0 ∨ y = 0.
+#x @(nat_ind_plus … x) -x /2 width=1 by or_introl/
+#x #_ #y @(nat_ind_plus … y) -y /2 width=1 by or_intror/
+#y #_ >minus_plus_plus_l
+#H lapply (discr_plus_xy_minus_xz … H) -H
+#H destruct
+qed-.
+
+lemma lt_inv_O1: ∀n. 0 < n → ∃m. ↑m = n.
+* /2 width=2 by ex_intro/
+#H cases (lt_le_false … H) -H //
+qed-.
+
+lemma lt_inv_S1: ∀m,n. ↑m < n → ∃∃p. m < p & ↑p = n.
+#m * /3 width=3 by lt_S_S_to_lt, ex2_intro/
+#H cases (lt_le_false … H) -H //
+qed-.
+
+lemma lt_inv_gen: ∀y,x. x < y → ∃∃z. x ≤ z & ↑z = y.
+* /3 width=3 by le_S_S_to_le, ex2_intro/
+#x #H elim (lt_le_false … H) -H //
+qed-.
+
+lemma plus_inv_O3: ∀x,y. x + y = 0 → x = 0 ∧ y = 0.
+/2 width=1 by plus_le_0/ qed-.
+
+lemma plus_inv_S3_sn: ∀x1,x2,x3. x1+x2 = ↑x3 →
+ ∨∨ ∧∧ x1 = 0 & x2 = ↑x3
+ | ∃∃y1. x1 = ↑y1 & y1 + x2 = x3.
+* /3 width=1 by or_introl, conj/
+#x1 #x2 #x3 <plus_S1 #H destruct
+/3 width=3 by ex2_intro, or_intror/
+qed-.
+
+lemma plus_inv_S3_dx: ∀x2,x1,x3. x1+x2 = ↑x3 →
+ ∨∨ ∧∧ x2 = 0 & x1 = ↑x3
+ | ∃∃y2. x2 = ↑y2 & x1 + y2 = x3.
+* /3 width=1 by or_introl, conj/
+#x2 #x1 #x3 <plus_n_Sm #H destruct
+/3 width=3 by ex2_intro, or_intror/
+qed-.
+
+lemma zero_eq_plus: ∀x,y. 0 = x + y → 0 = x ∧ 0 = y.
+* /2 width=1 by conj/ #x #y normalize #H destruct
+qed-.
+
+lemma nat_split: ∀x. x = 0 ∨ ∃y. ↑y = x.
+* /3 width=2 by ex_intro, or_introl, or_intror/
+qed-.
+
+lemma nat_elim_le_sn (Q:relation …):
+ (∀m1,m2. (∀m. m < m2-m1 → Q (m2-m) m2) → m1 ≤ m2 → Q m1 m2) →
+ ∀n1,n2. n1 ≤ n2 → Q n1 n2.
+#Q #IH #n1 #n2 #Hn
+<(minus_minus_m_m … Hn) -Hn
+lapply (minus_le n2 n1)
+let d ≝ (n2-n1)
+@(nat_elim1 … d) -d -n1 #d
+@pull_2 #Hd
+<(minus_minus_m_m … Hd) in ⊢ (%→?); -Hd
+let n1 ≝ (n2-d) #IHd
+@IH -IH [| // ] #m #Hn
+/4 width=3 by lt_to_le, lt_to_le_to_lt/
+qed-.
+
+(* Decidability of predicates ***********************************************)
+
+lemma dec_lt (R:predicate nat):
+ (∀n. Decidable … (R n)) →
+ ∀n. Decidable … (∃∃m. m < n & R m).
+#R #HR #n elim n -n [| #n * ]
+[ @or_intror * /2 width=2 by lt_zero_false/
+| * /4 width=3 by lt_S, or_introl, ex2_intro/
+| #H0 elim (HR n) -HR
+ [ /3 width=3 by or_introl, ex2_intro/
+ | #Hn @or_intror * #m #Hmn #Hm
+ elim (le_to_or_lt_eq … Hmn) -Hmn #H destruct [ -Hn | -H0 ]
+ /4 width=3 by lt_S_S_to_lt, ex2_intro/
+ ]
+]
+qed-.
+
+lemma dec_min (R:predicate nat):
+ (∀n. Decidable … (R n)) → ∀n. R n →
+ ∃∃m. m ≤ n & R m & (∀p. p < m → R p → ⊥).
+#R #HR #n
+@(nat_elim1 n) -n #n #IH #Hn
+elim (dec_lt … HR n) -HR [ -Hn | -IH ]
+[ * #p #Hpn #Hp
+ elim (IH … Hpn Hp) -IH -Hp #m #Hmp #Hm #HNm
+ @(ex3_intro … Hm HNm) -HNm
+ /3 width=3 by lt_to_le, le_to_lt_to_lt/
+| /4 width=4 by ex3_intro, ex2_intro/
+]
+qed-.
#
"cic:/matita/arithmetics/nat/max.con"
"cic:/matita/arithmetics/nat/commutative_max.con"
-
-####################################
-
+#
"cic:/matita/arithmetics/nat/to_max.con"
-"cic:/matita/arithmetics/nat/leb.con"
-"cic:/matita/arithmetics/nat/leb_elim.con"
"cic:/matita/arithmetics/nat/le_maxl.con"
"cic:/matita/arithmetics/nat/le_maxr.con"
-"cic:/matita/arithmetics/nat/le_to_leb_true.con"
-"cic:/matita/arithmetics/nat/not_le_to_leb_false.con"
+
+####################################
"cic:/matita/arithmetics/nat/nat_discr.con"
"cic:/matita/arithmetics/nat/times.con"
"cic:/matita/arithmetics/nat/times_n_1.con"
"cic:/matita/arithmetics/nat/times_Sn_m.con"
+"cic:/matita/arithmetics/nat/leb.con"
+"cic:/matita/arithmetics/nat/leb_elim.con"
+"cic:/matita/arithmetics/nat/le_to_leb_true.con"
+"cic:/matita/arithmetics/nat/not_le_to_leb_false.con"
(* ITERATED FUNCTION FOR NON-NEGATIVE INTEGERS ******************************)
+(*** iter *)
definition niter (n:nat) (A:Type[0]) (f:A→A) (a:A) ≝
match n with
[ nzero ⇒ a
"iterated function (non-negative integers)"
'Exp A f n = (niter n A f).
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
+(*** iter_O *)
lemma niter_zero (A) (f) (a): a = (f^{A}𝟎) a.
// qed.
lemma niter_inj (A) (f) (p) (a): f^p a = f^{A}(ninj p) a.
// qed.
-(* Advanced rewrites ********************************************************)
+(* Advanced constructions ***************************************************)
+(*** iter_n_Sm *)
lemma niter_appl (A) (f) (n) (a): f (f^n a) = f^{A}n (f a).
#A #f * //
#p #a <niter_inj <niter_inj <piter_appl //
(*** le_O_n *)
lemma nle_zero_sx (m): 𝟎 ≤ m.
-#m @(nat_ind … m) -m /2 width=1 by nle_succ_dx/
+#m @(nat_ind_succ … m) -m /2 width=1 by nle_succ_dx/
qed.
(*** le_S_S *)
(*** le_or_ge *)
lemma nle_ge_dis (m) (n): ∨∨ m ≤ n | n ≤ m.
-#m @(nat_ind … m) -m [ /2 width=1 by or_introl/ ]
-#m #IH #n @(nat_ind … n) -n [ /2 width=1 by or_intror/ ]
-#n #_ elim (IH n) -IH /3 width=2 by nle_succ_bi, or_introl, or_intror/
+#m #n @(nat_ind_succ_2 … m n) -m -n
+[ /2 width=1 by or_introl/
+| /2 width=1 by or_intror/
+| #m #n * /3 width=2 by nle_succ_bi, or_introl, or_intror/
+]
qed-.
(* Basic inversions *********************************************************)
/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
+#m @(nat_ind_succ … m) -m [| #m #IH ] #H
[ /3 width=2 by nle_inv_zero_dx, eq_inv_nzero_succ/
| /3 width=1 by nle_inv_succ_bi/
]
(* Advanced eliminations ****************************************************)
+(*** le_elim *)
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 //
+#Q #IH1 #IH2 #m #n @(nat_ind_succ_2 … m n) -m -n //
[ #m #H elim (nle_inv_succ_zero … H)
| /4 width=1 by nle_inv_succ_bi/
]
--- /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_max.ma".
+include "ground/arith/nat_le.ma".
+
+(* ORDER FOR NON-NEGATIVE INTEGERS ******************************************)
+
+(* Basic constructions with nmax ********************************************)
+
+(*** to_max *)
+lemma nle_max_sn (n):
+ ∀m1. m1 ≤ n → ∀m2. m2 ≤ n → (m1 ∨ m2) ≤ n.
+#n #m1 #H @(nle_ind_alt … H) -n -m1 //
+#n #m1 #Hnm1 #IH #m2 @(nat_ind_succ … m2) -m2
+[ #_ -IH /3 width=1 by nle_succ_bi/
+| #m2 #_ #H -Hnm1 /4 width=1 by nle_inv_succ_bi, nle_succ_bi/
+]
+qed.
+
+lemma nle_max_dx_refl_sn (m) (n): m ≤ (m ∨ n).
+#m #n @(nat_ind_succ_2 … m n) -m -n //
+#m #n #IH <nmax_succ_bi /2 width=1 by nle_succ_bi/
+qed.
+
+lemma nle_max_dx_refl_dx (m) (n): n ≤ (m ∨ n).
+#m #n @(nat_ind_succ_2 … n m) -m -n //
+#m #n #IH <nmax_succ_bi /2 width=1 by nle_succ_bi/
+qed.
+
+(* Basic destructions with nmax *********************************************)
+
+(*** le_maxl *)
+lemma nle_des_max_sn_sn (m1) (m2) (n): (m1 ∨ m2) ≤ n → m1 ≤ n.
+/2 width=3 by nle_trans/ qed-.
+
+(*** le_maxr *)
+lemma nle_des_max_sn_dx (m1) (m2) (n): (m1 ∨ m2) ≤ n → m2 ≤ n.
+/2 width=3 by nle_trans/ qed-.
+
+(* Advanced constructions with nmax *****************************************)
+
+(*** max_S1_le_S *)
+lemma nle_max_sn_succ_sn (m1) (m2) (n): (m1 ∨ m2) ≤ n → (↑m1 ∨ m2) ≤ ↑n.
+/4 width=2 by nle_des_max_sn_sn, nle_des_max_sn_dx, nle_max_sn, nle_succ_bi, nle_succ_dx/ qed.
+
+(*** max_S2_le_S *)
+lemma nle_max_sn_succ_dx (m1) (m2) (n): (m1 ∨ m2) ≤ n → (m1 ∨ ↑m2) ≤ ↑n.
+/4 width=2 by nle_des_max_sn_sn, nle_des_max_sn_dx, nle_max_sn, nle_succ_bi, nle_succ_dx/ qed.
(*** minus_le *)
lemma nle_minus_sn_refl_sn (m) (n): m - n ≤ m.
-#m #n elim n -n //
+#m #n @(nat_ind_succ … 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) //
+#m #n @(nat_ind_succ_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 //
+#m #n #o @(nat_ind_succ … o) -o //
#o #IH #Hmn /3 width=1 by nle_pred_bi/
qed.
(*** le_plus_minus_m_m *)
lemma nle_plus_minus_sn_refl_sn (n) (m): m ≤ m - n + n.
-#n elim n -n //
+#n @(nat_ind_succ … n) -n //
#n #IH #m <nminus_succ_dx_pred_sn <nplus_succ_dx
/2 width=1 by nle_inv_pred_sn/
qed.
(*** le_plus_to_le_r *)
lemma nle_inv_plus_bi_dx (o) (m) (n): n + o ≤ m + o → n ≤ m.
-#o @(nat_ind … o) -o /3 width=1 by nle_inv_succ_bi/
+#o @(nat_ind_succ … o) -o /3 width=1 by nle_inv_succ_bi/
qed-.
(*** le_plus_to_le *)
(* Destructions with npred **************************************************)
lemma nle_inv_pred_sn (m) (n): ↓m ≤ n → m ≤ ↑n.
-#m #n elim m -m
+#m #n @(nat_ind_succ … m) -m
/2 width=1 by nle_succ_bi/
qed-.
(*** le_pred_n *)
lemma nle_pred_sn_refl (m): ↓m ≤ m.
-#m elim m -m //
+#m @(nat_ind_succ … m) -m //
qed.
(*** monotonic_pred *)
qed.
lemma nle_pred_sn (m) (n): m ≤ ↑n → ↓m ≤ n.
-#m #n elim m -m //
+#m #n @(nat_ind_succ … m) -m //
/2 width=1 by nle_pred_bi/
qed-.
lemma nlt_le_trans (o) (m) (n): m < o → o ≤ n → m < n.
/2 width=3 by nle_trans/ qed-.
+(*** le_to_lt_to_lt *)
lemma le_nlt_trans (o) (m) (n): m ≤ o → o < n → m < n.
/3 width=3 by nle_succ_bi, nle_trans/ qed-.
(* Basic inversions *********************************************************)
+lemma nlt_inv_succ_bi (m) (n): ↑m < ↑n → m < n.
+/2 width=1 by nle_inv_succ_bi/ qed-.
+
(*** lt_to_not_le *)
lemma nlt_ge_false (m) (n): m < n → n ≤ m → ⊥.
/3 width=4 by nle_inv_succ_sn_refl, nlt_le_trans/ qed-.
lemma nat_ind_lt_le (Q:predicate …):
(∀n. (∀m. m < n → Q m) → Q n) → ∀n,m. m ≤ n → Q m.
-#Q #H1 #n @(nat_ind … n) -n
+#Q #H1 #n @(nat_ind_succ … n) -n
[ #m #H <(nle_inv_zero_dx … H) -m
@H1 -H1 #o #H elim (nlt_inv_zero_dx … H)
| /5 width=3 by nlt_le_trans, nle_inv_succ_bi/
lemma nat_ind_lt (Q:predicate …):
(∀n. (∀m. m < n → Q m) → Q n) → ∀n. Q n.
/4 width=2 by nat_ind_lt_le/ qed-.
+
+(*** lt_elim *)
+lemma nlt_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_succ_2 … n m) -m -n //
+[ #m #H
+ elim (nlt_inv_zero_dx … H)
+| /4 width=1 by nlt_inv_succ_bi/
+]
+qed-.
(* 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 *)
(* Destructions 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-.
+
lemma nlt_des_minus_dx (o) (m) (n): m < n - o → o < n.
-#o elim o -o
+#o @(nat_ind_succ … o) -o
[ #m #n <nminus_zero_dx
/2 width=3 by le_nlt_trans/
| #o #IH #m #n <nminus_succ_dx_pred_sn #H
(*** S_pred *)
lemma nlt_inv_zero_sn (m): 𝟎 < m → m = ↑↓m.
-#m @(nat_ind … m) -m //
+#m @(nat_ind_succ … m) -m //
#H elim (nlt_inv_refl … H)
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_succ_tri.ma".
+include "ground/arith/nat_lt.ma".
+
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS ***********************************)
+
+(* Destructions with ntri ***************************************************)
+
+(*** tri_lt *)
+lemma ntri_lt (A) (a1) (a2) (a3) (n1) (n2):
+ n1 < n2 → a1 = ntri A n1 n2 a1 a2 a3.
+#A #a1 #a2 #a3 #n1 #n2 #H @(nlt_ind_alt … H) -H //
+qed-.
+
+(*** tri_gt *)
+lemma ntri_gt (A) (a1) (a2) (a3) (n1) (n2):
+ n2 < n1 → a3 = ntri A n1 n2 a1 a2 a3.
+#A #a1 #a2 #a3 #n1 #n2 #H @(nlt_ind_alt … H) -H //
+qed-.
"maximum (non-negative integers)"
'or m n = (nmax m n).
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
(*** max_O1 *)
lemma nmax_zero_sn (n2): n2 = (𝟎 ∨ n2).
<ntri_f_tri //
qed.
-(* Advanced rewrites ********************************************************)
+(* Advanced constructions ***************************************************)
(*** idempotent_max *)
lemma nmax_idem (n): n = (n ∨ n).
(*** commutative_max *)
lemma nmax_comm: commutative … nmax.
-#m #n @(nat_ind_2 … m n) -m -n //
+#m #n @(nat_ind_succ_2 … m n) -m -n //
qed-.
(*** associative_max *)
lemma nmax_assoc: associative … nmax.
-#n1 elim n1 -n1 //
-#n1 #IH #n2 elim n2 -n2 //
-#n2 #_ #n3 elim n3 -n3 //
-qed-.
+#n1 #n2 @(nat_ind_succ_2 … n1 n2) -n1 -n2 //
+#n1 #n2 #IH #n3 @(nat_ind_succ … n3) -n3 //
+qed.
(* Basic inversions *********************************************************)
(*** max_inv_O3 *)
lemma nmax_inv_zero (n1) (n2): 𝟎 = (n1 ∨ n2) → ∧∧ 𝟎 = n1 & 𝟎 = n2.
-#n1 elim n1 -n1 [ /2 width=1 by conj/ ]
-#n1 #_ #n2 elim n2 -n2 [ /2 width=1 by conj/ ]
-#n2 #_ <nmax_succ_bi #H
+#n1 #n2 @(nat_ind_succ_2 … n1 n2) -n1 -n2 /2 width=1 by conj/
+#n1 #n2 #_ <nmax_succ_bi #H
elim (eq_inv_nzero_succ … H)
qed-.
"minus (positive integers)"
'minus m n = (nminus m n).
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
(*** 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.
+(*** minus_SO_dx *)
+lemma nminus_one_dx (m): ↓m = m - 𝟏 .
+// qed.
(*** eq_minus_S_pred *)
lemma nminus_succ_dx (m) (n): ↓(m - n) = m - ↑n.
#m #n @(niter_succ … npred)
qed.
+(* Advanced constructions ***************************************************)
+
+lemma nminus_pred_sn (m) (n): ↓(m - n) = ↓m - n.
+#m #n @(niter_appl … npred)
+qed.
+
(*** minus_O_n *)
lemma nminus_zero_sn (n): 𝟎 = 𝟎 - n.
-#n elim n -n //
+#n @(nat_ind_succ … n) -n //
qed.
(*** minus_S_S *)
lemma nminus_succ_bi (m) (n): m - n = ↑m - ↑n.
-#m #n elim n -n //
+#m #n @(nat_ind_succ … 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 //
+#m @(nat_ind_succ … m) -m //
qed.
(*** minus_Sn_n *)
lemma nminus_succ_sn_refl (m): ninj (𝟏) = ↑m - m.
-#m elim m -m //
+#m @(nat_ind_succ … 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 //
+#o #m #n @(nat_ind_succ … n) -n //
qed-.
(* SUBTRACTION FOR NON-NEGATIVE INTEGERS ************************************)
-(* Rewrites with nplus ******************************************************)
+(* Constructions with nplus *************************************************)
(*** minus_plus_m_m *)
lemma nminus_plus_sn_refl_sn (m) (n): m = m + n - n.
-#m #n elim n -n //
+#m #n @(nat_ind_succ … n) -n //
#n #IH <nplus_succ_dx <nminus_succ_bi //
qed.
(*** minus_plus *)
theorem nminus_plus_assoc (o) (m) (n): o-m-n = o-(m+n).
-#o #m #n elim n -n //
+#o #m #n @(nat_ind_succ … n) -n //
#n #IH <nplus_succ_dx <nminus_succ_dx <nminus_succ_dx //
qed-.
m + o = m - n →
∨∨ ∧∧ 𝟎 = m & 𝟎 = o
| ∧∧ 𝟎 = n & 𝟎 = o.
-#m elim m -m
+#m #n @(nat_ind_succ_2 … m n) -m -n
[ /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)
- ]
+| #m #o #Ho
+ lapply (eq_inv_nplus_bi_sn … (𝟎) Ho) -Ho
+ /3 width=1 by or_intror, conj/
+| #m #n #IH #o
+ <nminus_succ_bi >nplus_succ_shift #Ho
+ elim (IH … Ho) -IH -Ho * #_ #H
+ elim (eq_inv_nzero_succ … H)
]
qed-.
"plus (positive 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.
-(* Advanved rewrites (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) (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 //
+qed.
+
+(* Advanved constructions (semigroup properties) ****************************)
+
(*** plus_S1 *)
lemma nplus_succ_sn (m) (n): ↑(m+n) = ↑m + n.
#m #n @(niter_appl … nsucc)
(*** 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 //
+#m @(nat_ind_succ … m) -m //
qed-.
(*** 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.
-(* Advanced constructions ***************************************************)
+(* Helper constructions *****************************************************)
+(*** plus_SO_sn *)
lemma nplus_one_sn (n): ↑n = 𝟏 + n.
#n <nplus_comm // 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)
+#m #n @(nat_ind_succ … n) -n
+[ /2 width=1 by conj/
+| #n #_ <nplus_succ_dx #H
+ elim (eq_inv_nzero_succ … H)
+]
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 *)
(*** 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-.
"predecessor (non-negative integers)"
'DownArrow m = (npred m).
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
(*** pred_O *)
lemma npred_zero: 𝟎 = ↓𝟎.
(* PREDECESSOR FOR NON-NEGATIVE INTEGERS ************************************)
-(* Rewrites with nsucc ******************************************************)
+(* Constructions with nsucc *************************************************)
(*** pred_Sn pred_S *)
lemma npred_succ (n): n = ↓↑n.
"successor (non-negative integers)"
'UpArrow m = (nsucc m).
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
lemma nsucc_zero: ninj (𝟏) = ↑𝟎.
// qed.
(* Basic eliminations *******************************************************)
(*** nat_ind *)
-lemma nat_ind (Q:predicate …):
+lemma nat_ind_succ (Q:predicate …):
Q (𝟎) → (∀n. Q n → Q (↑n)) → ∀n. Q n.
#Q #IH1 #IH2 * //
#p elim p -p /2 width=1 by/
qed-.
(*** nat_elim2 *)
-lemma nat_ind_2 (Q:relation2 …):
+lemma nat_ind_succ_2 (Q:relation2 …):
(∀n. Q (𝟎) n) →
(∀m. Q (↑m) (𝟎)) →
(∀m,n. Q m n → Q (↑m) (↑n)) →
∀m,n. Q m n.
-#Q #IH1 #IH2 #IH3 #m elim m -m [ // ]
-#m #IH #n elim n -n /2 width=1 by/
+#Q #IH1 #IH2 #IH3 #m @(nat_ind_succ … m) -m [ // ]
+#m #IH #n @(nat_ind_succ … n) -n /2 width=1 by/
qed-.
(* Basic inversions ***************************************************************)
(* SUCCESSOR FOR NON-NEGATIVE INTEGERS **************************************)
-(* Rewrites with niter ******************************************************)
+(* Constructions with niter *************************************************)
+(*** iter_S *)
lemma niter_succ (A) (f) (n) (a): f (f^n a) = f^{A}(↑n) a.
#A #f * //
qed.
(* SUCCESSOR FOR NON-NEGATIVE INTEGERS **************************************)
-(* Rewrites with ntri *******************************************************)
+(* Constructions with ntri **************************************************)
+
+lemma ntri_zero_succ (A) (a1) (a2) (a3) (n):
+ a1 = ntri A (𝟎) (↑n) a1 a2 a3.
+#A #a1 #a2 #a3 * //
+qed.
+
+lemma ntri_succ_zero (A) (a1) (a2) (a3) (n):
+ a3 = ntri A (↑n) (𝟎) a1 a2 a3.
+#A #a1 #a2 #a3 * //
+qed.
lemma ntri_succ_bi (A) (a1) (a2) (a3) (n1) (n2):
ntri A (n1) (n2) a1 a2 a3 = ntri A (↑n1) (↑n2) a1 a2 a3.
| ninj p1 ⇒ match n2 with [ nzero ⇒ a3 | ninj p2 ⇒ ptri A p1 p2 a1 a2 a3 ]
].
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
lemma ntri_zero_bi (A) (a1) (a2) (a3):
a2 = ntri A (𝟎) (𝟎) a1 a2 a3.
ptri A (p1) (p2) a1 a2 a3 = ntri A (p1) (p2) a1 a2 a3.
// qed.
-(* Advanced rewrites ********************************************************)
+(* Advanced constructions ***************************************************)
(*** tri_eq *)
lemma ntri_eq (A) (a1) (a2) (a3) (n): a2 = ntri A n n a1 a2 a3.
(* ITERATED FUNCTION FOR POSITIVE INTEGERS **********************************)
+(* Note: see also: lib/arithemetics/bigops.ma *)
rec definition piter (p:pnat) (A:Type[0]) (f:A→A) (a:A) ≝
match p with
[ punit ⇒ f a
"iterated function (positive integers)"
'Exp A f p = (piter p A f).
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
lemma piter_unit (A) (f) (a): f a = (f^{A}𝟏) a.
// qed.
lemma piter_succ (A) (f) (p) (a): f (f^p a) = f^{A}(↑p) a.
// qed.
-(* Advanced rewrites ********************************************************)
+(* Advanced constructions ***************************************************)
lemma piter_appl (A) (f) (p) (a): f (f^p a) = f^{A}p (f a).
#A #f #p elim p -p //
"plus (positive integers)"
'plus p q = (pplus p q).
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
lemma pplus_one_dx (p): ↑p = p + 𝟏.
// qed.
lemma pplus_succ_dx (p) (q): ↑(p+q) = p + ↑q.
// qed.
-(* Advanced reweites (semigroup properties) *********************************)
+(* Advanced constructions (semigroup properties) ****************************)
lemma pplus_succ_sn (p) (q): ↑(p+q) = ↑p + q.
#p #q @(piter_appl … psucc)
lemma pplus_comm: commutative … pplus.
#p elim p -p //
-qed.
+qed-.
lemma pplus_assoc: associative … pplus.
#p #q #r elim r -r //
| psucc p1 ⇒ match p2 with [ punit ⇒ a3 | psucc p2 ⇒ ptri A p1 p2 a1 a2 a3 ]
].
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
lemma ptri_unit_bi (A) (a1) (a2) (a3):
a2 = ptri A (𝟏) (𝟏) a1 a2 a3.
ptri A (p1) (p2) a1 a2 a3 = ptri A (↑p1) (↑p2) a1 a2 a3.
// qed.
-(* Advanced rewrites ********************************************************)
+(* Advanced constructions ***************************************************)
lemma ptri_eq (A) (a1) (a2) (a3) (p): a2 = ptri A p p a1 a2 a3.
#A #a1 #a2 #a3 #p elim p -p //
class "grass"
[ { "arithmetics" * } {
[ { "non-negative integers" * } {
- [ "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_lt ( ?<? )" "nat_lt_tri" "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_le_max" * ]
[ "nat_max ( ?∨? )" * ]
[ "nat_minus ( ?-? )" "nat_minus_plus" * ]
[ "nat_plus ( ?+? )" * ]
projects / helm.git / commitdiff