diff options
Diffstat (limited to 'src/ModularArithmetic/ModularArithmeticTheorems.v')
| -rw-r--r-- | src/ModularArithmetic/ModularArithmeticTheorems.v | 1037 |
1 files changed, 324 insertions, 713 deletions
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index be9307b50..e36d15c8b 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -2,54 +2,20 @@ Require Import Coq.omega.Omega. Require Import Crypto.Spec.ModularArithmetic. Require Import Crypto.ModularArithmetic.Pre. -Require Import Coq.Logic.Eqdep_dec. -Require Import Crypto.Tactics.VerdiTactics. Require Import Coq.ZArith.BinInt Coq.ZArith.Zdiv Coq.ZArith.Znumtheory Coq.NArith.NArith. (* import Zdiv before Znumtheory *) Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid. -Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Field_theory Coq.setoid_ring.Field_tac. -Require Export Crypto.Util.IterAssocOp. +Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Ring_tac. +Require Import Crypto.Algebra Crypto.Util.Decidable. Require Export Crypto.Util.FixCoqMistakes. -Section ModularArithmeticPreliminaries. - Context {m:Z}. - Let ZToFm := ZToField : BinNums.Z -> F m. Hint Unfold ZToFm. Local Coercion ZToFm : Z >-> F. - - Theorem F_eq: forall (x y : F m), x = y <-> FieldToZ x = FieldToZ y. - Proof. - destruct x, y; intuition; simpl in *; try congruence. - subst_max. - f_equal. - eapply UIP_dec, Z.eq_dec. - Qed. - - Lemma F_pow_spec : forall (a:F m), - pow a 0%N = 1%F /\ forall x, pow a (1 + x)%N = mul a (pow a x). - Proof. - intros a. - pose (@pow_with_spec m) as H. - change (@pow m) with (proj1_sig H). - destruct H; eauto. - Qed. -End ModularArithmeticPreliminaries. - (* Fails iff the input term does some arithmetic with mod'd values. *) Ltac notFancy E := -match E with -| - (_ mod _) => idtac -| context[_ mod _] => fail 1 -| _ => idtac -end. - -Lemma Zplus_neg : forall n m, n + -m = n - m. -Proof. - auto. -Qed. - -Lemma Zmod_eq : forall a b n, a = b -> a mod n = b mod n. -Proof. - intros; rewrite H; trivial. -Qed. + match E with + | - (_ mod _) => idtac + | context[_ mod _] => fail 1 + | _ => idtac + end. (* Remove redundant [mod] operations from the conclusion. *) Ltac demod := @@ -68,680 +34,325 @@ Ltac demod := notFancy y; rewrite (Zmult_mod_idemp_r y) | [ |- context[(?x mod _) mod _] ] => notFancy x; rewrite (Zmod_mod x) - | _ => rewrite Zplus_neg in * || rewrite Z.sub_diag in * end. -(* Remove exists under equals: we do this a lot *) -Ltac eq_remove_proofs := lazymatch goal with -| [ |- @eq (F _) ?a ?b ] => - assert (Q := F_eq a b); - simpl in *; apply Q; clear Q -end. - -(** TODO FIXME(from jgross): This tactic is way too powerful for - arcane reasons. It should not be using so many databases with - [intuition]. *) -Ltac Fdefn := +Ltac unwrap_F := intros; repeat match goal with [ x : F _ |- _ ] => destruct x end; - try eq_remove_proofs; - demod; - rewrite ?Z.mul_1_l; - intuition auto with zarith lia relations typeclass_instances; demod; try solve [ f_equal; intuition auto with zarith lia relations typeclass_instances ]. - -Local Open Scope F_scope. - -Section FEquality. - Context {m:Z}. - - (** Equality **) - Definition F_eqb (x y : F m) : bool := Z.eqb x y. - - Lemma F_eqb_eq x y : F_eqb x y = true -> x = y. - Proof. - unfold F_eqb; Fdefn; apply Z.eqb_eq; trivial. - Qed. - - Lemma F_eqb_complete : forall x y: F m, x = y -> F_eqb x y = true. - Proof. - intros; subst; apply Z.eqb_refl. - Qed. - - Lemma F_eqb_refl : forall x, F_eqb x x = true. - Proof. - intros; apply F_eqb_complete; trivial. - Qed. - - Lemma F_eqb_neq x y : F_eqb x y = false -> x <> y. - Proof. - intuition; subst y. - pose proof (F_eqb_refl x). - congruence. - Qed. - - Lemma F_eqb_neq_complete x y : x <> y -> F_eqb x y = false. - Proof. - intros. - case_eq (F_eqb x y); intros; trivial. - pose proof (F_eqb_eq x y); intuition. - Qed. - - Lemma F_eq_dec : forall x y : F m, {x = y} + {x <> y}. - Proof. - intros; case_eq (F_eqb x y); [left|right]; auto using F_eqb_eq, F_eqb_neq. - Qed. - - Lemma if_F_eq_dec_if_F_eqb : forall {T} x y (a b:T), (if F_eq_dec x y then a else b) = (if F_eqb x y then a else b). - Proof. - intros; intuition; break_if. - - rewrite F_eqb_complete; trivial. - - rewrite F_eqb_neq_complete; trivial. - Defined. -End FEquality. - -Section FandZ. - Context {m:Z}. - - Lemma ZToField_small_nonzero : forall z, (0 < z < m)%Z -> ZToField z <> (0:F m). - Proof. - intuition; find_inversion; rewrite ?Z.mod_0_l, ?Z.mod_small in *; intuition auto with zarith. - Qed. - - Require Crypto.Algebra. - Global Instance commutative_ring_modulo : @Algebra.commutative_ring (F m) Logic.eq (ZToField 0) (ZToField 1) opp add sub mul. - Proof. - repeat split; Fdefn; try apply F_eq_dec. - { rewrite Z.add_0_r. auto. } - { rewrite Z.mul_1_r. auto. } - Qed. - - Lemma F_opp_spec : forall (a:F m), add a (opp a) = 0. - Fdefn. - Qed. - - Lemma ZToField_0 : @ZToField m 0 = 0. - Proof. - Fdefn. - Qed. - - Lemma FieldToZ_ZToField : forall z, FieldToZ (@ZToField m z) = z mod m. - Proof. - Fdefn. - Qed. - - Lemma mod_FieldToZ : forall x, (@FieldToZ m x) mod m = FieldToZ x. - Proof. - Fdefn. - Qed. - - (** ZToField distributes over operations **) - Lemma ZToField_add : forall (x y : Z), - @ZToField m (x + y) = ZToField x + ZToField y. - Proof. - Fdefn. - Qed. - - Lemma FieldToZ_add : forall x y : F m, - FieldToZ (x + y) = ((FieldToZ x + FieldToZ y) mod m)%Z. - Proof. - Fdefn. - Qed. - - Lemma FieldToZ_mul : forall x y : F m, - FieldToZ (x * y) = ((FieldToZ x * FieldToZ y) mod m)%Z. - Proof. - Fdefn. - Qed. - - Lemma FieldToZ_pow_Zpow_mod : forall (x : F m) n, - (FieldToZ x ^ Z.of_N n mod m = FieldToZ (x ^ n)%F)%Z. - Proof. - intros. - induction n using N.peano_ind; - destruct (F_pow_spec x) as [pow_0 pow_succ] . { - rewrite pow_0. - rewrite Z.pow_0_r; auto. - } { - rewrite N2Z.inj_succ. - rewrite Z.pow_succ_r by apply N2Z.is_nonneg. - rewrite <- N.add_1_l. - rewrite pow_succ. - rewrite <- Zmult_mod_idemp_r. - rewrite IHn. - apply FieldToZ_mul. - } - Qed. - - Lemma FieldToZ_pow_efficient : forall (x : F m) n, FieldToZ (x^n) = powmod m (FieldToZ x) n. - Proof. - intros. - rewrite powmod_Zpow_mod. - rewrite <-FieldToZ_pow_Zpow_mod. - reflexivity. - Qed. - - Lemma pow_nat_iter_op_correct: forall (x:F m) n, (@nat_iter_op _ mul 1) (N.to_nat n) x = x^n. - Proof. - induction n using N.peano_ind; - destruct (F_pow_spec x) as [pow_0 pow_succ]; - rewrite ?N2Nat.inj_succ, ?pow_0, <-?N.add_1_l, ?pow_succ; - simpl; congruence. - Qed. - - Lemma mod_plus_zero_subproof a b : 0 mod m = (a + b) mod m -> - b mod m = (- a) mod m. - Proof. - rewrite <-Z.sub_0_l; intros. - replace (0-a)%Z with (b-(a + b))%Z by omega. - rewrite Zminus_mod. - rewrite <- H. - rewrite Zmod_0_l. - replace (b mod m - 0)%Z with (b mod m) by omega. - rewrite Zmod_mod. - reflexivity. - Qed. - - Lemma FieldToZ_opp' : forall x, FieldToZ (@opp m x) mod m = -x mod m. - Proof. - intros. - pose proof (FieldToZ_add x (opp x)) as H. - rewrite F_opp_spec, FieldToZ_ZToField in H. - auto using mod_plus_zero_subproof. - Qed. - - Lemma FieldToZ_opp : forall x, FieldToZ (@opp m x) = -x mod m. - Proof. - intros. - pose proof (FieldToZ_opp' x) as H; rewrite mod_FieldToZ in H; trivial. - Qed. - - Lemma sub_intersperse_modulus : forall x y, ((x - y) mod m = (x + (m - y)) mod m)%Z. - Proof. - intros. - replace (x + (m - y))%Z with (m+(x-y))%Z by omega. - rewrite Zplus_mod. - rewrite Z_mod_same_full; simpl Z.add. - rewrite Zmod_mod. - reflexivity. - Qed. - - (* Compatibility between inject and subtraction *) - Lemma ZToField_sub : forall (x y : Z), - @ZToField m (x - y) = ZToField x - ZToField y. - Proof. - Fdefn. - Qed. - - (* Compatibility between inject and multiplication *) - Lemma ZToField_mul : forall (x y : Z), - @ZToField m (x * y) = ZToField x * ZToField y. - Proof. - Fdefn. - Qed. - - (* Compatibility between inject and GFtoZ *) - Lemma ZToField_idempotent : forall (x : F m), ZToField x = x. - Proof. - Fdefn. - Qed. - Definition ZToField_FieldToZ := ZToField_idempotent. (* alias *) - - (* Compatibility between inject and mod *) - Lemma ZToField_mod : forall x, @ZToField m x = ZToField (x mod m). - Proof. - Fdefn. - Qed. - - (* Compatibility between inject and pow *) - Lemma ZToField_pow : forall x n, - @ZToField m x ^ n = ZToField (x ^ (Z.of_N n) mod m). - Proof. - intros. - induction n using N.peano_ind; - destruct (F_pow_spec (@ZToField m x)) as [pow_0 pow_succ] . { - rewrite pow_0. - Fdefn. - } { - rewrite N2Z.inj_succ. - rewrite Z.pow_succ_r by apply N2Z.is_nonneg. - rewrite <- N.add_1_l. - rewrite pow_succ. - rewrite IHn. - Fdefn. - } - Qed. - - Lemma ZToField_eqmod : forall x y : Z, x mod m = y mod m -> ZToField x = @ZToField m y. - Fdefn. - Qed. - - Lemma FieldToZ_nonzero: - forall x0 : F m, x0 <> 0 -> FieldToZ x0 <> 0%Z. - Proof. - intros x0 Hnz Hz. - rewrite <- Hz, ZToField_FieldToZ in Hnz; auto. - Qed. - -End FandZ. - -Section RingModuloPre. - Context {m:Z}. - Let ZToFm := ZToField : Z -> F m. Hint Unfold ZToFm. Local Coercion ZToFm : Z >-> F. - (* Substitution to prove all Compats *) - Ltac compat := repeat intro; subst; trivial. - - Instance Fplus_compat : Proper (eq==>eq==>eq) (@add m). - Proof. - compat. - Qed. - - Instance Fminus_compat : Proper (eq==>eq==>eq) (@sub m). - Proof. - compat. - Qed. - - Instance Fmult_compat : Proper (eq==>eq==>eq) (@mul m). - Proof. - compat. - Qed. - - Instance Fopp_compat : Proper (eq==>eq) (@opp m). - Proof. - compat. - Qed. - - Instance Finv_compat : Proper (eq==>eq) (@inv m). - Proof. - compat. - Qed. - - Instance Fdiv_compat : Proper (eq==>eq==>eq) (@div m). - Proof. - compat. - Qed. - - (***** Ring Theory *****) - Definition Fring_theory : ring_theory 0%F 1%F (@add m) (@mul m) (@sub m) (@opp m) eq. - Proof. - constructor; Fdefn. - Qed. - - Lemma F_mul_1_r: - forall x : F m, x * 1 = x. - Proof. - Fdefn; rewrite Z.mul_1_r; auto. - Qed. - - Lemma F_mul_assoc: - forall x y z : F m, x * (y * z) = x * y * z. - Proof. - Fdefn. - Qed. - - Lemma F_pow_pow_N (x : F m) : forall (n : N), (x ^ id n)%F = pow_N 1%F mul x n. - Proof. - destruct (F_pow_spec x) as [HO HS]; intros. - destruct n; auto; unfold id. - rewrite Pre.N_pos_1plus at 1. - rewrite HS. - simpl. - induction p using Pos.peano_ind. - - simpl. rewrite HO; apply F_mul_1_r. - - rewrite (@pow_pos_succ (F m) (@mul m) eq _ _ F_mul_assoc x). - rewrite <-IHp, Pos.pred_N_succ, Pre.N_pos_1plus, HS. - f_equal. - Qed. - - (***** Power theory *****) - Lemma Fpower_theory : power_theory 1%F (@mul m) eq id (@pow m). - Proof. - constructor; apply F_pow_pow_N. - Qed. - - (***** Division Theory *****) - Definition Fquotrem(a b: F m): F m * F m := - let '(q, r) := (Z.quotrem a b) in (q : F m, r : F m). - Lemma Fdiv_theory : div_theory eq (@add m) (@mul m) (@id _) Fquotrem. - Proof. - constructor; intros; unfold Fquotrem, id. - - replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b) by - try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial). - - Fdefn; rewrite <-Z.quot_rem'; trivial. - Qed. - - Lemma Z_mul_mod_modulus_r : forall x m, ((x*m) mod m = 0)%Z. - intros. - rewrite Zmult_mod, Z_mod_same_full. - rewrite Z.mul_0_r, Zmod_0_l. - reflexivity. - Qed. - - Lemma Z_mod_opp_equiv : forall x y m, x mod m = (-y) mod m -> - (-x) mod m = y mod m. - Proof. - intros. - rewrite <-Z.sub_0_l. - rewrite Zminus_mod. rewrite H. - rewrite ?Zminus_mod_idemp_l, ?Zminus_mod_idemp_r; f_equal. - destruct y; auto. - Qed. - - Lemma Z_opp_opp : forall x : Z, (-(-x)) = x. - destruct x; auto. - Qed. - - Lemma Z_mod_opp : forall x m, (- x) mod m = (- (x mod m)) mod m. - intros. - apply Z_mod_opp_equiv. - rewrite Z_opp_opp. - demod; auto. - Qed. - - (* Define a "ring morphism" between GF and Z, i.e. an equivalence - * between 'inject (ZFunction (X))' and 'GFFunction (inject (X))'. - * - * Doing this allows us to do our coefficient manipulations in Z - * rather than GF, because we know it's equivalent to inject the - * result afterward. - *) - Lemma Fring_morph: - ring_morph 0%F 1%F (@add m) (@mul m) (@sub m) (@opp m) eq - 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Z.eqb - (@ZToField m). - Proof. - constructor; intros; try Fdefn; unfold id; - try (apply gf_eq; simpl; intuition). - - apply Z_mod_opp_equiv; rewrite Z_opp_opp, Zmod_mod; reflexivity. - - rewrite (proj1 (Z.eqb_eq x y)); trivial. - Qed. - - (* Redefine our division theory under the ring morphism *) - Lemma Fmorph_div_theory: + lazy iota beta delta [add sub mul opp FieldToZ ZToField proj1_sig] in *; + try apply eqsig_eq; + demod. + +Global Instance eq_dec {m} : DecidableRel (@eq (F m)). exact _. Defined. + +Global Instance commutative_ring_modulo m + : @Algebra.commutative_ring (F m) Logic.eq 0%F 1%F opp add sub mul. +Proof. + repeat (split || intro); unwrap_F; + autorewrite with zsimplify; solve [ exact _ | auto with zarith | congruence]. +Qed. + + +Module Zmod. + Lemma pow_spec {m} a : pow a 0%N = 1%F :> F m /\ forall x, pow a (1 + x)%N = mul a (pow a x). + Proof. change (@pow m) with (proj1_sig (@pow_with_spec m)); destruct (@pow_with_spec m); eauto. Qed. + + Section FandZ. + Context {m:Z}. + Local Open Scope F_scope. + + Theorem eq_FieldToZ_iff (x y : F m) : x = y <-> FieldToZ x = FieldToZ y. + Proof. destruct x, y; intuition; simpl in *; try apply (eqsig_eq _ _); congruence. Qed. + + Lemma eq_ZToField_iff : forall x y : Z, x mod m = y mod m <-> ZToField m x = ZToField m y. + Proof. split; unwrap_F; congruence. Qed. + + + Lemma FieldToZ_ZToField : forall z, FieldToZ (@ZToField m z) = z mod m. + Proof. unwrap_F; trivial. Qed. + + Lemma ZToField_FieldToZ x : ZToField m (FieldToZ x) = x :> F m. + Proof. unwrap_F; congruence. Qed. + + + Lemma ZToField_mod : forall x, ZToField m x = ZToField m (x mod m). + Proof. unwrap_F; trivial. Qed. + + Lemma mod_FieldToZ : forall (x:F m), FieldToZ x mod m = FieldToZ x. + Proof. unwrap_F. congruence. Qed. + + Lemma FieldToZ_0 : FieldToZ (0:F m) = 0%Z. + Proof. unwrap_F. apply Zmod_0_l. Qed. + + Lemma ZToField_small_nonzero z : (0 < z < m)%Z -> ZToField m z <> 0. + Proof. intros Hrange Hnz. inversion Hnz. rewrite Zmod_small, Zmod_0_l in *; omega. Qed. + + Lemma FieldToZ_nonzero (x:F m) : x <> 0 -> FieldToZ x <> 0%Z. + Proof. intros Hnz Hz. rewrite <- Hz, ZToField_FieldToZ in Hnz; auto. Qed. + + Lemma FieldToZ_range (x : F m) : 0 < m -> 0 <= x < m. + Proof. intros. rewrite <- mod_FieldToZ. apply Z.mod_pos_bound. trivial. Qed. + + Lemma FieldToZ_nonzero_range (x : F m) : (x <> 0) -> 0 < m -> (1 <= x < m)%Z. + Proof. + unfold not; intros Hnz Hlt. + rewrite eq_FieldToZ_iff, FieldToZ_0 in Hnz; pose proof (FieldToZ_range x Hlt). + omega. + Qed. + + Lemma ZToField_add : forall (x y : Z), + ZToField m (x + y) = ZToField m x + ZToField m y. + Proof. unwrap_F; trivial. Qed. + + Lemma FieldToZ_add : forall x y : F m, + FieldToZ (x + y) = ((FieldToZ x + FieldToZ y) mod m)%Z. + Proof. unwrap_F; trivial. Qed. + + Lemma ZToField_mul x y : ZToField m (x * y) = ZToField _ x * ZToField _ y :> F m. + Proof. unwrap_F. trivial. Qed. + + Lemma FieldToZ_mul : forall x y : F m, + FieldToZ (x * y) = ((FieldToZ x * FieldToZ y) mod m)%Z. + Proof. unwrap_F; trivial. Qed. + + Lemma ZToField_sub x y : ZToField _ (x - y) = ZToField _ x - ZToField _ y :> F m. + Proof. unwrap_F. trivial. Qed. + + Lemma FieldToZ_opp : forall x, FieldToZ (@opp m x) = -x mod m. + Proof. unwrap_F; trivial. Qed. + + Lemma ZToField_pow x n : ZToField _ x ^ n = ZToField _ (x ^ (Z.of_N n) mod m) :> F m. + Proof. + intros. + induction n using N.peano_ind; + destruct (pow_spec (@ZToField m x)) as [pow_0 pow_succ] . { + rewrite pow_0. + unwrap_F; trivial. + } { + rewrite N2Z.inj_succ. + rewrite Z.pow_succ_r by apply N2Z.is_nonneg. + rewrite <- N.add_1_l. + rewrite pow_succ. + rewrite IHn. + unwrap_F; trivial. + } + Qed. + + Lemma FieldToZ_pow : forall (x : F m) n, + FieldToZ (x ^ n)%F = (FieldToZ x ^ Z.of_N n mod m)%Z. + Proof. + intros. + symmetry. + induction n using N.peano_ind; + destruct (pow_spec x) as [pow_0 pow_succ] . { + rewrite pow_0, Z.pow_0_r; auto. + } { + rewrite N2Z.inj_succ. + rewrite Z.pow_succ_r by apply N2Z.is_nonneg. + rewrite <- N.add_1_l. + rewrite pow_succ. + rewrite <- Zmult_mod_idemp_r. + rewrite IHn. + apply FieldToZ_mul. + } + Qed. + + Lemma square_iff (x:F m) : + (exists y : F m, y * y = x) <-> (exists y : Z, y * y mod m = x)%Z. + Proof. + setoid_rewrite eq_FieldToZ_iff; setoid_rewrite FieldToZ_mul; split; intro H; destruct H as [x' H]. + - eauto. + - exists (ZToField _ x'); rewrite !FieldToZ_ZToField; demod; auto. + Qed. + + (* TODO: move to ZUtil *) + Lemma sub_intersperse_modulus : forall x y, ((x - y) mod m = (x + (m - y)) mod m)%Z. + Proof. + intros. + replace (x + (m - y))%Z with (m+(x-y))%Z by omega. + rewrite Zplus_mod. + rewrite Z_mod_same_full; simpl Z.add. + rewrite Zmod_mod. + reflexivity. + Qed. + End FandZ. + + Section RingTacticGadgets. + Context (m:Z). + + Definition ring_theory : ring_theory 0%F 1%F (@add m) (@mul m) (@sub m) (@opp m) eq + := Algebra.Ring.ring_theory_for_stdlib_tactic. + + Lemma pow_pow_N (x : F m) : forall (n : N), (x ^ id n)%F = pow_N 1%F mul x n. + Proof. + destruct (pow_spec x) as [HO HS]; intros. + destruct n; auto; unfold id. + rewrite Pre.N_pos_1plus at 1. + rewrite HS. + simpl. + induction p using Pos.peano_ind. + - simpl. rewrite HO. apply Algebra.right_identity. + - rewrite (@pow_pos_succ (F m) (@mul m) eq _ _ associative x). + rewrite <-IHp, Pos.pred_N_succ, Pre.N_pos_1plus, HS. + trivial. + Qed. + + Lemma power_theory : power_theory 1%F (@mul m) eq id (@pow m). + Proof. split; apply pow_pow_N. Qed. + + (***** Division Theory *****) + Definition quotrem(a b: F m): F m * F m := + let '(q, r) := (Z.quotrem a b) in (ZToField _ q , ZToField _ r). + Lemma Fdiv_theory : div_theory eq (@add m) (@mul m) (@id _) quotrem. + Proof. + constructor; intros; unfold quotrem, id. + + replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b) by + try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial). + + unwrap_F; rewrite <-Z.quot_rem'; trivial. + Qed. + + Lemma Z_mod_opp_equiv : forall x y m, x mod m = (-y) mod m -> + (-x) mod m = y mod m. + Proof. + intros. + rewrite <-Z.sub_0_l. + rewrite Zminus_mod. rewrite H. + rewrite ?Zminus_mod_idemp_l, ?Zminus_mod_idemp_r; f_equal. + destruct y; auto. + Qed. + + Lemma Z_opp_opp : forall x : Z, (-(-x)) = x. + destruct x; auto. + Qed. + + Lemma Z_mod_opp : forall x m, (- x) mod m = (- (x mod m)) mod m. + intros. + apply Z_mod_opp_equiv. + rewrite Z_opp_opp. + demod; auto. + Qed. + + (* Define a "ring morphism" between GF and Z, i.e. an equivalence + * between 'inject (ZFunction (X))' and 'GFFunction (inject (X))'. + * + * Doing this allows the [ring] tactic to do coefficient + * manipulations in Z rather than F, because we know it's equivalent + * to inject the result afterward. *) + Lemma ring_morph: ring_morph 0%F 1%F (@add m) (@mul m) (@sub m) (@opp m) eq + 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Z.eqb (@ZToField m). + Proof. split; intros; unwrap_F; solve [ auto | rewrite (proj1 (Z.eqb_eq x y)); trivial]. Qed. + + (* Redefine our division theory under the ring morphism *) + Lemma morph_div_theory: div_theory eq Zplus Zmult (@ZToField m) Z.quotrem. - Proof. - constructor; intros; intuition. - replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b); - try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial). - - eq_remove_proofs; demod; - rewrite <- (Z.quot_rem' a b); - destruct a; simpl; trivial. - Qed. - - Lemma ZToField_1 : @ZToField m 1 = 1. - Proof. - Fdefn. - Qed. -End RingModuloPre. - -Ltac Fconstant t := match t with @ZToField _ ?x => x | _ => NotConstant end. -Ltac Fexp_tac t := Ncst t. -Ltac Fpreprocess := rewrite <-?ZToField_0, ?ZToField_1. -Ltac Fpostprocess := repeat split; - repeat match goal with [ |- context[exist ?a ?b (Pre.Z_mod_mod ?x ?q)] ] => - change (exist a b (Pre.Z_mod_mod x q)) with (@ZToField q x%Z) end; - rewrite ?ZToField_0, ?ZToField_1. - -Module Type Modulus. - Parameter modulus : Z. -End Modulus. - -(* Example of how to instantiate the ring tactic *) -Module RingModulo (Export M : Modulus). - Definition ring_theory_modulo := @Fring_theory modulus. - Definition ring_morph_modulo := @Fring_morph modulus. - Definition morph_div_theory_modulo := @Fmorph_div_theory modulus. - Definition power_theory_modulo := @Fpower_theory modulus. - - Add Ring GFring_Z : ring_theory_modulo - (morphism ring_morph_modulo, - constants [Fconstant], - div morph_div_theory_modulo, - power_tac power_theory_modulo [Fexp_tac]). -End RingModulo. - -Section VariousModulo. - Context {m:Z}. - - Add Ring GFring_Z : (@Fring_theory m) - (morphism (@Fring_morph m), - constants [Fconstant], - div (@Fmorph_div_theory m), - power_tac (@Fpower_theory m) [Fexp_tac]). - - Lemma F_mul_0_l : forall x : F m, 0 * x = 0. - Proof. - intros; ring. - Qed. - - Lemma F_mul_0_r : forall x : F m, x * 0 = 0. - Proof. - intros; ring. - Qed. - - Lemma F_mul_nonzero_l : forall a b : F m, a*b <> 0 -> a <> 0. - intros; intuition; subst. - assert (0 * b = 0) by ring; intuition. - Qed. - - Lemma F_mul_nonzero_r : forall a b : F m, a*b <> 0 -> b <> 0. - intros; intuition; subst. - assert (a * 0 = 0) by ring; intuition. - Qed. - - Lemma F_pow_distr_mul : forall (x y:F m) z, (0 <= z)%N -> - (x ^ z) * (y ^ z) = (x * y) ^ z. - Proof. - intros. - replace z with (Z.to_N (Z.of_N z)) by apply N2Z.id. - apply natlike_ind with (x := Z.of_N z); simpl; [ ring | | - replace 0%Z with (Z.of_N 0%N) by auto; apply N2Z.inj_le; auto]. - intros z' z'_nonneg IHz'. - rewrite Z2N.inj_succ by auto. - rewrite <-N.add_1_l. - rewrite !(proj2 (@F_pow_spec m _) _). - rewrite <- IHz'. - ring. - Qed. - - Lemma F_opp_0 : opp (0 : F m) = 0%F. - Proof. - intros; ring. - Qed. - - Lemma F_opp_swap : forall x y : F m, opp x = y <-> x = opp y. - Proof. - split; intro; subst; ring. - Qed. - - Lemma F_opp_involutive : forall x : F m, opp (opp x) = x. - Proof. - intros; ring. - Qed. - - Lemma F_square_opp : forall x : F m, (opp x ^ 2 = x ^ 2)%F. - Proof. - intros; ring. - Qed. - - Lemma F_mul_opp_r : forall x y : F m, (x * opp y = opp (x * y))%F. - intros; ring. - Qed. - - Lemma F_mul_opp_l : forall x y : F m, (opp x * y = opp (x * y))%F. - intros; ring. - Qed. - - Lemma F_mul_opp_both : forall x y : F m, (opp x * opp y = x * y)%F. - intros; ring. - Qed. - - Lemma F_add_0_r : forall x : F m, (x + 0)%F = x. - Proof. - intros; ring. - Qed. - - Lemma F_add_0_l : forall x : F m, (0 + x)%F = x. - Proof. - intros; ring. - Qed. - - Lemma F_add_reg_r : forall x y z : F m, y + x = z + x -> y = z. - Proof. - intros ? ? ? A. - replace y with (y + x - x) by ring. - rewrite A; ring. - Qed. - - Lemma F_add_reg_l : forall x y z : F m, x + y = x + z -> y = z. - Proof. - intros ? ? ? A. - replace y with (x + y - x) by ring. - rewrite A; ring. - Qed. - - Lemma F_sub_0_r : forall x : F m, (x - 0)%F = x. - Proof. - intros; ring. - Qed. - - Lemma F_sub_0_l : forall x : F m, (0 - x)%F = opp x. - Proof. - intros; ring. - Qed. - - Lemma F_mul_1_l : forall x : F m, (1 * x)%F = x. - Proof. - intros; ring. - Qed. - - Lemma F_ZToField_m : ZToField m = @ZToField m 0. - Proof. - Fdefn. - rewrite Zmod_0_l. - apply Z_mod_same_full. - Qed. - - Lemma F_sub_m_l : forall x : F m, opp x = ZToField m - x. - Proof. - rewrite F_ZToField_m. - symmetry. - apply F_sub_0_l. - Qed. - - Lemma opp_ZToField : forall x : Z, opp (ZToField x) = @ZToField m (m - x). - Proof. - Fdefn. - rewrite Zminus_mod, Z_mod_same_full, (Z.sub_0_l (x mod m)); reflexivity. - Qed. - - Lemma F_pow_2_r : forall x : F m, x^2 = x*x. - Proof. - intros. ring. - Qed. - - Lemma F_pow_3_r : forall x : F m, x^3 = x*x*x. - Proof. - intros. ring. - Qed. - - Lemma F_pow_add : forall (x : F m) k j, x ^ j * x ^ k = x ^ (j + k). - Proof. - intros. - destruct (F_pow_spec x) as [exp_zero exp_succ]. - induction j using N.peano_ind. - + rewrite exp_zero. - ring_simplify; eauto. - + - rewrite N.add_succ_l. - do 2 rewrite <- N.add_1_l. - do 2 rewrite exp_succ by apply N.neq_succ_0. - rewrite <- IHj. - ring. - Qed. - - Lemma F_pow_compose : forall (x : F m) k j, (x ^ j) ^ k = x ^ (k * j). - Proof. - intros. - induction k using N.peano_ind; [rewrite Nmult_0_l; ring | ]. - rewrite Nmult_Sn_m. - rewrite <- F_pow_add. - rewrite <- IHk. - rewrite <- N.add_1_l. - rewrite (proj2 (F_pow_spec _)). - ring. - Qed. - - Lemma F_sub_add_swap : forall w x y z : F m, w - x = y - z <-> w + z = y + x. - Proof. - split; intro A; - [ replace w with (w - x + x) by ring - | replace w with (w + z - z) by ring ]; rewrite A; ring. - Qed. - - Definition isSquare (x : F m) := exists sqrt_x, sqrt_x ^ 2 = x. - - Lemma square_Zmod_F : forall (a : F m), isSquare a <-> - (exists b : Z, ((b * b) mod m)%Z = a). - Proof. - split; intro A; destruct A as [sqrt_a sqrt_a_id]. { - exists sqrt_a. - rewrite <- FieldToZ_mul. - apply F_eq. - ring_simplify; auto. - } { - exists (ZToField sqrt_a). - rewrite ZToField_pow. - replace (Z.of_N 2) with 2%Z by auto. - rewrite Z.pow_2_r. - rewrite sqrt_a_id. - apply ZToField_FieldToZ. - } - Qed. - - Lemma FieldToZ_range : forall x : F m, 0 < m -> 0 <= x < m. - Proof. - intros. - rewrite <- mod_FieldToZ. - apply Z.mod_pos_bound. - omega. - Qed. - - Lemma FieldToZ_nonzero_range : forall x : F m, (x <> 0) -> 0 < m -> - (1 <= x < m)%Z. - Proof. - intros. - pose proof (FieldToZ_range x). - unfold not in *. - rewrite F_eq in H. - replace (FieldToZ 0) with 0%Z in H by auto. - omega. - Qed. - - Lemma F_mul_comm : forall x y : F m, x*y = y*x. - intros; ring. - Qed. - - Lemma Fq_sub_eq : forall x y a b : F m, a = b -> x-a = y-b -> x = y. - Proof. - intros x y a b Hab Hxayb; subst. - replace x with ((x - b) + b) by ring. - replace y with ((y - b) + b) by ring. - rewrite Hxayb; ring. - Qed. - - Lemma F_FieldToZ_add_opp : forall x : F m, x <> 0 -> (FieldToZ x + FieldToZ (opp x) = m)%Z. - Proof. - intros. - rewrite FieldToZ_opp. - rewrite Z_mod_nz_opp_full, mod_FieldToZ; try omega. - rewrite mod_FieldToZ. - replace 0%Z with (@FieldToZ m 0) by auto. - intro false_eq. - rewrite <-F_eq in false_eq. - congruence. - Qed. - -End VariousModulo. + Proof. + split; intros. + replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b); + try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial). + unwrap_F; rewrite <- (Z.quot_rem' a b); trivial. + Qed. + + End RingTacticGadgets. + + Ltac is_constant t := match t with @ZToField _ ?x => x | _ => NotConstant end. + Ltac is_pow_constant t := Ncst t. + + Module Type Modulus. Parameter modulus : Z. End Modulus. + + (* Example of how to instantiate the ring tactic *) + Module RingModulo (Export M : Modulus). + Add Ring _theory : (ring_theory modulus) + (morphism (ring_morph modulus), + constants [is_constant], + div (morph_div_theory modulus), + power_tac (power_theory modulus) [is_pow_constant]). + + Example ring_modulo_example : forall x y z, x*z + z*y = z*(x+y). + Proof. intros. ring. Qed. + End RingModulo. + + Section VariousModulo. + Context {m:Z}. + Local Open Scope F_scope. + + Add Ring _theory : (ring_theory m) + (morphism (ring_morph m), + constants [is_constant], + div (morph_div_theory m), + power_tac (power_theory m) [is_pow_constant]). + + Lemma mul_nonzero_l : forall a b : F m, a*b <> 0 -> a <> 0. + Proof. intros a b Hnz Hz. rewrite Hz in Hnz; apply Hnz; ring. Qed. + + Lemma mul_nonzero_r : forall a b : F m, a*b <> 0 -> b <> 0. + Proof. intros a b Hnz Hz. rewrite Hz in Hnz; apply Hnz; ring. Qed. + End VariousModulo. + + Section Pow. + Context {m:Z}. + Add Ring _theory' : (ring_theory m) + (morphism (ring_morph m), + constants [is_constant], + div (morph_div_theory m), + power_tac (power_theory m) [is_pow_constant]). + Local Open Scope F_scope. + + Import Algebra.ScalarMult. + Global Instance pow_is_scalarmult + : is_scalarmult (G:=F m) (eq:=eq) (add:=mul) (zero:=1%F) (mul := fun n x => x ^ (N.of_nat n)). + Proof. + split; intros; rewrite ?Nat2N.inj_succ, <-?N.add_1_l; + match goal with + | [x:F m |- _ ] => solve [destruct (@pow_spec m P); auto] + | |- Proper _ _ => solve_proper + end. + Qed. + + (* TODO: move this somewhere? *) + Create HintDb nat2N discriminated. + Hint Rewrite Nat2N.inj_iff + (eq_refl _ : (0%N = N.of_nat 0)) + (eq_refl _ : (1%N = N.of_nat 1)) + (eq_refl _ : (2%N = N.of_nat 2)) + (eq_refl _ : (3%N = N.of_nat 3)) + : nat2N. + Hint Rewrite <- Nat2N.inj_double Nat2N.inj_succ_double Nat2N.inj_succ + Nat2N.inj_add Nat2N.inj_mul Nat2N.inj_sub Nat2N.inj_pred + Nat2N.inj_div2 Nat2N.inj_max Nat2N.inj_min Nat2N.id + : nat2N. + + Ltac pow_to_scalarmult_ref := + repeat (autorewrite with nat2N; + match goal with + | |- context [ (_^?n)%F ] => + rewrite <-(N2Nat.id n); generalize (N.to_nat n); clear n; + let m := fresh n in intro m + | |- context [ (_^N.of_nat ?n)%F ] => + let rw := constr:(scalarmult_ext(zero:=ZToField m 1) n) in + setoid_rewrite rw (* rewriting moduloa reduction *) + end). + + Lemma pow_0_r (x:F m) : x^0 = 1. + Proof. pow_to_scalarmult_ref. apply scalarmult_0_l. Qed. + + Lemma pow_add_r (x:F m) (a b:N) : x^(a+b) = x^a * x^b. + Proof. pow_to_scalarmult_ref; apply scalarmult_add_l. Qed. + + Lemma pow_0_l (n:N) : n <> 0%N -> 0^n = 0 :> F m. + Proof. pow_to_scalarmult_ref; destruct n; simpl; intros; [congruence|ring]. Qed. + + Lemma pow_pow_l (x:F m) (a b:N) : (x^a)^b = x^(a*b). + Proof. pow_to_scalarmult_ref. apply scalarmult_assoc. Qed. + + Lemma pow_1_r (x:F m) : x^1 = x. + Proof. pow_to_scalarmult_ref; simpl; ring. Qed. + + Lemma pow_2_r (x:F m) : x^2 = x*x. + Proof. pow_to_scalarmult_ref; simpl; ring. Qed. + + Lemma pow_3_r (x:F m) : x^3 = x*x*x. + Proof. pow_to_scalarmult_ref; simpl; ring. Qed. + End Pow. +End Zmod. |