From d3135a69f653034f07b7657486f926a7a20ef3ee Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 1 Jun 2017 23:59:55 -0400 Subject: Strip trailing whitespace With ```bash bash ./etc/coq-scripts/formatting/strip-trailing-whitespace.sh ``` --- src/Algebra/Field_test.v | 2 +- src/Algebra/Group.v | 2 +- src/Algebra/ScalarMult.v | 2 +- src/Arithmetic/Core.v | 2 +- src/Arithmetic/ModularArithmeticPre.v | 2 +- src/Arithmetic/ModularArithmeticTheorems.v | 10 ++++----- src/Arithmetic/PrimeFieldTheorems.v | 8 +++---- src/Arithmetic/Saturated.v | 34 +++++++++++++++--------------- src/Curves/Edwards/Pre.v | 2 +- src/Curves/Montgomery/Affine.v | 2 +- src/Curves/Montgomery/AffineInstances.v | 4 ++-- src/Curves/Montgomery/AffineProofs.v | 4 ++-- src/Curves/Weierstrass/Affine.v | 2 +- src/Curves/Weierstrass/AffineProofs.v | 2 +- src/LegacyArithmetic/BaseSystem.v | 2 +- src/LegacyArithmetic/BaseSystemProofs.v | 2 +- src/LegacyArithmetic/Pow2BaseProofs.v | 2 +- src/Spec/CompleteEdwardsCurve.v | 2 +- src/Spec/Ed25519.v | 6 +++--- src/Spec/Test/X25519.v | 2 +- src/Spec/WeierstrassCurve.v | 2 +- src/Specific/ArithmeticSynthesisTest.v | 4 ++-- src/Util/CPSUtil.v | 2 +- src/Util/Factorize.v | 2 +- src/Util/NUtil.v | 2 +- src/Util/NumTheoryUtil.v | 2 +- src/Util/Relations.v | 2 +- src/Util/ZUtil/Zselect.v | 2 +- 28 files changed, 56 insertions(+), 56 deletions(-) (limited to 'src') diff --git a/src/Algebra/Field_test.v b/src/Algebra/Field_test.v index 59ca72c6b..149a6373e 100644 --- a/src/Algebra/Field_test.v +++ b/src/Algebra/Field_test.v @@ -92,4 +92,4 @@ Module _fsatz_test. : x7 = x9 /\ y7 = y9. Proof using Type*. fsatz_prepare_hyps; split; fsatz. Qed. End _test. -End _fsatz_test. \ No newline at end of file +End _fsatz_test. diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v index 27c45dcec..01325de3f 100644 --- a/src/Algebra/Group.v +++ b/src/Algebra/Group.v @@ -196,4 +196,4 @@ Section CommutativeGroupByIsomorphism. | _ => solve [ eauto ] end. Qed. -End CommutativeGroupByIsomorphism. \ No newline at end of file +End CommutativeGroupByIsomorphism. diff --git a/src/Algebra/ScalarMult.v b/src/Algebra/ScalarMult.v index f52fc93ee..034ed4d4c 100644 --- a/src/Algebra/ScalarMult.v +++ b/src/Algebra/ScalarMult.v @@ -89,4 +89,4 @@ End ScalarMultHomomorphism. Global Instance scalarmult_ref_is_scalarmult {G eq add zero} `{@monoid G eq add zero} : @is_scalarmult G eq add zero (@scalarmult_ref G add zero). -Proof. split; try exact _; intros; reflexivity. Qed. \ No newline at end of file +Proof. split; try exact _; intros; reflexivity. Qed. diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index b86ac09b9..d61ff5ba4 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -837,7 +837,7 @@ Module B. Section Select. Context {weight : nat -> Z}. - + Definition select_cps {n} (mask cond:Z) (p:tuple Z n) {T} (f:tuple Z n->T) := dlet t := Z.zselect cond 0 mask in Tuple.map_cps (runtime_and t) p f. diff --git a/src/Arithmetic/ModularArithmeticPre.v b/src/Arithmetic/ModularArithmeticPre.v index b27ffd16d..3063d3a51 100644 --- a/src/Arithmetic/ModularArithmeticPre.v +++ b/src/Arithmetic/ModularArithmeticPre.v @@ -136,4 +136,4 @@ Next Obligation. replace (Z.succ (m - 2)) with (m-1) by omega. rewrite (Zmod_small 1) by omega. apply (fermat_little m Hm a Ha). -Qed. \ No newline at end of file +Qed. diff --git a/src/Arithmetic/ModularArithmeticTheorems.v b/src/Arithmetic/ModularArithmeticTheorems.v index 990aa9dc8..8f9277f35 100644 --- a/src/Arithmetic/ModularArithmeticTheorems.v +++ b/src/Arithmetic/ModularArithmeticTheorems.v @@ -17,10 +17,10 @@ Module F. lazy iota beta delta [F.add F.sub F.mul F.opp F.to_Z F.of_Z proj1_sig] in *; try apply eqsig_eq; pull_Zmod. - + (* 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.Hierarchy.commutative_ring (F m) Logic.eq 0%F 1%F F.opp F.add F.sub F.mul. Proof. @@ -48,14 +48,14 @@ Module F. Lemma eq_of_Z_iff : forall x y : Z, x mod m = y mod m <-> F.of_Z m x = F.of_Z m y. Proof using Type. split; unwrap_F; congruence. Qed. - + Lemma to_Z_of_Z : forall z, F.to_Z (F.of_Z m z) = z mod m. Proof using Type. unwrap_F; trivial. Qed. Lemma of_Z_to_Z x : F.of_Z m (F.to_Z x) = x :> F m. Proof using Type. unwrap_F; congruence. Qed. - + Lemma of_Z_mod : forall x, F.of_Z m x = F.of_Z m (x mod m). Proof using Type. unwrap_F; trivial. Qed. @@ -95,7 +95,7 @@ Module F. Lemma to_Z_mul : forall x y : F m, F.to_Z (x * y) = ((F.to_Z x * F.to_Z y) mod m)%Z. Proof using Type. unwrap_F; trivial. Qed. - + Lemma of_Z_sub x y : F.of_Z _ (x - y) = F.of_Z _ x - F.of_Z _ y :> F m. Proof using Type. unwrap_F. trivial. Qed. diff --git a/src/Arithmetic/PrimeFieldTheorems.v b/src/Arithmetic/PrimeFieldTheorems.v index c253752c5..edab4e065 100644 --- a/src/Arithmetic/PrimeFieldTheorems.v +++ b/src/Arithmetic/PrimeFieldTheorems.v @@ -95,7 +95,7 @@ Module F. rewrite <-H in q_3mod4; discriminate. Qed. Local Hint Resolve two_lt_q_3mod4. - + Lemma sqrt_3mod4_correct (x:F q) : ((exists y, y*y = x) <-> (sqrt_3mod4 x)*(sqrt_3mod4 x) = x)%F. Proof using Type*. @@ -130,7 +130,7 @@ Module F. constants [F.is_constant], div (F.morph_div_theory q), power_tac (F.power_theory q) [F.is_pow_constant]). - + (* Any nonsquare element raised to (q-1)/4 (real implementations use 2 ^ ((q-1)/4) ) would work for sqrt_minus1 *) Context (sqrt_minus1 : F q) (sqrt_minus1_valid : sqrt_minus1 * sqrt_minus1 = F.opp 1). @@ -241,7 +241,7 @@ Module F. Module Iso. Section IsomorphicRings. Context {q:positive} {prime_q:prime q} {two_lt_q:2 < Z.pos q}. - Context + Context {H : Type} {eq : H -> H -> Prop} {zero one : H} {opp : H -> H} {add sub mul : H -> H -> H} {phi : F q -> H} {phi' : H -> F q} @@ -256,7 +256,7 @@ Module F. {pow_is_scalarmult:ScalarMult.is_scalarmult(G:=H)(eq:=eq)(add:=mul)(zero:=one)(mul:=fun (n:nat) (k:H) => pow k (NtoP (N.of_nat n)))}. Definition inv (x:H) := pow x (NtoP (Z.to_N (q - 2)%Z)). Definition div x y := mul (inv y) x. - + Lemma ring : @Algebra.Hierarchy.ring H eq zero one opp add sub mul /\ @Ring.is_homomorphism (F q) Logic.eq F.one F.add F.mul H eq one add mul phi diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v index 650cd7bcf..a66c268b0 100644 --- a/src/Arithmetic/Saturated.v +++ b/src/Arithmetic/Saturated.v @@ -49,14 +49,14 @@ a [tuple Z n] as output. This operation is called "compact". As an example, let's compact the product of 571 and 645 in base 10. At first, the partial products look like this: - - 1*6 + + 1*6 1*4 7*4 7*6 1*5 7*5 5*5 5*4 5*6 ------------------------------------ 1 10 100 1000 10000 - - 6 + + 6 4 28 42 5 35 25 20 30 ------------------------------------ @@ -75,7 +75,7 @@ bit. We add a 0 to the next column and continue. {carry_acc = 0; output=(5,)} STEP [4,35] (4 + 35 = 39) {carry_acc = 3; output=(9,5)} - + This time, we have a carry. We add it to the third column and process that: @@ -93,7 +93,7 @@ columns: {carry_acc = 4; output=(8,9,5)} STEP [4,20] (4 + 20 = 24) {carry_acc = 6; output=(4,8,9,5)} - + STEP [6,30] (6 + 30 = 36) {carry_acc = 3; output=(6,4,8,9,5)} @@ -213,7 +213,7 @@ Module Columns. | _ => progress (autorewrite with uncps push_id cancel_pair in * ) | _ => progress break_match; try discriminate | _ => reflexivity - | _ => f_equal; ring + | _ => f_equal; ring end. Qed. Hint Rewrite compact_digit_mod : div_mod. @@ -229,9 +229,9 @@ Module Columns. | _ => progress (autorewrite with uncps push_id cancel_pair in * ) | _ => progress break_match; try discriminate | _ => reflexivity - | _ => f_equal; ring + | _ => f_equal; ring end. - assert (weight (S i) / weight i <> 0) by auto using Z.positive_is_nonzero. + assert (weight (S i) / weight i <> 0) by auto using Z.positive_is_nonzero. match goal with |- _ = (?a + ?X) / ?D => transitivity ((a + X mod D + D * (X / D)) / D); [| rewrite (Z.div_mod'' X D) at 3; f_equal; auto; ring] @@ -279,7 +279,7 @@ Module Columns. with (fun i s a => compact_digit i (s :: a)). apply mapi_with'_linvariant; [|tauto]. - + clear n inp. intros until 0. intros Hst Hys [Hmod Hdiv]. pose proof (weight_positive n). pose proof (weight_divides n). autorewrite with push_basesystem_eval. @@ -292,8 +292,8 @@ Module Columns. | _ => rewrite map_left_append | _ => rewrite B.Positional.eval_left_append | _ => rewrite weight_0, ?Z.div_1_r, ?Z.mod_1_r - | _ => rewrite Hdiv - | _ => rewrite Hmod + | _ => rewrite Hdiv + | _ => rewrite Hmod | _ => progress subst | _ => progress autorewrite with natsimplify cancel_pair push_basesystem_eval | _ => solve [split; ring_simplify; f_equal; ring] @@ -424,7 +424,7 @@ Module Columns. (fun nq => B.Positional.to_associational_cps weight nq (fun Q => from_associational_cps weight n (P++Q) (fun R => compact_cps (div:=div) (modulo:=modulo) (add_get_carry:=add_get_carry) weight R f)))). - + End Wrappers. End Columns. Hint Unfold @@ -491,8 +491,8 @@ Section Freeze. Qed. Hint Rewrite @eval_conditional_add using (omega || assumption) : push_basesystem_eval. - - + + (* The input to [freeze] should be less than 2*m (this can probably be accomplished by a single carry_reduce step, for most moduli). @@ -552,7 +552,7 @@ Section Freeze. by (pose proof (Z.div_small (y - (s-c)) s); omega). f_equal. ring. } Qed. - + Lemma eval_freeze {n} c mask m p (n_nonzero:n<>0%nat) (Hc : 0 < B.Associational.eval c < weight n) @@ -589,7 +589,7 @@ Section Freeze. Qed. End Freeze. - + (* (* Just some pretty-printing *) Local Notation "fst~ a" := (let (x,_) := a in x) (at level 40, only printing). diff --git a/src/Curves/Edwards/Pre.v b/src/Curves/Edwards/Pre.v index 244acc9b5..9f5d5cfab 100644 --- a/src/Curves/Edwards/Pre.v +++ b/src/Curves/Edwards/Pre.v @@ -43,4 +43,4 @@ Section Edwards. Lemma onCurve_add : onCurve ((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)). Proof using Type*. pose proof denominator_nonzero. Field.fsatz. Qed. End Addition. -End Edwards. \ No newline at end of file +End Edwards. diff --git a/src/Curves/Montgomery/Affine.v b/src/Curves/Montgomery/Affine.v index 70e8a3f6f..bfd7dce60 100644 --- a/src/Curves/Montgomery/Affine.v +++ b/src/Curves/Montgomery/Affine.v @@ -62,4 +62,4 @@ Module M. Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed. End MontgomeryWeierstrass. End MontgomeryCurve. -End M. \ No newline at end of file +End M. diff --git a/src/Curves/Montgomery/AffineInstances.v b/src/Curves/Montgomery/AffineInstances.v index ef5ccd578..049a7695b 100644 --- a/src/Curves/Montgomery/AffineInstances.v +++ b/src/Curves/Montgomery/AffineInstances.v @@ -19,7 +19,7 @@ Module M. Local Notation "0" := Fzero. Local Notation "1" := Fone. Local Notation "4" := (1+1+1+1). - + Global Instance MontgomeryWeierstrassIsomorphism {a b: F} (b_nonzero : b <> 0) @@ -40,7 +40,7 @@ Module M. (M.add(char_ge_3:=char_ge_3)(b_nonzero:=b_nonzero)) M.zero (M.opp(b_nonzero:=b_nonzero)) - + (M.of_Weierstrass(Haw:=reflexivity _)(Hbw:=reflexivity _)(b_nonzero:=b_nonzero)) (M.to_Weierstrass(Haw:=reflexivity _)(Hbw:=reflexivity _)(b_nonzero:=b_nonzero)). Proof. diff --git a/src/Curves/Montgomery/AffineProofs.v b/src/Curves/Montgomery/AffineProofs.v index 4601c3b66..588605c35 100644 --- a/src/Curves/Montgomery/AffineProofs.v +++ b/src/Curves/Montgomery/AffineProofs.v @@ -13,7 +13,7 @@ Module M. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq}. - + Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Infix "+" := Fadd. Local Infix "*" := Fmul. Local Infix "-" := Fsub. Local Infix "/" := Fdiv. @@ -74,7 +74,7 @@ Module M. (M.add(char_ge_3:=_3)(b_nonzero:=_4)) M.zero (M.opp(b_nonzero:=_7)) - + (M.of_Weierstrass(Haw:=Haw)(Hbw:=Hbw)(b_nonzero:=_5)) (M.to_Weierstrass(Haw:=Haw)(Hbw:=Hbw)(b_nonzero:=_6)). Proof. diff --git a/src/Curves/Weierstrass/Affine.v b/src/Curves/Weierstrass/Affine.v index 3a48bf998..cdcb1bec7 100644 --- a/src/Curves/Weierstrass/Affine.v +++ b/src/Curves/Weierstrass/Affine.v @@ -17,4 +17,4 @@ Module W. cbv [W.coordinates]; break_match; trivial; fsatz. Qed. End W. -End W. \ No newline at end of file +End W. diff --git a/src/Curves/Weierstrass/AffineProofs.v b/src/Curves/Weierstrass/AffineProofs.v index 3401d7b31..2faac22eb 100644 --- a/src/Curves/Weierstrass/AffineProofs.v +++ b/src/Curves/Weierstrass/AffineProofs.v @@ -35,7 +35,7 @@ Module W. {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12%positive} (* FIXME: shouldn't need we need 4, not 12? *) {discriminant_nonzero:id(4*a*a*a + 27*b*b <> 0)} : commutative_group(eq:=W.eq(a:=a)(b:=b))(op:=W.add(char_ge_3:=char_ge_3))(id:=W.zero)(inv:=W.opp). - Proof using Type. + Proof using Type. Time cbv [W.opp W.eq W.zero W.add W.coordinates proj1_sig]; repeat match goal with diff --git a/src/LegacyArithmetic/BaseSystem.v b/src/LegacyArithmetic/BaseSystem.v index a54bc483f..3f426e98b 100644 --- a/src/LegacyArithmetic/BaseSystem.v +++ b/src/LegacyArithmetic/BaseSystem.v @@ -36,4 +36,4 @@ Section BaseSystem. Definition decode' bs u := fold_right accumulate 0 (combine u bs). Definition decode := decode' base. Definition mul_each u := map (Z.mul u). -End BaseSystem. \ No newline at end of file +End BaseSystem. diff --git a/src/LegacyArithmetic/BaseSystemProofs.v b/src/LegacyArithmetic/BaseSystemProofs.v index 9a06109d1..b87df814d 100644 --- a/src/LegacyArithmetic/BaseSystemProofs.v +++ b/src/LegacyArithmetic/BaseSystemProofs.v @@ -130,4 +130,4 @@ Section BaseSystemProofs. rewrite plus_0_r in *; congruence); simpl in HH; congruence. } Qed. -End BaseSystemProofs. \ No newline at end of file +End BaseSystemProofs. diff --git a/src/LegacyArithmetic/Pow2BaseProofs.v b/src/LegacyArithmetic/Pow2BaseProofs.v index 681f0b0a9..35540f39a 100644 --- a/src/LegacyArithmetic/Pow2BaseProofs.v +++ b/src/LegacyArithmetic/Pow2BaseProofs.v @@ -552,4 +552,4 @@ Section UniformBase. rewrite decode_shift_app by auto using uniform_limb_widths_nonneg. reflexivity. Qed. -End UniformBase. \ No newline at end of file +End UniformBase. diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index 83e5645d5..9cde8d004 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -52,4 +52,4 @@ End E. Delimit Scope E_scope with E. Infix "=" := E.eq : E_scope. Infix "+" := E.add : E_scope. -Infix "*" := E.mul : E_scope. \ No newline at end of file +Infix "*" := E.mul : E_scope. diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index b8526bb0e..56d5c1bf0 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -54,11 +54,11 @@ Section Ed25519. Local Instance char_gt_e : (* TODO: prove this in PrimeFieldTheorems *) @Ring.char_ge (F.F q) (@eq (F.F q)) (F.of_Z q BinNums.Z0) - (F.of_Z q (BinNums.Zpos BinNums.xH)) (@F.opp q) + (F.of_Z q (BinNums.Zpos BinNums.xH)) (@F.opp q) (@F.add q) (@F.sub q) (@F.mul q) (BinNat.N.succ_pos BinNat.N.two). Proof. intros p ?. edestruct (fun p:p = (BinNat.N.succ_pos BinNat.N.zero) \/ p = (BinNat.N.succ_pos BinNat.N.one) => p); subst. - { admit. (* + { admit. (* p : BinNums.positive H : BinPos.Pos.le p (BinNat.N.succ_pos BinNat.N.one) ============================ @@ -89,7 +89,7 @@ Section Ed25519. (l:=l) (b:=b) (n:=n) (c:=c) (Eenc:=Eenc) (Senc:=Senc) (H:=SHA512). Proof using Type. - split; + split; match goal with | |- ?P => match goal with [H:P|-_] => exact H end (* COQBUG: https://coq.inria.fr/bugs/show_bug.cgi?id=5366 *) | _ => exact _ diff --git a/src/Spec/Test/X25519.v b/src/Spec/Test/X25519.v index 15ca468c1..a4fed8dd4 100644 --- a/src/Spec/Test/X25519.v +++ b/src/Spec/Test/X25519.v @@ -19,4 +19,4 @@ Proof. vm_decide_no_check. Qed. Example testvector_two : F.to_Z (monty 35156891815674817266734212754503633747128614016119564763269015315466259359304%N (F.of_Z _ 8883857351183929894090759386610649319417338800022198945255395922347792736741%Z)) = 39566196721700740701373067725336211924689549479508623342842086701180565506965%Z. -Proof. vm_decide_no_check. Qed. \ No newline at end of file +Proof. vm_decide_no_check. Qed. diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v index fc7c64198..9a3a9185d 100644 --- a/src/Spec/WeierstrassCurve.v +++ b/src/Spec/WeierstrassCurve.v @@ -41,7 +41,7 @@ Module W. Program Definition zero : point := ∞. Local Notation "0" := Fzero. Local Notation "1" := Fone. - Local Notation "2" := (1+1). Local Notation "3" := (1+2). + Local Notation "2" := (1+1). Local Notation "3" := (1+2). Program Definition add (P1 P2:point) : point := match coordinates P1, coordinates P2 return F*F+∞ with diff --git a/src/Specific/ArithmeticSynthesisTest.v b/src/Specific/ArithmeticSynthesisTest.v index 438f8305e..d9e801a0c 100644 --- a/src/Specific/ArithmeticSynthesisTest.v +++ b/src/Specific/ArithmeticSynthesisTest.v @@ -254,7 +254,7 @@ Section Ops51. Hint Opaque freeze : uncps. Hint Rewrite freeze_id : uncps. - + Definition freeze_sig : {freeze : (Z^sz -> Z^sz)%type | forall a : Z^sz, @@ -281,7 +281,7 @@ Section Ops51. cbv - [runtime_opp runtime_add runtime_mul runtime_shr runtime_and Let_In Z.add_get_carry Z.zselect]. reflexivity. Defined. - + Definition ring_51 := (Ring.ring_by_isomorphism (F := F m) diff --git a/src/Util/CPSUtil.v b/src/Util/CPSUtil.v index c09edc891..41b21feb7 100644 --- a/src/Util/CPSUtil.v +++ b/src/Util/CPSUtil.v @@ -288,4 +288,4 @@ Module Tuple. End Tuple. Hint Rewrite @Tuple.map_cps_correct : uncps. Hint Rewrite @Tuple.mapi_with_cps_correct @Tuple.mapi_with'_cps_correct - using (intros; autorewrite with uncps; auto): uncps. \ No newline at end of file + using (intros; autorewrite with uncps; auto): uncps. diff --git a/src/Util/Factorize.v b/src/Util/Factorize.v index 8ccb7d119..12893cd75 100644 --- a/src/Util/Factorize.v +++ b/src/Util/Factorize.v @@ -70,4 +70,4 @@ Lemma product_factorize_or_fail (n:N) (factors:list N) (H:Logic.eq (factorize_or_fail n) (Some factors)) : Logic.eq (List.fold_right N.mul 1%N factors) n. Proof. cbv [factorize_or_fail] in H; destruct ((fold_right N.mul 1 (factorize n) =? n)%N) eqn:?; - try apply N.eqb_eq; congruence. Qed. \ No newline at end of file + try apply N.eqb_eq; congruence. Qed. diff --git a/src/Util/NUtil.v b/src/Util/NUtil.v index 1faa1da95..d76be63aa 100644 --- a/src/Util/NUtil.v +++ b/src/Util/NUtil.v @@ -117,7 +117,7 @@ Module N. replace (Z.of_nat 2) with 2%Z by reflexivity. omega. Qed. - + Let ZNWord sz x := Word.NToWord sz (BinInt.Z.to_N x). Lemma combine_ZNWord : forall sz1 sz2 z1 z2, (0 <= Z.of_nat sz1)%Z -> diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index 2ccb0455f..74fe96d6b 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -304,4 +304,4 @@ 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 +Qed. diff --git a/src/Util/Relations.v b/src/Util/Relations.v index 7dc654ec3..d6b63b38f 100644 --- a/src/Util/Relations.v +++ b/src/Util/Relations.v @@ -56,4 +56,4 @@ Global Instance Symmetric_not {T:Type} (R:T->T->Prop) {SymmetricR:Symmetric R} : Symmetric (fun a b => not (R a b)). Proof. cbv [Symmetric] in *; repeat intro; eauto. Qed. -Lemma not_exfalso (P:Prop) (H:P->False) : not P. auto with nocore. Qed. \ No newline at end of file +Lemma not_exfalso (P:Prop) (H:P->False) : not P. auto with nocore. Qed. diff --git a/src/Util/ZUtil/Zselect.v b/src/Util/ZUtil/Zselect.v index 0166ce6f4..fa9235a0b 100644 --- a/src/Util/ZUtil/Zselect.v +++ b/src/Util/ZUtil/Zselect.v @@ -13,4 +13,4 @@ Module Z. try reflexivity; try discriminate. rewrite <-Z.eqb_neq in *; congruence. Qed. -End Z. \ No newline at end of file +End Z. -- cgit v1.2.3