diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-02-11 21:59:58 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-03-02 13:37:14 -0500 |
| commit | e8fab6b839e19da231333ca8173bbb2a3d8a4033 (patch) | |
| tree | b8128c428ed4b4e58211071b207859ec37999db1 /src/ModularArithmetic | |
| parent | c56ca7b46711128f9287b5105a5b457ca09d4723 (diff) | |
split the algebra library; use fsatz more
Diffstat (limited to 'src/ModularArithmetic')
| -rw-r--r-- | src/ModularArithmetic/ModularArithmeticTheorems.v | 3 | ||||
| -rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 6 |
2 files changed, 5 insertions, 4 deletions
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index 44b422767..262b20e3e 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -6,7 +6,8 @@ Require Import Coq.ZArith.BinInt Coq.ZArith.Zdiv Coq.ZArith.Znumtheory Coq.NArit Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid. Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Ring_tac. -Require Import Crypto.Algebra Crypto.Util.Decidable Crypto.Util.ZUtil. +Require Import Crypto.Algebra Crypto.Algebra.Ring Crypto.Algebra.Field. +Require Import Crypto.Util.Decidable Crypto.Util.ZUtil. Require Export Crypto.Util.FixCoqMistakes. Module F. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index e0dfc8f1a..abc30056f 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -12,7 +12,7 @@ Require Import Crypto.Util.NumTheoryUtil Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Decidable. Require Export Crypto.Util.FixCoqMistakes. -Require Crypto.Algebra. +Require Crypto.Algebra Crypto.Algebra.Field. Existing Class prime. @@ -226,7 +226,7 @@ Module F. split; try apply eq_b4_a2. intro Hyy. rewrite !@F.pow_2_r in *. - destruct (Algebra.only_two_square_roots_choice _ x (x * x) Hyy eq_refl); clear Hyy; + destruct (Field.only_two_square_roots_choice _ x (x * x) Hyy eq_refl); clear Hyy; [ eexists; eassumption | ]. match goal with H : ?a * ?a = F.opp _ |- _ => exists (sqrt_minus1 * a); rewrite mul_square_sqrt_minus1; rewrite H end. @@ -254,7 +254,7 @@ Module F. break_if. intuition (f_equal; eauto). split; intro A. { - destruct (Algebra.only_two_square_roots_choice _ x (x * x) A eq_refl) as [B | B]; + destruct (Field.only_two_square_roots_choice _ x (x * x) A eq_refl) as [B | B]; clear A; try congruence. rewrite mul_square_sqrt_minus1, B; field. } { |