aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic/ModularBaseSystemOpt.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemOpt.v')
-rw-r--r--src/ModularArithmetic/ModularBaseSystemOpt.v34
1 files changed, 17 insertions, 17 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index 6a3a4f7c2..dba1afd29 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -43,7 +43,7 @@ Definition Z_shiftl_by_opt := Eval compute in Z.shiftl_by.
Definition nth_default_opt {A} := Eval compute in @nth_default A.
Definition set_nth_opt {A} := Eval compute in @set_nth A.
Definition update_nth_opt {A} := Eval compute in @update_nth A.
-Definition map_opt {A B} := Eval compute in @map A B.
+Definition map_opt {A B} := Eval compute in @List.map A B.
Definition full_carry_chain_opt := Eval compute in @Pow2Base.full_carry_chain.
Definition length_opt := Eval compute in length.
Definition base_from_limb_widths_opt := Eval compute in @Pow2Base.base_from_limb_widths.
@@ -143,7 +143,7 @@ Definition construct_mul2modulus {m} (prm : PseudoMersenneBaseParams m) : digits
match limb_widths with
| nil => nil
| x :: tail =>
- 2 ^ (x + 1) - (2 * c) :: map (fun w => 2 ^ (w + 1) - 2) tail
+ 2 ^ (x + 1) - (2 * c) :: List.map (fun w => 2 ^ (w + 1) - 2) tail
end.
Ltac compute_preconditions :=
@@ -459,7 +459,7 @@ Section Subtraction.
Definition opp_opt_correct us
: opp_opt us = opp coeff coeff_mod us
:= proj2_sig (opp_opt_sig us).
-
+
End Subtraction.
Section Multiplication.
@@ -532,7 +532,7 @@ Section Multiplication.
end.
Lemma map_zeros : forall a n l,
- map (Z.mul a) (zeros n ++ l) = zeros n ++ map (Z.mul a) l.
+ List.map (Z.mul a) (zeros n ++ l) = zeros n ++ List.map (Z.mul a) l.
Proof.
induction n; simpl; [ reflexivity | intros; apply f_equal2; [ omega | congruence ] ].
Qed.
@@ -553,7 +553,7 @@ Section Multiplication.
{ cbv [mul_each mul_bi].
rewrite <- mul_bi'_opt_correct.
rewrite map_zeros.
- change @map with @map_opt.
+ change @List.map with @map_opt.
cbv [zeros].
reflexivity. }
Defined.
@@ -598,7 +598,7 @@ Section Multiplication.
rewrite Z.map_shiftl by apply k_nonneg.
rewrite c_subst.
fold k; rewrite k_subst.
- change @map with @map_opt.
+ change @List.map with @map_opt.
change @Z.shiftl_by with @Z_shiftl_by_opt.
reflexivity.
Defined.
@@ -670,7 +670,7 @@ Section PowInv.
{cc : CarryChain limb_widths}.
Local Notation digits := (tuple Z (length limb_widths)).
Context (one_ : digits) (one_subst : one = one_).
-
+
Fixpoint fold_chain_opt {T} (id : T) op chain acc :=
match chain with
| [] => match acc with
@@ -761,7 +761,7 @@ Section Conversion.
Definition convert'_opt {lwA lwB}
(nonnegA : forall x, In x lwA -> 0 <= x)
(nonnegB : forall x, In x lwB -> 0 <= x)
- bits_fit inp i out :=
+ bits_fit inp i out :=
Eval cbv [proj1_sig convert'_opt_sig] in
proj1_sig (convert'_opt_sig nonnegA nonnegB bits_fit inp i out).
@@ -769,10 +769,10 @@ Section Conversion.
(nonnegA : forall x, In x lwA -> 0 <= x)
(nonnegB : forall x, In x lwB -> 0 <= x)
bits_fit inp i out :
- convert'_opt nonnegA nonnegB bits_fit inp i out = convert' nonnegA nonnegB bits_fit inp i out :=
+ convert'_opt nonnegA nonnegB bits_fit inp i out = convert' nonnegA nonnegB bits_fit inp i out :=
Eval cbv [proj2_sig convert'_opt_sig] in
proj2_sig (convert'_opt_sig nonnegA nonnegB bits_fit inp i out).
-
+
Context {modulus} (prm : PseudoMersenneBaseParams modulus)
{target_widths} (target_widths_nonneg : forall x, In x target_widths -> 0 <= x) (bits_eq : sum_firstn limb_widths (length limb_widths) = sum_firstn target_widths (length target_widths)).
Local Notation digits := (tuple Z (length limb_widths)).
@@ -813,7 +813,7 @@ Section Conversion.
Definition unpack_opt (x : target_digits) : digits :=
Eval cbv [proj1_sig unpack_opt_sig] in proj1_sig (unpack_opt_sig x).
-
+
Definition unpack_correct (x : target_digits) :
unpack_opt x = unpack target_widths_nonneg bits_eq x
:= Eval cbv [proj2_sig unpack_opt_sig] in proj2_sig (unpack_opt_sig x).
@@ -883,7 +883,7 @@ Section Canonicalization.
change @max_ones with max_ones_opt.
reflexivity.
Defined.
-
+
Definition conditional_subtract_modulus_opt f cond : list Z
:= Eval cbv [proj1_sig conditional_subtract_modulus_opt_sig] in proj1_sig (conditional_subtract_modulus_opt_sig f cond).
@@ -937,10 +937,10 @@ Section SquareRoots.
Proof.
intros; repeat break_if; congruence.
Qed.
-
+
Section SquareRoot3mod4.
Context {ec : ExponentiationChain (modulus / 4 + 1)}.
-
+
Definition sqrt_3mod4_opt_sig (us : digits) :
{ vs : digits | eq vs (sqrt_3mod4 chain chain_correct us)}.
Proof.
@@ -954,7 +954,7 @@ Section SquareRoots.
Definition sqrt_3mod4_opt_correct us
: eq (sqrt_3mod4_opt us) (sqrt_3mod4 chain chain_correct us)
:= Eval cbv [proj2_sig sqrt_3mod4_opt_sig] in proj2_sig (sqrt_3mod4_opt_sig us).
-
+
End SquareRoot3mod4.
Import Morphisms.
@@ -963,7 +963,7 @@ Section SquareRoots.
Section SquareRoot5mod8.
Context {ec : ExponentiationChain (modulus / 8 + 1)}.
Context (sqrt_m1 : digits) (sqrt_m1_correct : rep (mul sqrt_m1 sqrt_m1) (F.opp 1%F)).
-
+
Definition sqrt_5mod8_opt_sig (us : digits) :
{ vs : digits |
eq vs (sqrt_5mod8 (carry_mul_opt k_ c_) (pow_opt k_ c_ one_) chain chain_correct sqrt_m1 us)}.
@@ -982,7 +982,7 @@ Section SquareRoots.
Definition sqrt_5mod8_opt_correct us
: eq (sqrt_5mod8_opt us) (ModularBaseSystem.sqrt_5mod8 _ _ chain chain_correct sqrt_m1 us)
:= Eval cbv [proj2_sig sqrt_5mod8_opt_sig] in proj2_sig (sqrt_5mod8_opt_sig us).
-
+
End SquareRoot5mod8.
End SquareRoots.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-19 05:14:50 +0000