X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Farithmetics%2Fcongruence.ma;h=6217aa57c3d61fc73cb29b8707572bc05dd4196a;hb=87f57ddc367303c33e19c83cd8989cd561f3185b;hp=d1afc19eec57ae6674c1d5e67e06e453ef88998d;hpb=8f08fac33a366b2267b35af1a50ad3a9df8dbb88;p=helm.git

diff --git a/weblib/arithmetics/congruence.ma b/weblib/arithmetics/congruence.ma
index d1afc19ee..6217aa57c 100644
--- a/weblib/arithmetics/congruence.ma
+++ b/weblib/arithmetics/congruence.ma
@@ -12,11 +12,11 @@
 include "arithmetics/primes.ma".
 
 (* successor mod n *)
-definition S_mod: nat → nat → nat ≝
-λn,m:nat. (S m) \mod n.
+definition S_mod: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a ≝
+λn,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m) a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a n.
 
-definition congruent: nat → nat → nat → Prop ≝
-λn,m,p:nat. mod n p = mod m p.
+definition congruent: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝
+λn,m,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"mod/a n p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"mod/a m p.
 
 interpretation "congruent" 'congruent n m p = (congruent n m p).
 
@@ -24,84 +24,84 @@ 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 .
+theorem congruent_n_n: ∀n,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.n a title="congruent" href="cic:/fakeuri.def(1)"≅/a_{p} n .
 // qed.
 
 theorem transitive_congruent: 
-  ∀p.transitive nat (λn,m.congruent n m p).
+  ∀p.a href="cic:/matita/basics/relations/transitive.def(2)"transitive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a (λn,m.a href="cic:/matita/arithmetics/congruence/congruent.def(4)"congruent/a n m p).
 /2/ 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))
-% // @lt_mod_m_m @(ltn_to_ltO … ltnm) 
+theorem le_to_mod: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a m.
+#n #m #ltnm @(a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(10)"div_mod_spec_to_eq2/a n m a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a n (na title="natural divide" href="cic:/fakeuri.def(1)"//am) (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a m))
+% // @a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"lt_mod_m_m/a @(a href="cic:/matita/arithmetics/nat/ltn_to_ltO.def(6)"ltn_to_ltO/a … ltnm) 
 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 ⊢ (? ? % ?) 
->(eq_div_O ? p) // @lt_mod_m_m //
+theorem mod_mod : ∀n,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural 'less than'" href="cic:/fakeuri.def(1)"</ap → n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p) a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p.
+#n #p #posp >(a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"div_mod/a (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p) p) in ⊢ (? ? % ?) 
+>(a href="cic:/matita/arithmetics/div_and_mod/eq_div_O.def(14)"eq_div_O/a ? p) // @a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"lt_mod_m_m/a //
 qed.
 
