X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fchinese_reminder.ma;h=30cc7440f8a723d99fc1b6cd8371ce5bdbcf1931;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=748b066320d4592e195adcc99cc42c104f5d1c69;hpb=65312e560c25b49336241762107e401e7f9c5c3c;p=helm.git

diff --git a/helm/matita/library/nat/chinese_reminder.ma b/helm/matita/library/nat/chinese_reminder.ma
index 748b06632..30cc7440f 100644
--- a/helm/matita/library/nat/chinese_reminder.ma
+++ b/helm/matita/library/nat/chinese_reminder.ma
@@ -22,15 +22,15 @@ include "nat/congruence.ma".
 theorem and_congruent_congruent: \forall m,n,a,b:nat. O < n \to O < m \to 
 gcd n m = (S O) \to ex nat (\lambda x. congruent x a m \land congruent x b n).
 intros.
-cut \exists c,d.c*n - d*m = (S O) \lor d*m - c*n = (S O).
+cut (\exists c,d.c*n - d*m = (S O) \lor d*m - c*n = (S O)).
 elim Hcut.elim H3.elim H4.
-apply ex_intro nat ? ((a+b*m)*a1*n-b*a2*m).
+apply (ex_intro nat ? ((a+b*m)*a1*n-b*a2*m)).
 split.
 (* congruent to a *)
-cut a1*n = a2*m + (S O).
+cut (a1*n = a2*m + (S O)).
 rewrite > assoc_times.
 rewrite > Hcut1.
-rewrite < sym_plus ? (a2*m).
+rewrite < (sym_plus ? (a2*m)).
 rewrite > distr_times_plus.
 rewrite < times_n_SO.
 rewrite > assoc_plus.
@@ -39,12 +39,12 @@ rewrite < times_plus_l.
 rewrite > eq_minus_plus_plus_minus.
 rewrite < times_minus_l.
 rewrite > sym_plus.
-apply eq_times_plus_to_congruent ? ? ? ((b+(a+b*m)*a2)-b*a2).
+apply (eq_times_plus_to_congruent ? ? ? ((b+(a+b*m)*a2)-b*a2)).
 assumption.reflexivity.
 apply le_times_l.
-apply trans_le ? ((a+b*m)*a2).
+apply (trans_le ? ((a+b*m)*a2)).
 apply le_times_l.
-apply trans_le ? (b*m).
+apply (trans_le ? (b*m)).
 rewrite > times_n_SO in \vdash (? % ?).
 apply le_times_r.assumption.
 apply le_plus_n.
@@ -53,11 +53,11 @@ apply minus_to_plus.
 apply lt_to_le.
 change with (O + a2*m < a1*n).
 apply lt_minus_to_plus.
-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.
 assumption.
 (* congruent to b *)
-cut a2*m = a1*n - (S O).
-rewrite > assoc_times b a2.
+cut (a2*m = a1*n - (S O)).
+rewrite > (assoc_times b a2).
 rewrite > Hcut1.
 rewrite > distr_times_minus.
 rewrite < assoc_times.
@@ -65,16 +65,16 @@ rewrite < eq_plus_minus_minus_minus.
 rewrite < times_n_SO.
 rewrite < times_minus_l.
 rewrite < sym_plus.
-apply eq_times_plus_to_congruent ? ? ? ((a+b*m)*a1-b*a1).
+apply (eq_times_plus_to_congruent ? ? ? ((a+b*m)*a1-b*a1)).
 assumption.reflexivity.
 rewrite > assoc_times.
 apply le_times_r.
-apply trans_le ? (a1*n - a2*m).
+apply (trans_le ? (a1*n - a2*m)).
 rewrite > H5.apply le_n.
-apply le_minus_m ? (a2*m).
+apply (le_minus_m ? (a2*m)).
 apply le_times_l.
 apply le_times_l.
-apply trans_le ? (b*m).
+apply (trans_le ? (b*m)).
 rewrite > times_n_SO in \vdash (? % ?).
 apply le_times_r.assumption.
 apply le_plus_n.
@@ -84,15 +84,15 @@ apply minus_to_plus.
 apply lt_to_le.
 change with (O + a2*m < a1*n).
 apply lt_minus_to_plus.
