X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fcongruence.ma;h=acf873f85d0aeece079d997eab2f11a263cc1d24;hb=9c0398174ebfa6b483dbdd5c10e8b15e39067329;hp=d9792b5ebbe3fd079b48548325e7e1235d98d39f;hpb=e28ee799d0281fb76d484d9b4c01d8bed4716bbe;p=helm.git

diff --git a/matita/matita/lib/arithmetics/congruence.ma b/matita/matita/lib/arithmetics/congruence.ma
index d9792b5eb..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<p → n \mod p = (n \mod p) \mod p.
-#n #p #posp >(div_mod (n \mod p) p) in ⊢ (? ? % ?); 
+#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<p → O<m → 
   n \mod p = (n \mod (m*p)) \mod p.
-#n #m #p #posp #posm
-@(div_mod_spec_to_eq2 n p (n/p) (n \mod p) 
-(n/(m*p)*m + (n \mod (m*p)/p))) 
+#n #m #p #posp #posm 
+@(div_mod_spec_to_eq2 n p (n/p) (n \mod p) (n/(m*p)*m + (n \mod (m*p)/p)))
   [@div_mod_spec_div_mod //
-  |% [@lt_mod_m_m //] >distributive_times_plus_r
-   >associative_plus <div_mod >associative_times <div_mod //
+  |% [@lt_mod_m_m //]
+   >distributive_times_plus_r >associative_plus <div_mod //
   ]
 qed.
 
-theorem congruent_n_mod_n : ∀n,p:nat. O < p →
- n ≅_{p} (n \mod p).
-/2/ qed.
+theorem congruent_n_mod_n: ∀n,p. 0 < p → 
+  congruent n (n \mod p) p.
+#n #p #posp @mod_mod //
+qed.
 
-theorem congruent_n_mod_times : ∀n,m,p:nat. O < p → O < m → 
-  n ≅_{p} (n \mod (m*p)).
-/2/ qed.
+theorem congruent_n_mod_times: ∀n,m,p. 0 < p → 0 < m → 
+  congruent n (n \mod (m*p)) p.
+#n #p #posp @mod_times_mod 
+qed.
 
-theorem eq_times_plus_to_congruent: ∀n,m,p,r:nat. O< p → 
-  n = r*p+m → n ≅_{p} m .
-#n #m #p #r #posp #eqn
+theorem eq_times_plus_to_congruent: ∀n,m,p,r:nat. 0 < p → 
+  n = r*p+m → congruent n m p.
+#n #m #p #r #posp #Hn
 @(div_mod_spec_to_eq2 n p (div n p) (mod n p) (r +(div m p)) (mod m p))
   [@div_mod_spec_div_mod //
-  |% [@lt_mod_m_m //] >distributive_times_plus_r
-   >associative_plus <div_mod //
+  |% [@lt_mod_m_m //]
+   >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)))
+theorem congruent_to_divides: ∀n,m,p:nat.
+  0 < p → congruent n m p → divides p (n - m).
+#n #m #p #posp #Hcong %{((n / p)-(m / p))}
 >commutative_times >(div_mod n p) in ⊢ (??%?);
->(div_mod m p) in ⊢ (??%?); <(commutative_plus (m \mod p))
-<congnm <(minus_plus ? (n \mod p)) <minus_plus_m_m //
+>(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 <associative_plus @eq_f2 //
+@(trans_eq ? ? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p)))) //
+@(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)))
+  [cut (∀a,b,c,d.(a+b)*(c+d) = a*c +a*d + b*c + b*d) 
+    [#a #b #c #d >(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 >(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. *)