From fd43be3ef81a857ad5a108ef11844944d83f5e2f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 29 Sep 2016 11:31:12 -0400 Subject: map -> List.map (not Tuple.map) --- src/ModularArithmetic/ModularBaseSystemOpt.v | 34 +++++++++--------- src/ModularArithmetic/ModularBaseSystemProofs.v | 46 ++++++++++++------------- 2 files changed, 40 insertions(+), 40 deletions(-) (limited to 'src/ModularArithmetic') 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. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 5d7a1c24d..c160eca7f 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -138,8 +138,8 @@ Section FieldOperationProofs. Lemma modular_base_system_add_monoid : @monoid digits eq add zero. Proof. repeat match goal with - | |- _ => progress intro - | |- _ => cbv [zero]; rewrite encode_rep + | |- _ => progress intro + | |- _ => cbv [zero]; rewrite encode_rep | |- _ digits eq add => econstructor | |- _ digits eq add _ => econstructor | |- (_ + _)%F = decode (add ?a ?b) => rewrite (add_rep a b) by (try apply add_rep; reflexivity) @@ -149,7 +149,7 @@ Section FieldOperationProofs. | |- add _ _ ~= decode _ => etransitivity | x : digits |- ?x ~= _ => reflexivity | |- _ => apply associative - | |- _ => apply left_identity + | |- _ => apply left_identity | |- _ => apply right_identity | |- _ => solve [eauto using eq_Equivalence, eq_dec] | |- _ => congruence @@ -165,7 +165,7 @@ Section FieldOperationProofs. Proof. cbv [reduce]; intros. rewrite extended_shiftadd, base_from_limb_widths_length, pseudomersenne_add, BaseSystemProofs.add_rep. - change (map (Z.mul c)) with (BaseSystem.mul_each c). + change (List.map (Z.mul c)) with (BaseSystem.mul_each c). rewrite mul_each_rep; auto. Qed. @@ -186,8 +186,8 @@ Section FieldOperationProofs. Lemma modular_base_system_mul_monoid : @monoid digits eq mul one. Proof. repeat match goal with - | |- _ => progress intro - | |- _ => cbv [one]; rewrite encode_rep + | |- _ => progress intro + | |- _ => cbv [one]; rewrite encode_rep | |- _ digits eq mul => econstructor | |- _ digits eq mul _ => econstructor | |- (_ * _)%F = decode (mul ?a ?b) => rewrite (mul_rep a b) by (try apply mul_rep; reflexivity) @@ -197,7 +197,7 @@ Section FieldOperationProofs. | |- mul _ _ ~= decode _ => etransitivity | x : digits |- ?x ~= _ => reflexivity | |- _ => apply associative - | |- _ => apply left_identity + | |- _ => apply left_identity | |- _ => apply right_identity | |- _ => solve [eauto using eq_Equivalence, eq_dec] | |- _ => congruence @@ -290,7 +290,7 @@ Section FieldOperationProofs. cbv beta delta [eq] in *. erewrite !add_rep; cbv [rep] in *; try reflexivity; assumption. Qed. - + Global Instance sub_Proper mm mm_correct : Proper (eq ==> eq ==> eq) (sub mm mm_correct). Proof. @@ -298,7 +298,7 @@ Section FieldOperationProofs. cbv beta delta [eq] in *. erewrite !sub_rep; cbv [rep] in *; try reflexivity; assumption. Qed. - + Global Instance opp_Proper mm mm_correct : Proper (eq ==> eq) (opp mm mm_correct). Proof. @@ -361,7 +361,7 @@ Section FieldOperationProofs. + trivial. Qed. End FieldProofs. - + End FieldOperationProofs. Opaque encode add mul sub inv pow. @@ -579,7 +579,7 @@ Section CanonicalizationProofs. then if eq_nat_dec n (pred i) then Z.pow2_mod (us {{ pred i }} [n]) (limb_widths [n]) - else us{{ pred i }} [n] + else us{{ pred i }} [n] else us{{ pred i}} [n] + (if eq_nat_dec n i then (us{{ pred i}} [pred i]) >> (limb_widths [pred i]) @@ -631,11 +631,11 @@ Section CanonicalizationProofs. reflexivity. Qed. - Ltac bound_during_loop := + Ltac bound_during_loop := repeat match goal with | |- _ => progress (intros; subst) | |- _ => unique pose proof lt_1_length_limb_widths - | |- _ => unique pose proof c_reduce2 + | |- _ => unique pose proof c_reduce2 | |- _ => break_if; try omega | |- _ => progress simpl pred in * | |- _ => progress rewrite ?Z.add_0_r, ?Z.sub_0_r in * @@ -770,7 +770,7 @@ Section CanonicalizationProofs. if lt_dec i (length limb_widths) then if Z_lt_dec (us [0]) (2 ^ limb_widths [0]) - then + then 2 ^ limb_widths [n] else if eq_nat_dec n 0 @@ -798,7 +798,7 @@ Section CanonicalizationProofs. auto using length_carry_full, bound_after_second_loop. Qed. - Local Notation initial_bounds u := + Local Notation initial_bounds u := (forall n : nat, 0 <= to_list (length limb_widths) u [n] < 2 ^ B - @@ -807,7 +807,7 @@ Section CanonicalizationProofs. else (2 ^ B) >> (limb_widths [pred n]))). Local Notation minimal_rep u := ((bounded limb_widths (to_list (length limb_widths) u)) /\ (ge_modulus (to_list _ u) = false)). - + Lemma decode_bitwise_eq_iff : forall u v, minimal_rep u -> minimal_rep v -> (fieldwise Logic.eq u v <-> decode_bitwise limb_widths (to_list _ u) = decode_bitwise limb_widths (to_list _ v)). @@ -851,7 +851,7 @@ Section CanonicalizationProofs. Qed. Lemma bounded_canonical : forall u v x y, rep u x -> rep v y -> - minimal_rep u -> minimal_rep v -> + minimal_rep u -> minimal_rep v -> (x = y <-> fieldwise Logic.eq u v). Proof. intros. @@ -921,7 +921,7 @@ Section CanonicalizationProofs. erewrite <-!Fdecode_decode_mod by eauto. apply freeze_decode. Qed. - + Lemma freeze_canonical : forall u v x y, rep u x -> rep v y -> initial_bounds u -> initial_bounds v -> @@ -939,15 +939,15 @@ Section SquareRootProofs. Local Notation base := (base_from_limb_widths limb_widths). Local Hint Resolve (@limb_widths_nonneg _ prm) sum_firstn_limb_widths_nonneg. - Definition freeze_input_bounds n := + Definition freeze_input_bounds n := (2 ^ B - (if eq_nat_dec n 0 then 0 else (2 ^ B) >> (nth_default 0 limb_widths (pred n)))). - Definition bounded_by u bounds := + Definition bounded_by u bounds := (forall n : nat, 0 <= nth_default 0 (to_list (length limb_widths) u) n < bounds n). - + Lemma eqb_true_iff : forall u v x y, bounded_by u freeze_input_bounds -> bounded_by v freeze_input_bounds -> u ~= x -> v ~= y -> (x = y <-> eqb u v = true). @@ -1002,7 +1002,7 @@ Section SquareRootProofs. {pow_input_bounds : nat -> Z} (pow_bounded : forall x is, bounded_by x pow_input_bounds -> bounded_by (pow_ x is) mul_input_bounds). - + Lemma sqrt_5mod8_correct : forall u x, u ~= x -> bounded_by u pow_input_bounds -> bounded_by u freeze_input_bounds -> (sqrt_5mod8 mul_ pow_ chain chain_correct sqrt_m1 u) ~= F.sqrt_5mod8 (decode sqrt_m1) x. @@ -1031,4 +1031,4 @@ Section SquareRootProofs. Qed. End Sqrt5mod8. -End SquareRootProofs. \ No newline at end of file +End SquareRootProofs. -- cgit v1.2.3