diff options
Diffstat (limited to 'src/Encoding/ModularWordEncodingTheorems.v')
| -rw-r--r-- | src/Encoding/ModularWordEncodingTheorems.v | 25 |
1 files changed, 9 insertions, 16 deletions
diff --git a/src/Encoding/ModularWordEncodingTheorems.v b/src/Encoding/ModularWordEncodingTheorems.v index 033e99665..03f98b2ca 100644 --- a/src/Encoding/ModularWordEncodingTheorems.v +++ b/src/Encoding/ModularWordEncodingTheorems.v @@ -3,7 +3,7 @@ Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems. Require Import Bedrock.Word. -Require Import Crypto.Tactics.VerdiTactics. +Require Import Crypto.Tactics.VerdiTactics Crypto.Util.Tactics. Require Import Crypto.Spec.Encoding. Require Import Crypto.Util.ZUtil. Require Import Crypto.Spec.ModularWordEncoding. @@ -24,7 +24,7 @@ Section SignBit. assert (m < 1)%Z by (apply Z2Nat.inj_lt; try omega; assumption). omega. + assert (0 < m)%Z as m_pos by (pose proof prime_ge_2 m prime_m; omega). - pose proof (FieldToZ_range x m_pos). + pose proof (Zmod.FieldToZ_range x m_pos). destruct (FieldToZ x); auto. - destruct p; auto. - pose proof (Pos2Z.neg_is_neg p); omega. @@ -35,20 +35,13 @@ Section SignBit. rewrite sign_bit_parity; auto. Qed. - Lemma sign_bit_opp : forall (x : F m), x <> 0 -> negb (@sign_bit m sz x) = @sign_bit m sz (opp x). + 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. - intros. - pose proof sign_bit_zero as sign_zero. - rewrite !sign_bit_parity in *. - pose proof (F_opp_spec x) as opp_spec_x. - apply F_eq in opp_spec_x. - rewrite FieldToZ_add in opp_spec_x. - rewrite <-opp_spec_x, Z.odd_mod in sign_zero by (pose proof prime_ge_2 m prime_m; omega). - replace (Z.odd m) with true in sign_zero by (destruct (Z.prime_odd_or_2 m prime_m); auto || omega). - rewrite Z.odd_add, F_FieldToZ_add_opp, Z.div_same, Bool.xorb_true_r in sign_zero by assumption || omega. - apply Bool.xorb_eq. - rewrite <-Bool.negb_xorb_l. - assumption. + 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. Qed. - End SignBit. |