From 68e028d053806177e218ee1a5f8778d3011bef83 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 4 Jan 2021 21:33:13 +0100 Subject: [PATCH] =?utf8?q?arithmetics=20for=20=CE=BB=CE=B4?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit + maximum for non-negative integers + minor corrections --- .../contribs/lambdadelta/ground/arith/nat.ma | 4 +- .../contribs/lambdadelta/ground/arith/nat.txt | 5 +- .../lambdadelta/ground/arith/nat_le.ma | 4 +- .../lambdadelta/ground/arith/nat_lt.ma | 14 ++-- .../lambdadelta/ground/arith/nat_lt_minus.ma | 2 +- .../ground/arith/nat_lt_minus_plus.ma | 2 +- .../lambdadelta/ground/arith/nat_max.ma | 73 +++++++++++++++++++ .../lambdadelta/ground/arith/nat_minus.ma | 2 +- .../lambdadelta/ground/arith/nat_plus.ma | 3 +- .../lambdadelta/ground/arith/nat_pred.ma | 3 +- .../lambdadelta/ground/arith/nat_pred_succ.ma | 2 +- .../lambdadelta/ground/arith/nat_succ.ma | 2 +- .../lambdadelta/ground/arith/nat_succ_tri.ma | 25 +++++++ .../lambdadelta/ground/arith/nat_tri.ma | 58 +++++++++++++++ .../lambdadelta/ground/arith/pnat_plus.ma | 2 +- .../lambdadelta/ground/arith/pnat_tri.ma | 53 ++++++++++++++ .../lambdadelta/ground/web/ground_src.tbl | 7 +- 17 files changed, 238 insertions(+), 23 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat_succ_tri.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat_tri.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/pnat_tri.ma diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat.ma index 1bc7286b6..80a2aa200 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat.ma @@ -25,7 +25,9 @@ inductive nat: Type[0] ≝ coercion ninj. -interpretation "zero (non-negative integers" 'Zero = nzero. +interpretation + "zero (non-negative integers)" + 'Zero = nzero. (* Basic inversions *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat.txt b/matita/matita/contribs/lambdadelta/ground/arith/nat.txt index 2bd0eabca..915a45dbf 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat.txt +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat.txt @@ -117,17 +117,18 @@ "cic:/matita/arithmetics/nat/lt_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/max.con" +"cic:/matita/arithmetics/nat/commutative_max.con" #################################### "cic:/matita/arithmetics/nat/to_max.con" -"cic:/matita/arithmetics/nat/commutative_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/max.con" "cic:/matita/arithmetics/nat/not_le_to_leb_false.con" "cic:/matita/arithmetics/nat/nat_discr.con" diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma index 73c143964..ae98e3a5e 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma @@ -45,7 +45,7 @@ lemma nle_succ_bi (m) (n): m ≤ n → ↑m ≤ ↑n. qed. (*** le_or_ge *) -lemma nle_ge_e (m) (n): ∨∨ m ≤ n | n ≤ m. +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/ @@ -117,7 +117,7 @@ qed-. (*** decidable_le *) lemma nle_dec (m) (n): Decidable … (m ≤ n). -#m #n elim (nle_ge_e m n) [ /2 width=1 by or_introl/ ] +#m #n elim (nle_ge_dis m n) [ /2 width=1 by or_introl/ ] #Hnm elim (eq_nat_dec m n) [ #H destruct /2 width=1 by nle_refl, or_introl/ ] /4 width=1 by nle_antisym, or_intror/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma index 388c8aace..a8ffe2e4c 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma @@ -40,25 +40,25 @@ lemma nlt_succ_bi (m) (n): m < n → ↑m < ↑n. /2 width=1 by nle_succ_bi/ qed. (*** le_to_or_lt_eq *) -lemma nle_lt_eq_e (m) (n): m ≤ n → ∨∨ m < n | m = n. +lemma nle_lt_eq_dis (m) (n): m ≤ n → ∨∨ m < n | m = n. #m #n * -n /3 width=1 by nle_succ_bi, or_introl/ qed-. (*** eq_or_gt *) -lemma eq_gt_e (n): ∨∨ 𝟎 = n | 𝟎 < n. -#n elim (nle_lt_eq_e (𝟎) n ?) +lemma eq_gt_dis (n): ∨∨ 𝟎 = n | 𝟎 < n. +#n elim (nle_lt_eq_dis (𝟎) n ?) /2 width=1 by or_introl, or_intror/ qed-. (*** lt_or_ge *) -lemma nlt_ge_e (m) (n): ∨∨ m < n | n ≤ m. -#m #n elim (nle_ge_e m n) /2 width=1 by or_intror/ -#H elim (nle_lt_eq_e … H) -H /2 width=1 by nle_refl, or_introl, or_intror/ +lemma nlt_ge_dis (m) (n): ∨∨ m < n | n ≤ m. +#m #n elim (nle_ge_dis m n) /2 width=1 by or_intror/ +#H elim (nle_lt_eq_dis … H) -H /2 width=1 by nle_refl, or_introl, or_intror/ qed-. (*** not_le_to_lt *) lemma le_false_nlt (m) (n): (n ≤ m → ⊥) → m < n. -#m #n elim (nlt_ge_e m n) [ // ] +#m #n elim (nlt_ge_dis m n) [ // ] #H #Hn elim Hn -Hn // qed. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma index 5ee4b80eb..bf889def7 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma @@ -38,7 +38,7 @@ qed. (* Destructions with nminus *************************************************) -lemma nlt_fwd_minus_dx (o) (m) (n): m < n - o → o < n. +lemma nlt_des_minus_dx (o) (m) (n): m < n - o → o < n. #o elim o -o [ #m #n