(* ========================================================================= *)
(* Integer congruences.                                                      *)
(* ========================================================================= *)

prioritize_int();;

(* ------------------------------------------------------------------------- *)
(* Combined rewrite, for later proofs.                                       *)
(* ------------------------------------------------------------------------- *)

let CONG = 
prove (`(x == y) (mod n) <=> ?q. x - y = q * n`,
REWRITE_TAC[int_congruent; int_divides] THEN MESON_TAC[INT_MUL_SYM]);;
(* ------------------------------------------------------------------------- *) (* Trivial consequences. *) (* ------------------------------------------------------------------------- *)
let CONG_MOD_0 = 
prove (`(x == y) (mod (&0)) <=> (x = y)`,
INTEGER_TAC);;
let CONG_MOD_1 = 
prove (`(x == y) (mod (&1))`,
INTEGER_TAC);;
(* ------------------------------------------------------------------------- *) (* Congruence is an equivalence relation. *) (* ------------------------------------------------------------------------- *)
let CONG_REFL = 
prove (`!n x. (x == x) (mod n)`,
INTEGER_TAC);;
let CONG_SYM = 
prove (`!n x y. (x == y) (mod n) ==> (y == x) (mod n)`,
INTEGER_TAC);;
let CONG_TRANS = 
prove (`!n x y z. (x == y) (mod n) /\ (y == z) (mod n) ==> (x == z) (mod n)`,
INTEGER_TAC);;
(* ------------------------------------------------------------------------- *) (* Congruences are indeed congruences. *) (* ------------------------------------------------------------------------- *)
let CONG_ADD = 
prove (`!n x1 x2 y1 y2. (x1 == x2) (mod n) /\ (y1 == y2) (mod n) ==> (x1 + y1 == x2 + y2) (mod n)`,
INTEGER_TAC);;
let CONG_NEG = 
prove (`!n x1 x2. (x1 == x2) (mod n) ==> (--x1 == --x2) (mod n)`,
INTEGER_TAC);;
let CONG_SUB = 
prove (`!n x1 x2 y1 y2. (x1 == x2) (mod n) /\ (y1 == y2) (mod n) ==> (x1 - y1 == x2 - y2) (mod n)`,
INTEGER_TAC);;
let CONG_MUL = 
prove (`!n x1 x2 y1 y2. (x1 == x2) (mod n) /\ (y1 == y2) (mod n) ==> (x1 * y1 == x2 * y2) (mod n)`,
INTEGER_TAC);;
(* ------------------------------------------------------------------------- *) (* Various other trivial properties of congruences. *) (* ------------------------------------------------------------------------- *)
let CONG_MOD_NEG = 
prove (`!x y n. (x == y) (mod (--n)) <=> (x == y) (mod n)`,
INTEGER_TAC);;
let CONG_MOD_ABS = 
prove (`!x y n. (x == y) (mod (abs n)) <=> (x == y) (mod n)`,
REPEAT GEN_TAC THEN REWRITE_TAC[INT_ABS] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[CONG_MOD_NEG]);;
let CONG_MULTIPLE = 
prove (`!m n. (m * n == &0) (mod n)`,
INTEGER_TAC);;
let CONG_SELF = 
prove (`!n. (n == &0) (mod n)`,
INTEGER_TAC);;
let CONG_SELF_ABS = 
prove (`!n. (abs(n) == &0) (mod n)`,
ONCE_REWRITE_TAC[GSYM CONG_MOD_ABS] THEN REWRITE_TAC[CONG_SELF]);;
let CONG_MOD_1 = 
prove (`(x == y) (mod &1)`,
INTEGER_TAC);;
(* ------------------------------------------------------------------------- *) (* Can choose a representative, either positive or with minimal magnitude. *) (* ------------------------------------------------------------------------- *)
let CONG_REP_POS_POS = 
prove (`!n x. &0 <= x /\ ~(n = &0) ==> ?y. &0 <= y /\ y < abs(n) /\ (x == y) (mod n)`,
REWRITE_TAC[IMP_CONJ] THEN REWRITE_TAC[GSYM INT_FORALL_POS] THEN MAP_EVERY X_GEN_TAC [`n:int`; `k:num`] THEN ONCE_REWRITE_TAC[GSYM CONG_MOD_ABS] THEN MP_TAC(SPEC `n:int` INT_ABS_POS) THEN ONCE_REWRITE_TAC[INT_ARITH `(n = &0) <=> (abs n = &0)`] THEN SPEC_TAC(`abs n`,`n:int`) THEN REWRITE_TAC[GSYM INT_FORALL_POS] THEN X_GEN_TAC `n:num` THEN REWRITE_TAC[INT_OF_NUM_EQ] THEN DISCH_TAC THEN EXISTS_TAC `&(k MOD n)` THEN REWRITE_TAC[CONG; INT_OF_NUM_LE; INT_OF_NUM_LT] THEN ASM_SIMP_TAC[DIVISION; LE_0] THEN EXISTS_TAC `&(k DIV n)` THEN REWRITE_TAC[INT_ARITH `(x - y = z) <=> (x = z + y)`] THEN REWRITE_TAC[INT_OF_NUM_MUL; INT_OF_NUM_ADD; INT_OF_NUM_EQ] THEN ASM_SIMP_TAC[DIVISION]);;
let CONG_REP_POS = 
prove (`!n x. ~(n = &0) ==> ?y. &0 <= y /\ y < abs(n) /\ (x == y) (mod n)`,
REPEAT STRIP_TAC THEN DISJ_CASES_TAC(INT_ARITH `&0 <= x \/ &0 <= --x`) THEN ASM_SIMP_TAC[CONG_REP_POS_POS] THEN MP_TAC(SPECL [`n:int`; `--x`] CONG_REP_POS_POS) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `y:int` STRIP_ASSUME_TAC) THEN ASM_CASES_TAC `y = &0` THENL [EXISTS_TAC `y:int` THEN FIRST_ASSUM(MP_TAC o MATCH_MP CONG_NEG) THEN ASM_REWRITE_TAC[INT_NEG_0; INT_NEG_NEG]; ALL_TAC] THEN EXISTS_TAC `abs(n) - y` THEN ASM_SIMP_TAC[INT_ARITH `y < abs(n) ==> &0 <= abs(n) - y`; INT_ARITH `&0 <= y /\ ~(y = &0) ==> abs(n) - y < abs(n)`] THEN FIRST_ASSUM(MP_TAC o MATCH_MP CONG_NEG) THEN DISCH_THEN(MP_TAC o MATCH_MP CONG_SYM) THEN DISCH_THEN(MP_TAC o CONJ (SPEC `abs n` CONG_SELF)) THEN REWRITE_TAC[CONG_MOD_ABS] THEN DISCH_THEN(MP_TAC o MATCH_MP CONG_ADD) THEN REWRITE_TAC[INT_NEG_NEG; INT_ADD_LID] THEN MESON_TAC[INT_ARITH `x + --y = x - y`; CONG_SYM]);;
let CONG_REP_MIN = 
prove (`!n x. ~(n = &0) ==> ?y. --(abs n) <= &2 * y /\ &2 * y < abs n /\ (x == y) (mod n)`,
REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP CONG_REP_POS) THEN DISCH_THEN(X_CHOOSE_THEN `y:int` STRIP_ASSUME_TAC o SPEC `x:int`) THEN MP_TAC(INT_ARITH `&0 <= y /\ y < abs n ==> --(abs n) <= &2 * y /\ &2 * y < abs(n) \/ --(abs n) <= &2 * (y - abs(n)) /\ &2 * (y - abs(n)) < abs(n)`) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THENL [ASM_MESON_TAC[CONG_REP_POS; INT_LT_IMP_LE]; ALL_TAC] THEN EXISTS_TAC `y - abs(n)` THEN ASM_REWRITE_TAC[] THEN MP_TAC(SPEC `n:int` CONG_SELF_ABS) THEN DISCH_THEN(MP_TAC o MATCH_MP CONG_SYM) THEN UNDISCH_TAC `(x == y) (mod n)` THEN REWRITE_TAC[IMP_IMP] THEN DISCH_THEN(MP_TAC o MATCH_MP CONG_SUB) THEN REWRITE_TAC[INT_ARITH `x - &0 = x`]);;
let CONG_REP_MIN_ABS = 
prove (`!n x. ~(n = &0) ==> ?y. &2 * abs(y) <= abs(n) /\ (x == y) (mod n)`,
REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP CONG_REP_MIN) THEN DISCH_THEN(MP_TAC o SPEC `x:int`) THEN MATCH_MP_TAC MONO_EXISTS THEN SIMP_TAC[] THEN INT_ARITH_TAC);;