From b913b3ee973dfc9f1e6d7c0fd0c720d03699689e Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 8 Jan 2010 08:19:24 +0000 Subject: [PATCH] rebuilding the library --- .../matita/nlibrary/arithmetics/nat.ma | 232 ++++++++++++++++++ 1 file changed, 232 insertions(+) create mode 100644 helm/software/matita/nlibrary/arithmetics/nat.ma diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma new file mode 100644 index 000000000..189f2f152 --- /dev/null +++ b/helm/software/matita/nlibrary/arithmetics/nat.ma @@ -0,0 +1,232 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +(* include "higher_order_defs/functions.ma". *) +include "basics/functions.ma". +include "basics/eq.ma". + +ninductive nat : Type[0] ≝ + | O : nat + | S : nat → nat. + +interpretation "Natural numbers" 'N = nat. + +default "natural numbers" cic:/matita/ng/arithmetics/nat/nat.ind. + +alias num (instance 0) = "natural number". + +ndefinition pred ≝ + λn. match n with + [ O ⇒ O + | (S p) ⇒ p]. + +ntheorem pred_Sn : ∀n. n = pred (S n). +//. nqed. + +ntheorem injective_S : injective nat nat S. +(* nwhd; #a; #b;#H;napplyS pred_Sn. *) +//. nqed. + +(* +ntheorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m. +//. nqed. *) + +ntheorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m. +/2/; nqed. + +ndefinition not_zero: nat → Prop ≝ + λn: nat. match n with + [ O ⇒ False + | (S p) ⇒ True ]. + +ntheorem not_eq_O_S : ∀n:nat. O ≠ S n. +#n; #eqOS; nchange with (not_zero O); nrewrite > eqOS; //. +nqed. + +ntheorem not_eq_n_Sn : ∀n:nat. n ≠ S n. +#n; nelim n; /2/; nqed. + +ntheorem nat_case: + ∀n:nat.∀P:nat → Prop. + (n=O → P O) → (∀m:nat. (n=(S m) → P (S m))) → P n. +#n; #P; nelim n; /2/; nqed. + +ntheorem nat_elim2 : + ∀R:nat → nat → Prop. + (∀n:nat. R O n) + → (∀n:nat. R (S n) O) + → (∀n,m:nat. R n m → R (S n) (S m)) + → ∀n,m:nat. R n m. +#R; #ROn; #RSO; #RSS; #n; nelim n;//; +#n0; #Rn0m; #m; ncases m;/2/; nqed. + +ntheorem decidable_eq_nat : \forall n,m:nat.decidable (n=m). +napply nat_elim2;#n; + ##[ ncases n; /2/; + ##| /3/; + ##| #m; #Hind; ncases Hind; /3/; (* ??? /2/;#neqnm; /3/; *) + ##] +nqed. + +(*************************** plus ******************************) + +nlet rec plus n m ≝ + match n with + [ O ⇒ m + | S p ⇒ S (plus p m) ]. + +interpretation "natural plus" 'plus x y = (plus x y). + +ntheorem plus_n_O: ∀n:nat. n = n+O. +#n; nelim n; /2/; nqed. + +ntheorem plus_n_Sm : ∀n,m:nat. S (n+m) = n+(S m). +#n; nelim n; nnormalize; //; nqed. + +ntheorem plus_n_SO : ∀n:nat. S n = n+(S O). +//; nqed. + +ntheorem sym_plus: ∀n,m:nat. n+m = m+n. +#n; nelim n; nnormalize; //; nqed. + +ntheorem associative_plus : associative nat plus. +#n; nelim n; nnormalize; //; nqed. + +(* ntheorem assoc_plus : \forall n,m,p:nat. (n+m)+p = n+(m+p) +\def associative_plus. *) + +ntheorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m). +#n; nelim n; nnormalize; /3/; nqed. + +(* ntheorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m +\def injective_plus_r. *) + +ntheorem injective_plus_l: ∀m:nat.injective nat nat (λn.n+m). +/2/; nqed. + +(* ntheorem inj_plus_l: \forall p,n,m:nat. n+p = m+p \to n=m +\def injective_plus_l. *) + +(*************************** times *****************************) + +nlet rec times n m ≝ + match n with + [ O ⇒ O + | S p ⇒ m+(times p m) ]. + +interpretation "natural times" 'times x y = (times x y). + +ntheorem times_Sn_m: ∀n,m:nat. m+n*m = S n*m. +//; nqed. + +ntheorem times_n_O: ∀n:nat. O = n*O. +#n; nelim n; //; nqed. + +ntheorem times_n_Sm : ∀n,m:nat. n+(n*m) = n*(S m). +#n; nelim n; nnormalize; /2/; nqed. + +ntheorem times_O_to_O: ∀n,m:nat.n*m=O → n=O ∨ m=O. +napply nat_elim2; (* /2/ slow! *) + ##[#n; #H; @1; //; + ##|#n; #H; @2; //; (* ?? *) + ##|#n; #m; #H; #H1; napply False_ind;napply not_eq_O_S; + (* why two steps? *) /2/; + ##] +nqed. + +ntheorem times_n_SO : ∀n:nat. n = n * S O. +//; nqed. + +(* + +ntheorem times_SSO_n : ∀n:nat. n + n = 2 * n. +intros. +simplify. +rewrite < plus_n_O. +reflexivity. +qed. + +alias num (instance 0) = "natural number". +lemma times_SSO: \forall n.2*(S n) = S(S(2*n)). +intro. +simplify.rewrite < plus_n_Sm.reflexivity. +qed. + +theorem or_eq_eq_S: \forall n.\exists m. +n = (S(S O))*m \lor n = S ((S(S O))*m). +intro.elim n + [apply (ex_intro ? ? O). + left.reflexivity + |elim H. elim H1 + [apply (ex_intro ? ? a). + right.apply eq_f.assumption + |apply (ex_intro ? ? (S a)). + left. rewrite > H2. + apply sym_eq. + apply times_SSO + ] + ] +qed. + +theorem symmetric_times : symmetric nat times. +unfold symmetric. +intros.elim x + [simplify.apply times_n_O. + | simplify.rewrite > H.apply times_n_Sm.] +qed. + +variant sym_times : \forall n,m:nat. n*m = m*n \def +symmetric_times. + +theorem distributive_times_plus : distributive nat times plus. +unfold distributive. +intros.elim x. +simplify.reflexivity. +simplify. +demodulate all. +(* +rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus. +apply eq_f.rewrite < assoc_plus. rewrite < (sym_plus ? z). +rewrite > assoc_plus.reflexivity. *) +qed. + +variant distr_times_plus: \forall n,m,p:nat. n*(m+p) = n*m + n*p +\def distributive_times_plus. + +theorem associative_times: associative nat times. +unfold associative. +intros. +elim x. simplify.apply refl_eq. +simplify. +demodulate all. +(* +rewrite < sym_times. +>>>>>>> .r9770 +rewrite > distr_times_plus. +rewrite < sym_times. +rewrite < (sym_times (times n y) z). +rewrite < H.apply refl_eq. +*) +qed. + +variant assoc_times: \forall n,m,p:nat. (n*m)*p = n*(m*p) \def +associative_times. + +lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z). +intros. +demodulate. reflexivity. +(* autobatch paramodulation. *) +qed. + +*) \ No newline at end of file -- 2.39.2