# Congruence

Require Export ZArith.
Require Import Zdivides.
Require Import sTactic.

Useful lemmae

Theorem Zabs_absolu : z : Z, Zabs z = Z_of_nat (Zabs_nat z).
intros z; case z; simpl in |- *; auto; intros p; apply POS_inject.
Qed.

Theorem Zlt_ZERO_minus : a b : Z, (a < b)%Z → (0 < b - a)%Z.
intros; unfold Zminus in |- *; apply Zlt_left_lt; auto.
Qed.

Theorem lt_inj : a b : nat, (Z_of_nat a < Z_of_nat b)%Za < b.
intros a b H; case (le_or_lt b a); auto; intros H0.
Contradict H; apply Zle_not_lt; apply Znat.inj_le; auto with zarith arith.
Qed.

Definition of the congruence
Definition congZ (i : nat) (a b : Z) :=
c : Z, a = (b + c × Z_of_nat i)%Z.

Some basic properties of the congruence
Theorem congZ_id : (i : nat) (a : Z), congZ i a a.
intros i a; 0%Z; simpl in |- *; ring.
Qed.
Hint Resolve congZ_id.

Theorem congZ_sym : (a b : Z) (i : nat), congZ i a bcongZ i b a.
intros a b i (x, H); (- x)%Z; rewrite H; ring.
Qed.

Theorem congZ_trans :
(a b c : Z) (i : nat), congZ i a bcongZ i b ccongZ i a c.
intros a b c i (x, H) (y, H1); (x + y)%Z; rewrite H; rewrite H1; ring.
Qed.

Theorem congZ_plus :
(a b c d : Z) (i : nat),
congZ i a bcongZ i c dcongZ i (a + c) (b + d).
intros a b c d i (x, H) (y, H1); (x + y)%Z; rewrite H; rewrite H1;
ring.
Qed.

Theorem congZ_minus :
(a b c d : Z) (i : nat),
congZ i a bcongZ i c dcongZ i (a - c) (b - d).
intros a b c d i (x, H) (y, H1); (x - y)%Z; rewrite H; rewrite H1;
ring.
Qed.

Theorem congZ_mult :
(a b : Z) (i j : nat),
congZ i a bcongZ (i × j) (a × Z_of_nat j) (b × Z_of_nat j).
intros a b i j (x, H); x; rewrite H; rewrite Znat.inj_mult; ring.
Qed.

Definition fcong (i : nat) (a b : Z) :=
match i with
| O ⇒ 0
| S i1
let ab := (a - b)%Z in
match (ab - Z_of_nat i × Zquotient ab (Z_of_nat i))%Z with
| Zneg p1Zabs_nat (Z_of_nat i + Zneg p1)
| pZabs_nat p
end
end.

Theorem fcong_correct :
(i : nat) (a b : Z),
i 0 → congZ i a (b + Z_of_nat (fcong i a b)) fcong i a b < i.
intros i a b; unfold fcong in |- *; case i; auto.
intros H; elim H; auto.
intros n H.
case (ZquotientProp (a - b) (Z_of_nat (S n))); auto with arith.
simpl in |- *; red in |- *; intros; discriminate.
intros x (H1, H2).
replace (a - b - Z_of_nat (S n) × Zquotient (a - b) (Z_of_nat (S n)))%Z with
x; [ idtac | pattern (a - b)%Z at 1 in |- *; rewrite H1; ring ].
generalize H1 H2; case x; clear H1 H2 x.
intros H1 (H2, H3); split; simpl in |- ×.
(Zquotient (a - b) (Z_of_nat (S n))).
apply trans_equal with (b + (a - b))%Z.
ring.
pattern (a - b)%Z at 1 in |- *; rewrite H1; ring; auto with arith.
auto with arith.
intros p H1 (H2, H3); split; auto.
(Zquotient (a - b) (Z_of_nat (S n))).
apply trans_equal with (b + (a - b))%Z.
ring.
pattern (a - b)%Z at 1 in |- *; rewrite H1; ring_simplify;
eapply Zplus_eq_compat; [reflexivity | simpl; apply POS_inject].
case (le_or_lt (S n) (Zabs_nat (Zpos p))); intros H4; auto.
Contradict H3; simpl in |- ×.
apply Zle_not_lt.
repeat rewrite POS_inject.
rewrite nat_of_P_o_P_of_succ_nat_eq_succ; apply Znat.inj_le;
auto with zarith arith.
intros p H1 (H2, H3); split; auto.
(Zquotient (a - b) (Z_of_nat (S n)) - 1)%Z.
apply trans_equal with (b + (a - b))%Z.
ring.
replace (Z_of_nat (Zabs_nat (Z_of_nat (S n) + Zneg p))) with
(Z_of_nat (S n) + Zneg p)%Z.
pattern (a - b)%Z at 1 in |- *; rewrite H1; ring.
rewrite <- Zabs_absolu; auto.
apply sym_equal; apply Zabs_eq.
change (0 Z_of_nat (S n) - Zpos p)%Z in |- ×.
apply Zlt_le_weak; apply Zlt_ZERO_minus.
rewrite <- (Zabs_eq (Z_of_nat (S n))); auto with zarith arith.
apply lt_inj.
rewrite <- Zabs_absolu; auto.
rewrite Zabs_eq.
pattern (Z_of_nat (S n)) at 2 in |- *;
replace (Z_of_nat (S n)) with (Z_of_nat (S n) + 0)%Z;
auto with zarith.
change (0 Z_of_nat (S n) - Zpos p)%Z in |- ×.
apply Zlt_le_weak; apply Zlt_ZERO_minus.
rewrite <- (Zabs_eq (Z_of_nat (S n))); auto with zarith arith.
Qed.

Theorem neg_cong :
(i : nat) (a b : Z),
i 0 →
¬ congZ i a b x : _, 0 < x x < i congZ i a (b + Z_of_nat x).
intros i a b H H0; (fcong i a b).
case (fcong_correct i a b); auto; intros H1 H2.
repeat split; auto.
generalize H1; case (fcong i a b); simpl in |- *; auto with arith.
replace (b + 0)%Z with b; auto with zarith.
intros H3; case H0; auto.
Qed.

Congruence is decidable
Definition congZ_dec :
(i : nat) (a b : Z), {congZ i a b} + {¬ congZ i a b}.
intros i a b; case i.
generalize (Z_eq_bool_correct a b); case (Z_eq_bool a b).
intros H; left; 0%Z; rewrite H; ring.
intros H; right; red in |- *; intros (x, H0); case H; rewrite H0; ring.
intros n; case (ZdividesP (a - b) (Z_of_nat (S n))).
intros H; left; case H; intros x H1.
x; replace a with (b + (a - b))%Z; [ rewrite H1 | idtac ]; ring.
intros H; right; red in |- *; intros (x, H0); case H.
x; rewrite H0; ring.
Defined.

Theorem congZ_O_Eq : a b, congZ 0 a b a = b.
intros a b; split.
intros (m1, H1); rewrite H1; ring.
intros H1; rewrite H1; 0%Z; ring.
Qed.