-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.
 assumption.
 (* and now the symmetric case; the price to pay for working
    in nat instead than Z *)
-apply ex_intro nat ? ((b+a*n)*a2*m-a*a1*n).
+apply (ex_intro nat ? ((b+a*n)*a2*m-a*a1*n)).
 split.
 (* congruent to a *)
-cut a1*n = a2*m - (S O).
-rewrite > assoc_times a a1.
+cut (a1*n = a2*m - (S O)).
+rewrite > (assoc_times a a1).
 rewrite > Hcut1.
 rewrite > distr_times_minus.
 rewrite < assoc_times.
@@ -100,16 +100,16 @@ rewrite < eq_plus_minus_minus_minus.
 rewrite < times_n_SO.
 rewrite < times_minus_l.
 rewrite < sym_plus.
-apply eq_times_plus_to_congruent ? ? ? ((b+a*n)*a2-a*a2).
+apply (eq_times_plus_to_congruent ? ? ? ((b+a*n)*a2-a*a2)).
 assumption.reflexivity.
 rewrite > assoc_times.
 apply le_times_r.
-apply trans_le ? (a2*m - a1*n).
+apply (trans_le ? (a2*m - a1*n)).
 rewrite > H5.apply le_n.
-apply le_minus_m ? (a1*n).
+apply (le_minus_m ? (a1*n)).
 rewrite > assoc_times.rewrite > assoc_times.
 apply le_times_l.
-apply trans_le ? (a*n).
+apply (trans_le ? (a*n)).
 rewrite > times_n_SO in \vdash (? % ?).
 apply le_times_r.assumption.
 apply le_plus_n.
@@ -119,13 +119,13 @@ apply minus_to_plus.
 apply lt_to_le.
 change with (O + a1*n < a2*m).
 apply lt_minus_to_plus.
-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.
 assumption.
 (* congruent to a *)
-cut a2*m = a1*n + (S O).
+cut (a2*m = a1*n + (S O)).
 rewrite > assoc_times.
 rewrite > Hcut1.
-rewrite > sym_plus (a1*n).
+rewrite > (sym_plus (a1*n)).
 rewrite > distr_times_plus.
 rewrite < times_n_SO.
 rewrite < assoc_times.
@@ -134,12 +134,12 @@ rewrite < times_plus_l.
 rewrite > eq_minus_plus_plus_minus.
 rewrite < times_minus_l.
 rewrite > sym_plus.
-apply eq_times_plus_to_congruent ? ? ? ((a+(b+a*n)*a1)-a*a1).
+apply (eq_times_plus_to_congruent ? ? ? ((a+(b+a*n)*a1)-a*a1)).
 assumption.reflexivity.
 apply le_times_l.
-apply trans_le ? ((b+a*n)*a1).
+apply (trans_le ? ((b+a*n)*a1)).
 apply le_times_l.
-apply trans_le ? (a*n).
+apply (trans_le ? (a*n)).
 rewrite > times_n_SO in \vdash (? % ?).
 apply le_times_r.
 assumption.
@@ -149,7 +149,7 @@ apply minus_to_plus.
 apply lt_to_le.
 change with (O + a1*n < a2*m).
 apply lt_minus_to_plus.
-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.
 assumption.
 (* proof of the cut *)
 rewrite < H2.
@@ -160,25 +160,25 @@ theorem and_congruent_congruent_lt: \forall m,n,a,b:nat. O < n \to O < m \to
 gcd n m = (S O) \to 
 ex nat (\lambda x. (congruent x a m \land congruent x b n) \land
  (x < m*n)).
-intros.elim and_congruent_congruent m n a b.
+intros.elim (and_congruent_congruent m n a b).
 elim H3.
-apply ex_intro ? ? (a1 \mod (m*n)).
+apply (ex_intro ? ? (a1 \mod (m*n))).
 split.split.
-apply transitive_congruent m ? a1.
+apply (transitive_congruent m ? a1).
 unfold congruent.
 apply sym_eq.
-change with congruent a1 (a1 \mod (m*n)) m.
+change with (congruent a1 (a1 \mod (m*n)) m).
 rewrite < sym_times.
 apply congruent_n_mod_times.
 assumption.assumption.assumption.
