From: Ferruccio Guidi Date: Mon, 28 Dec 2020 18:43:58 +0000 (+0100) Subject: arithmetics for λδ X-Git-Tag: make_still_working~167 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=5e72e41f4f86814e56d4b00959ccc56c71042a4c arithmetics for λδ + subtraction for non-negative integers + web site update + apps_2/examples: minor update --- diff --git a/helm/www/lambdadelta/images/bronze-03B4.png b/helm/www/lambdadelta/images/bronze-03B4.png index d65392f09..98b99d5b3 100644 Binary files a/helm/www/lambdadelta/images/bronze-03B4.png and b/helm/www/lambdadelta/images/bronze-03B4.png differ diff --git a/helm/www/lambdadelta/images/bronze-03BB.png b/helm/www/lambdadelta/images/bronze-03BB.png index 3cf590000..801644b0f 100644 Binary files a/helm/www/lambdadelta/images/bronze-03BB.png and b/helm/www/lambdadelta/images/bronze-03BB.png differ diff --git a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma index 0cd18e341..f95df96fd 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma @@ -12,9 +12,8 @@ (* *) (**************************************************************************) -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 *****************************************************************) diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat.txt b/matita/matita/contribs/lambdadelta/ground/arith/nat.txt index 7fbb2d7b7..fc8e9e241 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat.txt +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat.txt @@ -70,51 +70,56 @@ "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" diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma index 89c464804..94875efc1 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma @@ -15,7 +15,7 @@ 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 diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma index 82d285e8e..73c143964 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma @@ -15,7 +15,7 @@ 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 *) @@ -75,6 +75,11 @@ lemma nle_inv_zero_dx (m): m ≤ 𝟎 → 𝟎 = m. ] 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/ @@ -82,8 +87,6 @@ lemma nle_inv_succ_sn_refl (m): ↑m ≤ m → ⊥. ] 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 // @@ -93,13 +96,25 @@ lapply (IH H) -IH -H #H destruct 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/ ] diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus.ma new file mode 100644 index 000000000..e3da0c922 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus.ma @@ -0,0 +1,64 @@ +(**************************************************************************) +(* ___ *) +(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus_plus.ma new file mode 100644 index 000000000..d569e0cb3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus_plus.ma @@ -0,0 +1,109 @@ +(**************************************************************************) +(* ___ *) +(* ||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_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_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_assoc +(nplus_minus_sn_refl_sn … Hm) in ⊢ (??%?); // +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma index 513ea5257..37a0efbb2 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma @@ -15,9 +15,9 @@ 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. @@ -46,14 +46,14 @@ lemma nle_plus_dx_dx (m) (n) (o): n + o ≤ m → n ≤ 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. @@ -67,4 +67,3 @@ qed-. (*** 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-. - diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_pred.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_pred.ma index f1824e22e..da1de97f5 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_pred.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_pred.ma @@ -15,9 +15,9 @@ 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. @@ -26,6 +26,18 @@ qed. (*** 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-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma index 1df0f857d..f7a868b53 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma @@ -14,7 +14,7 @@ include "ground/arith/nat_le.ma". -(* NON-NEGATIVE INTEGERS ****************************************************) +(* STRICT ORDER FOR NON-NEGATIVE INTEGERS ***********************************) (*** lt *) definition nlt: relation2 nat nat ≝ diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma new file mode 100644 index 000000000..34a16e01f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma @@ -0,0 +1,37 @@ +(**************************************************************************) +(* ___ *) +(* ||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. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_plus.ma index e9920e928..05776ef20 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_plus.ma @@ -15,9 +15,9 @@ 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. @@ -35,7 +35,7 @@ qed. 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. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma index 16e5bb239..2b3502259 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma @@ -15,14 +15,14 @@ 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. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma new file mode 100644 index 000000000..8129ad55c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma @@ -0,0 +1,71 @@ +(**************************************************************************) +(* ___ *) +(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma new file mode 100644 index 000000000..47e88de49 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma @@ -0,0 +1,84 @@ +(**************************************************************************) +(* ___ *) +(* ||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_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-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma index e7702b80d..75349d2da 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma @@ -14,7 +14,7 @@ include "ground/arith/nat_succ_iter.ma". -(* NON-NEGATIVE INTEGERS ****************************************************) +(* ADDITION FOR NON-NEGATIVE INTEGERS ***************************************) (*** plus *) definition nplus: nat → nat → nat ≝ @@ -33,7 +33,7 @@ lemma nplus_zero_dx (m): m = m + 𝟎. 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. @@ -54,15 +54,20 @@ lemma nplus_comm: commutative … nplus. #m @(nat_ind … m) -m // qed-. -lemma nplus_one_sn (n): ↑n = 𝟏 + n. -#n