X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Farithmetics%2Fcongruence.ma;h=acf873f85d0aeece079d997eab2f11a263cc1d24;hb=87fbbf33fcc2ed91cc8b8a08e1c378ef49ac723d;hp=2a9e06b0fabd6a47304d544bcb523c83e7af0724;hpb=ddc80515997a3f56085c6234d4db326141e189aa;p=helm.git
diff --git a/matita/matita/lib/arithmetics/congruence.ma b/matita/matita/lib/arithmetics/congruence.ma
index 2a9e06b0f..acf873f85 100644
--- a/matita/matita/lib/arithmetics/congruence.ma
+++ b/matita/matita/lib/arithmetics/congruence.ma
@@ -11,25 +11,21 @@
include "arithmetics/primes.ma".
-(* successor mod n *)
-definition S_mod: nat â nat â nat â
-λn,m:nat. (S m) \mod n.
+definition S_mod â λn,m:nat. S m \mod n.
-definition congruent: nat â nat â nat â Prop â
-λn,m,p:nat. mod n p = mod m p.
-
-interpretation "congruent" 'congruent n m p = (congruent n m p).
+definition congruent â λn,m,p:nat. mod n p = mod m p.
notation "hvbox(n break â
_{p} m)"
non associative with precedence 45
- for @{ 'congruent $n $m $p }.
-
-theorem congruent_n_n: ân,p:nat.n â
_{p} n .
+for @{ 'congruent $n $m $p }.
+
+interpretation "congruent" 'congruent n m p = (congruent n m p).
+
+theorem congruent_n_n: ân,p:nat.congruent n n p.
// qed.
-theorem transitive_congruent:
- âp.transitive nat (λn,m.congruent n m p).
-/2/ qed.
+theorem transitive_congruent: âp. transitive ? (λn,m. congruent n m p).
+// qed.
theorem le_to_mod: ân,m:nat. n < m â n = n \mod m.
#n #m #ltnm @(div_mod_spec_to_eq2 n m O n (n/m) (n \mod m))
@@ -37,82 +33,79 @@ theorem le_to_mod: ân,m:nat. n < m â n = n \mod m.
qed.
theorem mod_mod : ân,p:nat. O
(div_mod (n \mod p) p) {⢠(? ? % ?) }
+#n #p #posp >(div_mod (n \mod p) p) in ⢠(??%?);
>(eq_div_O ? p) // @lt_mod_m_m //
qed.
theorem mod_times_mod : ân,m,p:nat. O
distributive_times_plus_r
- >associative_plus associative_times distributive_times_plus_r >associative_plus distributive_times_plus_r
- >associative_plus commutative_times >distributive_times_plus >commutative_times
+ >(commutative_times p) >associative_plus //
]
qed.
-theorem divides_to_congruent: ân,m,p:nat. O < p â m ⤠n â
- p â£(n - m) â n â
_{p} m .
-#n #m #p #posp #lemn * #l #eqpl
-@(eq_times_plus_to_congruent ⦠l posp) /2/
+theorem divides_to_congruent: ân,m,p:nat. 0 < p â m ⤠n â
+ divides p (n - m) â congruent n m p.
+#n #m #p #posp #lemn * #q #Hdiv @(eq_times_plus_to_congruent n m p q) //
+>commutative_plus @minus_to_plus //
qed.
-theorem congruent_to_divides: ân,m,p:nat.O < p â
- n â
_{p} m â p ⣠(n - m).
-#n #m #p #posp #congnm @(quotient ? ? ((n / p)-(m / p)))
->commutative_times >(div_mod n p) {⢠(??%?)}
->(div_mod m p) {⢠(??%?)} <(commutative_plus (m \mod p))
-commutative_times >(div_mod n p) in ⢠(??%?);
+>(div_mod m p) in ⢠(??%?); //
qed.
-theorem mod_times: ân,m,p:nat. O < p â
- n*m â
_{p} (n \mod p)*(m \mod p).
-#n #m #p #posp @(eq_times_plus_to_congruent ?? p
+theorem mod_times: ân,m,p. 0 < p â
+ mod (n*m) p = mod ((mod n p)*(mod m p)) p.
+#n #m #p #posp
+@(eq_times_plus_to_congruent ? ? p
((n / p)*p*(m / p) + (n / p)*(m \mod p) + (n \mod p)*(m / p))) //
-@(trans_eq ?? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p))))
- [@eq_f2 //
- |@(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))) //
- >distributive_times_plus >distributive_times_plus_r
- >distributive_times_plus_r (distributive_times_plus_r (c+d) a b)
+ >(distributive_times_plus a c d)
+ >(distributive_times_plus b c d) //] #Hcut
+ @Hcut
+ |@eq_f2
+ [(associative_times (n/p) p (m \mod p))
+ >(commutative_times p (m \mod p)) <(associative_times (n/p) (m \mod p) p)
+ >distributive_times_plus_r //
+ |%
+ ]
]
qed.
-theorem congruent_times: ân,m,n1,m1,p. O < p â
- n â
_{p} n1 â m â
_{p} m1 â n*m â
_{p} n1*m1 .
-#n #m #n1 #m1 #p #posp #congn #congm
-@(transitive_congruent ⦠(mod_times n m p posp))
->congn >congm @sym_eq @mod_times //
+theorem congruent_times: ân,m,n1,m1,p. O < p â congruent n n1 p â
+ congruent m m1 p â congruent (n*m) (n1*m1) p.
+#n #m #n1 #m1 #p #posp #Hcongn #Hcongm whd
+>(mod_times n m p posp) >Hcongn >Hcongm @sym_eq @mod_times //
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. simplify.
-apply congruent_n_mod_n.assumption.
-simplify.
-apply congruent_times.
-assumption.
-apply congruent_n_mod_n.assumption.
-assumption.
-qed. *)