Require Import RIneq. Require Import ZArith. Require Export Cfield_facts. Set Implicit Arguments. Unset Strict Implicit. Comments " " "we" "want" "to" "define" "Zq" "like" "a" "setoid" "". Comments " " "we" "define" "the" "equivalence" "relation" "mod" "as" "being" "the" "relation" "on" "the" "setoid" "in" "which" "its" "elements" "are" "in" "Z". Section Zq. Definition mod_ (q a b : Z) := exists k : Z, (a - b)%Z = (k * q)%Z. Variable q : nat. Hypothesis Q : (Z_of_nat q > 1)%Z. Comments " " "we" "demonstrate" "mod" "is" "an" "equivalence" "relation". Lemma mod_refl : forall a : Z, mod_ (Z_of_nat q) a a. intros. unfold mod_ in |- *. exists (Z_of_nat 0). simpl in |- *. auto with *. Qed. Lemma mod_sym : forall a b : Z, mod_ (Z_of_nat q) a b -> mod_ (Z_of_nat q) b a. intros. elim H. intros. unfold mod_ in |- *. exists (- x)%Z. cut ((b - a)%Z = (- (x * Z_of_nat q))%Z). intros. cut ((- (x * Z_of_nat q))%Z = (- x * Z_of_nat q)%Z). intros. rewrite <- H2. try exact H1. apply Zopp_mult_distr_l. auto with *. Qed. Lemma mod_trans : forall a b c : Z, mod_ (Z_of_nat q) a b -> mod_ (Z_of_nat q) b c -> mod_ (Z_of_nat q) a c. intros. unfold mod_ in |- *. inversion H. inversion H0. exists (x + x0)%Z. cut ((a - b + (b - c))%Z = ((x + x0) * Z_of_nat q)%Z). intros. auto with *. rewrite H1. rewrite H2. auto with *. Qed. Lemma mod_equiv : equivalence (mod_ (Z_of_nat q)). red in |- *. split. exact mod_refl. split. exact mod_trans. exact mod_sym. Qed. Comments " " "now" "we" "can" "define" "Z(INZ q)". Definition Zq := Build_Setoid mod_equiv. Comments " " " " "it" "'" "s" "just" "a" "test" "to" "see" "if" "Zq" "is" "well" "defined" " ". Lemma test : forall a : Zq, mod_ (Z_of_nat q) a (a + a * Z_of_nat q). intros. red in |- *. exists (- a)%Z. cut ((a - (a + a * Z_of_nat q))%Z = (a - a - a * Z_of_nat q)%Z). intros. rewrite H. cut ((a - a)%Z = Z_of_nat 0). intros. rewrite H0. cut ((Z_of_nat 0 - a * Z_of_nat q)%Z = (- (a * Z_of_nat q))%Z). intros. rewrite H1. apply Zopp_mult_distr_l. auto with *. cut (Z_of_nat 0 = (a - a)%Z). intros. auto with *. apply Zminus_diag_reverse. auto with *. Qed. Lemma Zq_plus_eq : forall a b c d : Zq, mod_ (Z_of_nat q) a b -> mod_ (Z_of_nat q) c d -> mod_ (Z_of_nat q) (a + c) (b + d). intros. inversion H0. inversion H. exists (x + x0)%Z. cut ((a + c - (b + d))%Z = (c - d + (a - b))%Z). intros. rewrite H3. rewrite H2. rewrite H1. auto with *. auto with *. Qed. Hint Resolve Zq_plus_eq: Zq. Comments " " " " "there" "are" "some" "lemma" "I" "must" "use" "to" "demonstrate" "Zq_mult" " ". Lemma inv : forall (c d : Zq) (x : Z), (c - d)%Z = (x * Z_of_nat q)%Z -> c = (d + x * Z_of_nat q)%Z :>Z. intros. omega. Qed. Hint Resolve inv: setoid. Lemma Zmult_distr_plus : forall a b c d : Z, ((a + b) * (c + d))%Z = (a * c + a * d + b * c + b * d)%Z. intros. assert (((a + b) * (c + d))%Z = ((a + b) * c + (a + b) * d)%Z). apply Zmult_plus_distr_r. rewrite H. assert (((a + b) * c)%Z = (a * c + b * c)%Z). auto with *. rewrite H0. assert (((a + b) * d)%Z = (a * d + b * d)%Z). auto with *. rewrite H1. auto with *. Qed. Hint Resolve Zmult_distr_plus: setoid. Lemma mult_perm : forall a b c : Z, (a * b * c)%Z = (a * c * b)%Z. intros. assert ((a * b * c)%Z = (a * (b * c))%Z). apply Zmult_assoc_reverse. rewrite H. assert ((a * (b * c))%Z = (b * (a * c))%Z). apply Zmult_permute. rewrite H0. auto with *. Qed. Hint Resolve mult_perm: setoid. Lemma Zmult_distr : forall a b c d q : Z, (a * (b * q) + c * d * q)%Z = ((a * b + c * d) * q)%Z. intros. assert ((a * (b * q0))%Z = (a * b * q0)%Z). auto with *. rewrite H. auto with *. Qed. Hint Resolve Zmult_distr: setoid. Lemma Zq_mult_eq : forall a b c d : Zq, mod_ (Z_of_nat q) a b -> mod_ (Z_of_nat q) c d -> mod_ (Z_of_nat q) (a * c) (b * d). intros. inversion H0. inversion H. assert ((a:Z) = (b + x0 * Z_of_nat q)%Z). apply inv. try exact H2. assert ((c:Z) = (d + x * Z_of_nat q)%Z). apply inv. try exact H1. exists (b * x + x0 * d + x0 * Z_of_nat q * x)%Z. rewrite H3. rewrite H4. assert (((b + x0 * Z_of_nat q) * (d + x * Z_of_nat q))%Z = (b * d + b * (x * Z_of_nat q) + x0 * Z_of_nat q * d + x0 * Z_of_nat q * (x * Z_of_nat q))%Z). apply Zmult_distr_plus. rewrite H5. assert ((b * d + b * (x * Z_of_nat q) + x0 * Z_of_nat q * d + x0 * Z_of_nat q * (x * Z_of_nat q) - b * d)%Z = (b * (x * Z_of_nat q) + x0 * Z_of_nat q * d + x0 * Z_of_nat q * (x * Z_of_nat q))%Z). auto with *. rewrite H6. assert ((x0 * Z_of_nat q * d)%Z = (x0 * d * Z_of_nat q)%Z). apply mult_perm. rewrite H7. assert ((b * (x * Z_of_nat q) + x0 * d * Z_of_nat q)%Z = ((b * x + x0 * d) * Z_of_nat q)%Z). apply Zmult_distr. rewrite H8. assert ((x0 * Z_of_nat q * (x * Z_of_nat q))%Z = (x0 * Z_of_nat q * x * Z_of_nat q)%Z). auto with *. rewrite H9. auto with *. Qed. Hint Resolve Zq_mult_eq: Zq. Comments " " "we" "demonstrate" "each" "element" "in" "Zq" "is" "the" "sum" "of" "itself" "and" "a" "multiple" "of" "(INZ q)". Lemma mod_eq : forall (a : Zq) (k : Z), mod_ (Z_of_nat q) a (a + k * Z_of_nat q). intros. red in |- *. exists (- k)%Z. cut ((a - (a + k * Z_of_nat q))%Z = (a - a - k * Z_of_nat q)%Z). intros. rewrite H. cut ((a - a)%Z = Z_of_nat 0). intros. rewrite H0. cut ((Z_of_nat 0 - k * Z_of_nat q)%Z = (- (k * Z_of_nat q))%Z). intros. rewrite H1. apply Zopp_mult_distr_l. auto with *. cut (Z_of_nat 0 = (a - a)%Z). intros. auto with *. apply Zminus_diag_reverse. auto with *. Qed. Hint Resolve mod_eq: Zq. Comments " " "we" "demonstrate" "associativity" "of" "*". Lemma Zq_mult_ass : forall a b c : Zq, mod_ (Z_of_nat q) (a * (b * c)) (a * b * c). intros. red in |- *. exists 0%Z. simpl in |- *. assert ((a * (b * c))%Z = (a * b * c)%Z). auto with *. rewrite H. auto with *. Qed. Comments " " "we" "demonstrate" "distributivity" "of" "*". Lemma Zq_mult_distr_l : forall a b c : Zq, mod_ (Z_of_nat q) (a * (b + c)) (a * b + a * c). intros. red in |- *. exists 0%Z. simpl in |- *. assert ((a * (b + c))%Z = (a * b + a * c)%Z). auto with *. rewrite H. auto with *. Qed. Lemma Zq_mult_distr_r : forall a b c : Zq, mod_ (Z_of_nat q) ((a + b) * c) (a * c + b * c). intros. red in |- *. exists 0%Z. simpl in |- *. assert (((a + b) * c)%Z = (a * c + b * c)%Z). auto with *. rewrite H. auto with *. Qed. Require Export Fermat. Hypothesis pow_Zpow : forall a b : nat, Z_of_nat (power a b) = (Z_of_nat a ^ Z_of_nat b)%Z. Lemma nat_Z : forall a b : nat, a = b -> Z_of_nat a = Z_of_nat b. intros. auto with *. Qed. Hypothesis min_Zmin : forall a b : nat, Z_of_nat (a - b) = (Z_of_nat a - Z_of_nat b)%Z. Hypothesis in_abs : forall a : Z, (a > 0)%Z -> Z_of_nat (Zabs_nat a) = a. Lemma cong_mod : forall x : Zq, (0 < x)%Z -> (x < Z_of_nat q)%Z -> congruent (Zabs_nat (Z_of_nat q)) (power (Zabs_nat x) (Zabs_nat (Z_of_nat q) - 1)) 1 -> mod_ (Z_of_nat q) (x ^ (Z_of_nat q - 1)) 1. intros. inversion H1. assert (Z_of_nat (power (Zabs_nat x) (Zabs_nat (Z_of_nat q) - 1)) = (Z_of_nat (Zabs_nat x) ^ Z_of_nat (Zabs_nat (Z_of_nat q) - 1))%Z). apply pow_Zpow. assert (Z_of_nat (power (Zabs_nat x) (Zabs_nat (Z_of_nat q) - 1) + u * Zabs_nat (Z_of_nat q)) = (Z_of_nat (power (Zabs_nat x) (Zabs_nat (Z_of_nat q) - 1)) + Z_of_nat (u * Zabs_nat (Z_of_nat q)))%Z). apply Znat.inj_plus. assert (Z_of_nat (1 + v * Zabs_nat (Z_of_nat q)) = (Z_of_nat 1 + Z_of_nat (v * Zabs_nat (Z_of_nat q)))%Z). apply Znat.inj_plus. assert ((Z_of_nat (power (Zabs_nat x) (Zabs_nat (Z_of_nat q) - 1)) + Z_of_nat (u * Zabs_nat (Z_of_nat q)))%Z = (Z_of_nat 1 + Z_of_nat (v * Zabs_nat (Z_of_nat q)))%Z). rewrite <- H6. rewrite <- H7. apply nat_Z. try exact H2. assert ((Z_of_nat (power (Zabs_nat x) (Zabs_nat (Z_of_nat q) - 1)) - Z_of_nat 1)%Z = (Z_of_nat (v * Zabs_nat (Z_of_nat q)) - Z_of_nat (u * Zabs_nat (Z_of_nat q)))%Z). auto with *. assert (Z_of_nat (v * Zabs_nat (Z_of_nat q) - u * Zabs_nat (Z_of_nat q)) = (Z_of_nat (v * Zabs_nat (Z_of_nat q)) - Z_of_nat (u * Zabs_nat (Z_of_nat q)))%Z). apply min_Zmin. rewrite <- H10 in H9. assert (v * Zabs_nat (Z_of_nat q) - u * Zabs_nat (Z_of_nat q) = (v - u) * Zabs_nat (Z_of_nat q)). auto with *. rewrite H11 in H9. exists (Z_of_nat (v - u)). assert (Z_of_nat (power (Zabs_nat x) (Zabs_nat (Z_of_nat q) - 1)) = (Z_of_nat (Zabs_nat x) ^ Z_of_nat (Zabs_nat (Z_of_nat q) - 1))%Z). apply pow_Zpow. assert (Z_of_nat (Zabs_nat (Z_of_nat q) - 1) = (Z_of_nat (Zabs_nat (Z_of_nat q)) - Z_of_nat 1)%Z). apply min_Zmin. rewrite H13 in H12. assert (Z_of_nat (Zabs_nat x) = x). apply in_abs. auto with *. rewrite H14 in H12. assert (Z_of_nat (Zabs_nat (Z_of_nat q)) = Z_of_nat q). apply in_abs. auto with *. rewrite H15 in H12. rewrite H12 in H9. assert (Z_of_nat ((v - u) * Zabs_nat (Z_of_nat q)) = (Z_of_nat (v - u) * Z_of_nat (Zabs_nat (Z_of_nat q)))%Z). apply Znat.inj_mult. rewrite H16 in H9. rewrite H15 in H9. try exact H9. Qed. Lemma Fermat' : forall x : Zq, prime (Zabs_nat (Z_of_nat q)) -> (0 < x)%Z -> (x < Z_of_nat q)%Z -> mod_ (Z_of_nat q) (x ^ (Z_of_nat q - 1)) 1. intros. apply cong_mod. try exact H0. try exact H1. apply Fermat. try exact H. red in |- *. intros. inversion H2. induction q0 as [| q0 Hrecq0]. simpl in H3. assert (Z_of_nat (Zabs_nat x) = Z_of_nat 0). apply nat_Z. try exact H3. assert (Z_of_nat (Zabs_nat x) = x). apply in_abs. auto with *. rewrite <- H7 in H0. auto with *. assert (Z_of_nat (Zabs_nat x) = (Z_of_nat (S q0) * Z_of_nat (Zabs_nat (Z_of_nat q)))%Z). assert (Z_of_nat (S q0 * Zabs_nat (Z_of_nat q)) = (Z_of_nat (S q0) * Z_of_nat (Zabs_nat (Z_of_nat q)))%Z). apply Znat.inj_mult. rewrite <- H6. apply nat_Z. try exact H3. assert (Z_of_nat (Zabs_nat x) = x). apply in_abs. auto with *. rewrite <- H7 in H1. assert (Z_of_nat (Zabs_nat (Z_of_nat q)) = Z_of_nat q). apply in_abs. auto with *. rewrite H8 in H6. assert (Z_of_nat (S q0) * Z_of_nat q >= Z_of_nat q)%Z. assert (S q0 >= 1). auto with *. assert (Z_of_nat (S q0) >= Z_of_nat 1)%Z. apply Znat.inj_ge. try exact H9. assert (Z_of_nat q = (Z_of_nat 1 * Z_of_nat q)%Z). auto with *. pattern (Z_of_nat q) at 2 in |- *. rewrite H11. apply Zmult_ge_compat_r. try exact H10. auto with *. auto with *. Qed. Comments " " " " "we" "define" "the" "function" "giving" "opposite" "element" "for" "mult" " ". Hypothesis prem : prime (Zabs_nat (Z_of_nat q)). Definition Zq_inv (x : Zq) : Zq := ((x mod Z_of_nat q) ^ (Z_of_nat q - 2))%Z. Lemma Zmod_borne : forall x : Z, (0 <= x mod Z_of_nat q)%Z /\ (x mod Z_of_nat q < Z_of_nat q)%Z. intros. apply Z_mod_lt. assert (Z_of_nat q > 1)%Z. apply Q. auto with *. Qed. Lemma Zpow_id : forall x : Z, (x ^ 1)%Z = x. intros. unfold Zpower in |- *. unfold Zpower_pos in |- *. simpl in |- *. auto with *. Qed. Lemma modq : forall x : Zq, mod_ (Z_of_nat q) x (x mod Z_of_nat q). intros. red in |- *. assert ((x:Z) = (Z_of_nat q * (x / Z_of_nat q) + x mod Z_of_nat q)%Z). apply Z_div_mod_eq. assert (Z_of_nat q > 1)%Z. apply Q. auto with *. pattern x at 1 in |- *. rewrite H. exists (x / Z_of_nat q)%Z. assert ((Z_of_nat q * (x / Z_of_nat q) + x mod Z_of_nat q - x mod Z_of_nat q)%Z = (Z_of_nat q * (x / Z_of_nat q) + (x mod Z_of_nat q - x mod Z_of_nat q))%Z). auto with *. rewrite H0. assert ((x mod Z_of_nat q - x mod Z_of_nat q)%Z = 0%Z). auto with *. rewrite H1. assert ((Z_of_nat q * (x / Z_of_nat q))%Z = (x / Z_of_nat q * Z_of_nat q)%Z). auto with *. auto with *. Qed. Lemma Zmod_mod : forall x : Zq, ~ mod_ (Z_of_nat q) x 0 -> (x mod Z_of_nat q)%Z <> 0%Z. intros. red in |- *. intros. unfold not in H. apply H. red in |- *. exists (x / Z_of_nat q)%Z. rewrite <- H0. assert ((x:Z) = (Z_of_nat q * (x / Z_of_nat q) + x mod Z_of_nat q)%Z). apply Z_div_mod_eq. assert (Z_of_nat q > 1)%Z. apply Q. auto with *. assert ((x / Z_of_nat q * Z_of_nat q)%Z = (Z_of_nat q * (x / Z_of_nat q))%Z). auto with *. rewrite H2. auto with *. Qed. Lemma Zq_mult_inv_r : forall x : Zq, ~ mod_ (Z_of_nat q) x 0 -> mod_ (Z_of_nat q) (x * Zq_inv x) 1. intros. assert ((x mod Z_of_nat q)%Z <> 0%Z). apply Zmod_mod. try exact H. assert (mod_ (Z_of_nat q) x (x mod Z_of_nat q)). apply modq. inversion H1. assert ((x:Z) = (x mod Z_of_nat q + x0 * Z_of_nat q)%Z). auto with *. pattern x at 1 in |- *. rewrite H3. assert (((x mod Z_of_nat q + x0 * Z_of_nat q) * Zq_inv x)%Z = (x mod Z_of_nat q * Zq_inv x + x0 * Z_of_nat q * Zq_inv x)%Z). auto with *. rewrite H4. assert (mod_ (Z_of_nat q) ((x mod Z_of_nat q) ^ (Z_of_nat q - 1)) 1). assert ((0 <= x mod Z_of_nat q)%Z /\ (x mod Z_of_nat q < Z_of_nat q)%Z). apply Zmod_borne. elim H5. intros. apply Fermat'. apply prem. auto with *. try exact H7. unfold Zq_inv in |- *. inversion H5. assert (((x mod Z_of_nat q) ^ (Z_of_nat q - 1))%Z = (1 + x1 * Z_of_nat q)%Z). auto with *. cut (((x mod Z_of_nat q) ^ 1)%Z = (x mod Z_of_nat q)%Z). intros. pattern (x mod Z_of_nat q)%Z at 1 in |- *. rewrite <- H8. assert (((x mod Z_of_nat q) ^ (1 + (Z_of_nat q - 2)))%Z = ((x mod Z_of_nat q) ^ 1 * (x mod Z_of_nat q) ^ (Z_of_nat q - 2))%Z). apply Zpower_exp. auto with *. assert (Z_of_nat q > 1)%Z. apply Q. assert (Z_of_nat q >= 2)%Z. auto with *. auto with *. assert ((1 + (Z_of_nat q - 2))%Z = (Z_of_nat q - 1)%Z). auto with *. rewrite H10 in H9. rewrite <- H9. red in |- *. exists (x1 + x0 * (x mod Z_of_nat q) ^ (Z_of_nat q - 2))%Z. rewrite H7. assert ((1 + x1 * Z_of_nat q + x0 * Z_of_nat q * (x mod Z_of_nat q) ^ (Z_of_nat q - 2) - 1)%Z = (x1 * Z_of_nat q + x0 * Z_of_nat q * (x mod Z_of_nat q) ^ (Z_of_nat q - 2) + (1 - 1))%Z). auto with *. rewrite H11. simpl in |- *. assert ((x0 * Z_of_nat q * (x mod Z_of_nat q) ^ (Z_of_nat q - 2))%Z = (x0 * (x mod Z_of_nat q) ^ (Z_of_nat q - 2) * Z_of_nat q)%Z). auto with *. rewrite H12. assert ((x1 * Z_of_nat q + x0 * (x mod Z_of_nat q) ^ (Z_of_nat q - 2) * Z_of_nat q + 0)%Z = (x1 * Z_of_nat q + x0 * (x mod Z_of_nat q) ^ (Z_of_nat q - 2) * Z_of_nat q)%Z). auto with *. rewrite H13. auto with *. apply Zpow_id. Qed. Lemma Zq_mult_inv_l : forall x : Zq, ~ mod_ (Z_of_nat q) x 0 -> mod_ (Z_of_nat q) (Zq_inv x * x) 1. intros. assert ((x mod Z_of_nat q)%Z <> 0%Z). apply Zmod_mod. try exact H. assert (mod_ (Z_of_nat q) x (x mod Z_of_nat q)). apply modq. inversion H1. assert ((x:Z) = (x mod Z_of_nat q + x0 * Z_of_nat q)%Z). auto with *. pattern x at 2 in |- *. rewrite H3. assert ((Zq_inv x * (x mod Z_of_nat q + x0 * Z_of_nat q))%Z = (Zq_inv x * (x mod Z_of_nat q) + Zq_inv x * (x0 * Z_of_nat q))%Z). auto with *. rewrite H4. assert (mod_ (Z_of_nat q) ((x mod Z_of_nat q) ^ (Z_of_nat q - 1)) 1). assert ((0 <= x mod Z_of_nat q)%Z /\ (x mod Z_of_nat q < Z_of_nat q)%Z). apply Zmod_borne. elim H5. intros. apply Fermat'. apply prem. auto with *. try exact H7. unfold Zq_inv in |- *. inversion H5. assert (((x mod Z_of_nat q) ^ (Z_of_nat q - 1))%Z = (1 + x1 * Z_of_nat q)%Z). auto with *. cut (((x mod Z_of_nat q) ^ 1)%Z = (x mod Z_of_nat q)%Z). intros. pattern (x mod Z_of_nat q)%Z at 2 in |- *. rewrite <- H8. assert (((x mod Z_of_nat q) ^ (Z_of_nat q - 2 + 1))%Z = ((x mod Z_of_nat q) ^ (Z_of_nat q - 2) * (x mod Z_of_nat q) ^ 1)%Z). apply Zpower_exp. auto with *. assert (Z_of_nat q > 1)%Z. apply Q. assert (Z_of_nat q >= 2)%Z. auto with *. auto with *. auto with *. assert ((Z_of_nat q - 2 + 1)%Z = (Z_of_nat q - 1)%Z). auto with *. rewrite H10 in H9. rewrite <- H9. red in |- *. exists (x1 + x0 * (x mod Z_of_nat q) ^ (Z_of_nat q - 2))%Z. rewrite H7. assert ((1 + x1 * Z_of_nat q + (x mod Z_of_nat q) ^ (Z_of_nat q - 2) * (x0 * Z_of_nat q) - 1)%Z = (x1 * Z_of_nat q + (x mod Z_of_nat q) ^ (Z_of_nat q - 2) * (x0 * Z_of_nat q) + ( 1 - 1))%Z). auto with *. rewrite H11. simpl in |- *. assert (((x mod Z_of_nat q) ^ (Z_of_nat q - 2) * (x0 * Z_of_nat q))%Z = (x0 * Z_of_nat q * (x mod Z_of_nat q) ^ (Z_of_nat q - 2))%Z). auto with *. assert ((x0 * Z_of_nat q * (x mod Z_of_nat q) ^ (Z_of_nat q - 2))%Z = (x0 * (x mod Z_of_nat q) ^ (Z_of_nat q - 2) * Z_of_nat q)%Z). auto with *. rewrite H13 in H12. rewrite H12. assert ((x1 * Z_of_nat q + x0 * (x mod Z_of_nat q) ^ (Z_of_nat q - 2) * Z_of_nat q + 0)%Z = (x1 * Z_of_nat q + x0 * (x mod Z_of_nat q) ^ (Z_of_nat q - 2) * Z_of_nat q)%Z). auto with *. rewrite H14. auto with *. apply Zpow_id. Qed. Lemma Zq_plus_ass : forall a b c : Zq, mod_ (Z_of_nat q) (a + b + c) (a + (b + c)). intros. red in |- *. exists 0%Z. assert ((a + b + c)%Z = (a + (b + c))%Z). auto with *. simpl in |- *. rewrite H. auto with *. Qed. Lemma Zq_plus_unit : forall x : Zq, mod_ (Z_of_nat q) (x + 0) x. intros. red in |- *. exists 0%Z. auto with *. Qed. Lemma Zq_plus_inv : forall x : Zq, mod_ (Z_of_nat q) (x + - x) 0. intros. red in |- *. exists 0%Z. simpl in |- *. auto with *. Qed. Lemma Zq_mult_one : forall x : Zq, mod_ (Z_of_nat q) (x * 1) x. intros. red in |- *. exists 0%Z. simpl in |- *. auto with *. Qed. Require Export Ring_util. Lemma Zq_plus_opp : forall a b : Zq, mod_ (Z_of_nat q) a b -> mod_ (Z_of_nat q) (- a) (- b). intros. inversion H. red in |- *. exists (- x)%Z. assert ((- a - - b)%Z = (b - a)%Z). auto with *. rewrite H1. assert ((- x * Z_of_nat q)%Z = (- (x * Z_of_nat q))%Z). apply Zopp_mult_distr_l_reverse. rewrite H2. auto with *. Qed. Lemma Zq_plus_sym : forall a b : Zq, mod_ (Z_of_nat q) (a + b) (b + a). intros. red in |- *. exists 0%Z. simpl in |- *. auto with *. Qed. Lemma Zqmult_Zqplus : forall a b c : Zq, mod_ (Z_of_nat q) (a * (b + c)) (a * b + a * c). intros. red in |- *. exists 0%Z. simpl in |- *. assert ((a * (b + c))%Z = (a * b + a * c)%Z). auto with *. rewrite H. auto with *. Qed. Lemma Zqplus_Zqmult : forall a b c : Zq, mod_ (Z_of_nat q) ((a + b) * c) (a * c + b * c). intros. exists 0%Z. simpl in |- *. assert (((a + b) * c)%Z = (a * c + b * c)%Z). auto with *. rewrite H. auto with *. Qed. (*Zq sees like a ring *) Definition Zq_ring : RING. apply (BUILD_RING (E:=Zq) (ringplus:=Zplus) (ringmult:=Zmult) (zero:=0%Z) (un:=1%Z) (ringopp:=Zopp)). simpl in |- *. apply Zq_plus_eq. apply Zq_plus_ass. apply Zq_plus_unit. apply Zq_plus_opp. apply Zq_plus_inv. apply Zq_plus_sym. apply Zq_mult_eq. assert (forall x y z : Zq, Equal (s:=Zq) (x * (y * z))%Z (x * y * z)%Z). apply Zq_mult_ass. auto with *. apply Zq_mult_one. intros. exists 0%Z. auto with *. apply Zqmult_Zqplus. apply Zqplus_Zqmult. Defined. Lemma Zqmult_com : forall a b : Zq, mod_ (Z_of_nat q) (a * b) (b * a). intros. exists 0%Z. simpl in |- *. assert ((a * b)%Z = (b * a)%Z). auto with *. rewrite H. auto with *. Qed. (*Zq sees like a commutative ring *) Definition Zq_cring : CRING. apply (Build_cring (cring_ring:=Zq_ring)). apply (Build_cring_on (R:=Zq_ring)). red in |- *. simpl in |- *. apply Zqmult_com. Defined. Lemma mod_Zmod : forall a b : Zq, (a mod Z_of_nat q)%Z = (b mod Z_of_nat q)%Z -> mod_ (Z_of_nat q) a b. intros. assert ((a:Z) = (Z_of_nat q * (a / Z_of_nat q) + a mod Z_of_nat q)%Z). apply Z_div_mod_eq. assert (Z_of_nat q > 1)%Z. apply Q. auto with *. red in |- *. assert ((b:Z) = (Z_of_nat q * (b / Z_of_nat q) + b mod Z_of_nat q)%Z). apply Z_div_mod_eq. assert (Z_of_nat q > 1)%Z. apply Q. auto with *. exists (a / Z_of_nat q - b / Z_of_nat q)%Z. pattern a at 1 in |- *. rewrite H0. pattern b at 1 in |- *. rewrite H1. rewrite H. assert ((Z_of_nat q * (a / Z_of_nat q) + b mod Z_of_nat q - (Z_of_nat q * (b / Z_of_nat q) + b mod Z_of_nat q))%Z = (Z_of_nat q * (a / Z_of_nat q) - Z_of_nat q * (b / Z_of_nat q) + b mod Z_of_nat q - b mod Z_of_nat q)%Z). auto with *. rewrite H2. assert ((Z_of_nat q * (a / Z_of_nat q) - Z_of_nat q * (b / Z_of_nat q) + b mod Z_of_nat q - b mod Z_of_nat q)%Z = (Z_of_nat q * (a / Z_of_nat q) - Z_of_nat q * (b / Z_of_nat q))%Z). auto with *. rewrite H3. assert (((a / Z_of_nat q - b / Z_of_nat q) * Z_of_nat q)%Z = (Z_of_nat q * (a / Z_of_nat q - b / Z_of_nat q))%Z). auto with *. rewrite H4. assert ((Z_of_nat q * (a / Z_of_nat q - b / Z_of_nat q))%Z = (Z_of_nat q * (a / Z_of_nat q) - Z_of_nat q * (b / Z_of_nat q))%Z). apply Zmult_minus_distr_l. rewrite H5. auto with *. Qed. Hypothesis rest_0 : forall a b c : Zq, (- Z_of_nat q < c)%Z /\ (c < Z_of_nat q)%Z -> (Z_of_nat q * b + c)%Z = (Z_of_nat q * a)%Z :>Z -> c = 0%Z :>Z. Lemma Zmod_eq : forall a b : Zq, mod_ (Z_of_nat q) a b -> (a mod Z_of_nat q)%Z = (b mod Z_of_nat q)%Z. intros. assert ((a:Z) = (Z_of_nat q * (a / Z_of_nat q) + a mod Z_of_nat q)%Z). apply Z_div_mod_eq. assert (Z_of_nat q > 1)%Z. apply Q. auto with *. assert ((b:Z) = (Z_of_nat q * (b / Z_of_nat q) + b mod Z_of_nat q)%Z). apply Z_div_mod_eq. assert (Z_of_nat q > 1)%Z. apply Q. auto with *. inversion H. rewrite H1 in H2. rewrite H0 in H2. assert ((Z_of_nat q * (a / Z_of_nat q) + a mod Z_of_nat q - (Z_of_nat q * (b / Z_of_nat q) + b mod Z_of_nat q))%Z = (Z_of_nat q * (a / Z_of_nat q) - Z_of_nat q * (b / Z_of_nat q) + a mod Z_of_nat q - b mod Z_of_nat q)%Z). auto with *. rewrite H3 in H2. assert ((Z_of_nat q * (a / Z_of_nat q - b / Z_of_nat q))%Z = (Z_of_nat q * (a / Z_of_nat q) - Z_of_nat q * (b / Z_of_nat q))%Z). apply Zmult_minus_distr_l. rewrite <- H4 in H2. assert ((- Z_of_nat q < a mod Z_of_nat q - b mod Z_of_nat q)%Z /\ (a mod Z_of_nat q - b mod Z_of_nat q < Z_of_nat q)%Z). assert ((0 <= a mod Z_of_nat q)%Z /\ (a mod Z_of_nat q < Z_of_nat q)%Z). apply Z_mod_lt. assert (Z_of_nat q > 1)%Z. apply Q. auto with *. assert ((0 <= b mod Z_of_nat q)%Z /\ (b mod Z_of_nat q < Z_of_nat q)%Z). apply Z_mod_lt. assert (Z_of_nat q > 1)%Z. apply Q. auto with *. auto with *. cut ((a mod Z_of_nat q - b mod Z_of_nat q)%Z = 0%Z). intros. auto with *. assert ((x * Z_of_nat q)%Z = (Z_of_nat q * x)%Z). auto with *. rewrite H6 in H2. apply rest_0 with (a := x) (b := (a / Z_of_nat q - b / Z_of_nat q)%Z). try exact H5. assert ((Z_of_nat q * (a / Z_of_nat q - b / Z_of_nat q) + a mod Z_of_nat q - b mod Z_of_nat q)%Z = (Z_of_nat q * (a / Z_of_nat q - b / Z_of_nat q) + (a mod Z_of_nat q - b mod Z_of_nat q))%Z). auto with *. rewrite H7 in H2. auto with *. Qed. Lemma Zq_inv_eq : forall a b : Zq, mod_ (Z_of_nat q) a b -> mod_ (Z_of_nat q) (Zq_inv a) (Zq_inv b). intros. unfold Zq_inv in |- *. inversion H. assert ((a:Z) = (b + x * Z_of_nat q)%Z). auto with *. cut ((a mod Z_of_nat q)%Z = (b mod Z_of_nat q)%Z). intros. rewrite H2. red in |- *. exists 0%Z. auto with *. rewrite H1. assert (mod_ (Z_of_nat q) b (b + x * Z_of_nat q)). apply mod_eq. apply Zmod_eq. apply mod_sym. try exact H2. Qed. Definition Zqinv : MAP Zq_cring Zq_cring. apply (Build_Map (A:=Zq_cring) (B:=Zq_cring) (Ap:=Zq_inv)). red in |- *. simpl in |- *. apply Zq_inv_eq. Defined. Lemma plus_0 : forall a b : nat, a + b = 1 -> a = 0 \/ a = 1. intros. omega. Qed. Lemma mult_eq_1 : forall a b : nat, a * b = 1 :>nat -> b = 1 :>nat. intros. induction a as [| a Hreca]; simpl in |- *. omega. simpl in H. cut (b = 0 \/ b = 1). intros. elim H0; [ intros H1; try clear H0 | intros H1; try clear H0; try exact H1 ]. rewrite H1 in H. omega. apply plus_0 with (b := a * b). try exact H. Qed. Lemma Z_nat : forall a b : Z, a = b -> Zabs_nat a = Zabs_nat b. intros. rewrite H. auto with *. Qed. Hypothesis mult_abs : forall a b : Z, Zabs_nat (a * b) = Zabs_nat a * Zabs_nat b. Hypothesis Zgt_gt : forall a : Z, (a > 1)%Z -> Zabs_nat a > 1. Lemma diff0 : ~ mod_ (Z_of_nat q) 1 0. red in |- *. intros. inversion H. assert (Z_of_nat q > 1)%Z. apply Q. simpl in H0. assert (Zabs_nat 1 = Zabs_nat (x * Z_of_nat q)). apply Z_nat. try exact H0. assert (Zabs_nat (x * Z_of_nat q) = Zabs_nat x * Zabs_nat (Z_of_nat q)). apply mult_abs. assert (Zabs_nat (Z_of_nat q) = 1). rewrite H3 in H2. assert (Zabs_nat x * Zabs_nat (Z_of_nat q) = Zabs_nat 1). auto with *. apply mult_eq_1 with (a := Zabs_nat x). auto with *. assert (Zabs_nat (Z_of_nat q) > 1). apply Zgt_gt. try exact H1. auto with *. Qed. Let Zq_field_on : field_on Zq_cring. apply (Build_field_on (R:=Zq_cring) (field_inverse_map:=Zqinv)). apply Zq_mult_inv_r. apply Zq_mult_inv_l. simpl in |- *. apply diff0. Qed. (*Zq sees like a commutative field *) Definition Zq_cfield := Build_cfield Zq_field_on. End Zq.