]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/congruence.ma
fixed, it seems the new handling of hints in some rare cases made inference stupid
[helm.git] / helm / software / matita / library / nat / congruence.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        Matita is distributed under the terms of the          *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "nat/relevant_equations.ma".
16 include "nat/primes.ma".
17
18 definition S_mod: nat \to nat \to nat \def
19 \lambda n,m:nat. (S m) \mod n.
20
21 definition congruent: nat \to nat \to nat \to Prop \def
22 \lambda n,m,p:nat. mod n p = mod m p.
23
24 interpretation "congruent" 'congruent n m p =
25   (cic:/matita/nat/congruence/congruent.con n m p).
26
27 notation < "hvbox(n break \cong\sub p m)"
28   (*non associative*) with precedence 45
29 for @{ 'congruent $n $m $p }.
30
31 theorem congruent_n_n: \forall n,p:nat.congruent n n p.
32 intros.unfold congruent.reflexivity.
33 qed.
34
35 theorem transitive_congruent: \forall p:nat. transitive nat 
36 (\lambda n,m. congruent n m p).
37 intros.unfold transitive.unfold congruent.intros.
38 whd.apply (trans_eq ? ? (y \mod p)).
39 apply H.apply H1.
40 qed.
41
42 theorem le_to_mod: \forall n,m:nat. n \lt m \to n = n \mod m.
43 intros.
44 apply (div_mod_spec_to_eq2 n m O n (n/m) (n \mod m)).
45 constructor 1.assumption.simplify.reflexivity.
46 apply div_mod_spec_div_mod.
47 apply (le_to_lt_to_lt O n m).apply le_O_n.assumption.
48 qed.
49
50 theorem mod_mod : \forall n,p:nat. O<p \to n \mod p = (n \mod p) \mod p.
51 intros.
52 rewrite > (div_mod (n \mod p) p) in \vdash (? ? % ?).
53 rewrite > (eq_div_O ? p).reflexivity.
54 (* uffa: hint non lo trova lt vs. le*)
55 apply lt_mod_m_m.
56 assumption.
57 assumption.
58 qed.
59
60 theorem mod_times_mod : \forall n,m,p:nat. O<p \to O<m \to n \mod p = (n \mod (m*p)) \mod p.
61 intros.
62 apply (div_mod_spec_to_eq2 n p (n/p) (n \mod p) 
63 (n/(m*p)*m + (n \mod (m*p)/p))).
64 apply div_mod_spec_div_mod.assumption.
65 constructor 1.
66 apply lt_mod_m_m.assumption.
67 rewrite > times_plus_l.
68 rewrite > assoc_plus.
69 rewrite < div_mod.
70 rewrite > assoc_times.
71 rewrite < div_mod.
72 reflexivity.
73 rewrite > (times_n_O O).
74 apply lt_times.
75 assumption.assumption.assumption.
76 qed.
77
78 theorem congruent_n_mod_n : 
79 \forall n,p:nat. O < p \to congruent n (n \mod p) p.
80 intros.unfold congruent.
81 apply mod_mod.assumption.
82 qed.
83
84 theorem congruent_n_mod_times : 
85 \forall n,m,p:nat. O < p \to O < m \to congruent n (n \mod (m*p)) p.
86 intros.unfold congruent.
87 apply mod_times_mod.assumption.assumption.
88 qed.
89
90 theorem eq_times_plus_to_congruent: \forall n,m,p,r:nat. O< p \to 
91 n = r*p+m \to congruent n m p.
92 intros.unfold congruent.
93 apply (div_mod_spec_to_eq2 n p (div n p) (mod n p) (r +(div m p)) (mod m p)).
94 apply div_mod_spec_div_mod.assumption.
95 constructor 1.
96 apply lt_mod_m_m.assumption.
97 (*cut (n = r * p + (m / p * p + m \mod p)).*)
98 (*lapply (div_mod m p H). 
99 rewrite > sym_times.
100 rewrite > distr_times_plus.
101 (*rewrite > (sym_times p (m/p)).*)
102 (*rewrite > sym_times.*)
103 rewrite > assoc_plus.
104 autobatch paramodulation.
105 rewrite < div_mod.
106 assumption.
107 assumption.
108 *)
109 rewrite > sym_times.
110 rewrite > distr_times_plus.
111 rewrite > sym_times.
112 rewrite > (sym_times p).
113 rewrite > assoc_plus.
114 rewrite < div_mod.
115 assumption.assumption.
116 qed.
117
118 theorem divides_to_congruent: \forall n,m,p:nat. O < p \to m \le n \to 
119 divides p (n - m) \to congruent n m p.
120 intros.elim H2.
121 apply (eq_times_plus_to_congruent n m p n1).
122 assumption.
123 rewrite < sym_plus.
124 apply minus_to_plus.assumption.
125 rewrite > sym_times. assumption.
126 qed.
127
128 theorem congruent_to_divides: \forall n,m,p:nat.
129 O < p \to congruent n m p \to divides p (n - m).
130 intros.unfold congruent in H1.
131 apply (witness ? ? ((n / p)-(m / p))).
132 rewrite > sym_times.
133 rewrite > (div_mod n p) in \vdash (? ? % ?).
134 rewrite > (div_mod m p) in \vdash (? ? % ?).
135 rewrite < (sym_plus (m \mod p)).
136 rewrite < H1.
137 rewrite < (eq_minus_minus_minus_plus ? (n \mod p)).
138 rewrite < minus_plus_m_m.
139 apply sym_eq.
140 apply times_minus_l.
141 assumption.assumption.
142 qed.
143
144 theorem mod_times: \forall n,m,p:nat. 
145 O < p \to mod (n*m) p = mod ((mod n p)*(mod m p)) p.
146 intros.
147 change with (congruent (n*m) ((mod n p)*(mod m p)) p).
148 apply (eq_times_plus_to_congruent ? ? p 
149 ((n / p)*p*(m / p) + (n / p)*(m \mod p) + (n \mod p)*(m / p))).
150 assumption.
151 apply (trans_eq ? ? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p)))).
152 apply eq_f2.
153 apply div_mod.assumption.
154 apply div_mod.assumption.
155 apply (trans_eq ? ? (((n/p)*p)*((m/p)*p) + (n/p)*p*(m \mod p) +
156 (n \mod p)*((m / p)*p) + (n \mod p)*(m \mod p))).
157 apply times_plus_plus.
158 apply eq_f2.
159 rewrite < assoc_times.
160 rewrite > (assoc_times (n/p) p (m \mod p)).
161 rewrite > (sym_times p (m \mod p)).
162 rewrite < (assoc_times (n/p) (m \mod p) p).
163 rewrite < times_plus_l.
164 rewrite < (assoc_times (n \mod p)).
165 rewrite < times_plus_l.
166 apply eq_f2.
167 apply eq_f2.reflexivity.
168 reflexivity.reflexivity.
169 reflexivity.
170 qed.
171
172 theorem congruent_times: \forall n,m,n1,m1,p. O < p \to congruent n n1 p \to 
173 congruent m m1 p \to congruent (n*m) (n1*m1) p.
174 unfold congruent. 
175 intros. 
176 rewrite > (mod_times n m p H).
177 rewrite > H1.
178 rewrite > H2.
179 apply sym_eq.
180 apply mod_times.assumption.
181 qed.
182
183 theorem congruent_pi: \forall f:nat \to nat. \forall n,m,p:nat.O < p \to
184 congruent (pi n f m) (pi n (\lambda m. mod (f m) p) m) p.
185 intros.
186 elim n. simplify.
187 apply congruent_n_mod_n.assumption.
188 simplify.
189 apply congruent_times.
190 assumption.
191 apply congruent_n_mod_n.assumption.
192 assumption.
193 qed.