ocaml 3.09 transition

[helm.git] / helm / matita / library / nat / congruence.ma

diff --git a/helm/matita/library/nat/congruence.ma b/helm/matita/library/nat/congruence.ma
index 20c73b3d1d110739e29df668e4c67681413ceebb..af744cf3475087290d2100638f3a6af3b729c732 100644 (file)
--- a/helm/matita/library/nat/congruence.ma
+++ b/helm/matita/library/nat/congruence.ma
@@ -30,45 +30,69 @@ 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).
+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).
+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.
+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.
+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 mod_times_mod : \forall n,m,p:nat. O<p \to O<m \to n \mod p = (n \mod (m*p)) \mod p.
+intros.
+apply (div_mod_spec_to_eq2 n p (n/p) (n \mod p) 
+(n/(m*p)*m + (n \mod (m*p)/p))).
+apply div_mod_spec_div_mod.assumption.
+constructor 1.
+apply lt_mod_m_m.assumption.
+rewrite > times_plus_l.
+rewrite > assoc_plus.
+rewrite < div_mod.
+rewrite > assoc_times.
+rewrite < div_mod.
+reflexivity.
+rewrite > (times_n_O O).
+apply lt_times.
+assumption.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 congruent_n_mod_times : 
+\forall n,m,p:nat. O < p \to O < m \to congruent n (n \mod (m*p)) p.
+intros.unfold congruent.
+apply mod_times_mod.assumption.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_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 > (sym_times p).
 rewrite > assoc_plus.
 rewrite < div_mod.
 assumption.assumption.
@@ -77,7 +101,7 @@ 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.
+apply (eq_times_plus_to_congruent n m p n2).
 assumption.
 rewrite < sym_plus.
 apply minus_to_plus.assumption.
@@ -87,13 +111,13 @@ 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)).
+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 > (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 < (eq_minus_minus_minus_plus ? (n \mod p)).
 rewrite < minus_plus_m_m.
 apply sym_eq.
 apply times_minus_l.
@@ -103,24 +127,24 @@ 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)).
+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 (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 (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 > (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 < (assoc_times (n \mod p)).
 rewrite < times_plus_l.
 apply eq_f2.
 apply eq_f2.reflexivity.
@@ -132,7 +156,7 @@ 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 > (mod_times n m p H).
 rewrite > H1.
 rewrite > H2.
 apply sym_eq.
@@ -142,12 +166,12 @@ 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.
+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.
+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
+qed.