From bec531b57a008238f67cd72edc751844d28b374f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 26 Nov 2013 19:59:01 +0000 Subject: [PATCH] - natural numbers with infinity for lambdadelta --- .../lambdadelta/ground_2/lib/arith.ma | 32 +++++ .../notation/constructors/infinity_0.ma | 20 ++++ .../notation/functions/predecessor_1.ma | 19 +++ .../notation/functions/successor_1.ma | 19 +++ .../lambdadelta/ground_2/ynat/ynat.ma | 34 ++++++ .../lambdadelta/ground_2/ynat/ynat_le.ma | 111 ++++++++++++++++++ .../lambdadelta/ground_2/ynat/ynat_pred.ma | 39 ++++++ .../lambdadelta/ground_2/ynat/ynat_succ.ma | 55 +++++++++ matita/matita/lib/arithmetics/nat.ma | 5 + matita/matita/predefined_virtuals.ml | 6 +- 10 files changed, 337 insertions(+), 3 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/constructors/infinity_0.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/functions/predecessor_1.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/functions/successor_1.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/ynat/ynat.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index 7d6f5dda4..732c1b64c 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -28,6 +28,9 @@ lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p). 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. + lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b. #a #b #c1 #H >minus_minus_comm >minus_le_minus_minus_comm // qed. @@ -44,6 +47,31 @@ lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b → #a1 #a2 #b #c1 #H1 #H2 >plus_minus // /2 width=1/ qed. +lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z. +/2 width=1 by plus_minus/ qed-. + +(* Properties ***************************************************************) + +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 arith_j: ∀x,y,z. x-y-1 ≤ x-(y-z)-1. +/3 width=1 by monotonic_le_minus_l, monotonic_le_minus_r/ qed. + +lemma arith_k_sn: ∀z,x,y,n. z < x → x+n ≤ y → x-z-1+n ≤ y-z-1. +#z #x #y #n #Hzx #Hxny +>plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ] +>plus_minus [2: /2 width=1 by lt_to_le/ ] +/2 width=1 by monotonic_le_minus_l2/ +qed. + +lemma arith_k_dx: ∀z,x,y,n. z < x → y ≤ x+n → y-z-1 ≤ x-z-1+n. +#z #x #y #n #Hzx #Hyxn +>plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ] +>plus_minus [2: /2 width=1 by lt_to_le/ ] +/2 width=1 by monotonic_le_minus_l2/ +qed. + (* Inversion & forward lemmas ***********************************************) axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2). @@ -69,6 +97,10 @@ lemma false_lt_to_le: ∀x,y. (x < y → ⊥) → y ≤ x. #Hxy elim (H Hxy) qed-. +lemma pred_inv_refl: ∀m. pred m = m → m = 0. +* // normalize #m #H elim (lt_refl_false m) // +qed-. + lemma le_plus_xySz_x_false: ∀y,z,x. x + y + S z ≤ x → ⊥. #y #z #x elim x -x [ #H lapply (le_n_O_to_eq … H) -H diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/infinity_0.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/infinity_0.ma new file mode 100644 index 000000000..f5c849158 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/infinity_0.ma @@ -0,0 +1,20 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "∞" + non associative with precedence 55 + for @{ 'Infinity }. + diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/predecessor_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/predecessor_1.ma new file mode 100644 index 000000000..038a6657e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/predecessor_1.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox( ⫰ term 55 T )" + non associative with precedence 55 + for @{ 'Predecessor $T }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/successor_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/successor_1.ma new file mode 100644 index 000000000..6271880b9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/successor_1.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox( ⫯ term 55 T )" + non associative with precedence 55 + for @{ 'Successor $T }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat.ma new file mode 100644 index 000000000..3dbc0c662 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "arithmetics/nat.ma". +include "ground_2/notation/constructors/infinity_0.ma". + +(* NATURAL NUMBERS WITH INFINITY ********************************************) + +(* the type of natural numbers with infinity *) +inductive ynat: Type[0] ≝ +| yinj: nat → ynat +| Y : ynat +. + +coercion yinj. + +interpretation "ynat infinity" 'Infinity = Y. + +(* Inversion lemmas *********************************************************) + +lemma yinj_inj: ∀m,n. yinj m = yinj n → m = n. +#m #n #H destruct // +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma new file mode 100644 index 000000000..e706fa4dd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma @@ -0,0 +1,111 @@ +(**************************************************************************) +(* ___ *) +(* ||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_2/ynat/ynat_succ.ma". + +(* NATURAL NUMBERS WITH INFINITY ********************************************) + +(* order relation *) +inductive yle: relation ynat ≝ +| yle_inj: ∀m,n. m ≤ n → yle m n +| yle_Y : ∀m. yle m (∞) +. + +interpretation "ynat 'less or equal to'" 'leq x y = (yle x y). + +(* Basic inversion lemmas ***************************************************) + +fact yle_inv_inj_aux: ∀x,y. x ≤ y → ∀m,n. x = yinj m → y = yinj n → m ≤ n. +#x #y * -x -y +[ #x #y #Hxy #m #n #Hx #Hy destruct // +| #x #m #n #_ #Hy destruct +] +qed-. + +lemma yle_inv_inj: ∀m,n. yinj m ≤ yinj n → m ≤ n. +/2 width=5 by yle_inv_inj_aux/ qed-. + +fact yle_inv_O2_aux: ∀m:ynat. ∀x:ynat. m ≤ x → x = 0 → m = 0. +#m #x * -m -x +[ #m #n #Hmn #H destruct /3 width=1 by le_n_O_to_eq, eq_f/ +| #m #H destruct +] +qed-. + +lemma yle_inv_O2: ∀m:ynat. m ≤ 0 → m = 0. +/2 width =3 by yle_inv_O2_aux/ qed-. + +fact yle_inv_Y1_aux: ∀x,n. x ≤ n → x = ∞ → n = ∞. +#x #n * -x -n // +#x #n #_ #H destruct +qed-. + +lemma yle_inv_Y1: ∀n. ∞ ≤ n → n = ∞. +/2 width=3 by yle_inv_Y1_aux/ qed-. + +(* Inversion lemmas on successor ********************************************) + +fact yle_inv_succ1_aux: ∀x,y. x ≤ y → ∀m. x = ⫯m → ∃∃n. m ≤ n & y = ⫯n. +#x #y * -x -y +[ #x #y #Hxy #m #H elim (ysucc_inv_inj_sn … H) -H + #n #H1 #H2 destruct elim (le_inv_S1 … Hxy) -Hxy + #m #Hnm #H destruct + @(ex2_intro … m) /2 width=1 by yle_inj/ (**) (* explicit constructor *) +| #x #y #H destruct + @(ex2_intro … (∞)) /2 width=1 by yle_Y/ +] +qed-. + +lemma yle_inv_succ1: ∀m,y. ⫯m ≤ y → ∃∃n. m ≤ n & y = ⫯n. +/2 width=3 by yle_inv_succ1_aux/ qed-. + +lemma yle_inv_succ: ∀m,n. ⫯m ≤ ⫯n → m ≤ n. +#m #n #H elim (yle_inv_succ1 … H) -H +#x #Hx #H destruct // +qed-. + +(* Basic properties *********************************************************) + +lemma yle_refl: reflexive … yle. +* /2 width=1 by le_n, yle_inj/ +qed. + +(* Properties on predecessor ************************************************) + +lemma yle_pred_sn: ∀m,n. m ≤ n → ⫰m ≤ n. +#m #n * -m -n /3 width=3 by transitive_le, yle_inj/ +qed. + +lemma yle_refl_pred_sn: ∀x. ⫰x ≤ x. +/2 width=1 by yle_refl, yle_pred_sn/ qed. + +(* Properties on successor **************************************************) + +lemma yle_succ_dx: ∀m,n. m ≤ n → m ≤ ⫯n. +#m #n * -m -n /3 width=1 by le_S, yle_inj/ +qed. + +lemma yle_refl_S_dx: ∀x. x ≤ ⫯x. +/2 width=1 by yle_refl, yle_succ_dx/ qed. + +(* Main properties **********************************************************) + +theorem yle_trans: Transitive … yle. +#x #y * -x -y +[ #x #y #Hxy * // + #z #H lapply (yle_inv_inj … H) -H + /3 width=3 by transitive_le, yle_inj/ (**) (* full auto too slow *) +| #x #z #H lapply ( yle_inv_Y1 … H) // +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma new file mode 100644 index 000000000..652b6e219 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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_2/notation/functions/predecessor_1.ma". +include "ground_2/lib/arith.ma". +include "ground_2/ynat/ynat.ma". + +(* NATURAL NUMBERS WITH INFINITY ********************************************) + +(* the predecessor function *) +definition ypred: ynat → ynat ≝ λm. match m with +[ yinj m ⇒ pred m +| Y ⇒ Y +]. + +interpretation "ynat predecessor" 'Predecessor m = (ypred m). + +(* Properties ***************************************************************) + +lemma ypred_inj_rew: ∀m:nat. ⫰m = pred m. +// qed. + +(* Inversion lemmas *********************************************************) + +lemma ypred_inv_refl: ∀m. ⫰m = m → m = 0 ∨ m = ∞. +* // #m #H lapply (yinj_inj … H) -H (**) (* destruct lemma needed *) +/4 width=1 by pred_inv_refl, or_introl, eq_f/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma new file mode 100644 index 000000000..d0ed1d6bd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma @@ -0,0 +1,55 @@ +(**************************************************************************) +(* ___ *) +(* ||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_2/notation/functions/successor_1.ma". +include "ground_2/ynat/ynat_pred.ma". + +(* NATURAL NUMBERS WITH INFINITY ********************************************) + +(* the successor function *) +definition ysucc: ynat → ynat ≝ λm. match m with +[ yinj m ⇒ S m +| Y ⇒ Y +]. + +interpretation "ynat successor" 'Successor m = (ysucc m). + +(* Properties ***************************************************************) + +lemma ypred_succ: ∀m. ⫰⫯m = m. +* // qed. + +(* Inversion lemmas *********************************************************) + +lemma ysucc_inj: ∀m,n. ⫯m = ⫯n → m = n. +#m #n #H <(ypred_succ m) <(ypred_succ n) // +qed-. + +lemma ysucc_inv_refl: ∀m. ⫯m = m → m = ∞. +* // normalize +#m #H lapply (yinj_inj … H) -H (**) (* destruct lemma needed *) +#H elim (lt_refl_false m) // +qed-. + +lemma ysucc_inv_inj_sn: ∀m2,n1. yinj m2 = ⫯n1 → + ∃∃m1. n1 = yinj m1 & m2 = S m1. +#m2 * normalize +[ #n1 #H destruct /2 width=3 by ex2_intro/ +| #H destruct +] +qed-. + +lemma ysucc_inv_inj_dx: ∀m2,n1. ⫯n1 = yinj m2 → + ∃∃m1. n1 = yinj m1 & m2 = S m1. +/2 width=1 by ysucc_inv_inj_sn/ qed-. diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma index bd23c6dd7..8613043b8 100644 --- a/matita/matita/lib/arithmetics/nat.ma +++ b/matita/matita/lib/arithmetics/nat.ma @@ -475,6 +475,11 @@ lemma le_or_ge: ∀m,n. m ≤ n ∨ n ≤ m. #m #n elim (decidable_le m n) /2/ /4/ qed-. +lemma le_inv_S1: ∀x,y. S x ≤ y → ∃∃z. x ≤ z & y = S z. +#x #y #H elim H -y /2 width=3 by ex2_intro/ +#y #_ * #n #Hxn #H destruct /3 width=3 by le_S, ex2_intro/ +qed-. + (* More general conclusion **************************************************) theorem nat_ind_plus: ∀R:predicate nat. diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 016806763..8fd858f54 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1503,13 +1503,13 @@ let load_predefined_virtuals () = ;; let predefined_classes = [ - ["!"; "¡"; ]; + ["!"; "¡"; "⫯"; "⫰"; ]; ["?"; "¿"; "⸮"; ]; [":"; "⁝"; ]; ["."; "•"; "◦"; ]; ["#"; "♯"; "⋕"; "⌘"; ]; ["-"; "÷"; "⊢"; "⊩"; ]; - ["="; "≃"; "≈"; "≝"; "≡"; "≅"; "≐"; "≑"; ]; + ["="; "≃"; "≈"; "≝"; "≡"; "≅"; "≐"; "≑"; "≚"; "≙"; "⌆"; ]; ["→"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; ["⇒"; "⤇"; "➾"; "⇨"; "➡"; "➤"; "➸"; "⇉"; "⥰"; ] ; ["^"; "↑"; ] ; @@ -1589,7 +1589,7 @@ let predefined_classes = [ ["5"; "𝟝"; "⑤"; "⓹"; ] ; ["6"; "𝟞"; "⑥"; "⓺"; ] ; ["7"; "𝟟"; "⑦"; "⓻"; ] ; - ["8"; "𝟠"; "⑧"; "⓼"; ] ; + ["8"; "𝟠"; "⑧"; "⓼"; "∞"; ] ; ["9"; "𝟡"; "⑨"; "⓽"; ] ; ] ;; -- 2.39.2