-theorem mod_times_mod : ∀n,m,p:nat. O<p → O<m → 
-  n \mod p = (n \mod (m*p)) \mod p.
+theorem mod_times_mod : ∀n,m,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural 'less than'" href="cic:/fakeuri.def(1)"</ap → a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural 'less than'" href="cic:/fakeuri.def(1)"</am → 
+  n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a (ma title="natural times" href="cic:/fakeuri.def(1)"*/ap)) a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a 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 //
+@(a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(10)"div_mod_spec_to_eq2/a n p (na title="natural divide" href="cic:/fakeuri.def(1)"//ap) (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p) 
+(na title="natural divide" href="cic:/fakeuri.def(1)"//a(ma title="natural times" href="cic:/fakeuri.def(1)"*/ap)a title="natural times" href="cic:/fakeuri.def(1)"*/am a title="natural plus" href="cic:/fakeuri.def(1)"+/a (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a (ma title="natural times" href="cic:/fakeuri.def(1)"*/ap)a title="natural divide" href="cic:/fakeuri.def(1)"//ap))) 
+  [@a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"div_mod_spec_div_mod/a //
+  |% [@a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"lt_mod_m_m/a //] >a href="cic:/matita/arithmetics/nat/distributive_times_plus_r.def(9)"distributive_times_plus_r/a
+   >a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"associative_plus/a <a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"div_mod/a >a href="cic:/matita/arithmetics/nat/associative_times.def(10)"associative_times/a <a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"div_mod/a //
   ]
 qed.
 
-theorem congruent_n_mod_n : ∀n,p:nat. O < p →
- n ≅_{p} (n \mod p).
+theorem congruent_n_mod_n : ∀n,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p →
+ n a title="congruent" href="cic:/fakeuri.def(1)"≅/a_{p} (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p).
 /2/ qed.
 
-theorem congruent_n_mod_times : ∀n,m,p:nat. O < p → O < m → 
-  n ≅_{p} (n \mod (m*p)).
+theorem congruent_n_mod_times : ∀n,m,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p → a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → 
+  n a title="congruent" href="cic:/fakeuri.def(1)"≅/a_{p} (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a (ma title="natural times" href="cic:/fakeuri.def(1)"*/ap)).
 /2/ qed.
 
-theorem eq_times_plus_to_congruent: ∀n,m,p,r:nat. O< p → 
-  n = r*p+m → n ≅_{p} m .
+theorem eq_times_plus_to_congruent: ∀n,m,p,r:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p → 
+  n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ra title="natural times" href="cic:/fakeuri.def(1)"*/apa title="natural plus" href="cic:/fakeuri.def(1)"+/am → n a title="congruent" href="cic:/fakeuri.def(1)"≅/a_{p} m .
 #n #m #p #r #posp #eqn
-@(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 //
+@(a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(10)"div_mod_spec_to_eq2/a n p (a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"div/a n p) (a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"mod/a n p) (r a title="natural plus" href="cic:/fakeuri.def(1)"+/a(a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"div/a m p)) (a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"mod/a m p))
+  [@a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"div_mod_spec_div_mod/a //
+  |% [@a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"lt_mod_m_m/a //] >a href="cic:/matita/arithmetics/nat/distributive_times_plus_r.def(9)"distributive_times_plus_r/a
+   >a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"associative_plus/a <a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"div_mod/a //
   ]
 qed.
 
-theorem divides_to_congruent: ∀n,m,p:nat. O < p → m ≤ n → 
-  p ∣(n - m) → n ≅_{p} m .
+theorem divides_to_congruent: ∀n,m,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → 
+  p a title="divides" href="cic:/fakeuri.def(1)"∣/a(n a title="natural minus" href="cic:/fakeuri.def(1)"-/a m) → n a title="congruent" href="cic:/fakeuri.def(1)"≅/a_{p} m .
 #n #m #p #posp #lemn * #l #eqpl 
-@(eq_times_plus_to_congruent … l posp) /2/
+@(a href="cic:/matita/arithmetics/congruence/eq_times_plus_to_congruent.def(14)"eq_times_plus_to_congruent/a … l posp) /2/
 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) in ⊢ (??%?)
->(div_mod m p) in ⊢ (??%?) <(commutative_plus (m \mod p))
-<congnm <(minus_plus ? (n \mod p)) <minus_plus_m_m //
+theorem congruent_to_divides: ∀n,m,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p → 
+  n a title="congruent" href="cic:/fakeuri.def(1)"≅/a_{p} m → p a title="divides" href="cic:/fakeuri.def(1)"∣/a (n a title="natural minus" href="cic:/fakeuri.def(1)"-/a m).
+#n #m #p #posp #congnm @(a href="cic:/matita/arithmetics/primes/divides.con(0,1,2)"quotient/a ? ? ((n a title="natural divide" href="cic:/fakeuri.def(1)"//a p)a title="natural minus" href="cic:/fakeuri.def(1)"-/a(m a title="natural divide" href="cic:/fakeuri.def(1)"//a p)))
+>a href="cic:/matita/arithmetics/nat/commutative_times.def(8)"commutative_times/a >(a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"div_mod/a n p) in ⊢ (??%?)
+>(a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"div_mod/a m p) in ⊢ (??%?) <(a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"commutative_plus/a (m a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p))
+<congnm <(a href="cic:/matita/arithmetics/nat/minus_plus.def(12)"minus_plus/a ? (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p)) <a href="cic:/matita/arithmetics/nat/minus_plus_m_m.def(6)"minus_plus_m_m/a //
 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 
-  ((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 //
+theorem mod_times: ∀n,m,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p → 
+  na title="natural times" href="cic:/fakeuri.def(1)"*/am a title="congruent" href="cic:/fakeuri.def(1)"≅/a_{p} (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p)a title="natural times" href="cic:/fakeuri.def(1)"*/a(m a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p).
+#n #m #p #posp @(a href="cic:/matita/arithmetics/congruence/eq_times_plus_to_congruent.def(14)"eq_times_plus_to_congruent/a ?? p 
+  ((n a title="natural divide" href="cic:/fakeuri.def(1)"//a p)a title="natural times" href="cic:/fakeuri.def(1)"*/apa title="natural times" href="cic:/fakeuri.def(1)"*/a(m a title="natural divide" href="cic:/fakeuri.def(1)"//a p) a title="natural plus" href="cic:/fakeuri.def(1)"+/a (n a title="natural divide" href="cic:/fakeuri.def(1)"//a p)a title="natural times" href="cic:/fakeuri.def(1)"*/a(m a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p) a title="natural plus" href="cic:/fakeuri.def(1)"+/a (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p)a title="natural times" href="cic:/fakeuri.def(1)"*/a(m a title="natural divide" href="cic:/fakeuri.def(1)"//a p))) //
+@(a href="cic:/matita/basics/logic/trans_eq.def(4)"trans_eq/a ?? (((na title="natural divide" href="cic:/fakeuri.def(1)"//ap)a title="natural times" href="cic:/fakeuri.def(1)"*/apa title="natural plus" href="cic:/fakeuri.def(1)"+/a(n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p))a title="natural times" href="cic:/fakeuri.def(1)"*/a((ma title="natural divide" href="cic:/fakeuri.def(1)"//ap)a title="natural times" href="cic:/fakeuri.def(1)"*/apa title="natural plus" href="cic:/fakeuri.def(1)"+/a(m a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p))))
+  [@a href="cic:/matita/basics/logic/eq_f2.def(3)"eq_f2/a //
+  |@(a href="cic:/matita/basics/logic/trans_eq.def(4)"trans_eq/a ? ? (((na title="natural divide" href="cic:/fakeuri.def(1)"//ap)a title="natural times" href="cic:/fakeuri.def(1)"*/ap)a title="natural times" href="cic:/fakeuri.def(1)"*/a((ma title="natural divide" href="cic:/fakeuri.def(1)"//ap)a title="natural times" href="cic:/fakeuri.def(1)"*/ap) a title="natural plus" href="cic:/fakeuri.def(1)"+/a (na title="natural divide" href="cic:/fakeuri.def(1)"//ap)a title="natural times" href="cic:/fakeuri.def(1)"*/apa title="natural times" href="cic:/fakeuri.def(1)"*/a(m a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p) a title="natural plus" href="cic:/fakeuri.def(1)"+/a
+    (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p)a title="natural times" href="cic:/fakeuri.def(1)"*/a((m a title="natural divide" href="cic:/fakeuri.def(1)"//a p)a title="natural times" href="cic:/fakeuri.def(1)"*/ap) a title="natural plus" href="cic:/fakeuri.def(1)"+/a (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p)a title="natural times" href="cic:/fakeuri.def(1)"*/a(m a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p))) //
+   >a href="cic:/matita/arithmetics/nat/distributive_times_plus.def(7)"distributive_times_plus/a >a href="cic:/matita/arithmetics/nat/distributive_times_plus_r.def(9)"distributive_times_plus_r/a 
+   >a href="cic:/matita/arithmetics/nat/distributive_times_plus_r.def(9)"distributive_times_plus_r/a <a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"associative_plus/a @a href="cic:/matita/basics/logic/eq_f2.def(3)"eq_f2/a //
   ]
 qed.
 
-theorem congruent_times: ∀n,m,n1,m1,p. O < p → 
-  n ≅_{p} n1 → m ≅_{p} m1 → n*m ≅_{p} n1*m1 .
+theorem congruent_times: ∀n,m,n1,m1,p. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p → 
+  n a title="congruent" href="cic:/fakeuri.def(1)"≅/a_{p} n1 → m a title="congruent" href="cic:/fakeuri.def(1)"≅/a_{p} m1 → na title="natural times" href="cic:/fakeuri.def(1)"*/am a title="congruent" href="cic:/fakeuri.def(1)"≅/a_{p} n1a title="natural times" href="cic:/fakeuri.def(1)"*/am1 .
 #n #m #n1 #m1 #p #posp #congn #congm
-@(transitive_congruent … (mod_times n m p posp))
->congn >congm @sym_eq @mod_times //
+@(a href="cic:/matita/arithmetics/congruence/transitive_congruent.def(5)"transitive_congruent/a … (a href="cic:/matita/arithmetics/congruence/mod_times.def(15)"mod_times/a n m p posp))
+>congn >congm @a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a @a href="cic:/matita/arithmetics/congruence/mod_times.def(15)"mod_times/a //
 qed.
 
 (*
@@ -115,4 +115,4 @@ apply congruent_times.
 assumption.
 apply congruent_n_mod_n.assumption.
 assumption.
-qed. *)
+qed. *)
\ No newline at end of file