]> matita.cs.unibo.it Git - helm.git/blob - weblib/arithmetics/chinese_reminder.ma
- support for atomic arities and candidates of reducibility started
[helm.git] / weblib / arithmetics / chinese_reminder.ma
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department of the University of Bologna, Italy.                     
5     ||I||                                                                 
6     ||T||  
7     ||A||  This file is distributed under the terms of the 
8     \   /  GNU General Public License Version 2        
9      \ /      
10       V_______________________________________________________________ *)
11
12 include "arithmetics/exp.ma".
13 include "arithmetics/gcd.ma".
14 include "arithmetics/congruence.ma".
15
16 theorem congruent_ab: ∀m,n,a,b:nat. O < n → O < m → 
17  gcd n m = 1 → ∃x.x ≅_{m} a ∧ x ≅_{n} b.
18 #m #n #a #b #posn #posm #pnm
19 cut (∃c,d.c*n - d*m = 1 ∨ d*m - c*n = 1) [<pnm @eq_minus_gcd]
20 * #c * #d * #H
21   [(* first case *)
22    @(ex_intro nat ? ((a+b*m)*c*n-b*d*m)) %
23     [(* congruent to a *)
24      cut (c*n = d*m + 1)
25       [@minus_to_plus // @(transitive_le … (le_n_Sn …)) 
26        @(lt_minus_to_plus_r 0) //] -H #H
27      >associative_times >H <(commutative_plus ? (d*m))
28      >distributive_times_plus <times_n_1 >associative_plus
29      <associative_times <distributive_times_plus_r 
30      <commutative_plus <plus_minus
31        [@(eq_times_plus_to_congruent … posm) //
32        |applyS monotonic_le_times_r @(transitive_le ? ((a+b*m)*d)) // 
33         applyS monotonic_le_times_r apply (transitive_le … (b*m)) /2/
34        ]
35     |(* congruent to b *)
36      -pnm (cut (d*m = c*n-1))
37        [@sym_eq @plus_to_minus >commutative_plus 
38         @minus_to_plus // @(transitive_le … (le_n_Sn …)) 
39      @(lt_minus_to_plus_r 0) //] #H1
40      >(associative_times b d) >H1 >distributive_times_minus 
41      <associative_times <minus_minus
42        [@(eq_times_plus_to_congruent … posn) //
43        |applyS monotonic_le_times_r >commutative_times
44         @monotonic_le_times_r @(transitive_le ? (m*b)) /2/
45        |applyS monotonic_le_times_r @le_plus_to_minus // 
46        ]
47     ]
48   |(* and now the symmetric case; the price to pay for working
49       in nat instead than Z *)
50    @(ex_intro nat ? ((b+a*n)*d*m-a*c*n)) %
51     [(* congruent to a *)
52      cut (c*n = d*m - 1) 
53        [@sym_eq @plus_to_minus >commutative_plus @minus_to_plus // @(transitive_le … (le_n_Sn …)) 
54         @(lt_minus_to_plus_r 0) //] #H1
55      >(associative_times a c) >H1
56      >distributive_times_minus
57      <minus_minus
58       [@(eq_times_plus_to_congruent … posm) //
59       |<associative_times applyS monotonic_le_times_r
60        >commutative_times @monotonic_le_times_r 
61        @(transitive_le ? (n*a)) /2/
62       |@monotonic_le_times_r <H @le_plus_to_minus //
63       ]
64     |(* congruent to b *)
65      cut (d*m = c*n + 1)
66       [@minus_to_plus // @(transitive_le … (le_n_Sn …)) 
67        @(lt_minus_to_plus_r 0) //] -H #H
68      >associative_times >H
69      >(commutative_plus (c*n))
70      >distributive_times_plus <times_n_1
71      <associative_times >associative_plus 
72      <distributive_times_plus_r <commutative_plus <plus_minus
73       [@(eq_times_plus_to_congruent … posn) //
74       |applyS monotonic_le_times_r @(transitive_le ? (c*(b+n*a))) // 
75        <commutative_times @monotonic_le_times_r
76        @(transitive_le ? (n*a)) /2/
77       ]
78     ]
79   ]
80 qed.
81        
82 theorem congruent_ab_lt: ∀m,n,a,b. O < n → O < m → 
83 gcd n m = 1 → ∃x.x ≅_{m} a ∧ x ≅_{n} b ∧ x < m*n.
84 #m #n #a #b #posn #posm #pnm
85 cases(congruent_ab m n a b posn posm pnm) #x * #cxa #cxb
86 @(ex_intro ? ? (x \mod (m*n))) % 
87   [% 
88     [@(transitive_congruent m ? x) // 
89      @sym_eq >commutative_times @congruent_n_mod_times //
90     |@(transitive_congruent n ? x) // 
91      @sym_eq @congruent_n_mod_times //
92     ]
93   |@lt_mod_m_m >(times_n_O 0) @lt_times //
94   ]
95 qed.
96
97 definition cr_pair ≝ λn,m,a,b. 
98 min (n*m) 0 (λx. andb (eqb (x \mod n) a) (eqb (x \mod m) b)).
99
100 example cr_pair1: cr_pair 2 3 O O = O.
101 // qed.
102
103 example cr_pair2: cr_pair 2 3 1 0 = 3.
104 // qed.
105
106 example cr_pair3: cr_pair 2 3 1 2 = 5.
107 // qed.
108
109 example cr_pair4: cr_pair 5 7 3 2 = 23.
110 // qed.
111
112 example cr_pair5: cr_pair 3 7 0 4 = ?.
113 normalize
114 // qed.
115
116 theorem mod_cr_pair : ∀m,n,a,b. a < m → b < n → gcd n m = 1 → 
117 (cr_pair m n a b) \mod m = a ∧ (cr_pair m n a b) \mod n = b.
118 #m #n #a #b #ltam #ltbn #pnm 
119 cut (andb (eqb ((cr_pair m n a b) \mod m) a) 
120          (eqb ((cr_pair m n a b) \mod n) b) = true)
121   [@f_min_true cases(congruent_ab_lt m n a b ?? pnm)
122     [#x * * #cxa #cxb #ltx @(ex_intro ?? x) % /2/
123      >eq_to_eqb_true 
124       [>eq_to_eqb_true // <(lt_to_eq_mod …ltbn) //
125       |<(lt_to_eq_mod …ltam) //
126       ]
127     |@(le_to_lt_to_lt … ltbn) //
128     |@(le_to_lt_to_lt … ltam) //
129     ]
130   |#H >(eqb_true_to_eq … (andb_true_l … H)) >(eqb_true_to_eq … (andb_true_r … H)) /2/
131   ]
132 qed.