Examples/cong.ml

   1 (* ========================================================================= *)
   2 (* Integer congruences.                                                      *)
   3 (* ========================================================================= *)
   4
   5 prioritize_int();;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* Combined rewrite, for later proofs.                                       *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 let CONG = prove
  12  (`(x == y) (mod n) <=> ?q. x - y = q * n`,
  13   REWRITE_TAC[int_congruent; int_divides] THEN MESON_TAC[INT_MUL_SYM]);;
  14
  15 (* ------------------------------------------------------------------------- *)
  16 (* Trivial consequences.                                                     *)
  17 (* ------------------------------------------------------------------------- *)
  18
  19 let CONG_MOD_0 = prove
  20  (`(x == y) (mod (&0)) <=> (x = y)`,
  21   INTEGER_TAC);;
  22
  23 let CONG_MOD_1 = prove
  24  (`(x == y) (mod (&1))`,
  25   INTEGER_TAC);;
  26
  27 (* ------------------------------------------------------------------------- *)
  28 (* Congruence is an equivalence relation.                                    *)
  29 (* ------------------------------------------------------------------------- *)
  30
  31 let CONG_REFL = prove
  32  (`!n x. (x == x) (mod n)`,
  33   INTEGER_TAC);;
  34
  35 let CONG_SYM = prove
  36  (`!n x y. (x == y) (mod n) ==> (y == x) (mod n)`,
  37   INTEGER_TAC);;
  38
  39 let CONG_TRANS = prove
  40  (`!n x y z. (x == y) (mod n) /\ (y == z) (mod n) ==> (x == z) (mod n)`,
  41   INTEGER_TAC);;
  42
  43 (* ------------------------------------------------------------------------- *)
  44 (* Congruences are indeed congruences.                                       *)
  45 (* ------------------------------------------------------------------------- *)
  46
  47 let CONG_ADD = prove
  48  (`!n x1 x2 y1 y2.
  49     (x1 == x2) (mod n) /\ (y1 == y2) (mod n) ==> (x1 + y1 == x2 + y2) (mod n)`,
  50   INTEGER_TAC);;
  51
  52 let CONG_NEG = prove
  53  (`!n x1 x2. (x1 == x2) (mod n) ==> (--x1 == --x2) (mod n)`,
  54   INTEGER_TAC);;
  55
  56 let CONG_SUB = prove
  57  (`!n x1 x2 y1 y2.
  58     (x1 == x2) (mod n) /\ (y1 == y2) (mod n) ==> (x1 - y1 == x2 - y2) (mod n)`,
  59   INTEGER_TAC);;
  60
  61 let CONG_MUL = prove
  62  (`!n x1 x2 y1 y2.
  63     (x1 == x2) (mod n) /\ (y1 == y2) (mod n) ==> (x1 * y1 == x2 * y2) (mod n)`,
  64   INTEGER_TAC);;
  65
  66 (* ------------------------------------------------------------------------- *)
  67 (* Various other trivial properties of congruences.                          *)
  68 (* ------------------------------------------------------------------------- *)
  69
  70 let CONG_MOD_NEG = prove
  71  (`!x y n. (x == y) (mod (--n)) <=> (x == y) (mod n)`,
  72   INTEGER_TAC);;
  73
  74 let CONG_MOD_ABS = prove
  75  (`!x y n. (x == y) (mod (abs n)) <=> (x == y) (mod n)`,
  76   REPEAT GEN_TAC THEN REWRITE_TAC[INT_ABS] THEN
  77   COND_CASES_TAC THEN ASM_REWRITE_TAC[CONG_MOD_NEG]);;
  78
  79 let CONG_MULTIPLE = prove
  80  (`!m n. (m * n == &0) (mod n)`,
  81   INTEGER_TAC);;
  82
  83 let CONG_SELF = prove
  84  (`!n. (n == &0) (mod n)`,
  85   INTEGER_TAC);;
  86
  87 let CONG_SELF_ABS = prove
  88  (`!n. (abs(n) == &0) (mod n)`,
  89   ONCE_REWRITE_TAC[GSYM CONG_MOD_ABS] THEN REWRITE_TAC[CONG_SELF]);;
  90
  91 let CONG_MOD_1 = prove
  92  (`(x == y) (mod &1)`,
  93   INTEGER_TAC);;
  94
  95 (* ------------------------------------------------------------------------- *)
  96 (* Can choose a representative, either positive or with minimal magnitude.   *)
  97 (* ------------------------------------------------------------------------- *)
  98
  99 let CONG_REP_POS_POS = prove
 100  (`!n x. &0 <= x /\ ~(n = &0)
 101          ==> ?y. &0 <= y /\ y < abs(n) /\ (x == y) (mod n)`,
 102   REWRITE_TAC[IMP_CONJ] THEN
 103   REWRITE_TAC[GSYM INT_FORALL_POS] THEN
 104   MAP_EVERY X_GEN_TAC [`n:int`; `k:num`] THEN
 105   ONCE_REWRITE_TAC[GSYM CONG_MOD_ABS] THEN
 106   MP_TAC(SPEC `n:int` INT_ABS_POS) THEN
 107   ONCE_REWRITE_TAC[INT_ARITH `(n = &0) <=> (abs n = &0)`] THEN
 108   SPEC_TAC(`abs n`,`n:int`) THEN REWRITE_TAC[GSYM INT_FORALL_POS] THEN
 109   X_GEN_TAC `n:num` THEN REWRITE_TAC[INT_OF_NUM_EQ] THEN DISCH_TAC THEN
 110   EXISTS_TAC `&(k MOD n)` THEN
 111   REWRITE_TAC[CONG; INT_OF_NUM_LE; INT_OF_NUM_LT] THEN
 112   ASM_SIMP_TAC[DIVISION; LE_0] THEN EXISTS_TAC `&(k DIV n)` THEN
 113   REWRITE_TAC[INT_ARITH `(x - y = z) <=> (x = z + y)`] THEN
 114   REWRITE_TAC[INT_OF_NUM_MUL; INT_OF_NUM_ADD; INT_OF_NUM_EQ] THEN
 115   ASM_SIMP_TAC[DIVISION]);;
 116
 117 let CONG_REP_POS = prove
 118  (`!n x. ~(n = &0) ==> ?y. &0 <= y /\ y < abs(n) /\ (x == y) (mod n)`,
 119   REPEAT STRIP_TAC THEN
 120   DISJ_CASES_TAC(INT_ARITH `&0 <= x \/ &0 <= --x`) THEN
 121   ASM_SIMP_TAC[CONG_REP_POS_POS] THEN
 122   MP_TAC(SPECL [`n:int`; `--x`] CONG_REP_POS_POS) THEN
 123   ASM_REWRITE_TAC[] THEN
 124   DISCH_THEN(X_CHOOSE_THEN `y:int` STRIP_ASSUME_TAC) THEN
 125   ASM_CASES_TAC `y = &0` THENL
 126    [EXISTS_TAC `y:int` THEN
 127     FIRST_ASSUM(MP_TAC o MATCH_MP CONG_NEG) THEN
 128     ASM_REWRITE_TAC[INT_NEG_0; INT_NEG_NEG];
 129     ALL_TAC] THEN
 130   EXISTS_TAC `abs(n) - y` THEN
 131   ASM_SIMP_TAC[INT_ARITH `y < abs(n) ==> &0 <= abs(n) - y`;
 132                INT_ARITH `&0 <= y /\ ~(y = &0) ==> abs(n) - y < abs(n)`] THEN
 133   FIRST_ASSUM(MP_TAC o MATCH_MP CONG_NEG) THEN
 134   DISCH_THEN(MP_TAC o MATCH_MP CONG_SYM) THEN
 135   DISCH_THEN(MP_TAC o CONJ (SPEC `abs n` CONG_SELF)) THEN
 136   REWRITE_TAC[CONG_MOD_ABS] THEN
 137   DISCH_THEN(MP_TAC o MATCH_MP CONG_ADD) THEN
 138   REWRITE_TAC[INT_NEG_NEG; INT_ADD_LID] THEN
 139   MESON_TAC[INT_ARITH `x + --y = x - y`; CONG_SYM]);;
 140
 141 let CONG_REP_MIN = prove
 142  (`!n x. ~(n = &0)
 143          ==> ?y. --(abs n) <= &2 * y /\ &2 * y < abs n /\ (x == y) (mod n)`,
 144   REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP CONG_REP_POS) THEN
 145   DISCH_THEN(X_CHOOSE_THEN `y:int` STRIP_ASSUME_TAC o SPEC `x:int`) THEN
 146   MP_TAC(INT_ARITH
 147    `&0 <= y /\ y < abs n
 148     ==> --(abs n) <= &2 * y /\ &2 * y < abs(n) \/
 149         --(abs n) <= &2 * (y - abs(n)) /\ &2 * (y - abs(n)) < abs(n)`) THEN
 150   ASM_REWRITE_TAC[] THEN STRIP_TAC THENL
 151    [ASM_MESON_TAC[CONG_REP_POS; INT_LT_IMP_LE]; ALL_TAC] THEN
 152   EXISTS_TAC `y - abs(n)` THEN ASM_REWRITE_TAC[] THEN
 153   MP_TAC(SPEC `n:int` CONG_SELF_ABS) THEN
 154   DISCH_THEN(MP_TAC o MATCH_MP CONG_SYM) THEN
 155   UNDISCH_TAC `(x == y) (mod n)` THEN
 156   REWRITE_TAC[IMP_IMP] THEN
 157   DISCH_THEN(MP_TAC o MATCH_MP CONG_SUB) THEN
 158   REWRITE_TAC[INT_ARITH `x - &0 = x`]);;
 159
 160 let CONG_REP_MIN_ABS = prove
 161  (`!n x. ~(n = &0) ==> ?y. &2 * abs(y) <= abs(n) /\ (x == y) (mod n)`,
 162   REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP CONG_REP_MIN) THEN
 163   DISCH_THEN(MP_TAC o SPEC `x:int`) THEN MATCH_MP_TAC MONO_EXISTS THEN
 164   SIMP_TAC[] THEN INT_ARITH_TAC);;