-apply transitive_congruent n ? a1.
+apply (transitive_congruent n ? a1).
 unfold congruent.
 apply sym_eq.
-change with congruent a1 (a1 \mod (m*n)) n.
+change with (congruent a1 (a1 \mod (m*n)) n).
 apply congruent_n_mod_times.
 assumption.assumption.assumption.
 apply lt_mod_m_m.
-rewrite > times_n_O O.
+rewrite > (times_n_O O).
 apply lt_times.assumption.assumption.
 assumption.assumption.assumption.
 qed.
@@ -209,43 +209,43 @@ theorem mod_cr_pair : \forall m,n,a,b. a \lt m \to b \lt n \to
 gcd n m = (S O) \to 
 (cr_pair m n a b) \mod m = a \land (cr_pair m n a b) \mod n = b.
 intros.
-cut andb (eqb ((cr_pair m n a b) \mod m) a) 
-         (eqb ((cr_pair m n a b) \mod n) b) = true.
+cut (andb (eqb ((cr_pair m n a b) \mod m) a) 
+         (eqb ((cr_pair m n a b) \mod n) b) = true).
 generalize in match Hcut.
 apply andb_elim.
 apply eqb_elim.intro.
 rewrite > H3.
 change with 
-eqb ((cr_pair m n a b) \mod n) b = true 
-\to a = a \land (cr_pair m n a b) \mod n = b.
+(eqb ((cr_pair m n a b) \mod n) b = true \to 
+a = a \land (cr_pair m n a b) \mod n = b).
 intro.split.reflexivity.
 apply eqb_true_to_eq.assumption.
 intro.
-change with false = true \to 
-(cr_pair m n a b) \mod m = a \land (cr_pair m n a b) \mod n = b.
+change with (false = true \to 
+(cr_pair m n a b) \mod m = a \land (cr_pair m n a b) \mod n = b).
 intro.apply False_ind.
 apply not_eq_true_false.apply sym_eq.assumption.
-apply f_min_aux_true 
-(\lambda x. andb (eqb (x \mod m) a) (eqb (x \mod n) b)) (pred (m*n)) (pred (m*n)).
-elim and_congruent_congruent_lt m n a b.
-apply ex_intro ? ? a1.split.split.
+apply (f_min_aux_true 
+(\lambda x. andb (eqb (x \mod m) a) (eqb (x \mod n) b)) (pred (m*n)) (pred (m*n))).
+elim (and_congruent_congruent_lt m n a b).
+apply (ex_intro ? ? a1).split.split.
 rewrite < minus_n_n.apply le_O_n.
-elim H3.apply le_S_S_to_le.apply trans_le ? (m*n).
-assumption.apply nat_case (m*n).apply le_O_n.
+elim H3.apply le_S_S_to_le.apply (trans_le ? (m*n)).
+assumption.apply (nat_case (m*n)).apply le_O_n.
 intro.
 rewrite < pred_Sn.apply le_n.
 elim H3.elim H4.
 apply andb_elim.
-cut a1 \mod m = a.
-cut a1 \mod n = b.
-rewrite > eq_to_eqb_true ? ? Hcut.
-rewrite > eq_to_eqb_true ? ? Hcut1.
+cut (a1 \mod m = a).
+cut (a1 \mod n = b).
+rewrite > (eq_to_eqb_true ? ? Hcut).
+rewrite > (eq_to_eqb_true ? ? Hcut1).
 simplify.reflexivity.
-rewrite < lt_to_eq_mod b n.assumption.
+rewrite < (lt_to_eq_mod b n).assumption.
 assumption.
-rewrite < lt_to_eq_mod a m.assumption.
+rewrite < (lt_to_eq_mod a m).assumption.
 assumption.
-apply le_to_lt_to_lt ? b.apply le_O_n.assumption.
-apply le_to_lt_to_lt ? a.apply le_O_n.assumption.
+apply (le_to_lt_to_lt ? b).apply le_O_n.assumption.
+apply (le_to_lt_to_lt ? a).apply le_O_n.assumption.
 assumption.
 qed.
\ No newline at end of file