From: Andrea Asperti Date: Wed, 28 Sep 2005 10:15:40 +0000 (+0000) Subject: New entry: relevant_equations. X-Git-Tag: V_0_7_2_3~286 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5c6b8eec9db4119a87eb4fd4055f1ac31a713d90;p=helm.git New entry: relevant_equations. --- diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma index 71734fad3..26e3dcc82 100644 --- a/helm/matita/library/nat/div_and_mod.ma +++ b/helm/matita/library/nat/div_and_mod.ma @@ -210,6 +210,15 @@ constructor 1.assumption. rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity. qed. +theorem eq_div_O: \forall n,m. n < m \to n / m = O. +intros. +apply div_mod_spec_to_eq n m (n/m) (n \mod m) O n. +apply div_mod_spec_div_mod. +apply le_to_lt_to_lt O n m. +apply le_O_n.assumption. +constructor 1.assumption.reflexivity. +qed. + theorem mod_n_n: \forall n:nat. O < n \to n \mod n = O. intros. apply div_mod_spec_to_eq2 n n (n / n) (n \mod n) (S O) O. diff --git a/helm/matita/library/nat/fermat_little_theorem.ma b/helm/matita/library/nat/fermat_little_theorem.ma index aafdc2f19..5d04a7c81 100644 --- a/helm/matita/library/nat/fermat_little_theorem.ma +++ b/helm/matita/library/nat/fermat_little_theorem.ma @@ -14,6 +14,7 @@ set "baseuri" "cic:/matita/nat/fermat_little_theorem". +include "nat/exp.ma". include "nat/gcd.ma". include "nat/permutation.ma". @@ -88,3 +89,10 @@ apply trans_lt ? (S O).simplify.apply le_n.assumption. apply H4. qed. +(* +theorem bad : \forall p,a:nat. prime p \to \lnot divides p a \to +mod (exp a (pred p)) p = (S O). +intros. +cut map_iter p (\lambda x.x) times (S O) = +map_iter p (\lambda n.(mod (a*n) p)) times (S O). +*) \ No newline at end of file diff --git a/helm/matita/library/nat/relevant_equations.ma b/helm/matita/library/nat/relevant_equations.ma new file mode 100644 index 000000000..fee1fd407 --- /dev/null +++ b/helm/matita/library/nat/relevant_equations.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* __ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/nat/relevant_equations.ma". + +include "nat/times.ma". + +theorem times_plus_l: \forall n,m,p:nat. (n+m)*p = n*p + m*p. +intros. +apply trans_eq ? ? (p*(n+m)). +apply sym_times. +apply trans_eq ? ? (p*n+p*m). +apply distr_times_plus. +apply eq_f2. +apply sym_times. +apply sym_times. +qed. + +theorem times_plus_plus: \forall n,m,p,q:nat. (n + m)*(p + q) = +n*p + n*q + m*p + m*q. +intros. +apply trans_eq nat ? ((n*(p+q) + m*(p+q))). +apply times_plus_l. +rewrite > distr_times_plus. +rewrite > distr_times_plus. +rewrite < assoc_plus.reflexivity. +qed.