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.