diff options
-rw-r--r-- | src/Algebra.v | 8 | ||||
-rw-r--r-- | src/Encoding/ModularWordEncodingTheorems.v | 9 | ||||
-rw-r--r-- | src/Experiments/SpecEd25519.v | 12 | ||||
-rw-r--r-- | src/ModularArithmetic/ModularArithmeticTheorems.v | 100 | ||||
-rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 7 | ||||
-rw-r--r-- | src/Util/Decidable.v | 10 | ||||
-rw-r--r-- | src/Util/NumTheoryUtil.v | 7 |
7 files changed, 71 insertions, 82 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index adbf5b86b..5601b9d28 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -365,12 +365,14 @@ Module ScalarMult. Global Instance Proper_scalarmult_ref : Proper (Logic.eq==>eq==>eq) scalarmult_ref. Proof. - repeat intro; subst. - match goal with [n:nat |- _ ] => induction n; simpl @scalarmult_ref; [reflexivity|] end. - repeat match goal with [H:_ |- _ ] => rewrite H end; reflexivity. + repeat intro; subst; + match goal with [n:nat |- _ ] => + solve [induction n; simpl scalarmult_ref; rewrite_hyp ?*; reflexivity] + end. Qed. Lemma scalarmult_ext : forall n P, mul n P = scalarmult_ref n P. + Proof. induction n; simpl @scalarmult_ref; intros; rewrite <-?IHn; (apply scalarmult_0_l || apply scalarmult_S_l). Qed. diff --git a/src/Encoding/ModularWordEncodingTheorems.v b/src/Encoding/ModularWordEncodingTheorems.v index 03f98b2ca..c42dd8c6f 100644 --- a/src/Encoding/ModularWordEncodingTheorems.v +++ b/src/Encoding/ModularWordEncodingTheorems.v @@ -6,6 +6,7 @@ Require Import Bedrock.Word. Require Import Crypto.Tactics.VerdiTactics Crypto.Util.Tactics. Require Import Crypto.Spec.Encoding. Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.FixCoqMistakes. Require Import Crypto.Spec.ModularWordEncoding. @@ -35,13 +36,11 @@ Section SignBit. rewrite sign_bit_parity; auto. Qed. - Lemma odd_m : Z.odd m = true. Admitted. - Lemma sign_bit_opp (x : F m) (Hnz:x <> 0) : negb (@sign_bit m sz x) = @sign_bit m sz (opp x). Proof. pose proof Zmod.FieldToZ_nonzero_range x Hnz; specialize_by omega. - rewrite !sign_bit_parity, Zmod.FieldToZ_opp, Z_mod_nz_opp_full, - Zmod_small, Z.odd_sub, odd_m, (Bool.xorb_true_l (Z.odd x)) by - (omega || rewrite Zmod_small by omega; auto using Zmod.FieldToZ_nonzero); trivial. + rewrite !sign_bit_parity, Zmod.FieldToZ_opp, Z_mod_nz_opp_full, Zmod_small, + Z.odd_sub, (NumTheoryUtil.p_odd m), (Bool.xorb_true_l (Z.odd x)); + try eapply Zrel_prime_neq_mod_0, rel_prime_le_prime; intuition omega. Qed. End SignBit. diff --git a/src/Experiments/SpecEd25519.v b/src/Experiments/SpecEd25519.v index 6d6de9dcb..aca633fe2 100644 --- a/src/Experiments/SpecEd25519.v +++ b/src/Experiments/SpecEd25519.v @@ -12,7 +12,7 @@ Require Import Coq.Logic.Decidable Crypto.Util.Decidable. Require Import Coq.omega.Omega. (* TODO: move to PrimeFieldTheorems *) -Lemma minus1_is_square {q} : prime q -> (q mod 4)%Z = 1%Z -> (exists y, y*y = opp (ZToField q 1))%F. +Lemma minus1_is_square {q} : prime q -> (q mod 4)%Z = 1%Z -> (exists y, y*y = opp (ZToField q 1))%F. intros; pose proof prime_ge_2 q _. rewrite Zmod.square_iff. destruct (minus1_square_1mod4 q) as [b b_id]; trivial; exists b. @@ -31,16 +31,6 @@ Lemma square_a : exists b, (b*b=a)%F. Proof. pose (@Zmod.Decidable_square q _ two_lt_q a); vm_decide_no_check. Qed. Definition d : F q := (opp (ZToField _ 121665) / (ZToField _ 121666))%F. -(* TODO: move to Decidable *) -Lemma not_not P {d:Decidable P} : not (not P) <-> P. -Proof. destruct (dec P); intuition. Qed. - -Global Instance dec_ex_forall_not T (P:T->Prop) {d:Decidable (exists b, P b)} : Decidable (forall b, ~ P b). -Proof. - destruct (dec (~ exists b, P b)) as [Hd|Hd]; [left|right]; - [abstract eauto | abstract (rewrite not_not in Hd by eauto; destruct Hd; eauto) ]. -Defined. - Lemma nonsquare_d : forall x, (x*x <> d)%F. Proof. pose (@Zmod.Decidable_square q _ two_lt_q d). vm_decide_no_check. Qed. diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index 5cbc4aa3c..cf0d9eed3 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -9,52 +9,51 @@ Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Ring_tac. Require Import Crypto.Algebra Crypto.Util.Decidable. Require Export Crypto.Util.FixCoqMistakes. -(* 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. - -(* Remove redundant [mod] operations from the conclusion. *) -Ltac demod := - repeat match goal with - | [ |- context[(?x mod _ + _) mod _] ] => - notFancy x; rewrite (Zplus_mod_idemp_l x) - | [ |- context[(_ + ?y mod _) mod _] ] => - notFancy y; rewrite (Zplus_mod_idemp_r y) - | [ |- context[(?x mod _ - _) mod _] ] => - notFancy x; rewrite (Zminus_mod_idemp_l x) - | [ |- context[(_ - ?y mod _) mod _] ] => - notFancy y; rewrite (Zminus_mod_idemp_r _ y) - | [ |- context[(?x mod _ * _) mod _] ] => - notFancy x; rewrite (Zmult_mod_idemp_l x) - | [ |- context[(_ * (?y mod _)) mod _] ] => - notFancy y; rewrite (Zmult_mod_idemp_r y) - | [ |- context[(?x mod _) mod _] ] => - notFancy x; rewrite (Zmod_mod x) - end. - -Ltac unwrap_F := - intros; - repeat match goal with [ x : F _ |- _ ] => destruct x end; - lazy iota beta delta [add sub mul opp FieldToZ ZToField proj1_sig] in *; - try apply eqsig_eq; - demod. - -(* FIXME: remove the pose proof once [monoid] no longer contains decidable equality *) -Global Instance eq_dec {m} : DecidableRel (@eq (F m)). pose proof dec_eq_Z. 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. + (* 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. + + (* Remove redundant [mod] operations from the conclusion. *) + Ltac demod := + repeat match goal with + | [ |- context[(?x mod _ + _) mod _] ] => + notFancy x; rewrite (Zplus_mod_idemp_l x) + | [ |- context[(_ + ?y mod _) mod _] ] => + notFancy y; rewrite (Zplus_mod_idemp_r y) + | [ |- context[(?x mod _ - _) mod _] ] => + notFancy x; rewrite (Zminus_mod_idemp_l x) + | [ |- context[(_ - ?y mod _) mod _] ] => + notFancy y; rewrite (Zminus_mod_idemp_r _ y) + | [ |- context[(?x mod _ * _) mod _] ] => + notFancy x; rewrite (Zmult_mod_idemp_l x) + | [ |- context[(_ * (?y mod _)) mod _] ] => + notFancy y; rewrite (Zmult_mod_idemp_r y) + | [ |- context[(?x mod _) mod _] ] => + notFancy x; rewrite (Zmod_mod x) + end. + + Ltac unwrap_F := + intros; + repeat match goal with [ x : F _ |- _ ] => destruct x end; + lazy iota beta delta [add sub mul opp FieldToZ ZToField proj1_sig] in *; + try apply eqsig_eq; + demod. + + (* FIXME: remove the pose proof once [monoid] no longer contains decidable equality *) + Global Instance eq_dec {m} : DecidableRel (@eq (F m)). pose proof dec_eq_Z. 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. + 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. @@ -165,17 +164,6 @@ Module Zmod. - 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. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index e0c778456..f30472911 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -78,13 +78,6 @@ Module Zmod. rewrite eq_FieldToZ_iff, FieldToZ_mul, FieldToZ_pow, Z2N.id, FieldToZ_1 by omega. apply (fermat_inv q _ (FieldToZ x)); rewrite mod_FieldToZ; eapply FieldToZ_nonzero; trivial. Qed. - - (* TODO: move to number thoery util *) - Lemma odd_as_div a : Z.odd a = true -> a = (2*(a/2) + 1)%Z. - Proof. - rewrite Zodd_mod, <-Zeq_is_eq_bool; intro H_1; rewrite <-H_1. - apply Z_div_mod_eq; reflexivity. - Qed. Lemma euler_criterion (a : F q) (a_nonzero : a <> 0) : (a ^ (Z.to_N (q / 2)) = 1) <-> (exists b, b*b = a). diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v index e19e23ca4..7b412caf0 100644 --- a/src/Util/Decidable.v +++ b/src/Util/Decidable.v @@ -1,6 +1,7 @@ (** Typeclass for decidable propositions *) Require Import Coq.Logic.Eqdep_dec. +Require Import Crypto.Util.FixCoqMistakes. Require Import Crypto.Util.Sigma. Require Import Crypto.Util.HProp. Require Import Crypto.Util.Equality. @@ -97,6 +98,15 @@ Global Instance dec_eq_nat : DecidableRel (@eq nat) | 10. exact _. Defined. Global Instance dec_eq_N : DecidableRel (@eq N) | 10 := N.eq_dec. Global Instance dec_eq_Z : DecidableRel (@eq Z) | 10 := Z.eq_dec. +Lemma not_not P {d:Decidable P} : not (not P) <-> P. +Proof. destruct (dec P); intuition. Qed. + +Global Instance dec_ex_forall_not T (P:T->Prop) {d:Decidable (exists b, P b)} : Decidable (forall b, ~ P b). +Proof. + destruct (dec (~ exists b, P b)) as [Hd|Hd]; [left|right]; + [abstract eauto | abstract (rewrite not_not in Hd by eauto; destruct Hd; eauto) ]. +Defined. + Lemma eqsig_eq {T} {U} {Udec:DecidableRel (@eq U)} (f g:T->U) (x x':T) pf pf' : (exist (fun x => f x = g x) x pf) = (exist (fun x => f x = g x) x' pf') <-> (x = x'). Proof. apply path_sig_hprop_iff; auto using UIP_dec, Udec. Qed. diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index 8b8595bb7..f89eb6996 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -298,3 +298,10 @@ Proof. + prime_bound. + apply minus1_even_pow; [apply divide2_1mod4 | | apply Z_div_pos]; prime_bound. Qed. + + +Lemma odd_as_div a : Z.odd a = true -> a = (2*(a/2) + 1)%Z. +Proof. + rewrite Zodd_mod, <-Zeq_is_eq_bool; intro H_1; rewrite <-H_1. + apply Z_div_mod_eq; reflexivity. +Qed.
\ No newline at end of file |