From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 3 Oct 2005 08:16:18 +0000 (+0000)
Subject: Added congruence.ma.
X-Git-Tag: V_0_7_2_3~262
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b2565147ddbf4f9c3baf37359ad0f6330903b4f8;p=helm.git

Added congruence.ma.
---

diff --git a/helm/matita/library/nat/congruence.ma b/helm/matita/library/nat/congruence.ma
new file mode 100644
index 000000000..20c73b3d1
--- /dev/null
+++ b/helm/matita/library/nat/congruence.ma
@@ -0,0 +1,153 @@
+(**************************************************************************)
+(*       ___	                                                          *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        Matita is distributed under the terms of the          *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/congruence".
+
+include "nat/relevant_equations.ma".
+include "nat/primes.ma".
+
+definition S_mod: nat \to nat \to nat \def
+\lambda n,m:nat. (S m) \mod n.
+
+definition congruent: nat \to nat \to nat \to Prop \def
+\lambda n,m,p:nat. mod n p = mod m p.
+
+theorem congruent_n_n: \forall n,p:nat.congruent n n p.
+intros.unfold congruent.reflexivity.
+qed.
+
+theorem transitive_congruent: \forall p:nat. transitive nat 
+(\lambda n,m. congruent n m p).
+intros.unfold transitive.unfold congruent.intros.
+whd.apply trans_eq ? ? (y \mod p).
+apply H.apply H1.
+qed.
+
+theorem le_to_mod: \forall n,m:nat. n \lt m \to n = n \mod m.
+intros.
+apply div_mod_spec_to_eq2 n m O n (n/m) (n \mod m).
+constructor 1.assumption.simplify.reflexivity.
+apply div_mod_spec_div_mod.
+apply le_to_lt_to_lt O n m.apply le_O_n.assumption.
+qed.
+
+theorem mod_mod : \forall n,p:nat. O<p \to n \mod p = (n \mod p) \mod p.
+intros.
+rewrite > div_mod (n \mod p) p in \vdash (? ? % ?).
+rewrite > eq_div_O ? p.reflexivity.
+(* uffa: hint non lo trova lt vs. le*)
+apply lt_mod_m_m.
+assumption.
+assumption.
+qed.
+
+theorem congruent_n_mod_n : 
+\forall n,p:nat. O < p \to congruent n (n \mod p) p.
+intros.unfold congruent.
+apply mod_mod.assumption.
+qed.
+
+theorem eq_times_plus_to_congruent: \forall n,m,p,r:nat. O< p \to 
+n = r*p+m \to congruent n m p.
+intros.unfold congruent.
+apply div_mod_spec_to_eq2 n p (div n p) (mod n p) (r +(div m p)) (mod m p).
+apply div_mod_spec_div_mod.assumption.
+constructor 1.
+apply lt_mod_m_m.assumption.
+rewrite > sym_times.
+rewrite > distr_times_plus.
+rewrite > sym_times.
+rewrite > sym_times p.
+rewrite > assoc_plus.
+rewrite < div_mod.
+assumption.assumption.
+qed.
+
+theorem divides_to_congruent: \forall n,m,p:nat. O < p \to m \le n \to 
+divides p (n - m) \to congruent n m p.
+intros.elim H2.
+apply eq_times_plus_to_congruent n m p n2.
+assumption.
+rewrite < sym_plus.
+apply minus_to_plus.assumption.
+rewrite > sym_times. assumption.
+qed.
+
+theorem congruent_to_divides: \forall n,m,p:nat.
+O < p \to congruent n m p \to divides p (n - m).
+intros.unfold congruent in H1.
+apply witness ? ? ((n / p)-(m / p)).
+rewrite > sym_times.
+rewrite > div_mod n p in \vdash (? ? % ?).
+rewrite > div_mod m p in \vdash (? ? % ?).
+rewrite < sym_plus (m \mod p).
+rewrite < H1.
+rewrite < eq_minus_minus_minus_plus ? (n \mod p).
+rewrite < minus_plus_m_m.
+apply sym_eq.
+apply times_minus_l.
+assumption.assumption.
+qed.
+
+theorem mod_times: \forall n,m,p:nat. 
+O < p \to mod (n*m) p = mod ((mod n p)*(mod m p)) p.
+intros.
+change with congruent (n*m) ((mod n p)*(mod m p)) p.
+apply eq_times_plus_to_congruent ? ? p 
+((n / p)*p*(m / p) + (n / p)*(m \mod p) + (n \mod p)*(m / p)).
+assumption.
+apply trans_eq ? ? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p))).
+apply eq_f2.
+apply div_mod.assumption.
+apply div_mod.assumption.
+apply trans_eq ? ? (((n/p)*p)*((m/p)*p) + (n/p)*p*(m \mod p) +
+(n \mod p)*((m / p)*p) + (n \mod p)*(m \mod p)).
+apply times_plus_plus.
+apply eq_f2.
+rewrite < assoc_times.
+rewrite > assoc_times (n/p) p (m \mod p).
+rewrite > sym_times p (m \mod p).
+rewrite < assoc_times (n/p) (m \mod p) p.
+rewrite < times_plus_l.
+rewrite < assoc_times (n \mod p).
+rewrite < times_plus_l.
+apply eq_f2.
+apply eq_f2.reflexivity.
+reflexivity.reflexivity.
+reflexivity.
+qed.
+
+theorem congruent_times: \forall n,m,n1,m1,p. O < p \to congruent n n1 p \to 
+congruent m m1 p \to congruent (n*m) (n1*m1) p.
+unfold congruent. 
+intros. 
+rewrite > mod_times n m p H.
+rewrite > H1.
+rewrite > H2.
+apply sym_eq.
+apply mod_times.assumption.
+qed.
+
+theorem congruent_pi: \forall f:nat \to nat. \forall n,m,p:nat.O < p \to
+congruent (pi n f m) (pi n (\lambda m. mod (f m) p) m) p.
+intros.
+elim n.change with congruent (f m) (f m \mod p) p.
+apply congruent_n_mod_n.assumption.
+change with congruent ((f (S n1+m))*(pi n1 f m)) 
+(((f (S n1+m))\mod p)*(pi n1 (\lambda m.(f m) \mod p) m)) p.
+apply congruent_times.
+assumption.
+apply congruent_n_mod_n.assumption.
+assumption.
+qed.
\ No newline at end of file