From 7488682db4cf259e0bb0c886e13301c32a2eeaa2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 2 Jun 2017 00:01:35 -0400 Subject: Don't rely on autogenerated names This fixes all of the private-names warnings emitted by compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus the ones in coqprime, which I didn't touch). --- src/Algebra/Field.v | 6 +- src/Algebra/Monoid.v | 4 +- src/Algebra/Ring.v | 27 ++-- src/Algebra/ScalarMult.v | 13 +- src/Arithmetic/Core.v | 14 +- src/Arithmetic/ModularArithmeticPre.v | 6 +- src/Arithmetic/ModularArithmeticTheorems.v | 23 ++- src/Arithmetic/PrimeFieldTheorems.v | 8 +- src/Arithmetic/Saturated.v | 8 +- src/Compilers/CommonSubexpressionEliminationWf.v | 4 +- src/Compilers/Equality.v | 4 +- src/Compilers/MapCastByDeBruijnInterp.v | 1 + src/Compilers/MapCastByDeBruijnWf.v | 1 + src/Compilers/Named/ContextProperties/NameUtil.v | 10 +- src/Compilers/Named/ContextProperties/Proper.v | 25 ++-- src/Compilers/Named/NameUtilProperties.v | 2 +- src/Compilers/TestCase.v | 6 +- src/Compilers/Z/ArithmeticSimplifierWf.v | 11 +- src/Compilers/Z/Bounds/Interpretation.v | 2 +- src/Curves/Edwards/AffineProofs.v | 7 +- src/Curves/Edwards/XYZT.v | 7 +- src/Curves/Montgomery/Affine.v | 7 +- src/Curves/Weierstrass/Projective.v | 7 +- src/LegacyArithmetic/BaseSystemProofs.v | 3 +- src/LegacyArithmetic/Double/Proofs/Decode.v | 20 +-- .../Double/Proofs/RippleCarryAddSub.v | 22 +-- src/LegacyArithmetic/InterfaceProofs.v | 5 +- src/LegacyArithmetic/Pow2BaseProofs.v | 37 ++--- src/Primitives/EdDSARepChange.v | 2 +- src/Primitives/MxDHRepChange.v | 2 +- src/Spec/CompleteEdwardsCurve.v | 2 +- src/Specific/ArithmeticSynthesisTest.v | 14 +- src/Specific/ArithmeticSynthesisTest130.v | 10 +- src/Specific/IntegrationTestFreeze.v | 2 +- src/Specific/IntegrationTestLadderstep.v | 2 +- src/Specific/IntegrationTestLadderstep130.v | 2 +- src/Specific/IntegrationTestMul.v | 2 +- src/Specific/IntegrationTestSquare.v | 2 +- src/Specific/IntegrationTestSub.v | 2 +- src/Util/AdditionChainExponentiation.v | 6 +- src/Util/CPSUtil.v | 14 +- src/Util/Decidable.v | 11 +- src/Util/Equality.v | 3 +- src/Util/FixedWordSizesEquality.v | 9 +- src/Util/ForLoop/InvariantFramework.v | 2 +- src/Util/ForLoop/Unrolling.v | 2 +- src/Util/HList.v | 7 +- src/Util/IterAssocOp.v | 11 +- src/Util/ListUtil.v | 157 +++++++++++---------- src/Util/NUtil.v | 6 +- src/Util/NatUtil.v | 14 +- src/Util/NumTheoryUtil.v | 30 ++-- src/Util/Relations.v | 3 +- src/Util/Sum.v | 8 +- src/Util/Tuple.v | 44 +++--- src/Util/WordUtil.v | 91 ++++++------ src/Util/ZUtil.v | 72 +++++----- src/Util/ZUtil/Land.v | 2 +- src/Util/ZUtil/Modulo.v | 28 ++-- src/Util/ZUtil/Testbit.v | 8 +- 60 files changed, 463 insertions(+), 397 deletions(-) (limited to 'src') diff --git a/src/Algebra/Field.v b/src/Algebra/Field.v index b5b65f161..d46f10190 100644 --- a/src/Algebra/Field.v +++ b/src/Algebra/Field.v @@ -19,7 +19,7 @@ Section Field. Lemma left_inv_unique x ix : ix * x = one -> ix = inv x. Proof using Type*. intro Hix. - assert (ix*x*inv x = inv x). + assert (H0 : ix*x*inv x = inv x). - rewrite Hix, left_identity; reflexivity. - rewrite <-associative, right_multiplicative_inverse, right_identity in H0; trivial. intro eq_x_0. rewrite eq_x_0, Ring.mul_0_r in Hix. @@ -39,8 +39,8 @@ Section Field. Lemma mul_cancel_l_iff : forall x y, y <> 0 -> (x * y = y <-> x = one). Proof using Type*. - intros. - split; intros. + intros x y H0. + split; intros H1. + rewrite <-(right_multiplicative_inverse y) by assumption. rewrite <-H1 at 1; rewrite <-associative. rewrite right_multiplicative_inverse by assumption. diff --git a/src/Algebra/Monoid.v b/src/Algebra/Monoid.v index e5755b6f0..aa30865c3 100644 --- a/src/Algebra/Monoid.v +++ b/src/Algebra/Monoid.v @@ -12,7 +12,7 @@ Section Monoid. Lemma cancel_right z iz (Hinv:op z iz = id) : forall x y, x * z = y * z <-> x = y. Proof using Type*. - split; intros. + intros x y; split; intro. { assert (op (op x z) iz = op (op y z) iz) as Hcut by (rewrite_hyp ->!*; reflexivity). rewrite <-associative in Hcut. rewrite <-!associative, !Hinv, !right_identity in Hcut; exact Hcut. } @@ -22,7 +22,7 @@ Section Monoid. Lemma cancel_left z iz (Hinv:op iz z = id) : forall x y, z * x = z * y <-> x = y. Proof using Type*. - split; intros. + intros x y; split; intros. { assert (op iz (op z x) = op iz (op z y)) as Hcut by (rewrite_hyp ->!*; reflexivity). rewrite !associative, !Hinv, !left_identity in Hcut; exact Hcut. } { rewrite_hyp ->!*; reflexivity. } diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v index 2e3bcba58..bf45155c8 100644 --- a/src/Algebra/Ring.v +++ b/src/Algebra/Ring.v @@ -4,6 +4,7 @@ Require Import Coq.Classes.Morphisms. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.OnSubterms. Require Import Crypto.Util.Tactics.Revert. +Require Import Crypto.Util.Tactics.RewriteHyp. Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Group Crypto.Algebra.Monoid. Require Coq.ZArith.ZArith Coq.PArith.PArith. @@ -16,7 +17,7 @@ Section Ring. Lemma mul_0_l : forall x, 0 * x = 0. Proof using Type*. - intros. + intros x. assert (0*x = 0*x) as Hx by reflexivity. rewrite <-(right_identity 0), right_distributive in Hx at 1. assert (0*x + 0*x - 0*x = 0*x - 0*x) as Hxx by (rewrite Hx; reflexivity). @@ -25,7 +26,7 @@ Section Ring. Lemma mul_0_r : forall x, x * 0 = 0. Proof using Type*. - intros. + intros x. assert (x*0 = x*0) as Hx by reflexivity. rewrite <-(left_identity 0), left_distributive in Hx at 1. assert (opp (x*0) + (x*0 + x*0) = opp (x*0) + x*0) as Hxx by (rewrite Hx; reflexivity). @@ -331,7 +332,7 @@ Section of_Z. Lemma of_Z_sub_1_r : forall x, of_Z (Z.sub x 1) = Rsub (of_Z x) Rone. Proof using Type*. - induction x. + induction x as [|p|]. { simpl; rewrite ring_sub_definition, !left_identity; reflexivity. } { case_eq (1 ?= p)%positive; intros; @@ -362,19 +363,27 @@ Section of_Z. Lemma of_Z_add : forall a b, of_Z (Z.add a b) = Radd (of_Z a) (of_Z b). Proof using Type*. - intros. + intros a b. let x := match goal with |- ?x => x end in let f := match (eval pattern b in x) with ?f _ => f end in apply (Z.peano_ind f); intros. { rewrite !right_identity. reflexivity. } - { replace (a + Z.succ x) with ((a + x) + 1) by ring. + { match goal with + | [ |- context[?a + Z.succ ?x'] ] + => rename x' into x + end. + replace (a + Z.succ x) with ((a + x) + 1) by ring. replace (Z.succ x) with (x+1) by ring. - rewrite !of_Z_add_1_r, H. + rewrite !of_Z_add_1_r; rewrite_hyp *. rewrite associative; reflexivity. } - { replace (a + Z.pred x) with ((a+x)-1) + { match goal with + | [ |- context[?a + Z.pred ?x'] ] + => rename x' into x + end. + replace (a + Z.pred x) with ((a+x)-1) by (rewrite <-Z.sub_1_r; ring). replace (Z.pred x) with (x-1) by apply Z.sub_1_r. - rewrite !of_Z_sub_1_r, H. + rewrite !of_Z_sub_1_r; rewrite_hyp *. rewrite !ring_sub_definition. rewrite associative; reflexivity. } Qed. @@ -382,7 +391,7 @@ Section of_Z. Lemma of_Z_mul : forall a b, of_Z (Z.mul a b) = Rmul (of_Z a) (of_Z b). Proof using Type*. - intros. + intros a b. let x := match goal with |- ?x => x end in let f := match (eval pattern b in x) with ?f _ => f end in apply (Z.peano_ind f); intros until 0; try intro IHb. diff --git a/src/Algebra/ScalarMult.v b/src/Algebra/ScalarMult.v index 034ed4d4c..99c1f6bbf 100644 --- a/src/Algebra/ScalarMult.v +++ b/src/Algebra/ScalarMult.v @@ -36,8 +36,7 @@ Section ScalarMultProperties. Lemma scalarmult_ext : forall n P, mul n P = scalarmult_ref n P. Proof using Type*. - - induction n; simpl @scalarmult_ref; intros; rewrite <-?IHn; (apply scalarmult_0_l || apply scalarmult_S_l). + induction n as [|n IHn]; simpl @scalarmult_ref; intros; rewrite <-?IHn; (apply scalarmult_0_l || apply scalarmult_S_l). Qed. Lemma scalarmult_1_l : forall P, 1*P = P. @@ -45,16 +44,16 @@ Section ScalarMultProperties. Lemma scalarmult_add_l : forall (n m:nat) (P:G), ((n + m)%nat * P = n * P + m * P). Proof using Type*. - induction n; intros; + induction n as [|n IHn]; intros; rewrite ?scalarmult_0_l, ?scalarmult_S_l, ?plus_Sn_m, ?plus_O_n, ?scalarmult_S_l, ?left_identity, <-?associative, <-?IHn; reflexivity. Qed. Lemma scalarmult_zero_r : forall m, m * zero = zero. - Proof using Type*. induction m; rewrite ?scalarmult_S_l, ?scalarmult_0_l, ?left_identity, ?IHm; try reflexivity. Qed. + Proof using Type*. induction m as [|? IHm]; rewrite ?scalarmult_S_l, ?scalarmult_0_l, ?left_identity, ?IHm; try reflexivity. Qed. Lemma scalarmult_assoc : forall (n m : nat) P, n * (m * P) = (m * n)%nat * P. Proof using Type*. - induction n; intros. + induction n as [|n IHn]; intros. { rewrite <-mult_n_O, !scalarmult_0_l. reflexivity. } { rewrite scalarmult_S_l, <-mult_n_Sm, <-Plus.plus_comm, scalarmult_add_l. rewrite IHn. reflexivity. } @@ -65,7 +64,7 @@ Section ScalarMultProperties. Lemma scalarmult_mod_order : forall l B, l <> 0%nat -> l*B = zero -> forall n, n mod l * B = n * B. Proof using Type*. - intros ? ? Hnz Hmod ?. + intros l B Hnz Hmod n. rewrite (NPeano.Nat.div_mod n l Hnz) at 2. rewrite scalarmult_add_l, scalarmult_times_order, left_identity by auto. reflexivity. Qed. @@ -83,7 +82,7 @@ Section ScalarMultHomomorphism. Lemma homomorphism_scalarmult : forall n P, phi (MUL n P) = mul n (phi P). Proof using Type*. setoid_rewrite scalarmult_ext. - induction n; intros; simpl; rewrite ?Monoid.homomorphism, ?IHn; easy. + induction n as [|n IHn]; intros; simpl; rewrite ?Monoid.homomorphism, ?IHn; easy. Qed. End ScalarMultHomomorphism. diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index d651514ad..7842c1b85 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -358,7 +358,7 @@ Module B. Lemma split_cps_id s p: forall {T} f, @split_cps s p T f = f (split s p). Proof. - induction p; + induction p as [|?? IHp]; repeat match goal with | _ => rewrite IHp | _ => progress (cbv [split]; prove_id) @@ -525,9 +525,9 @@ Module B. Proof using Type. cbv [eval Associational.eval to_associational_cps zeros]. pose proof (seq_length n 0). generalize dependent (seq 0 n). - intro xs; revert n; induction xs; intros; + intro xs; revert n; induction xs as [|?? IHxs]; intros n H; [autorewrite with uncps; reflexivity|]. - intros; destruct n; [distr_length|]. + destruct n as [|n]; [distr_length|]. specialize (IHxs n). autorewrite with uncps in *. rewrite !@Tuple.to_list_repeat in *. simpl List.repeat. rewrite map_cons, combine_cons, map_cons. @@ -835,7 +835,7 @@ Module B. eval wt (Tuple.left_append (n:=n) x xs) = wt n * x + eval wt xs. Proof. - induction n; intros; try destruct xs; + induction n as [|n IHn]; intros wt x xs; try destruct xs; unfold Tuple.left_append; fold @Tuple.left_append; autorewrite with push_basesystem_eval; [ring|]. rewrite (Tuple.subst_append xs), Tuple.hd_append, Tuple.tl_append. @@ -846,8 +846,8 @@ Module B. Lemma eval_wt_equiv {n} :forall wta wtb (x:tuple Z n), (forall i, wta i = wtb i) -> eval wta x = eval wtb x. Proof. - destruct n; [reflexivity|]. - induction n; intros; [rewrite !eval_single, H; reflexivity|]. + destruct n as [|n]; [reflexivity|]. + induction n as [|n IHn]; intros wta wtb x H; [rewrite !eval_single, H; reflexivity|]. simpl tuple in *; destruct x. change (t, z) with (Tuple.append (n:=S n) z t). rewrite !eval_step. rewrite (H 0%nat). apply Group.cancel_left. @@ -879,7 +879,7 @@ Module B. Lemma map_and_0 {n} (p:tuple Z n) : Tuple.map (Z.land 0) p = zeros n. Proof. - induction n; [destruct p; reflexivity | ]. + induction n as [|n IHn]; [destruct p; reflexivity | ]. rewrite (Tuple.subst_append p), Tuple.map_append, Z.land_0_l, IHn. reflexivity. Qed. diff --git a/src/Arithmetic/ModularArithmeticPre.v b/src/Arithmetic/ModularArithmeticPre.v index 3063d3a51..ae27b290f 100644 --- a/src/Arithmetic/ModularArithmeticPre.v +++ b/src/Arithmetic/ModularArithmeticPre.v @@ -60,7 +60,7 @@ Qed. Lemma powmod_Zpow_mod : forall m a n, powmod m a n = (a^Z.of_N n) mod m. Proof. - induction n using N.peano_ind; [auto|]. + induction n as [|n IHn] using N.peano_ind; [auto|]. rewrite <-N.add_1_l. rewrite powmod_1plus. rewrite IHn. @@ -76,7 +76,7 @@ Local Obligation Tactic := idtac. Program Definition pow_impl_sig {m} (a:{z : Z | z = z mod m}) (x:N) : {z : Z | z = z mod m} := powmod m (proj1_sig a) x. Next Obligation. - intros; destruct x; [simpl; rewrite Zmod_mod; reflexivity|]. + intros m a x; destruct x; [simpl; rewrite Zmod_mod; reflexivity|]. rewrite N_pos_1plus. rewrite powmod_1plus. rewrite Zmod_mod; reflexivity. @@ -122,7 +122,7 @@ Program Definition inv_impl {m : BinNums.Z} : exist (fun z : BinNums.Z => z = z mod m) (1 mod m) (Z_mod_mod 1 m))} := mod_inv_sig. Next Obligation. - split. + intros m; split. { apply exist_reduced_eq; rewrite Zmod_0_l; reflexivity. } intros Hm [a pfa] Ha'. apply exist_reduced_eq. assert (Hm':0 <= m - 2) by (pose proof prime_ge_2 m Hm; omega). diff --git a/src/Arithmetic/ModularArithmeticTheorems.v b/src/Arithmetic/ModularArithmeticTheorems.v index 8f9277f35..77186674f 100644 --- a/src/Arithmetic/ModularArithmeticTheorems.v +++ b/src/Arithmetic/ModularArithmeticTheorems.v @@ -104,8 +104,7 @@ Module F. Lemma of_Z_pow x n : F.of_Z _ x ^ n = F.of_Z _ (x ^ (Z.of_N n) mod m) :> F m. Proof using Type. - intros. - induction n using N.peano_ind; + induction n as [|n IHn] using N.peano_ind; destruct (pow_spec (F.of_Z m x)) as [pow_0 pow_succ] . { rewrite pow_0. unwrap_F; trivial. @@ -122,9 +121,9 @@ Module F. Lemma to_Z_pow : forall (x : F m) n, F.to_Z (x ^ n)%F = (F.to_Z x ^ Z.of_N n mod m)%Z. Proof using Type. - intros. + intros x n. symmetry. - induction n using N.peano_ind; + induction n as [|n IHn] using N.peano_ind; destruct (pow_spec x) as [pow_0 pow_succ] . { rewrite pow_0, Z.pow_0_r; auto. } { @@ -209,12 +208,12 @@ Module F. Lemma pow_pow_N (x : F m) : forall (n : N), (x ^ id n)%F = pow_N 1%F F.mul x n. Proof using Type. - destruct (pow_spec x) as [HO HS]; intros. - destruct n; auto; unfold id. + destruct (pow_spec x) as [HO HS]; intros n. + destruct n as [|p]; auto; unfold id. rewrite ModularArithmeticPre.N_pos_1plus at 1. rewrite HS. simpl. - induction p using Pos.peano_ind. + induction p as [|p IHp] using Pos.peano_ind. - simpl. rewrite HO. apply Algebra.Hierarchy.right_identity. - rewrite (@pow_pos_succ (F m) (@F.mul m) eq _ _ associative x). rewrite <-IHp, Pos.pred_N_succ, ModularArithmeticPre.N_pos_1plus, HS. @@ -229,7 +228,7 @@ Module F. let '(q, r) := (Z.quotrem (F.to_Z a) (F.to_Z b)) in (F.of_Z _ q , F.of_Z _ r). Lemma div_theory : div_theory eq (@F.add m) (@F.mul m) (@id _) quotrem. Proof using Type. - constructor; intros; unfold quotrem, id. + constructor; intros a b; unfold quotrem, id. replace (Z.quotrem (F.to_Z a) (F.to_Z b)) with (Z.quot (F.to_Z a) (F.to_Z b), Z.rem (F.to_Z a) (F.to_Z b)) by try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial). @@ -245,13 +244,13 @@ Module F. * to inject the result afterward. *) Lemma ring_morph: ring_morph 0%F 1%F F.add F.mul F.sub F.opp eq 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Z.eqb (F.of_Z m). - Proof using Type. split; intros; unwrap_F; solve [ auto | rewrite (proj1 (Z.eqb_eq x y)); trivial]. Qed. + Proof using Type. split; try intro x; try intro y; unwrap_F; solve [ auto | rewrite (proj1 (Z.eqb_eq x y)); trivial]. Qed. (* Redefine our division theory under the ring morphism *) Lemma morph_div_theory: Ring_theory.div_theory eq Zplus Zmult (F.of_Z m) Z.quotrem. Proof using Type. - split; intros. + split; intros a b. replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b); try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial). unwrap_F; rewrite <- (Z.quot_rem' a b); trivial. @@ -292,7 +291,7 @@ Module F. Global Instance pow_is_scalarmult : is_scalarmult (G:=F m) (eq:=eq) (add:=F.mul) (zero:=1%F) (mul := fun n x => x ^ (N.of_nat n)). Proof using Type. - split; intros; rewrite ?Nat2N.inj_succ, <-?N.add_1_l; + split; [ intro P | intros n P | ]; rewrite ?Nat2N.inj_succ, <-?N.add_1_l; match goal with | [x:F m |- _ ] => solve [destruct (@pow_spec m P); auto] | |- Proper _ _ => solve_proper @@ -317,7 +316,7 @@ Module F. match goal with | |- context [ (_^?n)%F ] => rewrite <-(N2Nat.id n); generalize (N.to_nat n); clear n; - let m := fresh n in intro m + intro n | |- context [ (_^N.of_nat ?n)%F ] => let rw := constr:(scalarmult_ext(zero:=F.of_Z m 1) n) in setoid_rewrite rw (* rewriting moduloa reduction *) diff --git a/src/Arithmetic/PrimeFieldTheorems.v b/src/Arithmetic/PrimeFieldTheorems.v index edab4e065..3d6260bba 100644 --- a/src/Arithmetic/PrimeFieldTheorems.v +++ b/src/Arithmetic/PrimeFieldTheorems.v @@ -66,9 +66,9 @@ Module F. rewrite F.square_iff, <-(euler_criterion (q/2)) by (trivial || omega); reflexivity. Qed. - Global Instance Decidable_square (x:F q) : Decidable (exists y, y*y = x). + Global Instance Decidable_square : forall (x:F q), Decidable (exists y, y*y = x). Proof. - destruct (dec (x = 0)). + intro x; destruct (dec (x = 0)). { left. abstract (exists 0; subst; apply Ring.mul_0_l). } { eapply Decidable_iff_to_impl; [eapply euler_criterion; assumption | exact _]. } Defined. @@ -186,7 +186,7 @@ Module F. Lemma mul_square_sqrt_minus1 : forall x, sqrt_minus1 * x * (sqrt_minus1 * x) = F.opp (x * x). Proof using prime_q sqrt_minus1_valid. - intros. + intros x. transitivity (F.opp 1 * (x * x)); [ | field]. rewrite <-sqrt_minus1_valid. field. @@ -208,7 +208,7 @@ Module F. Lemma sqrt_5mod8_correct : forall x, ((exists y, y*y = x) <-> (sqrt_5mod8 x)*(sqrt_5mod8 x) = x). Proof using Type*. - cbv [sqrt_5mod8]; intros. + cbv [sqrt_5mod8]; intros x. destruct (F.eq_dec x 0). { repeat match goal with diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v index a66c268b0..880adc8f1 100644 --- a/src/Arithmetic/Saturated.v +++ b/src/Arithmetic/Saturated.v @@ -145,7 +145,7 @@ Module Columns. Lemma eval_from_S {n}: forall i (inp : (list Z)^(S n)), eval_from i inp = eval_from (S i) (tl inp) + weight i * sum (hd inp). Proof using Type. - intros; cbv [eval_from]. + intros i inp; cbv [eval_from]. replace inp with (append (hd inp) (tl inp)) by (simpl in *; destruct n; destruct inp; reflexivity). rewrite map_append, B.Positional.eval_step, hd_append, tl_append. @@ -280,7 +280,7 @@ Module Columns. apply mapi_with'_linvariant; [|tauto]. - clear n inp. intros until 0. intros Hst Hys [Hmod Hdiv]. + clear n inp. intros n st x0 xs ys Hst Hys [Hmod Hdiv]. pose proof (weight_positive n). pose proof (weight_divides n). autorewrite with push_basesystem_eval. destruct n; cbv [mapi_with] in *; simpl tuple in *; @@ -338,7 +338,7 @@ Module Columns. List.map sum (update_nth i (cons x) l) = update_nth i (Z.add x) (List.map sum l). Proof using Type. - induction l; intros; destruct i; simpl; rewrite ?IHl; reflexivity. + induction l as [|a l IHl]; intros i x; destruct i; simpl; rewrite ?IHl; reflexivity. Qed. Lemma cons_to_nth_add_to_nth n i x t : @@ -367,7 +367,7 @@ Module Columns. Lemma map_sum_nils n : map sum (nils n) = B.Positional.zeros n. Proof using Type. - cbv [nils B.Positional.zeros]; induction n; [reflexivity|]. + cbv [nils B.Positional.zeros]; induction n as [|n]; [reflexivity|]. change (repeat nil (S n)) with (@nil Z :: repeat nil n). rewrite map_repeat, sum_nil. reflexivity. Qed. diff --git a/src/Compilers/CommonSubexpressionEliminationWf.v b/src/Compilers/CommonSubexpressionEliminationWf.v index 76ed1fa96..8d7bf2727 100644 --- a/src/Compilers/CommonSubexpressionEliminationWf.v +++ b/src/Compilers/CommonSubexpressionEliminationWf.v @@ -99,7 +99,7 @@ Section symbolic. : wff G' (@csef var1 t e1 m1) (@csef var2 t e2 m2). Proof. revert dependent m1; revert m2; revert dependent G'. - induction Hwf; simpl; intros; try constructor; auto. + induction Hwf; simpl; intros G' HGG' m2 m1 Hlen Hm1m2None Hm1m2Some; try constructor; auto. { erewrite wff_norm_symbolize_exprf by eassumption. break_innermost_match; try match goal with @@ -170,7 +170,7 @@ Section symbolic. (Hwf : wff G e1 e2) : wff G (@prepend_prefix var1' t e1 prefix1) (@prepend_prefix var2' t e2 prefix2). Proof. - revert dependent G; revert dependent prefix2; induction prefix1, prefix2; simpl; intros; try congruence. + revert dependent G; revert dependent prefix2; induction prefix1, prefix2; simpl; intros Hlen Hprefix G Hwf; try congruence. { pose proof (Hprefix 0) as H0; specialize (fun n => Hprefix (S n)). destruct_head sigT; simpl in *. specialize (H0 _ _ _ _ eq_refl eq_refl); destruct_head ex; subst; simpl in *. diff --git a/src/Compilers/Equality.v b/src/Compilers/Equality.v index 8e2b44de8..2b54a7892 100644 --- a/src/Compilers/Equality.v +++ b/src/Compilers/Equality.v @@ -51,7 +51,7 @@ Section language. Lemma flat_type_dec_bl X : forall Y, flat_type_beq X Y = true -> X = Y. Proof. clear base_type_code_lb; induction X, Y; t. Defined. Lemma flat_type_dec_lb X : forall Y, X = Y -> flat_type_beq X Y = true. - Proof. clear base_type_code_bl; intros; subst Y; induction X; t. Defined. + Proof. clear base_type_code_bl; intros Y **; subst Y; induction X; t. Defined. Definition flat_type_eq_dec (X Y : flat_type) : {X = Y} + {X <> Y} := match Sumbool.sumbool_of_bool (flat_type_beq X Y) with | left pf => left (flat_type_dec_bl _ _ pf) @@ -65,7 +65,7 @@ Section language. Lemma type_dec_bl X : forall Y, type_beq X Y = true -> X = Y. Proof. clear base_type_code_lb; pose proof flat_type_dec_bl; induction X, Y; t. Defined. Lemma type_dec_lb X : forall Y, X = Y -> type_beq X Y = true. - Proof. clear base_type_code_bl; pose proof flat_type_dec_lb; intros; subst Y; induction X; t. Defined. + Proof. clear base_type_code_bl; pose proof flat_type_dec_lb; intros Y **; subst Y; induction X; t. Defined. Definition type_eq_dec (X Y : type) : {X = Y} + {X <> Y} := match Sumbool.sumbool_of_bool (type_beq X Y) with | left pf => left (type_dec_bl _ _ pf) diff --git a/src/Compilers/MapCastByDeBruijnInterp.v b/src/Compilers/MapCastByDeBruijnInterp.v index 10e09242a..7674e5f0e 100644 --- a/src/Compilers/MapCastByDeBruijnInterp.v +++ b/src/Compilers/MapCastByDeBruijnInterp.v @@ -66,6 +66,7 @@ Section language. then fun pf => left (base_type_code_bl_transparent _ _ pf) else fun pf => right _) eq_refl). { clear -pf base_type_code_lb. + let pf := pf in abstract (intro; erewrite base_type_code_lb in pf by eassumption; congruence). } Defined. diff --git a/src/Compilers/MapCastByDeBruijnWf.v b/src/Compilers/MapCastByDeBruijnWf.v index 7c1e386b5..61a084ee7 100644 --- a/src/Compilers/MapCastByDeBruijnWf.v +++ b/src/Compilers/MapCastByDeBruijnWf.v @@ -64,6 +64,7 @@ Section language. then fun pf => left (base_type_code_bl_transparent _ _ pf) else fun pf => right _) eq_refl). { clear -pf base_type_code_lb. + let pf := pf in abstract (intro; erewrite base_type_code_lb in pf by eassumption; congruence). } Defined. diff --git a/src/Compilers/Named/ContextProperties/NameUtil.v b/src/Compilers/Named/ContextProperties/NameUtil.v index 0bc970357..320d910f0 100644 --- a/src/Compilers/Named/ContextProperties/NameUtil.v +++ b/src/Compilers/Named/ContextProperties/NameUtil.v @@ -47,7 +47,7 @@ Section with_context. : (exists t, @find_Name n T N = Some t) <-> List.In (Some n) (List.firstn (CountLets.count_pairs T) ls). Proof using Type. - revert dependent ls; intro ls; revert ls ls'; induction T; intros; + revert dependent ls; intro ls; revert ls ls'; induction T; intros ls ls' H; [ | | specialize (IHT1 (fst N) ls (snd (split_onames T1 ls))); specialize (IHT2 (snd N) (snd (split_onames T1 ls)) (snd (split_onames (T1 * T2) ls))) ]; repeat first [ misc_oname_t_step @@ -77,7 +77,11 @@ Section with_context. rewrite fst_split_onames_firstn, snd_split_onames_skipn in H. inversion_prod; subst. split; [ split | intros [? ?] ]; eauto using In_firstn, oname_list_unique_specialize. - eapply In_firstn_skipn_split in H; destruct_head' or; eauto; exfalso; eauto. + match goal with + | [ H : List.In (Some _) ?ls |- _ ] + => is_var ls; + eapply In_firstn_skipn_split in H; destruct_head' or; eauto; exfalso; eauto + end. Qed. Lemma split_onames_find_Name_Some_unique @@ -97,7 +101,7 @@ Section with_context. : @find_Name_and_val var' t n T N V None = Some v <-> List.In (existT (fun t => (Name * var' t)%type) t (n, v)) (Wf.flatten_binding_list N V). Proof using Type. - revert dependent ls; intro ls; revert ls ls'; induction T; intros; + revert dependent ls; intro ls; revert ls ls'; induction T; intros ls ls' Hls H; [ | | specialize (IHT1 (fst N) (fst V) ls (snd (split_onames T1 ls))); specialize (IHT2 (snd N) (snd V) (snd (split_onames T1 ls)) (snd (split_onames (T1 * T2) ls))) ]; repeat first [ find_Name_and_val_default_to_None_step diff --git a/src/Compilers/Named/ContextProperties/Proper.v b/src/Compilers/Named/ContextProperties/Proper.v index 48cecde8f..0c583e446 100644 --- a/src/Compilers/Named/ContextProperties/Proper.v +++ b/src/Compilers/Named/ContextProperties/Proper.v @@ -41,15 +41,15 @@ Section with_context. | rewrite lookupb_removeb_different by assumption | solve [ auto ] ]. - Global Instance extendb_Proper {t} : Proper (context_equiv ==> eq ==> eq ==> context_equiv) (@extendb t) | 10. + Global Instance extendb_Proper : forall {t}, Proper (context_equiv ==> eq ==> eq ==> context_equiv) (@extendb t) | 10. Proof. - intros ??? n n0 ???? n' t'; subst n0; subst; proper_t n n' t t'. + intros t ??? n n0 ???? n' t'; subst n0; subst; proper_t n n' t t'. Qed. - Global Instance removeb_Proper {t} : Proper (context_equiv ==> eq ==> context_equiv) (@removeb t) | 10. + Global Instance removeb_Proper : forall {t}, Proper (context_equiv ==> eq ==> context_equiv) (@removeb t) | 10. Proof. - intros ??? n n0 ? n' t'; subst n0; subst; proper_t n n' t t'. + intros t ??? n n0 ? n' t'; subst n0; subst; proper_t n n' t t'. Qed. - Global Instance lookupb_Proper {t} : Proper (context_equiv ==> eq ==> eq) (@lookupb t) | 10. + Global Instance lookupb_Proper : forall {t}, Proper (context_equiv ==> eq ==> eq) (@lookupb t) | 10. Proof. repeat intro; subst; auto. Qed. Local Ltac proper_t2 t := @@ -68,13 +68,14 @@ Section with_context. first [ eapply IHt2; [ eapply IHt1 | .. ]; auto | idtac ] ]. - Global Instance extend_Proper {t} : Proper (context_equiv ==> eq ==> eq ==> context_equiv) (@extend t) | 10. - Proof. proper_t2 t. Qed. - Global Instance remove_Proper {t} : Proper (context_equiv ==> eq ==> context_equiv) (@remove t) | 10. - Proof. proper_t2 t. Qed. - Global Instance lookup_Proper {t} : Proper (context_equiv ==> eq ==> eq) (@lookup t) | 10. + Global Instance extend_Proper : forall {t}, Proper (context_equiv ==> eq ==> eq ==> context_equiv) (@extend t) | 10. + Proof. intro t; proper_t2 t. Qed. + Global Instance remove_Proper : forall {t}, Proper (context_equiv ==> eq ==> context_equiv) (@remove t) | 10. + Proof. intro t; proper_t2 t. Qed. + + Global Instance lookup_Proper : forall {t}, Proper (context_equiv ==> eq ==> eq) (@lookup t) | 10. Proof. - proper_t2 t. + intro t; proper_t2 t. repeat match goal with | [ |- context G[lookup (?A * ?B) ?ctx (?na, ?nb)] ] => let G' := context G[match lookup A ctx na, lookup B ctx nb with @@ -88,7 +89,7 @@ Section with_context. | _ => progress subst | _ => progress inversion_option | _ => reflexivity - | [ H : lookup _ _ _ = ?x, H' : lookup _ _ _ = ?y |- _ ] + | [ IHt2 : Proper _ (lookup t2), H : lookup _ _ _ = ?x, H' : lookup _ _ _ = ?y |- _ ] => assert (x = y) by (rewrite <- H, <- H'; first [ eapply IHt1 | eapply IHt2 ]; (assumption || reflexivity)); clear H H' diff --git a/src/Compilers/Named/NameUtilProperties.v b/src/Compilers/Named/NameUtilProperties.v index d2791a5ea..944d164f2 100644 --- a/src/Compilers/Named/NameUtilProperties.v +++ b/src/Compilers/Named/NameUtilProperties.v @@ -171,7 +171,7 @@ Section language. (t : flat_type base_type_code) (ls : list Name) : fst (split_names t ls) <> None <-> List.length ls >= count_pairs t. Proof using Type. - revert ls; induction t; intros; + revert ls; induction t; intros ls; try solve [ destruct ls; simpl; intuition (omega || congruence) ]. repeat first [ progress simpl in * | progress break_innermost_match_step diff --git a/src/Compilers/TestCase.v b/src/Compilers/TestCase.v index 36774e4e3..e1fb0087a 100644 --- a/src/Compilers/TestCase.v +++ b/src/Compilers/TestCase.v @@ -212,17 +212,17 @@ Module bounds. Definition add_bounded_pf (x y : bounded_pf) : bounded_pf. Proof. exists (map_bounded_f2 plus false (proj1_sig x) (proj1_sig y)). - simpl; abstract (destruct x, y; simpl; omega). + simpl; let x := x in let y := y in abstract (destruct x, y; simpl; omega). Defined. Definition mul_bounded_pf (x y : bounded_pf) : bounded_pf. Proof. exists (map_bounded_f2 mult false (proj1_sig x) (proj1_sig y)). - simpl; abstract (destruct x, y; simpl; nia). + simpl; let x := x in let y := y in abstract (destruct x, y; simpl; nia). Defined. Definition sub_bounded_pf (x y : bounded_pf) : bounded_pf. Proof. exists (map_bounded_f2 minus true (proj1_sig x) (proj1_sig y)). - simpl; abstract (destruct x, y; simpl; omega). + simpl; let x := x in let y := y in abstract (destruct x, y; simpl; omega). Defined. Definition interp_base_type_bounds (v : base_type) : Type := match v with diff --git a/src/Compilers/Z/ArithmeticSimplifierWf.v b/src/Compilers/Z/ArithmeticSimplifierWf.v index ba5dd39cd..56dda81ab 100644 --- a/src/Compilers/Z/ArithmeticSimplifierWf.v +++ b/src/Compilers/Z/ArithmeticSimplifierWf.v @@ -115,7 +115,8 @@ Lemma wff_interp_as_expr_or_const_base {var1 var2 t} {G e1 e2 v1 v2} end. Proof. invert_one_expr e1; intros; break_innermost_match; intros; - try invert_one_expr e2; intros; + try (let e2 := match goal with Hwf : wff ?G ?e1 ?e2 |- _ => e2 end in + invert_one_expr e2); intros; repeat first [ fin_t | progress simpl in * | progress intros @@ -157,7 +158,9 @@ Lemma wff_interp_as_expr_or_const_prod_base {var1 var2 A B} {G e1 e2} {v1 v2 : _ end. Proof. invert_one_expr e1; intros; break_innermost_match; intros; try exact I; - try invert_one_expr e2; intros; break_innermost_match; intros; try exact I; + try (let e2 := match goal with Hwf : wff ?G ?e1 ?e2 |- _ => e2 end in + invert_one_expr e2); + intros; break_innermost_match; intros; try exact I; repeat first [ pret_step | pose_wff_base | break_t_step @@ -206,7 +209,9 @@ Lemma wff_interp_as_expr_or_const_prod3_base {var1 var2 A B C} {G e1 e2} {v1 v2 end. Proof. invert_one_expr e1; intros; break_innermost_match; intros; try exact I; - try invert_one_expr e2; intros; break_innermost_match; intros; try exact I; + try (let e2 := match goal with Hwf : wff ?G ?e1 ?e2 |- _ => e2 end in + invert_one_expr e2); + intros; break_innermost_match; intros; try exact I; repeat first [ pret_step | pose_wff_base | pose_wff_prod diff --git a/src/Compilers/Z/Bounds/Interpretation.v b/src/Compilers/Z/Bounds/Interpretation.v index dc29fe654..882cbde3a 100644 --- a/src/Compilers/Z/Bounds/Interpretation.v +++ b/src/Compilers/Z/Bounds/Interpretation.v @@ -288,7 +288,7 @@ Module Import Bounds. := interp_flat_type_rel_pointwise (@is_bounded_by'). Local Arguments interp_base_type !_ / . - Global Instance dec_eq_interp_flat_type {T} : DecidableRel (@eq (interp_flat_type interp_base_type T)) | 10. + Global Instance dec_eq_interp_flat_type : forall {T}, DecidableRel (@eq (interp_flat_type interp_base_type T)) | 10. Proof. induction T; destruct_head base_type; simpl; exact _. Defined. diff --git a/src/Curves/Edwards/AffineProofs.v b/src/Curves/Edwards/AffineProofs.v index e77e39f50..8e69b78fe 100644 --- a/src/Curves/Edwards/AffineProofs.v +++ b/src/Curves/Edwards/AffineProofs.v @@ -44,7 +44,7 @@ Module E. Local Notation mul := (E.mul(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)). Program Definition opp (P:point) : point := (Fopp (fst P), (snd P)). - Next Obligation. destruct P as [ [??]?]; cbv; fsatz. Qed. + Next Obligation. match goal with P : point |- _ => destruct P as [ [??]?] end; cbv; fsatz. Qed. Ltac t_step := match goal with @@ -203,7 +203,10 @@ Module E. cbv [compress decompress exist_option coordinates] in *; intros. t. intro. - apply (H0 f); [|congruence]. + match goal with + | [ H0 : _ |- False ] + => apply (H0 f); [|congruence] + end. admit. intro. Prod.inversion_prod; subst. rewrite solve_correct in y. diff --git a/src/Curves/Edwards/XYZT.v b/src/Curves/Edwards/XYZT.v index 2b126dfcb..3604e9b2e 100644 --- a/src/Curves/Edwards/XYZT.v +++ b/src/Curves/Edwards/XYZT.v @@ -105,7 +105,12 @@ Module Extended. let Z3 := F*G in (X3, Y3, Z3, T3) end. - Next Obligation. pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig (to_twisted P1)) _ _ (proj2_sig (to_twisted P2))); t. Qed. + Next Obligation. + match goal with + | [ |- match (let (_, _) := coordinates ?P1 in let (_, _) := _ in let (_, _) := _ in let (_, _) := coordinates ?P2 in _) with _ => _ end ] + => pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig (to_twisted P1)) _ _ (proj2_sig (to_twisted P2))) + end; t. + Qed. Global Instance isomorphic_commutative_group_m1 : @Group.isomorphic_commutative_groups diff --git a/src/Curves/Montgomery/Affine.v b/src/Curves/Montgomery/Affine.v index bfd7dce60..2e39c6b6c 100644 --- a/src/Curves/Montgomery/Affine.v +++ b/src/Curves/Montgomery/Affine.v @@ -2,6 +2,7 @@ Require Import Crypto.Algebra.Field. Require Import Crypto.Util.GlobalSettings. Require Import Crypto.Util.Sum Crypto.Util.Prod. Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Spec.MontgomeryCurve Crypto.Spec.WeierstrassCurve. Module M. @@ -30,7 +31,7 @@ Module M. | (x, y) => (x, -y) | ∞ => ∞ end. - Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed. + Next Obligation. Proof. destruct_head @M.point; cbv; break_match; trivial; fsatz. Qed. Local Notation add := (M.add(b_nonzero:=b_nonzero)). Local Notation point := (@M.point F Feq Fadd Fmul a b). @@ -52,14 +53,14 @@ Module M. | (x, y) => ((x + a/3)/b, y/b) | _ => ∞ end. - Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed. + Next Obligation. Proof. destruct_head' @point; cbv; break_match; trivial; fsatz. Qed. Program Definition of_Weierstrass (P:Wpoint) : point := match W.coordinates P return F*F+∞ with | (x,y) => (b*x-a/3, b*y) | _ => ∞ end. - Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed. + Next Obligation. Proof. destruct_head' @Wpoint; cbv; break_match; trivial; fsatz. Qed. End MontgomeryWeierstrass. End MontgomeryCurve. End M. diff --git a/src/Curves/Weierstrass/Projective.v b/src/Curves/Weierstrass/Projective.v index 20866ca5d..3c1fd204d 100644 --- a/src/Curves/Weierstrass/Projective.v +++ b/src/Curves/Weierstrass/Projective.v @@ -123,8 +123,11 @@ Module Projective. end. Next Obligation. Proof. - destruct P as [p ?]; destruct p as [p Z1]; destruct p as [X1 Y1]. - destruct Q as [q ?]; destruct q as [q Z2]; destruct q as [X2 Y2]. + match goal with + | [ |- match (let (_, _) := proj1_sig ?P in let (_, _) := _ in let (_, _) := proj1_sig ?Q in _) with _ => _ end ] + => destruct P as [p ?]; destruct p as [p Z1]; destruct p as [X1 Y1]; + destruct Q as [q ?]; destruct q as [q Z2]; destruct q as [X2 Y2] + end. t. all: try abstract fsatz. (* FIXME: the final fsatz starts requiring 56 <> 0 if diff --git a/src/LegacyArithmetic/BaseSystemProofs.v b/src/LegacyArithmetic/BaseSystemProofs.v index b87df814d..f0f0a80d2 100644 --- a/src/LegacyArithmetic/BaseSystemProofs.v +++ b/src/LegacyArithmetic/BaseSystemProofs.v @@ -122,7 +122,8 @@ Section BaseSystemProofs. end. rewrite (combine_truncate_r vs bs); apply (f_equal2 Z.add); trivial; []. unfold combine; break_match. - { apply (f_equal (@length _)) in Heql; simpl length in Heql; rewrite skipn_length in Heql; omega. } + { let Heql := match goal with H : _ = nil |- _ => H end in + apply (f_equal (@length _)) in Heql; simpl length in Heql; rewrite skipn_length in Heql; omega. } { cbv -[Z.add Z.mul]; ring_simplify; f_equal. assert (HH: nth_error (z0 :: l) 0 = Some z) by ( diff --git a/src/LegacyArithmetic/Double/Proofs/Decode.v b/src/LegacyArithmetic/Double/Proofs/Decode.v index b5b6d6623..1cd5bf06d 100644 --- a/src/LegacyArithmetic/Double/Proofs/Decode.v +++ b/src/LegacyArithmetic/Double/Proofs/Decode.v @@ -145,9 +145,10 @@ Hint Rewrite Hint Rewrite @tuple_decoder_S @tuple_decoder_O @tuple_decoder_m1 using solve [ auto with zarith ] : simpl_tuple_decoder. -Global Instance tuple_decoder_mod {n W} {decode : decoder n W} {k} {isdecode : is_decode decode} (w : tuple W (S (S k))) - : tuple_decoder (k := S k) (fst w) <~= tuple_decoder w mod 2^(S k * n). +Global Instance tuple_decoder_mod : forall {n W} {decode : decoder n W} {k} {isdecode : is_decode decode} (w : tuple W (S (S k))), + tuple_decoder (k := S k) (fst w) <~= tuple_decoder w mod 2^(S k * n). Proof. + intros n W decode k isdecode w. pose proof (snd w). assert (0 <= n) by eauto using decode_exponent_nonnegative. assert (0 <= (S k) * n) by nia. @@ -156,9 +157,10 @@ Proof. reflexivity. Qed. -Global Instance tuple_decoder_div {n W} {decode : decoder n W} {k} {isdecode : is_decode decode} (w : tuple W (S (S k))) - : decode (snd w) <~= tuple_decoder w / 2^(S k * n). +Global Instance tuple_decoder_div : forall {n W} {decode : decoder n W} {k} {isdecode : is_decode decode} (w : tuple W (S (S k))), + decode (snd w) <~= tuple_decoder w / 2^(S k * n). Proof. + intros n W decode k isdecode w. pose proof (snd w). assert (0 <= n) by eauto using decode_exponent_nonnegative. assert (0 <= (S k) * n) by nia. @@ -169,16 +171,18 @@ Proof. reflexivity. Qed. -Global Instance tuple2_decoder_mod {n W} {decode : decoder n W} {isdecode : is_decode decode} (w : tuple W 2) - : decode (fst w) <~= tuple_decoder w mod 2^n. +Global Instance tuple2_decoder_mod : forall {n W} {decode : decoder n W} {isdecode : is_decode decode} (w : tuple W 2), + decode (fst w) <~= tuple_decoder w mod 2^n. Proof. + intros n W decode isdecode w. generalize (@tuple_decoder_mod n W decode 0 isdecode w). autorewrite with simpl_tuple_decoder; trivial. Qed. -Global Instance tuple2_decoder_div {n W} {decode : decoder n W} {isdecode : is_decode decode} (w : tuple W 2) - : decode (snd w) <~= tuple_decoder w / 2^n. +Global Instance tuple2_decoder_div : forall {n W} {decode : decoder n W} {isdecode : is_decode decode} (w : tuple W 2), + decode (snd w) <~= tuple_decoder w / 2^n. Proof. + intros n W decode isdecode w. generalize (@tuple_decoder_div n W decode 0 isdecode w). autorewrite with simpl_tuple_decoder; trivial. Qed. diff --git a/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v b/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v index e703c2e57..d0514db57 100644 --- a/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v +++ b/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v @@ -122,12 +122,13 @@ Section ripple_carry_adc. Proof using Type. apply ripple_carry_tuple_SS. Qed. Local Opaque Z.of_nat. - Global Instance ripple_carry_is_add_with_carry {k} - {isdecode : is_decode decode} - {is_adc : is_add_with_carry adc} - : is_add_with_carry (ripple_carry_adc (k := k) adc). + Global Instance ripple_carry_is_add_with_carry + : forall {k} + {isdecode : is_decode decode} + {is_adc : is_add_with_carry adc}, + is_add_with_carry (ripple_carry_adc (k := k) adc). Proof using Type. - destruct k as [|k]. + destruct k as [|k]; intros isdecode is_adc. { constructor; simpl; intros; autorewrite with zsimplify; reflexivity. } { induction k as [|k IHk]. { cbv [ripple_carry_adc ripple_carry_tuple to_list]. @@ -166,12 +167,13 @@ Section ripple_carry_subc. Proof using Type. apply ripple_carry_tuple_SS. Qed. Local Opaque Z.of_nat. - Global Instance ripple_carry_is_sub_with_carry {k} - {isdecode : is_decode decode} - {is_subc : is_sub_with_carry subc} - : is_sub_with_carry (ripple_carry_subc (k := k) subc). + Global Instance ripple_carry_is_sub_with_carry + : forall {k} + {isdecode : is_decode decode} + {is_subc : is_sub_with_carry subc}, + is_sub_with_carry (ripple_carry_subc (k := k) subc). Proof using Type. - destruct k as [|k]. + destruct k as [|k]; intros isdecode is_subc. { constructor; repeat (intros [] || intro); autorewrite with simpl_tuple_decoder zsimplify; reflexivity. } { induction k as [|k IHk]. { cbv [ripple_carry_subc ripple_carry_tuple to_list]. diff --git a/src/LegacyArithmetic/InterfaceProofs.v b/src/LegacyArithmetic/InterfaceProofs.v index 9ef97fa55..33917e00d 100644 --- a/src/LegacyArithmetic/InterfaceProofs.v +++ b/src/LegacyArithmetic/InterfaceProofs.v @@ -99,8 +99,9 @@ Global Instance decode_proj n W (dec : W -> Z) : @decode n W {| decode := dec |} =~> dec. Proof. reflexivity. Qed. -Global Instance decode_if_bool n W (decode : decoder n W) (b : bool) x y - : decode (if b then x else y) +Global Instance decode_if_bool n W (decode : decoder n W) + : forall (b : bool) x y, + decode (if b then x else y) =~> if b then decode x else decode y. Proof. destruct b; reflexivity. Qed. diff --git a/src/LegacyArithmetic/Pow2BaseProofs.v b/src/LegacyArithmetic/Pow2BaseProofs.v index 35540f39a..b6df85f5c 100644 --- a/src/LegacyArithmetic/Pow2BaseProofs.v +++ b/src/LegacyArithmetic/Pow2BaseProofs.v @@ -73,7 +73,7 @@ Section Pow2BaseProofs. nth_error base (S i) = Some (two_p w * b). Proof using Type. clear limb_widths_nonneg. (* don't use this in the inductive hypothesis *) - induction limb_widths; intros ? ? ? ? nth_err_w nth_err_b; + induction limb_widths; intros i b w ? nth_err_w nth_err_b; unfold base_from_limb_widths in *; fold base_from_limb_widths in *; [rewrite (@nil_length0 Z) in *; omega | ]. simpl in *. @@ -97,7 +97,7 @@ Section Pow2BaseProofs. Lemma nth_error_base : forall i, (i < length limb_widths)%nat -> nth_error base i = Some (two_p (sum_firstn limb_widths i)). Proof using Type*. - induction i; intros. + induction i as [|i IHi]; intros H. + unfold sum_firstn, base_from_limb_widths in *; case_eq limb_widths; try reflexivity. intro lw_nil; rewrite lw_nil, (@nil_length0 Z) in *; omega. + assert (i < length limb_widths)%nat as lt_i_length by omega. @@ -165,6 +165,7 @@ Section Pow2BaseProofs. Z.pow2_mod (nth_default 0 us i) (nth_default 0 lw i) = nth_default 0 us i. Proof using Type. clear. + cbv [bounded]; intros lw us i H H0. repeat match goal with | |- _ => progress (cbv [bounded]; intros) | |- _ => break_if @@ -174,6 +175,7 @@ Section Pow2BaseProofs. end. specialize (H0 i). symmetry. + let n := match goal with n : Z |- _ => n end in rewrite <- (Z.mod_pow2_bits_high (nth_default 0 us i) (nth_default 0 lw i) n); [ rewrite Z.mod_small by omega; reflexivity | ]. split; try omega. @@ -183,15 +185,15 @@ Section Pow2BaseProofs. Lemma bounded_nil_iff : forall us, bounded nil us <-> (forall u, In u us -> u = 0). Proof using Type. clear. - split; cbv [bounded]; intros. - + edestruct (In_nth_error_value us u); try assumption. + intros us; split; cbv [bounded]; [ intros H u H0 | intros H i ]. + + edestruct (In_nth_error_value us u) as [x]; try assumption. specialize (H x). replace u with (nth_default 0 us x) by (auto using nth_error_value_eq_nth_default). rewrite nth_default_nil, Z.pow_0_r in H. omega. + rewrite nth_default_nil, Z.pow_0_r. apply nth_default_preserves_properties; try omega. - intros. + intros x H0. apply H in H0. omega. Qed. @@ -206,7 +208,8 @@ Section Pow2BaseProofs. Lemma digit_select : forall us i, bounded limb_widths us -> nth_default 0 us i = Z.pow2_mod (BaseSystem.decode base us >> sum_firstn limb_widths i) (nth_default 0 limb_widths i). Proof using Type*. - intro; revert limb_widths limb_widths_nonneg; induction us; intros. + intro us; revert limb_widths limb_widths_nonneg; induction us as [|a us IHus]; + intros limb_widths limb_widths_nonneg i H. + rewrite nth_default_nil, BaseSystemProofs.decode_nil, Z.shiftr_0_l, Z.pow2_mod_spec, Z.mod_0_l by (try (apply Z.pow_nonzero; try omega); apply nth_default_preserves_properties; auto; omega). reflexivity. @@ -226,7 +229,7 @@ Section Pow2BaseProofs. rewrite bounded_iff in *. specialize (H 0%nat); rewrite !nth_default_cons in H. rewrite <-Z.lor_shiftl by (auto using in_eq; omega). - apply Z.bits_inj'; intros. + apply Z.bits_inj'; intros n H0. rewrite Z.testbit_pow2_mod by auto using in_eq. break_if. { autorewrite with Ztestbit; break_match; @@ -270,7 +273,7 @@ Section Pow2BaseProofs. bounded limb_widths us -> BaseSystem.decode' base (firstn i us) = Z.pow2_mod (BaseSystem.decode' base us) (sum_firstn limb_widths i). Proof using Type*. - intros; induction i; + intros us i H H0 H1; induction i; repeat match goal with | |- _ => rewrite sum_firstn_0, BaseSystemProofs.decode_nil, Z.pow2_mod_0_r; reflexivity | |- _ => progress distr_length @@ -325,7 +328,7 @@ Section Pow2BaseProofs. sum_firstn limb_widths (length us) <= n -> Z.testbit (BaseSystem.decode base us) n = false. Proof using Type*. - intros. + intros us n H H0 H1. erewrite <-(firstn_all _ us) by reflexivity. auto using testbit_decode_firstn_high. Qed. @@ -336,7 +339,7 @@ Section Pow2BaseProofs. bounded limb_widths us -> 0 <= BaseSystem.decode base us. Proof using Type*. - intros. + intros us H H0. unfold bounded, BaseSystem.decode, BaseSystem.decode' in *; simpl in *. pose 0 as zero. assert (0 <= zero) by reflexivity. @@ -365,7 +368,7 @@ Section Pow2BaseProofs. bounded limb_widths us -> 0 <= BaseSystem.decode base us < upper_bound limb_widths. Proof using Type*. - cbv [upper_bound]; intros. + cbv [upper_bound]; intros us H H0. split. { apply decode_nonneg; auto. } { apply Z.testbit_false_bound; auto; intros. @@ -387,7 +390,7 @@ Section Pow2BaseProofs. Lemma decode_shift : forall us u0, (length (u0 :: us) <= length limb_widths)%nat -> BaseSystem.decode base (u0 :: us) = u0 + ((BaseSystem.decode (base_from_limb_widths (tl limb_widths)) us) << (nth_default 0 limb_widths 0)). Proof using Type*. - intros; etransitivity; [ apply (decode_shift_app (u0::nil)); assumption | ]. + intros us u0 H; etransitivity; [ apply (decode_shift_app (u0::nil)); assumption | ]. transitivity (u0 * 1 + 0 + ((BaseSystem.decode (base_from_limb_widths (tl limb_widths)) us) << (nth_default 0 limb_widths 0 + 0))); [ | autorewrite with zsimplify; reflexivity ]. destruct limb_widths; distr_length; reflexivity. Qed. @@ -437,10 +440,10 @@ Section UniformBase. Lemma bounded_uniform : forall us, (length us <= length limb_widths)%nat -> (bounded limb_widths us <-> (forall u, In u us -> 0 <= u < 2 ^ width)). Proof using Type*. - cbv [bounded]; split; intro A; intros. + cbv [bounded]; intros us H; split; intro A; [ intros u H0 | intros i ]. + let G := fresh "G" in match goal with H : In _ us |- _ => - eapply In_nth in H; destruct H as [? G]; destruct G as [? G]; + eapply In_nth in H; destruct H as [x G]; destruct G as [? G]; rewrite <-nth_default_eq in G; rewrite <-G end. specialize (A x). split; try eapply A. @@ -457,7 +460,7 @@ Section UniformBase. Lemma uniform_limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w. Proof using Type*. - intros. + intros w H. replace w with width by (symmetry; auto). assumption. Qed. @@ -502,7 +505,7 @@ Section UniformBase. Lemma decode_truncate_base : forall us bs, BaseSystem.decode bs us = BaseSystem.decode (firstn (length us) bs) us. Proof using Type. clear. - induction us; intros. + induction us as [|a us IHus]; intros bs. + rewrite !BaseSystemProofs.decode_nil; reflexivity. + distr_length. destruct bs. @@ -517,7 +520,7 @@ Section UniformBase. (n < length xs)%nat -> firstn n xs = firstn n (tl xs). Proof using Type. - intros. + intros A xs n x H H0. erewrite (repeat_spec_eq xs) by first [ eassumption | reflexivity ]. rewrite ListUtil.tl_repeat. autorewrite with push_firstn. diff --git a/src/Primitives/EdDSARepChange.v b/src/Primitives/EdDSARepChange.v index 1ad4611be..1c6282fb9 100644 --- a/src/Primitives/EdDSARepChange.v +++ b/src/Primitives/EdDSARepChange.v @@ -60,7 +60,7 @@ Section EdDSA. Definition verify'_sig : { verify | forall mlen (message:word mlen) (pk:word b) (sig:word (b+b)), verify mlen message pk sig = true <-> valid message pk sig }. Proof. - eexists; intros; set_evars. + eexists; intros mlen message pk sig; set_evars. unfold Spec.EdDSA.valid. setoid_rewrite solve_for_R. setoid_rewrite combine_eq_iff. diff --git a/src/Primitives/MxDHRepChange.v b/src/Primitives/MxDHRepChange.v index 9f0276ef8..eb3df559a 100644 --- a/src/Primitives/MxDHRepChange.v +++ b/src/Primitives/MxDHRepChange.v @@ -100,7 +100,7 @@ Section MxDHRepChange. R (proj (fold_left step xs init)) (fold_left step' xs init'). Proof using Type. generalize dependent init; generalize dependent init'. - induction xs; [solve [eauto]|]. + induction xs as [|?? IHxs]; [solve [eauto]|]. repeat intro; simpl; rewrite IHxs by eauto. apply (_ : Proper ((R ==> eq ==> R) ==> SetoidList.eqlistA eq ==> R ==> R) (@fold_left _ _)); try reflexivity; diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index 9cde8d004..de3bbb011 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -39,7 +39,7 @@ Module E. (x1, y1), (x2, y2) => (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))) end. - Next Obligation. destruct P1 as [[??]?], P2 as [[??]?]; eapply Pre.onCurve_add; eauto. Qed. + Next Obligation. do 2 match goal with P : point |- _ => destruct P as [[??]?] end; eapply Pre.onCurve_add; eauto. Qed. Fixpoint mul (n:nat) (P : point) : point := match n with diff --git a/src/Specific/ArithmeticSynthesisTest.v b/src/Specific/ArithmeticSynthesisTest.v index d9e801a0c..fa520f16c 100644 --- a/src/Specific/ArithmeticSynthesisTest.v +++ b/src/Specific/ArithmeticSynthesisTest.v @@ -115,7 +115,7 @@ Section Ops51. let eval := Positional.Fdecode (m:=m) wt in eval (add a b) = (eval a + eval b)%F }. Proof. - eexists; cbv beta zeta; intros. + eexists; cbv beta zeta; intros a b. pose proof wt_nonzero. let x := constr:( Positional.add_cps (n := sz) wt a b id) in @@ -128,7 +128,7 @@ Section Ops51. let eval := Positional.Fdecode (m:=m) wt in eval (sub a b) = (eval a - eval b)%F}. Proof. - eexists; cbv beta zeta; intros. + eexists; cbv beta zeta; intros a b. pose proof wt_nonzero. let x := constr:( Positional.sub_cps (n:=sz) (coef := coef) wt a b id) in @@ -141,7 +141,7 @@ Section Ops51. let eval := Positional.Fdecode (m := m) wt in eval (opp a) = F.opp (eval a)}. Proof. - eexists; cbv beta zeta; intros. + eexists; cbv beta zeta; intros a. pose proof wt_nonzero. let x := constr:( Positional.opp_cps (n:=sz) (coef := coef) wt a id) in @@ -154,7 +154,7 @@ Section Ops51. let eval := Positional.Fdecode (m := m) wt in eval (mul a b) = (eval a * eval b)%F}. Proof. - eexists; cbv beta zeta; intros. + eexists; cbv beta zeta; intros a b. pose proof wt_nonzero. let x := constr:( Positional.mul_cps (n:=sz) (m:=sz2) wt a b @@ -190,7 +190,7 @@ Section Ops51. let eval := Positional.Fdecode (m := m) wt in eval (square a) = (eval a * eval a)%F}. Proof. - eexists; cbv beta zeta; intros. + eexists; cbv beta zeta; intros a. pose proof wt_nonzero. let x := constr:( Positional.mul_cps (n:=sz) (m:=sz2) wt a a @@ -221,7 +221,7 @@ Section Ops51. let eval := Positional.Fdecode (m := m) wt in eval (carry a) = eval a}. Proof. - eexists; cbv beta zeta; intros. + eexists; cbv beta zeta; intros a. pose proof wt_nonzero. pose proof wt_divides_chain1. pose proof div_mod. pose proof wt_divides_chain2. let x := constr:( @@ -262,7 +262,7 @@ Section Ops51. let eval := Positional.Fdecode (m := m) wt in eval (freeze a) = eval a}. Proof. - eexists; cbv beta zeta; intros. + eexists; cbv beta zeta; intros a ?. pose proof wt_nonzero. pose proof wt_pos. pose proof div_mod. pose proof wt_divides_full_pos. pose proof wt_multiples. diff --git a/src/Specific/ArithmeticSynthesisTest130.v b/src/Specific/ArithmeticSynthesisTest130.v index 6454bfbf1..15485499b 100644 --- a/src/Specific/ArithmeticSynthesisTest130.v +++ b/src/Specific/ArithmeticSynthesisTest130.v @@ -115,7 +115,7 @@ Section Ops51. let eval := Positional.Fdecode (m:=m) wt in eval (add a b) = (eval a + eval b)%F }. Proof. - eexists; cbv beta zeta; intros. + eexists; cbv beta zeta; intros a b. pose proof wt_nonzero. let x := constr:( Positional.add_cps (n := sz) wt a b id) in @@ -128,7 +128,7 @@ Section Ops51. let eval := Positional.Fdecode (m:=m) wt in eval (sub a b) = (eval a - eval b)%F}. Proof. - eexists; cbv beta zeta; intros. + eexists; cbv beta zeta; intros a b. pose proof wt_nonzero. let x := constr:( Positional.sub_cps (n:=sz) (coef := coef) wt a b id) in @@ -141,7 +141,7 @@ Section Ops51. let eval := Positional.Fdecode (m := m) wt in eval (opp a) = F.opp (eval a)}. Proof. - eexists; cbv beta zeta; intros. + eexists; cbv beta zeta; intros a. pose proof wt_nonzero. let x := constr:( Positional.opp_cps (n:=sz) (coef := coef) wt a id) in @@ -154,7 +154,7 @@ Section Ops51. let eval := Positional.Fdecode (m := m) wt in eval (mul a b) = (eval a * eval b)%F}. Proof. - eexists; cbv beta zeta; intros. + eexists; cbv beta zeta; intros a b. pose proof wt_nonzero. let x := constr:( Positional.mul_cps (n:=sz) (m:=sz2) wt a b @@ -176,7 +176,7 @@ Section Ops51. let eval := Positional.Fdecode (m := m) wt in eval (carry a) = eval a}. Proof. - eexists; cbv beta zeta; intros. + eexists; cbv beta zeta; intros a. pose proof wt_nonzero. pose proof wt_divides_chain1. pose proof div_mod. pose proof wt_divides_chain2. let x := constr:( diff --git a/src/Specific/IntegrationTestFreeze.v b/src/Specific/IntegrationTestFreeze.v index 63cc76fc2..b9fad0e12 100644 --- a/src/Specific/IntegrationTestFreeze.v +++ b/src/Specific/IntegrationTestFreeze.v @@ -51,7 +51,7 @@ Section BoundedField25p5. | [ |- { f | forall a, ?phi (f a) = @?rhs a } ] => apply lift1_sig with (P:=fun a f => phi f = rhs a) end. - intros. + intros a. eexists_sig_etransitivity. all:cbv [phi]. rewrite <- (proj2_sig freeze_sig). { set (freezeZ := proj1_sig freeze_sig). diff --git a/src/Specific/IntegrationTestLadderstep.v b/src/Specific/IntegrationTestLadderstep.v index 06cd4f808..b88370a48 100644 --- a/src/Specific/IntegrationTestLadderstep.v +++ b/src/Specific/IntegrationTestLadderstep.v @@ -92,7 +92,7 @@ Section BoundedField25p5. | forall a24 x1 Q Q', let eval := B.Positional.Fdecode wt in Tuple.map (n:=2) (Tuple.map (n:=2) eval) (xzladderstep a24 x1 Q Q') = FMxzladderstep (eval a24) (eval x1) (Tuple.map (n:=2) eval Q) (Tuple.map (n:=2) eval Q') }. Proof. exists Mxzladderstep. - intros. + intros a24 x1 Q Q' eval. cbv [Mxzladderstep FMxzladderstep M.donnaladderstep]. destruct Q, Q'; cbv [map map' fst snd Let_In eval]. repeat rewrite ?(proj2_sig add_sig), ?(proj2_sig mul_sig), ?(proj2_sig square_sig), ?(proj2_sig sub_sig), ?(proj2_sig carry_sig). diff --git a/src/Specific/IntegrationTestLadderstep130.v b/src/Specific/IntegrationTestLadderstep130.v index c8e3ba2b8..541dcaee8 100644 --- a/src/Specific/IntegrationTestLadderstep130.v +++ b/src/Specific/IntegrationTestLadderstep130.v @@ -57,7 +57,7 @@ Section BoundedField25p5. | forall a24 x1 Q Q', let eval := B.Positional.Fdecode wt in Tuple.map (n:=2) (Tuple.map (n:=2) eval) (xzladderstep a24 x1 Q Q') = FMxzladderstep (eval a24) (eval x1) (Tuple.map (n:=2) eval Q) (Tuple.map (n:=2) eval Q') }. Proof. exists (@M.xzladderstep _ (proj1_sig add_sig) (proj1_sig sub_sig) (fun x y => proj1_sig carry_sig (proj1_sig mul_sig x y))). - intros. + intros a24 x1 Q Q' eval. cbv [FMxzladderstep M.xzladderstep]. destruct Q, Q'; cbv [map map' fst snd Let_In eval]. repeat rewrite ?(proj2_sig add_sig), ?(proj2_sig mul_sig), ?(proj2_sig sub_sig), ?(proj2_sig carry_sig). diff --git a/src/Specific/IntegrationTestMul.v b/src/Specific/IntegrationTestMul.v index 0cbc3966e..01d629bfb 100644 --- a/src/Specific/IntegrationTestMul.v +++ b/src/Specific/IntegrationTestMul.v @@ -50,7 +50,7 @@ Section BoundedField25p5. | [ |- { f | forall a b, ?phi (f a b) = @?rhs a b } ] => apply lift2_sig with (P:=fun a b f => phi f = rhs a b) end. - intros. + intros a b. eexists_sig_etransitivity. all:cbv [phi]. rewrite <- (proj2_sig mul_sig). symmetry; rewrite <- (proj2_sig carry_sig); symmetry. diff --git a/src/Specific/IntegrationTestSquare.v b/src/Specific/IntegrationTestSquare.v index eb91a13ff..d7d717c61 100644 --- a/src/Specific/IntegrationTestSquare.v +++ b/src/Specific/IntegrationTestSquare.v @@ -50,7 +50,7 @@ Section BoundedField25p5. | [ |- { f | forall a, ?phi (f a) = @?rhs a } ] => apply lift1_sig with (P:=fun a f => phi f = rhs a) end. - intros. + intros a. eexists_sig_etransitivity. all:cbv [phi]. rewrite <- (proj2_sig square_sig). symmetry; rewrite <- (proj2_sig carry_sig); symmetry. diff --git a/src/Specific/IntegrationTestSub.v b/src/Specific/IntegrationTestSub.v index 3eadc371d..7599c99e1 100644 --- a/src/Specific/IntegrationTestSub.v +++ b/src/Specific/IntegrationTestSub.v @@ -50,7 +50,7 @@ Section BoundedField25p5. | [ |- { f | forall a b, ?phi (f a b) = @?rhs a b } ] => apply lift2_sig with (P:=fun a b f => phi f = rhs a b) end. - intros. + intros a b. eexists_sig_etransitivity. all:cbv [phi]. rewrite <- (proj2_sig sub_sig). symmetry; rewrite <- (proj2_sig carry_sig); symmetry. diff --git a/src/Util/AdditionChainExponentiation.v b/src/Util/AdditionChainExponentiation.v index e03b2e36f..f35c4e9ea 100644 --- a/src/Util/AdditionChainExponentiation.v +++ b/src/Util/AdditionChainExponentiation.v @@ -39,7 +39,7 @@ Section AddChainExp. (Hl:Logic.eq (length acc) (length ref)), fold_chain id op is acc = (fold_chain 0 N.add is ref) * x. Proof using Type*. - induction is; intros; simpl @fold_chain. + intro x; induction is; intros acc ref H Hl; simpl @fold_chain. { repeat break_match; specialize (H 0%nat); rewrite ?nth_default_cons, ?nth_default_cons_S in H; solve [ simpl length in *; discriminate | apply H | rewrite scalarmult_0_l; reflexivity ]. } { repeat break_match. eapply IHis; intros; [|auto with distr_length]; []. @@ -52,8 +52,8 @@ Section AddChainExp. Lemma fold_chain_exp x is: fold_chain id op is [x] = (fold_chain 0 N.add is [1]) * x. Proof using Type*. - eapply fold_chain_exp'; intros; trivial. - destruct i; try destruct i; rewrite ?nth_default_cons_S, ?nth_default_cons, ?nth_default_nil; + eapply fold_chain_exp'; trivial; intros i. + destruct i as [|i]; try destruct i; rewrite ?nth_default_cons_S, ?nth_default_cons, ?nth_default_nil; rewrite ?scalarmult_1_l, ?scalarmult_0_l; reflexivity. Qed. End AddChainExp. diff --git a/src/Util/CPSUtil.v b/src/Util/CPSUtil.v index 41b21feb7..15782fa61 100644 --- a/src/Util/CPSUtil.v +++ b/src/Util/CPSUtil.v @@ -48,7 +48,7 @@ Fixpoint map_cps {A B} (g : A->B) ls end. Lemma map_cps_correct {A B} g ls: forall {T} f, @map_cps A B g ls T f = f (map g ls). -Proof. induction ls; simpl; intros; rewrite ?IHls; reflexivity. Qed. +Proof. induction ls as [|?? IHls]; simpl; intros; rewrite ?IHls; reflexivity. Qed. Create HintDb uncps discriminated. Hint Rewrite @map_cps_correct : uncps. Fixpoint flat_map_cps {A B} (g:A->forall {T}, (list B->T)->T) (ls : list A) {T} (f:list B->T) := @@ -61,7 +61,7 @@ Lemma flat_map_cps_correct {A B} (g:A->forall {T}, (list B->T)->T) ls : (forall x T h, @g x T h = h (g x id)) -> @flat_map_cps A B g ls T f = f (List.flat_map (fun x => g x id) ls). Proof. - induction ls; intros; [reflexivity|]. + induction ls as [|?? IHls]; intros T f H; [reflexivity|]. simpl flat_map_cps. simpl flat_map. rewrite H; erewrite IHls by eassumption. reflexivity. @@ -81,7 +81,7 @@ Fixpoint from_list_default'_cps {A} (d y:A) n xs: Lemma from_list_default'_cps_correct {A} n : forall d y l {T} f, @from_list_default'_cps A d y n l T f = f (Tuple.from_list_default' d y n l). Proof. - induction n; intros; simpl; [reflexivity|]. + induction n as [|? IHn]; intros; simpl; [reflexivity|]. break_match; subst; apply IHn. Qed. Definition from_list_default_cps {A} (d:A) n (xs:list A) : @@ -136,7 +136,7 @@ Lemma on_tuple_cps_correct {A B} d (g:list A -> forall {T}, (list B->T)->T) (Hg : forall x {T} h, @g x T h = h (g x id)) : forall H, @on_tuple_cps A B d g n m xs T f = f (@Tuple.on_tuple A B (fun x => g x id) n m H xs). Proof. - cbv [on_tuple_cps Tuple.on_tuple]; intros. + cbv [on_tuple_cps Tuple.on_tuple]; intros H. rewrite to_list_cps_correct, Hg, from_list_default_cps_correct. rewrite (Tuple.from_list_default_eq _ _ _ (H _ (Tuple.length_to_list _))). reflexivity. @@ -188,7 +188,7 @@ Lemma fold_right_cps2_correct {A B} g a0 l : forall {T} f, (forall b a T h, @g b a T h = h (@g b a A id)) -> @fold_right_cps2 A B g a0 l T f = f (List.fold_right (fun b a => @g b a A id) a0 l). Proof. - induction l; intros; [reflexivity|]. + induction l as [|?? IHl]; intros T f H; [reflexivity|]. simpl fold_right_cps2. simpl fold_right. rewrite H; erewrite IHl by eassumption. rewrite H; reflexivity. @@ -225,7 +225,7 @@ Fixpoint fold_right_cps {A B} (g:B->A->A) (a0:A) (l:list B) {T} (f:A->T) := end. Lemma fold_right_cps_correct {A B} g a0 l: forall {T} f, @fold_right_cps A B g a0 l T f = f (List.fold_right g a0 l). -Proof. induction l; intros; simpl; rewrite ?IHl; auto. Qed. +Proof. induction l as [|? l IHl]; intros; simpl; rewrite ?IHl; auto. Qed. Hint Rewrite @fold_right_cps_correct : uncps. Definition fold_right_no_starter_cps {A} g ls {T} (f:option A->T) := @@ -278,7 +278,7 @@ Module Tuple. Lemma mapi_with'_cps_correct {S A B n} : forall i f start xs T ret, (forall i s a R (ret:_->R), f i s a R ret = ret (f i s a _ id)) -> @mapi_with'_cps S A B n i f start xs T ret = ret (mapi_with' i (fun i s a => f i s a _ id) start xs). - Proof. induction n; intros; simpl; rewrite H, ?IHn by assumption; reflexivity. Qed. + Proof. induction n as [|n IHn]; intros i f start xs T ret H; simpl; rewrite H, ?IHn by assumption; reflexivity. Qed. Lemma mapi_with_cps_correct {S A B n} f start xs T ret (H:forall i s a R (ret:_->R), f i s a R ret = ret (f i s a _ id)) : @mapi_with_cps S A B n f start xs T ret = ret (mapi_with (fun i s a => f i s a _ id) start xs). diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v index cc144f062..e5f9cf0bd 100644 --- a/src/Util/Decidable.v +++ b/src/Util/Decidable.v @@ -16,8 +16,8 @@ Notation DecidableRel R := (forall x y, Decidable (R x y)). Global Instance hprop_eq_dec {A} `{DecidableRel (@eq A)} : IsHPropRel (@eq A) | 10. Proof. repeat intro; apply UIP_dec; trivial with nocore. Qed. -Global Instance eq_dec_hprop {A} {x y : A} `{hp : IsHProp A} : Decidable (@eq A x y) | 5. -Proof. left; apply hp. Qed. +Global Instance eq_dec_hprop {A} {x y : A} {hp : IsHProp A} : Decidable (@eq A x y) | 5. +Proof. left; auto. Qed. Ltac no_equalities_about x0 y0 := lazymatch goal with @@ -111,15 +111,16 @@ Global Instance dec_ge_Z : DecidableRel BinInt.Z.ge := ZArith_dec.Z_ge_dec. Global Instance dec_match_pair {A B} {P : A -> B -> Prop} {x : A * B} {HD : Decidable (P (fst x) (snd x))} : Decidable (let '(a, b) := x in P a b) | 1. -Proof. destruct x; assumption. Defined. +Proof. edestruct (_ : _ * _); assumption. Defined. Lemma not_not P {d:Decidable P} : not (not P) <-> P. Proof. destruct (dec P); intuition. Qed. -Global Instance dec_ex_forall_not T (P:T->Prop) {d:Decidable (exists b, P b)} : Decidable (forall b, ~ P b). +Global Instance dec_ex_forall_not : forall T (P:T->Prop) {d:Decidable (exists b, P b)}, Decidable (forall b, ~ P b). Proof. + intros T P d. destruct (dec (~ exists b, P b)) as [Hd|Hd]; [left|right]; - [abstract eauto | abstract (rewrite not_not in Hd by eauto; destruct Hd; eauto) ]. + [abstract eauto | let Hd := Hd in abstract (rewrite not_not in Hd by eauto; destruct Hd; eauto) ]. Defined. Lemma eqsig_eq {T} {U} {Udec:DecidableRel (@eq U)} (f g:T->U) (x x':T) pf pf' : diff --git a/src/Util/Equality.v b/src/Util/Equality.v index 456c9497a..affdb933a 100644 --- a/src/Util/Equality.v +++ b/src/Util/Equality.v @@ -83,8 +83,9 @@ Section gen. reflexivity. Defined. - Global Instance isiso_encode {y} : IsIso (encode y). + Global Instance isiso_encode : forall {y}, IsIso (encode y). Proof. + intro y. exists (@decode y). { intro H. unfold decode. diff --git a/src/Util/FixedWordSizesEquality.v b/src/Util/FixedWordSizesEquality.v index 430684070..56c7debf6 100644 --- a/src/Util/FixedWordSizesEquality.v +++ b/src/Util/FixedWordSizesEquality.v @@ -23,6 +23,7 @@ Lemma pow2_inj_helper x y : 2^x = 2^y -> x = y. Proof. destruct (NatUtil.nat_eq_dec x y) as [pf|pf]; [ intros; assumption | ]. intro H; exfalso. + let pf := pf in abstract (apply pf; eapply NPeano.Nat.pow_inj_r; [ | eassumption ]; omega). Defined. Lemma pow2_inj_helper_refl x p : pow2_inj_helper x x p = eq_refl. @@ -43,6 +44,7 @@ Proof. intros [pf H]; exists (pow2_inj_helper x y pf); subst v'. destruct (NatUtil.nat_eq_dec x y) as [H|H]; [ | exfalso; clear -pf H; + let pf := pf in abstract (apply pow2_inj_helper in pf; omega) ]. subst; rewrite pow2_inj_helper_refl; simpl. pose proof (NatUtil.UIP_nat_transparent _ _ pf eq_refl); subst pf. @@ -99,7 +101,10 @@ Proof. | _, _ => fun x y pf => match _ : False with end end; - try abstract (rewrite wordT_beq_hetero_type_lb_false in pf by omega; clear -pf; congruence). + match goal with + | [ pf : _ = _ |- _ ] + => abstract (rewrite wordT_beq_hetero_type_lb_false in pf by omega; clear -pf; congruence) + end. Defined. Lemma ZToWord_gen_wordToZ_gen : forall {sz} v, ZToWord_gen (@wordToZ_gen sz v) = v. @@ -123,7 +128,7 @@ Qed. Lemma wordToZ_gen_ZToWord_gen_mod : forall {sz} w, (0 <= w)%Z -> wordToZ_gen (@ZToWord_gen sz w) = (w mod (2^Z.of_nat sz))%Z. Proof. unfold ZToWord_gen, wordToZ_gen. - intros. + intros sz w H. rewrite wordToN_NToWord_mod. rewrite N2Z.inj_mod by (destruct sz; simpl; congruence). rewrite Z2N.id, N2Z.inj_pow, nat_N_Z by assumption. diff --git a/src/Util/ForLoop/InvariantFramework.v b/src/Util/ForLoop/InvariantFramework.v index 503cfcdc3..2bff6bef9 100644 --- a/src/Util/ForLoop/InvariantFramework.v +++ b/src/Util/ForLoop/InvariantFramework.v @@ -16,7 +16,7 @@ Lemma repeat_function_ind {stateT} (P : nat -> stateT -> Prop) : P 0 (repeat_function body count st). Proof. revert dependent st; revert dependent body; revert dependent P. - induction count; intros; [ exact Pbefore | ]. + induction count as [|? IHcount]; intros P body Pbody st Pbefore; [ exact Pbefore | ]. { rewrite repeat_function_unroll1_end; apply Pbody; [ omega | ]. apply (IHcount (fun c => P (S c))); auto with omega. } Qed. diff --git a/src/Util/ForLoop/Unrolling.v b/src/Util/ForLoop/Unrolling.v index e0518f39a..95b46e711 100644 --- a/src/Util/ForLoop/Unrolling.v +++ b/src/Util/ForLoop/Unrolling.v @@ -31,7 +31,7 @@ Section with_body. : repeat_function body (S count) st = body 1 (repeat_function (fun count => body (S count)) count st). Proof using Type. - revert st; induction count; [ reflexivity | ]. + revert st; induction count as [|? IHcount]; [ reflexivity | ]. intros; simpl in *; rewrite <- IHcount; reflexivity. Qed. diff --git a/src/Util/HList.v b/src/Util/HList.v index 2a135c75c..d2ea841d3 100644 --- a/src/Util/HList.v +++ b/src/Util/HList.v @@ -142,13 +142,14 @@ Proof. destruct n; [ simpl; tauto | apply fold_right_and_True_hlist' ]. Qed. -Global Instance mapt_Proper {n A F B} - : Proper +Global Instance mapt_Proper + : forall {n A F B}, + Proper ((forall_relation (fun x => pointwise_relation _ Logic.eq)) ==> forall_relation (fun ts => Logic.eq ==> Logic.eq)) (@mapt n A F B). Proof. - unfold forall_relation, pointwise_relation, respectful. + intro n; unfold forall_relation, pointwise_relation, respectful. repeat intro; subst; destruct n as [|n]; [ reflexivity | ]. induction n; simpl in *; congruence. Qed. diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v index e4f9dde08..4d9365e4d 100644 --- a/src/Util/IterAssocOp.v +++ b/src/Util/IterAssocOp.v @@ -26,7 +26,7 @@ Section IterAssocOp. Lemma Pos_iter_op_succ : forall p a, Pos.iter_op op (Pos.succ p) a === op a (Pos.iter_op op p a). Proof using Type*. - induction p; intros; simpl; rewrite ?Algebra.Hierarchy.associative, ?IHp; reflexivity. + induction p as [p IHp|p IHp|]; intros; simpl; rewrite ?Algebra.Hierarchy.associative, ?IHp; reflexivity. Qed. Lemma N_iter_op_succ : forall n a, N_iter_op (N.succ n) a === op a (N_iter_op n a). @@ -36,7 +36,7 @@ Section IterAssocOp. Lemma N_iter_op_is_nat_iter_op : forall n a, N_iter_op n a === nat_iter_op (N.to_nat n) a. Proof using Type*. - induction n using N.peano_ind; intros; rewrite ?N2Nat.inj_succ, ?N_iter_op_succ, ?IHn; reflexivity. + induction n as [|n IHn] using N.peano_ind; intros; rewrite ?N2Nat.inj_succ, ?N_iter_op_succ, ?IHn; reflexivity. Qed. Context {sel:bool->T->T->T} {sel_correct:forall b x y, sel b x y = if b then y else x}. @@ -90,7 +90,7 @@ Section IterAssocOp. Lemma funexp_test_and_op_index : forall a x acc y, fst (funexp (test_and_op a) (x, acc) y) = x - y. Proof using Type. - induction y; simpl; rewrite <- ?Minus.minus_n_O; try reflexivity. + induction y as [|? IHy]; simpl; rewrite <- ?Minus.minus_n_O; try reflexivity. match goal with |- context[funexp ?a ?b ?c] => destruct (funexp a b c) as [i acc'] end. simpl in IHy. unfold test_and_op. @@ -129,7 +129,7 @@ Global Instance Proper_funexp {T R} {Equivalence_R:Equivalence R} : Proper ((R==>R) ==> R ==> Logic.eq ==> R) (@funexp T). Proof. repeat intro; subst. - match goal with [n0 : nat |- _ ] => rename n0 into n; induction n end; [solve [trivial]|]. + match goal with [n0 : nat |- _ ] => rename n0 into n; induction n as [|n IHn] end; [solve [trivial]|]. match goal with [H: (_ ==> _)%signature _ _ |- _ ] => etransitivity; solve [eapply (H _ _ IHn)|reflexivity] @@ -169,7 +169,8 @@ Global Instance Proper_iter_op {T R} {Equivalence_R:@Equivalence T R} : Proof. repeat match goal with | _ => solve [ reflexivity | congruence | eauto 99 ] - | _ => progress eapply (Proper_funexp (R:=(fun nt NT => Logic.eq (fst nt) (fst NT) /\ R (snd nt) (snd NT)))) + | [ R : _ |- _ ] + => progress eapply (Proper_funexp (R:=(fun nt NT => Logic.eq (fst nt) (fst NT) /\ R (snd nt) (snd NT)))) | _ => progress eapply Proper_test_and_op | _ => progress split | _ => progress (cbv [fst snd pointwise_relation respectful] in * ) diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index b49367600..6c6f96761 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -7,6 +7,8 @@ Require Import Crypto.Util.NatUtil. Require Export Crypto.Util.FixCoqMistakes. Require Export Crypto.Util.Tactics.BreakMatch. Require Export Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.SpecializeBy. +Require Import Crypto.Util.Tactics.RewriteHyp. Create HintDb distr_length discriminated. Create HintDb simpl_set_nth discriminated. @@ -77,7 +79,7 @@ Module Export List. Lemma in_seq len start n : In n (seq start len) <-> start <= n < start+len. Proof. - revert start. induction len; simpl; intros. + revert start. induction len as [|len IHlen]; simpl; intros. - rewrite <- plus_n_O. split;[easy|]. intros (H,H'). apply (Lt.lt_irrefl _ (Lt.le_lt_trans _ _ _ H H')). - rewrite IHlen, <- plus_n_Sm; simpl; split. @@ -136,7 +138,7 @@ Module Export List. Lemma firstn_all2 n: forall (l:list A), (length l) <= n -> firstn n l = l. Proof using Type. induction n as [|k iHk]. - - intro. inversion 1 as [H1|?]. + - intro l. inversion 1 as [H1|?]. rewrite (length_zero_iff_nil l) in H1. subst. now simpl. - destruct l as [|x xs]; simpl. * now reflexivity. @@ -157,7 +159,7 @@ Module Export List. n <= length l -> length (firstn n l) = n. Proof using Type. induction l as [|x xs Hrec]. - simpl. intros n H. apply le_n_0_eq in H. rewrite <- H. now simpl. - - destruct n. + - destruct n as [|n]. * now simpl. * simpl. intro H. apply le_S_n in H. now rewrite (Hrec n H). Qed. @@ -318,26 +320,26 @@ Lemma nth_error_seq : forall i start len, if lt_dec i len then Some (start + i) else None. - induction i; destruct len; nth_tac'; erewrite IHi; nth_tac'. + induction i as [|? IHi]; destruct len; nth_tac'; erewrite IHi; nth_tac'. Qed. Lemma nth_error_error_length : forall A i (xs:list A), nth_error xs i = None -> i >= length xs. Proof. - induction i; destruct xs; nth_tac'; try specialize (IHi _ H); omega. + induction i as [|? IHi]; destruct xs; nth_tac'; try match goal with H : _ |- _ => specialize (IHi _ H) end; omega. Qed. Lemma nth_error_value_length : forall A i (xs:list A) x, nth_error xs i = Some x -> i < length xs. Proof. - induction i; destruct xs; nth_tac'; try specialize (IHi _ _ H); omega. + induction i as [|? IHi]; destruct xs; nth_tac'; try match goal with H : _ |- _ => specialize (IHi _ _ H) end; omega. Qed. Lemma nth_error_length_error : forall A i (xs:list A), i >= length xs -> nth_error xs i = None. Proof. - induction i; destruct xs; nth_tac'; rewrite IHi by omega; auto. + induction i as [|? IHi]; destruct xs; nth_tac'; rewrite IHi by omega; auto. Qed. Hint Resolve nth_error_length_error. Hint Rewrite @nth_error_length_error using omega : simpl_nth_error. @@ -345,11 +347,12 @@ Hint Rewrite @nth_error_length_error using omega : simpl_nth_error. Lemma map_nth_default : forall (A B : Type) (f : A -> B) n x y l, (n < length l) -> nth_default y (map f l) n = f (nth_default x l n). Proof. - intros. + intros A B f n x y l H. unfold nth_default. erewrite map_nth_error. reflexivity. nth_tac'. + let H0 := match goal with H0 : _ = None |- _ => H0 end in pose proof (nth_error_error_length A n l H0). omega. Qed. @@ -362,7 +365,7 @@ Proof. reflexivity. Qed. Lemma In_nth : forall {A} (x : A) d xs, In x xs -> exists i, i < length xs /\ nth i xs d = x. Proof. - induction xs; intros; + induction xs as [|?? IHxs]; intros; match goal with H : In _ _ |- _ => simpl in H; destruct H end. + subst. exists 0. simpl; split; auto || omega. + destruct IHxs as [i [ ]]; auto. @@ -423,7 +426,7 @@ Lemma update_nth_ext {T} f g n : forall xs, (forall x, nth_error xs n = Some x -> f x = g x) -> @update_nth T n f xs = @update_nth T n g xs. Proof. - induction n; destruct xs; simpl; intros H; + induction n as [|n IHn]; destruct xs; simpl; intros H; try rewrite IHn; try rewrite H; try congruence; trivial. Qed. @@ -436,7 +439,7 @@ Lemma update_nth_id_eq_specific {T} f n : forall (xs : list T) (H : forall x, nth_error xs n = Some x -> f x = x), update_nth n f xs = xs. Proof. - induction n; destruct xs; simpl; intros; + induction n as [|n IHn]; destruct xs; simpl; intros H; try rewrite IHn; try rewrite H; unfold value in *; try congruence; assumption. Qed. @@ -461,7 +464,7 @@ Lemma nth_update_nth : forall m {T} (xs:list T) (n:nat) (f:T -> T), then option_map f (nth_error xs n) else nth_error xs n. Proof. - induction m. + induction m as [|? IHm]. { destruct n, xs; auto. } { destruct xs, n; intros; simpl; auto; [ | rewrite IHm ]; clear IHm; @@ -499,7 +502,7 @@ Lemma nth_set_nth : forall m {T} (xs:list T) (n:nat) x, then (if lt_dec n (length xs) then Some x else None) else nth_error xs n. Proof. - intros; unfold set_nth; rewrite nth_update_nth. + intros m T xs n x; unfold set_nth; rewrite nth_update_nth. destruct (nth_error xs n) eqn:?, (lt_dec n (length xs)) as [p|p]; rewrite <- nth_error_Some in p; solve [ reflexivity @@ -522,7 +525,7 @@ Qed. Lemma nth_error_length_not_error : forall {A} (i : nat) (xs : list A), nth_error xs i = None -> (i < length xs)%nat -> False. Proof. - intros. + intros A i xs H H0. destruct (nth_error_length_exists_value i xs); intuition; congruence. Qed. @@ -540,7 +543,7 @@ Proof. auto. Qed. Lemma destruct_repeat : forall {A} xs y, (forall x : A, In x xs -> x = y) -> xs = nil \/ exists xs', xs = y :: xs' /\ (forall x : A, In x xs' -> x = y). Proof. - destruct xs; intros; try tauto. + destruct xs as [|? xs]; intros; try tauto. right. exists xs; split. + f_equal; auto using in_eq. @@ -590,7 +593,7 @@ Lemma update_nth_equiv_splice_nth: forall {T} n f (xs:list T), end else xs. Proof. - induction n; destruct xs; intros; + induction n as [|? IHn]; destruct xs; intros; autorewrite with simpl_update_nth simpl_nth_default in *; simpl in *; try (erewrite IHn; clear IHn); auto. repeat break_match; remove_nth_error; try reflexivity; try omega. @@ -601,17 +604,17 @@ Lemma splice_nth_equiv_set_nth : forall {T} n x (xs:list T), if lt_dec n (length xs) then set_nth n x xs else xs ++ x::nil. -Proof. intros; rewrite splice_nth_equiv_update_nth with (f := fun _ => x); auto. Qed. +Proof. intros T n x xs; rewrite splice_nth_equiv_update_nth with (f := fun _ => x); auto. Qed. Lemma splice_nth_equiv_set_nth_set : forall {T} n x (xs:list T), n < length xs -> splice_nth n x xs = set_nth n x xs. -Proof. intros; rewrite splice_nth_equiv_update_nth_update with (f := fun _ => x); auto. Qed. +Proof. intros T n x xs H; rewrite splice_nth_equiv_update_nth_update with (f := fun _ => x); auto. Qed. Lemma splice_nth_equiv_set_nth_snoc : forall {T} n x (xs:list T), n >= length xs -> splice_nth n x xs = xs ++ x::nil. -Proof. intros; rewrite splice_nth_equiv_update_nth_snoc with (f := fun _ => x); auto. Qed. +Proof. intros T n x xs H; rewrite splice_nth_equiv_update_nth_snoc with (f := fun _ => x); auto. Qed. Lemma set_nth_equiv_splice_nth: forall {T} n x (xs:list T), set_nth n x xs = @@ -619,7 +622,7 @@ Lemma set_nth_equiv_splice_nth: forall {T} n x (xs:list T), then splice_nth n x xs else xs. Proof. - intros; unfold set_nth; rewrite update_nth_equiv_splice_nth with (f := fun _ => x); auto. + intros T n x xs; unfold set_nth; rewrite update_nth_equiv_splice_nth with (f := fun _ => x); auto. repeat break_match; remove_nth_error; trivial. Qed. @@ -627,7 +630,7 @@ Lemma combine_update_nth : forall {A B} n f g (xs:list A) (ys:list B), combine (update_nth n f xs) (update_nth n g ys) = update_nth n (fun xy => (f (fst xy), g (snd xy))) (combine xs ys). Proof. - induction n; destruct xs, ys; simpl; try rewrite IHn; reflexivity. + induction n as [|? IHn]; destruct xs, ys; simpl; try rewrite IHn; reflexivity. Qed. (* grumble, grumble, [rewrite] is bad at inferring the identity function, and constant functions *) @@ -669,7 +672,7 @@ Lemma combine_set_nth : forall {A B} n (x:A) xs (ys:list B), | Some y => set_nth n (x,y) (combine xs ys) end. Proof. - intros; unfold set_nth; rewrite combine_update_nth_l. + intros A B n x xs ys; unfold set_nth; rewrite combine_update_nth_l. nth_tac; [ repeat rewrite_rev_combine_update_nth; apply f_equal2 | assert (nth_error (combine xs ys) n = None) @@ -686,15 +689,15 @@ Qed. Lemma In_nth_error_value : forall {T} xs (x:T), In x xs -> exists n, nth_error xs n = Some x. Proof. - induction xs; nth_tac; destruct_head or; subst. + induction xs as [|?? IHxs]; nth_tac; destruct_head or; subst. - exists 0; reflexivity. - - edestruct IHxs; eauto. exists (S x0). eauto. + - edestruct IHxs as [x0]; eauto. exists (S x0). eauto. Qed. Lemma nth_value_index : forall {T} i xs (x:T), nth_error xs i = Some x -> In i (seq 0 (length xs)). Proof. - induction i; destruct xs; nth_tac; right. + induction i as [|? IHi]; destruct xs; nth_tac; right. rewrite <- seq_shift; apply in_map; eapply IHi; eauto. Qed. @@ -703,7 +706,7 @@ Lemma nth_error_app : forall {T} n (xs ys:list T), nth_error (xs ++ ys) n = then nth_error xs n else nth_error ys (n - length xs). Proof. - induction n; destruct xs; nth_tac; + induction n as [|n IHn]; destruct xs as [|? xs]; nth_tac; rewrite IHn; destruct (lt_dec n (length xs)); trivial; omega. Qed. @@ -712,7 +715,7 @@ Lemma nth_default_app : forall {T} n x (xs ys:list T), nth_default x (xs ++ ys) then nth_default x xs n else nth_default x ys (n - length xs). Proof. - intros. + intros T n x xs ys. unfold nth_default. rewrite nth_error_app. destruct (lt_dec n (length xs)); auto. @@ -952,7 +955,7 @@ Lemma list012 : forall {T} (xs:list T), \/ (exists x, xs = x::nil) \/ (exists x xs' y, xs = x::xs'++y::nil). Proof. - destruct xs; auto. + destruct xs as [|? xs]; auto. right. destruct xs using rev_ind. { left; eexists; auto. @@ -1017,7 +1020,7 @@ Hint Rewrite @set_nth_nil : simpl_set_nth. Lemma skipn_nth_default : forall {T} n us (d : T), (n < length us)%nat -> skipn n us = nth_default d us n :: skipn (S n) us. Proof. - induction n; destruct us; intros; nth_tac. + induction n as [|n IHn]; destruct us as [|? us]; intros d H; nth_tac. rewrite (IHn us d) at 1 by omega. nth_tac. Qed. @@ -1025,10 +1028,13 @@ Qed. Lemma nth_default_out_of_bounds : forall {T} n us (d : T), (n >= length us)%nat -> nth_default d us n = d. Proof. - induction n; unfold nth_default; nth_tac; destruct us; nth_tac. + induction n as [|n IHn]; unfold nth_default; nth_tac; + let us' := match goal with us : list _ |- _ => us end in + destruct us' as [|? us]; nth_tac. assert (n >= length us)%nat by omega. - pose proof (nth_error_length_error _ n us H1). - rewrite H0 in H2. + pose proof (nth_error_length_error _ n us). + specialize_by_assumption. + rewrite_hyp * in *. congruence. Qed. @@ -1131,12 +1137,12 @@ Hint Rewrite @map_nth_default_always : push_nth_default. Lemma map_S_seq {A} (f:nat->A) len : forall start, List.map (fun i => f (S i)) (seq start len) = List.map f (seq (S start) len). -Proof. induction len; intros; simpl; rewrite ?IHlen; reflexivity. Qed. +Proof. induction len as [|len IHlen]; intros; simpl; rewrite ?IHlen; reflexivity. Qed. Lemma fold_right_and_True_forall_In_iff : forall {T} (l : list T) (P : T -> Prop), (forall x, In x l -> P x) <-> fold_right and True (map P l). Proof. - induction l; intros; simpl; try tauto. + induction l as [|?? IHl]; intros; simpl; try tauto. rewrite <- IHl. intuition (subst; auto). Qed. @@ -1145,7 +1151,7 @@ Lemma fold_right_invariant : forall {A B} P (f: A -> B -> B) l x, P x -> (forall y, In y l -> forall z, P z -> P (f y z)) -> P (fold_right f x l). Proof. - induction l; intros ? ? step; auto. + induction l as [|a l IHl]; intros ? ? step; auto. simpl. apply step; try apply in_eq. apply IHl; auto. @@ -1167,7 +1173,7 @@ Qed. Lemma In_firstn_skipn_split {T} n (x : T) : forall l, In x l <-> In x (firstn n l) \/ In x (skipn n l). Proof. - split; revert l; induction n; destruct l; boring. + intro l; split; revert l; induction n; destruct l; boring. match goal with | [ IH : forall l, In ?x l -> _ \/ _, H' : In ?x ?ls |- _ ] => destruct (IH _ H') @@ -1177,7 +1183,7 @@ Qed. Lemma firstn_firstn_min : forall {A} m n (l : list A), firstn n (firstn m l) = firstn (min n m) l. Proof. - induction m; destruct n; intros; try omega; auto. + induction m as [|? IHm]; destruct n; intros l; try omega; auto. destruct l; auto. simpl. f_equal. @@ -1187,7 +1193,7 @@ Qed. Lemma firstn_firstn : forall {A} m n (l : list A), (n <= m)%nat -> firstn n (firstn m l) = firstn n l. Proof. - intros; rewrite firstn_firstn_min. + intros A m n l H; rewrite firstn_firstn_min. apply Min.min_case_strong; intro; [ reflexivity | ]. assert (n = m) by omega; subst; reflexivity. Qed. @@ -1197,7 +1203,7 @@ Hint Rewrite @firstn_firstn using omega : push_firstn. Lemma firstn_succ : forall {A} (d : A) n l, (n < length l)%nat -> firstn (S n) l = (firstn n l) ++ nth_default d l n :: nil. Proof. - induction n; destruct l; rewrite ?(@nil_length0 A); intros; try omega. + intros A d; induction n as [|? IHn]; destruct l; rewrite ?(@nil_length0 A); intros; try omega. + rewrite nth_default_cons; auto. + simpl. rewrite nth_default_cons_S. @@ -1208,20 +1214,20 @@ Qed. Lemma firstn_seq k a b : firstn k (seq a b) = seq a (min k b). Proof. - revert k a; induction b, k; simpl; try reflexivity. + revert k a; induction b as [|? IHb], k; simpl; try reflexivity. intros; rewrite IHb; reflexivity. Qed. Lemma skipn_seq k a b : skipn k (seq a b) = seq (k + a) (b - k). Proof. - revert k a; induction b, k; simpl; try reflexivity. + revert k a; induction b as [|? IHb], k; simpl; try reflexivity. intros; rewrite IHb; simpl; f_equal; omega. Qed. Lemma update_nth_out_of_bounds : forall {A} n f xs, n >= length xs -> @update_nth A n f xs = xs. Proof. - induction n; destruct xs; simpl; try congruence; try omega; intros. + induction n as [|n IHn]; destruct xs; simpl; try congruence; try omega; intros. rewrite IHn by omega; reflexivity. Qed. @@ -1235,8 +1241,8 @@ Lemma update_nth_nth_default_full : forall {A} (d:A) n f l i, else nth_default d l i else d. Proof. - induction n; (destruct l; simpl in *; [ intros; destruct i; simpl; try reflexivity; omega | ]); - intros; repeat break_match; subst; try destruct i; + induction n as [|n IHn]; (destruct l; simpl in *; [ intros i **; destruct i; simpl; try reflexivity; omega | ]); + intros i **; repeat break_match; subst; try destruct i; repeat first [ progress break_match | progress subst | progress boring @@ -1273,7 +1279,7 @@ Hint Rewrite @set_nth_nth_default using (omega || distr_length; omega) : push_nt Lemma nth_default_preserves_properties : forall {A} (P : A -> Prop) l n d, (forall x, In x l -> P x) -> P d -> P (nth_default d l n). Proof. - intros; rewrite nth_default_eq. + intros A P l n d H H0; rewrite nth_default_eq. destruct (nth_in_or_default n l d); auto. congruence. Qed. @@ -1282,7 +1288,7 @@ Lemma nth_default_preserves_properties_length_dep : forall {A} (P : A -> Prop) l n d, (forall x, In x l -> n < (length l) -> P x) -> ((~ n < length l) -> P d) -> P (nth_default d l n). Proof. - intros. + intros A P l n d H H0. destruct (lt_dec n (length l)). + rewrite nth_default_eq; auto using nth_In. + rewrite nth_default_out_of_bounds by omega. @@ -1300,7 +1306,7 @@ Qed. Lemma nth_error_exists_first : forall {T} l (x : T) (H : nth_error l 0 = Some x), exists l', l = x :: l'. Proof. - induction l; try discriminate; eexists. + induction l; try discriminate; intros x H; eexists. apply nth_error_first in H. subst; eauto. Qed. @@ -1308,7 +1314,7 @@ Qed. Lemma list_elementwise_eq : forall {T} (l1 l2 : list T), (forall i, nth_error l1 i = nth_error l2 i) -> l1 = l2. Proof. - induction l1, l2; intros; try reflexivity; + induction l1, l2; intros H; try reflexivity; pose proof (H 0%nat) as Hfirst; simpl in Hfirst; inversion Hfirst. f_equal. apply IHl1. @@ -1337,7 +1343,7 @@ Hint Rewrite @sum_firstn_all using omega : simpl_sum_firstn. Lemma sum_firstn_succ_default : forall l i, sum_firstn l (S i) = (nth_default 0 l i + sum_firstn l i)%Z. Proof. - unfold sum_firstn; induction l, i; + unfold sum_firstn; induction l as [|a l IHl], i; intros; autorewrite with simpl_nth_default simpl_firstn simpl_fold_right in *; try reflexivity. rewrite IHl; omega. @@ -1404,7 +1410,7 @@ Hint Resolve sum_firstn_nonnegative : znonzero. Lemma sum_firstn_app : forall xs ys n, sum_firstn (xs ++ ys) n = (sum_firstn xs n + sum_firstn ys (n - length xs))%Z. Proof. - induction xs; simpl. + induction xs as [|a xs IHxs]; simpl. { intros ys n; autorewrite with simpl_sum_firstn; simpl. f_equal; omega. } { intros ys [|n]; autorewrite with simpl_sum_firstn; simpl; [ reflexivity | ]. @@ -1428,7 +1434,7 @@ Proof. reflexivity. Qed. Lemma nth_error_skipn : forall {A} n (l : list A) m, nth_error (skipn n l) m = nth_error l (n + m). Proof. -induction n; destruct l; boring. +induction n as [|n IHn]; destruct l; boring. apply nth_error_nil_error. Qed. Hint Rewrite @nth_error_skipn : push_nth_error. @@ -1454,7 +1460,7 @@ Qed. Lemma sum_firstn_prefix_le' : forall l n m, (forall x, In x l -> (0 <= x)%Z) -> (sum_firstn l n <= sum_firstn l (n + m))%Z. Proof. -intros. +intros l n m H. rewrite sum_firstn_skipn. pose proof (sum_firstn_nonnegative m (skipn n l)) as Hskipn_nonneg. match type of Hskipn_nonneg with @@ -1468,7 +1474,7 @@ Lemma sum_firstn_prefix_le : forall l n m, (forall x, In x l -> (0 <= x)%Z) -> (n <= m)%nat -> (sum_firstn l n <= sum_firstn l m)%Z. Proof. -intros. +intros l n m H H0. replace m with (n + (m - n))%nat by omega. auto using sum_firstn_prefix_le'. Qed. @@ -1478,17 +1484,17 @@ Lemma sum_firstn_pos_lt_succ : forall l n m, (forall x, In x l -> (0 <= x)%Z) -> (sum_firstn l n < sum_firstn l (S m))%Z -> (n <= m)%nat. Proof. -intros. +intros l n m H H0 H1. destruct (le_dec n m); auto. replace n with (m + (n - m))%nat in H1 by omega. rewrite sum_firstn_skipn in H1. rewrite sum_firstn_succ_default in *. -match goal with H : (?a + ?b < ?c + ?a)%Z |- _ => assert (b < c)%Z by omega end. +match goal with H : (?a + ?b < ?c + ?a)%Z |- _ => assert (H2 : (b < c)%Z) by omega end. destruct (lt_dec m (length l)). { rewrite skipn_nth_default with (d := 0%Z) in H2 by assumption. replace (n - m)%nat with (S (n - S m))%nat in H2 by omega. rewrite sum_firstn_succ_cons in H2. - pose proof (sum_firstn_nonnegative (n - S m) (skipn (S m) l)). + pose proof (sum_firstn_nonnegative (n - S m) (skipn (S m) l)) as H3. match type of H3 with ?P -> _ => assert P as Q; [ | specialize (H3 Q); omega ] end. intros ? A. @@ -1522,7 +1528,7 @@ Lemma nth_default_map2 : forall {A B C} (f : A -> B -> C) ls1 ls2 i d d1 d2, then f (nth_default d1 ls1 i) (nth_default d2 ls2 i) else d. Proof. - induction ls1, ls2. + induction ls1 as [|a ls1 IHls1], ls2. + cbv [map2 length min]. intros. break_match; try omega. @@ -1539,7 +1545,7 @@ Proof. destruct i. - intros. rewrite !nth_default_cons. break_match; auto; omega. - - intros. rewrite !nth_default_cons_S. + - intros d d1 d2. rewrite !nth_default_cons_S. rewrite IHls1 with (d1 := d1) (d2 := d2). repeat break_match; auto; omega. Qed. @@ -1576,7 +1582,7 @@ Section OpaqueMap2. Lemma map2_length : forall A B C (f : A -> B -> C) ls1 ls2, length (map2 f ls1 ls2) = min (length ls1) (length ls2). Proof. - induction ls1, ls2; intros; try solve [cbv; auto]. + induction ls1 as [|a ls1 IHls1], ls2; intros; try solve [cbv; auto]. rewrite map2_cons, !length_cons, IHls1. auto. Qed. @@ -1587,7 +1593,7 @@ Section OpaqueMap2. (length ls1 = length ls2) -> map2 f (ls1 ++ ls1') (ls2 ++ ls2') = map2 f ls1 ls2 ++ map2 f ls1' ls2'. Proof. - induction ls1, ls2; intros; rewrite ?map2_nil_r, ?app_nil_l; try congruence; + induction ls1 as [|a ls1 IHls1], ls2; intros; rewrite ?map2_nil_r, ?app_nil_l; try congruence; simpl_list_lengths; try omega. rewrite <-!app_comm_cons, !map2_cons. rewrite IHls1; auto. @@ -1611,15 +1617,15 @@ Require Import Coq.Lists.SetoidList. Global Instance Proper_nth_default : forall A eq, Proper (eq==>eqlistA eq==>Logic.eq==>eq) (nth_default (A:=A)). Proof. - do 5 intro; subst; induction 1. + intros A ee x y H; subst; induction 1. + repeat intro; rewrite !nth_default_nil; assumption. - + repeat intro; subst; destruct y0; rewrite ?nth_default_cons, ?nth_default_cons_S; auto. + + intros x1 y0 H2; subst; destruct y0; rewrite ?nth_default_cons, ?nth_default_cons_S; auto. Qed. Lemma fold_right_andb_true_map_iff A (ls : list A) f : List.fold_right andb true (List.map f ls) = true <-> forall i, List.In i ls -> f i = true. Proof. - induction ls; simpl; [ | rewrite Bool.andb_true_iff, IHls ]; try tauto. + induction ls as [|a ls IHls]; simpl; [ | rewrite Bool.andb_true_iff, IHls ]; try tauto. intuition (congruence || eauto). Qed. @@ -1633,16 +1639,17 @@ Qed. Lemma Forall2_forall_iff : forall {A} R (xs ys : list A) d, length xs = length ys -> (Forall2 R xs ys <-> (forall i, (i < length xs)%nat -> R (nth_default d xs i) (nth_default d ys i))). Proof. - split; intros. + intros A R xs ys d H; split; [ intros H0 i H1 | intros H0 ]. + + revert xs ys H H0 H1. - induction i; intros; destruct H0; distr_length; autorewrite with push_nth_default; auto. + induction i as [|i IHi]; intros xs ys H H0 H1; destruct H0; distr_length; autorewrite with push_nth_default; auto. eapply IHi; auto. omega. - + revert xs ys H H0; induction xs; intros; destruct ys; distr_length; econstructor. + + revert xs ys H H0; induction xs as [|a xs IHxs]; intros ys H H0; destruct ys; distr_length; econstructor. - specialize (H0 0%nat). autorewrite with push_nth_default in *; auto. apply H0; omega. - apply IHxs; try omega. - intros. + intros i H1. specialize (H0 (S i)). autorewrite with push_nth_default in *; auto. apply H0; omega. @@ -1653,7 +1660,7 @@ Lemma nth_default_firstn : forall {A} (d : A) l i n, then if lt_dec i n then nth_default d l i else d else nth_default d l i. Proof. - induction n; intros; break_match; autorewrite with push_nth_default; auto; try omega. + intros A d l i; induction n as [|n IHn]; break_match; autorewrite with push_nth_default; auto; try omega. + rewrite (firstn_succ d) by omega. autorewrite with push_nth_default; repeat (break_match_hyps; break_match; distr_length); rewrite Min.min_l in * by omega; try omega. @@ -1677,8 +1684,8 @@ Hint Rewrite repeat_length : distr_length. Lemma repeat_spec_iff : forall {A} (ls : list A) x n, (length ls = n /\ forall y, In y ls -> y = x) <-> ls = repeat x n. Proof. - split; [ revert A ls x n | intro; subst; eauto using repeat_length, repeat_spec ]. - induction ls, n; simpl; intros; intuition try congruence. + intros A ls x n; split; [ revert A ls x n | intro; subst; eauto using repeat_length, repeat_spec ]. + induction ls as [|a ls IHls], n; simpl; intros; intuition try congruence. f_equal; auto. Qed. @@ -1714,13 +1721,13 @@ Qed. Lemma pointwise_map {A B} : Proper ((pointwise_relation _ eq) ==> eq ==> eq) (@List.map A B). Proof. repeat intro; cbv [pointwise_relation] in *; subst. - match goal with [H:list _ |- _ ] => induction H as [|? IH] end; [reflexivity|]. + match goal with [H:list _ |- _ ] => induction H as [|? IH IHIH] end; [reflexivity|]. simpl. rewrite IHIH. congruence. Qed. Lemma map_map2 {A B C D} (f:A -> B -> C) (g:C -> D) (xs:list A) (ys:list B) : List.map g (map2 f xs ys) = map2 (fun (a : A) (b : B) => g (f a b)) xs ys. Proof. - revert ys; induction xs; intros; [reflexivity|]. + revert ys; induction xs as [|a xs IHxs]; intros ys; [reflexivity|]. destruct ys; [reflexivity|]. simpl. rewrite IHxs. reflexivity. Qed. @@ -1728,7 +1735,7 @@ Qed. Lemma map2_fst {A B C} (f:A -> C) (xs:list A) : forall (ys:list B), length xs = length ys -> map2 (fun (a : A) (_ : B) => f a) xs ys = List.map f xs. Proof. - induction xs; intros; [reflexivity|]. + induction xs as [|a xs IHxs]; intros ys **; [reflexivity|]. destruct ys; [simpl in *; discriminate|]. simpl. rewrite IHxs by eauto. reflexivity. Qed. @@ -1736,7 +1743,7 @@ Qed. Lemma map2_flip {A B C} (f:A -> B -> C) (xs:list A) : forall (ys: list B), map2 (fun b a => f a b) ys xs = map2 f xs ys. Proof. - induction xs; destruct ys; try reflexivity; []. + induction xs as [|a xs IHxs]; destruct ys; try reflexivity; []. simpl. rewrite IHxs. reflexivity. Qed. @@ -1747,6 +1754,6 @@ Proof. intros. rewrite map2_flip. eauto using map2_fst. Qed. Lemma map2_map {A B C A' B'} (f:A -> B -> C) (g:A' -> A) (h:B' -> B) (xs:list A') (ys:list B') : map2 f (List.map g xs) (List.map h ys) = map2 (fun a b => f (g a) (h b)) xs ys. Proof. - revert ys; induction xs; destruct ys; intros; try reflexivity; []. + revert ys; induction xs as [|a xs IHxs]; destruct ys; intros; try reflexivity; []. simpl. rewrite IHxs. reflexivity. Qed. diff --git a/src/Util/NUtil.v b/src/Util/NUtil.v index d76be63aa..9321f2b23 100644 --- a/src/Util/NUtil.v +++ b/src/Util/NUtil.v @@ -26,7 +26,7 @@ Module N. Lemma size_nat_equiv : forall n, N.size_nat n = N.to_nat (N.size n). Proof. - destruct n; auto; simpl; induction p; simpl; auto; rewrite IHp, Pnat.Pos2Nat.inj_succ; reflexivity. + destruct n as [|p]; auto; simpl; induction p as [p IHp|p IHp|]; simpl; auto; rewrite IHp, Pnat.Pos2Nat.inj_succ; reflexivity. Qed. Lemma size_nat_le a b : (a <= b)%N -> (N.size_nat a <= N.size_nat b)%nat. @@ -39,7 +39,7 @@ Module N. Lemma shiftr_size : forall n bound, N.size_nat n <= bound -> N.shiftr_nat n bound = 0%N. Proof. - intros. + intros n bound H. rewrite <- (Nat2N.id bound). rewrite Nshiftr_nat_equiv. destruct (N.eq_dec n 0); subst; [apply N.shiftr_0_l|]. @@ -86,7 +86,7 @@ Module N. then S (2 * N.to_nat (N.shiftr_nat n (S i))) else (2 * N.to_nat (N.shiftr_nat n (S i))). Proof. - intros. + intros n i. rewrite Nshiftr_nat_S. case_eq (N.testbit_nat n i); intro testbit_i; pose proof (Nshiftr_nat_spec n i 0) as shiftr_n_odd; diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 99d0be29c..80169c784 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -105,8 +105,8 @@ Ltac nat_beq_to_eq := Lemma div_minus : forall a b, b <> 0 -> (a + b) / b = a / b + 1. Proof. - intros. - assert (b = 1 * b) by omega. + intros a b H. + assert (H0 : b = 1 * b) by omega. rewrite H0 at 1. rewrite <- Nat.div_add by auto. reflexivity. @@ -114,7 +114,7 @@ Qed. Lemma pred_mod : forall m, (0 < m)%nat -> ((pred m) mod m)%nat = pred m. Proof. - intros; apply Nat.mod_small. + intros m H; apply Nat.mod_small. destruct m; try omega; rewrite Nat.pred_succ; auto. Qed. @@ -141,7 +141,7 @@ Qed. Lemma divide2_1mod4_nat : forall c x, c = x / 4 -> x mod 4 = 1 -> exists y, 2 * y = (x / 2). Proof. assert (4 <> 0) as ne40 by omega. - induction c; intros; pose proof (div_mod x 4 ne40); rewrite <- H in H1. { + induction c; intros x H H0; pose proof (div_mod x 4 ne40) as H1; rewrite <- H in H1. { rewrite H0 in H1. simpl in H1. rewrite H1. @@ -155,8 +155,8 @@ Proof. apply Nat.add_cancel_r in H. replace x with ((x - 4) + (1 * 4)) in H0 by omega. rewrite Nat.mod_add in H0 by auto. - pose proof (IHc _ H H0). - destruct H2. + pose proof (IHc _ H H0) as H2. + destruct H2 as [x0 H2]. exists (x0 + 1). rewrite <- (Nat.sub_add 4 x) in H1 at 1 by auto. replace (4 * c + 4 + x mod 4) with (4 * c + x mod 4 + 4) in H1 by omega. @@ -265,7 +265,7 @@ Hint Rewrite eq_nat_dec_refl : natsimplify. (** Helper to get around the lack of function extensionality *) Definition eq_nat_dec_right_val n m (pf0 : n <> m) : { pf | eq_nat_dec n m = right pf }. Proof. - revert dependent n; induction m; destruct n as [|n]; simpl; + revert dependent n; induction m as [|m IHm]; destruct n as [|n]; simpl; intro pf0; [ (exists pf0; exfalso; abstract congruence) | eexists; reflexivity diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index 74fe96d6b..e99197ece 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -11,7 +11,7 @@ Lemma in_ZPGroup_range (n : Z) (n_pos : 1 < n) (p : Z) : List.In p (FGroup.s (ZPGroup n n_pos)) -> 1 <= p < n. Proof. unfold ZPGroup; simpl; intros Hin. -pose proof (IGroup.isupport_incl Z (pmult n) (mkZp n) 1 Z.eq_dec). +pose proof (IGroup.isupport_incl Z (pmult n) (mkZp n) 1 Z.eq_dec) as H. unfold List.incl in *. specialize (H p Hin). apply in_mkZp in H; auto. @@ -29,7 +29,7 @@ Lemma generator_subgroup_is_group p (lt_1_p : 1 < p): forall y, -> forall a, List.In a (FGroup.s (ZPGroup p lt_1_p)) -> List.In a (EGroup.support Z.eq_dec y (ZPGroup p lt_1_p)). Proof. - intros. + intros y H a H0. destruct H as [in_ZPGroup_y y_order]. pose proof (EGroup.support_incl_G Z Z.eq_dec (pmult p) y (ZPGroup p lt_1_p) in_ZPGroup_y). eapply Permutation.permutation_in; [|eauto]. @@ -67,7 +67,7 @@ Qed. Lemma p_odd : Z.odd p = true. Proof using neq_p_2 prime_p. - pose proof (Z.prime_odd_or_2 p prime_p). + pose proof (Z.prime_odd_or_2 p prime_p) as H. destruct H; auto. Qed. @@ -82,7 +82,7 @@ Qed. Lemma fermat_little: forall a (a_nonzero : a mod p <> 0), a ^ (p - 1) mod p = 1. Proof using prime_p. - intros. + intros a a_nonzero. assert (rel_prime a p). { apply rel_prime_mod_rev; try prime_bound. assert (0 < p) as p_pos by prime_bound. @@ -97,7 +97,7 @@ Qed. Lemma fermat_inv : forall a, a mod p <> 0 -> ((a^(p-2) mod p) * a) mod p = 1. Proof using prime_p. - intros. + intros a H. pose proof (prime_ge_2 _ prime_p). rewrite Zmult_mod_idemp_l. replace (a ^ (p - 2) * a) with (a^(p-1)). @@ -120,7 +120,7 @@ Qed. Lemma euler_criterion_square_reverse : forall a (a_nonzero : a mod p <> 0), (exists b, b * b mod p = a) -> (a ^ x mod p = 1). Proof using Type*. - intros ? ? a_square. + intros a a_nonzero a_square. destruct a_square as [b a_square]. assert (b mod p <> 0) as b_nonzero. { intuition. @@ -170,7 +170,7 @@ Ltac ereplace x := match type of x with ?t => Lemma euler_criterion_square : forall a (a_range : 1 <= a <= p - 1) (pow_a_x : a ^ x mod p = 1), exists b, b * b mod p = a. Proof using Type*. - intros. + intros a a_range pow_a_x. destruct (exists_primitive_root_power) as [y [in_ZPGroup_y [y_order gpow_y]]]; auto. destruct (gpow_y a a_range) as [j [j_range pow_y_j]]; clear gpow_y. rewrite Z.mod_pow in pow_a_x by prime_bound. @@ -207,7 +207,7 @@ Qed. Lemma euler_criterion : forall a (a_range : 1 <= a <= p - 1), (a ^ x mod p = 1) <-> exists b, b * b mod p = a. Proof using Type*. - intros; split. { + intros a a_range; split. { exact (euler_criterion_square _ a_range). } { apply euler_criterion_square_reverse; auto. @@ -219,21 +219,21 @@ Qed. Lemma euler_criterion_nonsquare : forall a (a_range : 1 <= a <= p - 1), (a ^ x mod p <> 1) <-> ~ (exists b, b * b mod p = a). Proof using Type*. - split; intros A B; apply (euler_criterion a a_range) in B; congruence. + intros a a_range; split; intros A B; apply (euler_criterion a a_range) in B; congruence. Qed. End EulerCriterion. Lemma divide2_1mod4 : forall x (x_1mod4 : x mod 4 = 1) (x_nonneg : 0 <= x), (2 | x / 2). Proof. - intros. + intros x x_1mod4 x_nonneg0. assert (Z.to_nat x mod 4 = 1)%nat as x_1mod4_nat. { replace 1 with (Z.of_nat 1) in * by auto. replace (x mod 4) with (Z.of_nat (Z.to_nat x mod 4)) in * by (rewrite mod_Zmod by omega; rewrite Z2Nat.id; auto). apply Nat2Z.inj in x_1mod4; auto. } - remember (Z.to_nat x / 4)%nat as c. + remember (Z.to_nat x / 4)%nat as c eqn:Heqc. destruct (divide2_1mod4_nat c (Z.to_nat x) Heqc x_1mod4_nat) as [k k_id]. replace 2%nat with (Z.to_nat 2) in * by auto. apply inj_eq in k_id. @@ -247,7 +247,7 @@ Qed. Lemma minus1_even_pow : forall x y, (2 | y) -> (1 < x) -> (0 <= y) -> ((x - 1) ^ y mod x = 1). Proof. - intros ? ? divide_2_y lt_1_x y_nonneg. + intros x y divide_2_y lt_1_x y_nonneg. apply Zdivide_Zdiv_eq in divide_2_y; try omega. rewrite divide_2_y. rewrite Z.pow_mul_r by omega. @@ -261,7 +261,7 @@ Proof. do 2 rewrite Zmod_1_l by auto; auto. } rewrite <- (Z2Nat.id (y / 2)) by omega. - induction (Z.to_nat (y / 2)); try apply Zmod_1_l; auto. + induction (Z.to_nat (y / 2)) as [|n IHn]; try apply Zmod_1_l; auto. rewrite Nat2Z.inj_succ. rewrite Z.pow_succ_r by apply Zle_0_nat. rewrite Zmult_mod. @@ -281,7 +281,7 @@ Qed. Lemma div2_p_1mod4 : forall (p : Z) (prime_p : prime p) (neq_p_2: p <> 2), (p / 2) * 2 + 1 = p. Proof. - intros. + intros p prime_p neq_p_2. destruct (Z.prime_odd_or_2 p prime_p); intuition. rewrite <- Zdiv2_div. pose proof (Zdiv2_odd_eqn p); break_match; break_match_hyps; congruence || omega. @@ -290,7 +290,7 @@ Qed. Lemma minus1_square_1mod4 : forall (p : Z) (prime_p : prime p), (p mod 4 = 1)%Z -> exists b : Z, (b * b mod p = p - 1)%Z. Proof. - intros. + intros p prime_p H. assert (p <> 2) as neq_p_2 by (apply prime_1mod4_neq2; auto). apply (euler_criterion (p / 2) p prime_p). + auto. diff --git a/src/Util/Relations.v b/src/Util/Relations.v index d6b63b38f..8859a3bcc 100644 --- a/src/Util/Relations.v +++ b/src/Util/Relations.v @@ -38,7 +38,8 @@ Global Instance Equivalence_and {A B RA RB} {Equivalence_RB:@Equivalence B RB} : Equivalence (fun ab AB => RA (fst ab) (fst AB) /\ RB (snd ab) (snd AB)). Proof. - destruct Equivalence_RA as [], Equivalence_RB as []; cbv in *|-. + do 2 match goal with H : Equivalence _ |- _ => destruct H end; + cbv in *|-. repeat match goal with | _ => intro | _ => split diff --git a/src/Util/Sum.v b/src/Util/Sum.v index fe7fe662b..4d4fde6ac 100644 --- a/src/Util/Sum.v +++ b/src/Util/Sum.v @@ -10,10 +10,12 @@ Definition sumwise {A B} (RA:relation A) (RB : relation B) : relation (A + B) | _, _ => False end. -Global Instance Equivalence_sumwise {A B} {RA:relation A} {RB:relation B} - {RA_equiv:Equivalence RA} {RB_equiv:Equivalence RB} - : Equivalence (sumwise RA RB). +Global Instance Equivalence_sumwise + : forall {A B} {RA:relation A} {RB:relation B} + {RA_equiv:Equivalence RA} {RB_equiv:Equivalence RB}, + Equivalence (sumwise RA RB). Proof. + intros A B RA RB RA_equiv RB_equiv. split; repeat intros [?|?]; simpl; trivial; destruct RA_equiv, RB_equiv; try tauto; eauto. Qed. diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 3fa0dabde..3f3c31fe2 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -137,7 +137,7 @@ end. Lemma to_list_from_list : forall {T} (n:nat) (xs:list T) pf, to_list n (from_list n xs pf) = xs. Proof. - destruct xs; simpl; intros; subst; auto. + destruct xs as [|t xs]; simpl; intros; subst; auto. generalize dependent t. simpl in *. induction xs; simpl in *; intros; congruence. Qed. @@ -156,7 +156,7 @@ Lemma from_list'_to_list' : forall T n (xs:tuple' T n), forall x xs' pf, to_list' n xs = cons x xs' -> from_list' x n xs' pf = xs. Proof. - induction n; intros. + induction n; intros xs x xs' pf H. { simpl in *. injection H; clear H; intros; subst. congruence. } { destruct xs eqn:Hxs; destruct xs' eqn:Hxs'; @@ -166,7 +166,7 @@ Qed. Lemma from_list_to_list : forall {T n} (xs:tuple T n) pf, from_list n (to_list n xs) pf = xs. Proof. - destruct n; auto; intros; simpl in *. + destruct n as [|n]; auto; intros xs pf; simpl in *. { destruct xs; auto. } { destruct (to_list' n xs) eqn:H; try discriminate. eapply from_list'_to_list'; assumption. } @@ -356,7 +356,9 @@ Lemma map_S' {n A B} (f:A -> B) (xs:tuple A (S n)) (x:A) : map (n:=S (S n)) f (xs, x) = (map (n:=S n) f xs, f x). Proof. tuple_maps_to_list_maps. + let lxs := match goal with lxs : list _ |- _ => lxs end in destruct lxs as [|x' lxs']; [simpl in *; discriminate|]. + let x0 := match goal with H : _ = _ |- _ => H end in change ( f x :: List.map f (to_list (S n) (from_list (S n) (x' :: lxs') x0)) = f x :: to_list (S n) (map f (from_list (S n) (x' :: lxs') x0)) ). tuple_maps_to_list_maps. reflexivity. @@ -369,7 +371,9 @@ Lemma map2_S' {n A B C} (f:A -> B -> C) (xs:tuple A (S n)) (ys:tuple B (S n)) (x : map2 (n:=S (S n)) f (xs, x) (ys, y) = (map2 (n:=S n) f xs ys, f x y). Proof. tuple_maps_to_list_maps. + let lxs := match goal with lxs : list A |- _ => lxs end in destruct lxs as [|x' lxs']; [simpl in *; discriminate|]. + let lys := match goal with lxs : list B |- _ => lxs end in destruct lys as [|y' lys']; [simpl in *; discriminate|]. change ( f x y :: ListUtil.map2 f (to_list (S n) (from_list (S n) (x' :: lxs') x1)) (to_list (S n) (from_list (S n) (y' :: lys') x0)) = f x y :: to_list (S n) (map2 f (from_list (S n) (x' :: lxs') x1) (from_list (S n) (y' :: lys') x0)) ). @@ -497,13 +501,13 @@ Section Equivalence. Global Instance Equivalence_fieldwise' {R_equiv:Equivalence R} {n:nat} : Equivalence (fieldwise' n R). Proof using Type. constructor; exact _. Qed. - Global Instance Reflexive_fieldwise {R_Reflexive:Reflexive R} {n:nat} : Reflexive (fieldwise n R) | 5. + Global Instance Reflexive_fieldwise {R_Reflexive:Reflexive R} : forall {n:nat}, Reflexive (fieldwise n R) | 5. Proof using Type. destruct n; (repeat constructor || exact _). Qed. - Global Instance Symmetric_fieldwise {R_Symmetric:Symmetric R} {n:nat} : Symmetric (fieldwise n R) | 5. + Global Instance Symmetric_fieldwise {R_Symmetric:Symmetric R} : forall {n:nat}, Symmetric (fieldwise n R) | 5. Proof using Type. destruct n; (repeat constructor || exact _). Qed. - Global Instance Transitive_fieldwise {R_Transitive:Transitive R} {n:nat} : Transitive (fieldwise n R) | 5. + Global Instance Transitive_fieldwise {R_Transitive:Transitive R} : forall {n:nat}, Transitive (fieldwise n R) | 5. Proof using Type. destruct n; (repeat constructor || exact _). Qed. - Global Instance Equivalence_fieldwise {R_equiv:Equivalence R} {n:nat} : Equivalence (fieldwise n R). + Global Instance Equivalence_fieldwise {R_equiv:Equivalence R} : forall {n:nat}, Equivalence (fieldwise n R). Proof using Type. constructor; exact _. Qed. End Equivalence. @@ -511,7 +515,7 @@ Arguments fieldwise' {A B n} _ _ _. Arguments fieldwise {A B n} _ _ _. Local Hint Extern 0 => solve [ solve_decidable_transparent ] : typeclass_instances. -Global Instance dec_fieldwise' {A RA} {HA : DecidableRel RA} {n} : DecidableRel (@fieldwise' A A n RA) | 10. +Global Instance dec_fieldwise' {A RA} {HA : DecidableRel RA} : forall {n}, DecidableRel (@fieldwise' A A n RA) | 10. Proof. induction n; simpl @fieldwise'. { exact _. } @@ -519,7 +523,7 @@ Proof. exact _. } Defined. -Global Instance dec_fieldwise {A RA} {HA : DecidableRel RA} {n} : DecidableRel (@fieldwise A A n RA) | 10. +Global Instance dec_fieldwise {A RA} {HA : DecidableRel RA} : forall {n}, DecidableRel (@fieldwise A A n RA) | 10. Proof. destruct n; unfold fieldwise; exact _. Defined. @@ -574,7 +578,7 @@ Lemma fieldwiseb'_fieldwise' :forall {A B} n R Rb (forall a b, Rb a b = true <-> R a b) -> (fieldwiseb' Rb a b = true <-> fieldwise' R a b). Proof. - intros. + intros A B n R Rb a b H. revert n a b; induction n; intros; simpl @tuple' in *; simpl fieldwiseb'; simpl fieldwise'; auto. @@ -588,7 +592,7 @@ Lemma fieldwiseb_fieldwise :forall {A B} n R Rb (forall a b, Rb a b = true <-> R a b) -> (fieldwiseb Rb a b = true <-> fieldwise R a b). Proof. - intros; destruct n; simpl @tuple in *; + intros A B n R Rb a b H; destruct n; simpl @tuple in *; simpl @fieldwiseb; simpl @fieldwise; try tauto. auto using fieldwiseb'_fieldwise'. Qed. @@ -617,7 +621,7 @@ end. Lemma from_list_default'_eq : forall {T} (d : T) xs n y pf, from_list_default' d y n xs = from_list' y n xs pf. Proof. - induction xs; destruct n; intros; simpl in *; + induction xs as [|?? IHxs]; destruct n; intros; simpl in *; solve [ congruence (* 8.5 *) | erewrite IHxs; reflexivity ]. (* 8.4 *) Qed. @@ -652,7 +656,7 @@ Require Import Coq.Lists.SetoidList. Lemma fieldwise_to_list_iff : forall {T n} R (s t : tuple T n), (fieldwise R s t <-> Forall2 R (to_list _ s) (to_list _ t)). Proof. - induction n; split; intros. + induction n as [|n IHn]; intros R s t; split; intros. + constructor. + cbv [fieldwise]. auto. + destruct n; cbv [tuple to_list fieldwise] in *. @@ -774,7 +778,7 @@ Lemma from_list_cons {A n}: forall (xs : list A) a (H:length (a::xs)=S n), from_list (S n) (a :: xs) H = append a (from_list n xs (length_cons_full _ _ _ H)). Proof. - destruct n; intros; destruct xs; distr_length; [reflexivity|]. + destruct n; intros xs a H; destruct xs; distr_length; [reflexivity|]. cbv [from_list]; rewrite !from_list'_cons. rewrite <-!from_list_default'_eq with (d:=a). reflexivity. @@ -904,7 +908,7 @@ Lemma mapi_with'_left_step {T A B n} f a0: (fst (mapi_with' i f start xs)) a0)) (snd (mapi_with' i f start xs))). Proof. - induction n; intros; [subst; simpl; repeat f_equal; omega|]. + induction n as [|? IHn]; intros; [subst; simpl; repeat f_equal; omega|]. rewrite mapi_with'_step; autorewrite with cancel_pair. rewrite tl_left_append, hd_left_append. erewrite IHn by reflexivity; subst; autorewrite with cancel_pair. @@ -951,12 +955,12 @@ Proof. Qed. Lemma to_list_repeat {A} (a:A) n : to_list _ (repeat a n) = List.repeat a n. -Proof. induction n; [reflexivity|destruct n; simpl in *; congruence]. Qed. +Proof. induction n as [|n]; [reflexivity|destruct n; simpl in *; congruence]. Qed. -Global Instance map'_Proper {n A B} : Proper (pointwise_relation _ eq ==> eq ==> eq) (fun f => @map' A B f n) | 10. +Global Instance map'_Proper : forall {n A B}, Proper (pointwise_relation _ eq ==> eq ==> eq) (fun f => @map' A B f n) | 10. Proof. - induction n. + induction n as [|n IHn]; intros. { compute; intros; subst; auto. } { cbv [pointwise_relation Proper respectful] in *. intros f g Hfg x y ?; subst y. @@ -964,8 +968,8 @@ Proof. congruence. } Qed. -Global Instance map_Proper {n A B} : Proper (pointwise_relation _ eq ==> eq ==> eq) (@map n A B) | 10. +Global Instance map_Proper : forall {n A B}, Proper (pointwise_relation _ eq ==> eq ==> eq) (@map n A B) | 10. Proof. - destruct n; [ | apply map'_Proper ]. + destruct n; intros; [ | apply map'_Proper ]. { repeat (intros [] || intro); auto. } Qed. diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index c8aa9a4e5..64cfda434 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -66,9 +66,9 @@ Module Word. Theorem weqb_hetero_homo_true_iff : forall sz x y, @weqb_hetero sz sz x y = true <-> x = y. Proof. - etransitivity; [ apply weqb_hetero_true_iff | ]. + intros sz x y; etransitivity; [ apply weqb_hetero_true_iff | ]. split; [ intros [pf H] | intro ]; try (subst y; exists eq_refl; reflexivity). - revert y H; induction x as [|b n x IHx]; intros. + revert y H; induction x as [|b n x IHx]; intros y H. { subst y; refine match pf in (_ = z) return match z return 0 = z -> Prop with @@ -184,7 +184,7 @@ Section Pow2. Lemma Zpow_pow2 : forall n, pow2 n = Z.to_nat (2 ^ (Z.of_nat n)). Proof. - induction n; intros; auto. + induction n as [|n IHn]; intros; auto. simpl pow2. rewrite Nat2Z.inj_succ. rewrite Z.pow_succ_r by apply Zle_0_nat. @@ -196,7 +196,7 @@ Section Pow2. Lemma Npow2_gt0 : forall x, (0 < Npow2 x)%N. Proof. - intros; induction x. + intros x; induction x as [|x IHx]. - simpl; apply N.lt_1_r; intuition. @@ -218,7 +218,7 @@ Section Pow2. Lemma Npow2_N: forall n, Npow2 n = (2 ^ N.of_nat n)%N. Proof. - induction n. + induction n as [|n IHn]. - simpl; intuition. @@ -232,7 +232,7 @@ Section Pow2. (Z.log2 (Z.of_N x) < Z.of_nat n)%Z -> (x < Npow2 n)%N. Proof. - intros. + intros x n H. apply N2Z.inj_lt. rewrite Npow2_N, N2Z.inj_pow, nat_N_Z. destruct (N.eq_dec x 0%N) as [e|e]. @@ -247,7 +247,7 @@ Section Pow2. Lemma Npow2_ordered: forall n m, (n <= m)%nat -> (Npow2 n <= Npow2 m)%N. Proof. - induction n; intros m H; try rewrite Npow2_succ. + induction n as [|n IHn]; intros m H; try rewrite Npow2_succ. - simpl; apply Npow2_ge1. @@ -299,7 +299,7 @@ Section WordToN. Lemma wbit_large {n} (x: word n) (k: nat) : n <= k -> wbit x k = false. Proof. - revert k; induction x, k; intro H; simpl; try reflexivity; try omega. + revert k; induction x as [|b n x IHx], k; intro H; simpl; try reflexivity; try omega. apply IHx; omega. Qed. @@ -354,17 +354,17 @@ Section WordToN. end = N.double x) as kill_match by ( induction x; simpl; intuition). - induction n; intros. + induction n as [|n IHn]; intros x k. - shatter x; simpl; intuition. - revert IHn; rewrite <- (N2Nat.id k). - generalize (N.to_nat k) as k'; intros; clear k. + generalize (N.to_nat k) as k'; intros k' IHn; clear k. rewrite Nat2N.id in *. - induction k'. + induction k' as [|k' IHk']. - + clear IHn; induction x; simpl; intuition. + + clear IHn; induction x as [|b ? x IHx]; simpl; intuition. destruct (wordToN x), b; simpl; intuition. + clear IHk'. @@ -386,10 +386,11 @@ Section WordToN. destruct (whd x); try rewrite N.testbit_odd_succ; try rewrite N.testbit_even_succ; + let k' := k' in try abstract ( unfold N.le; simpl; induction (N.of_nat k'); intuition; - try inversion H); + match goal with H : _ |- _ => solve [ inversion H ] end); rewrite IHn; rewrite Nat2N.id; reflexivity. @@ -400,7 +401,7 @@ Section WordToN. then N.testbit v (N.of_nat k) else false. Proof. - revert k v; induction sz, k; intros; try reflexivity. + revert k v; induction sz as [|sz IHsz], k; intros v **; try reflexivity. { destruct v as [|p]; simpl; try reflexivity. destruct p; simpl; reflexivity. } { pose proof (fun v k => IHsz k (Npos v)) as IHszp. @@ -483,7 +484,7 @@ Section WordToN. Lemma wordToN_split1: forall {n m} x, wordToN (@split1 n m x) = N.land (wordToN x) (wordToN (wones n)). Proof. - intros. + intros n m x. pose proof (Word.combine_split _ _ x) as C; revert C. generalize (split1 n m x) as a, (split2 n m x) as b. @@ -494,7 +495,7 @@ Section WordToN. repeat rewrite wordToN_testbit. revert x a b. - induction n, m; intros; + induction n as [|n IHn], m; intros; shatter a; shatter b; induction (N.to_nat x) as [|n0]; try rewrite <- (Nat2N.id n0); @@ -506,7 +507,7 @@ Section WordToN. Lemma wordToN_split2: forall {n m} x, wordToN (@split2 n m x) = N.shiftr (wordToN x) (N.of_nat n). Proof. - intros. + intros n m x. pose proof (Word.combine_split _ _ x) as C; revert C. generalize (split1 n m x) as a, (split2 n m x) as b. @@ -519,7 +520,7 @@ Section WordToN. try apply N_ge_0. revert x a b. - induction n, m; intros; + induction n as [|n IHn], m; intros; shatter a; try apply N_ge_0. @@ -545,7 +546,7 @@ Section WordToN. Lemma wordToN_wones: forall x, wordToN (wones x) = N.ones (N.of_nat x). Proof. - induction x. + induction x as [|x IHx]. - simpl; intuition. @@ -576,7 +577,7 @@ Section WordToN. wordToN (@Word.combine n a m b) = N.lxor (N.shiftl (wordToN b) (N.of_nat n)) (wordToN a). Proof. - intros; symmetry. + intros n m a b; symmetry. replaceAt1 a with (Word.split1 _ _ (Word.combine a b)) by (apply Word.split1_combine). @@ -608,7 +609,7 @@ Section WordToN. Lemma NToWord_equal: forall n (x y: word n), wordToN x = wordToN y -> x = y. Proof. - intros. + intros n x y H. rewrite <- (NToWord_wordToN _ x). rewrite <- (NToWord_wordToN _ y). rewrite H; reflexivity. @@ -617,7 +618,7 @@ Section WordToN. Lemma Npow2_ignore: forall {n} (x: word n), x = NToWord _ (wordToN x + Npow2 n). Proof. - intros. + intros n x. rewrite <- (NToWord_wordToN n x) at 1. repeat rewrite NToWord_nat. rewrite N2Nat.inj_add. @@ -632,7 +633,7 @@ End WordToN. Section WordBounds. Lemma word_size_bound : forall {n} (w: word n), (wordToN w < Npow2 n)%N. Proof. - intros; pose proof (wordToNat_bound w) as B; + intros n w; pose proof (wordToNat_bound w) as B; rewrite of_nat_lt in B; rewrite <- Npow2_nat in B; rewrite N2Nat.id in B; @@ -714,13 +715,13 @@ Section WordBounds. Lemma wordize_and: forall {n} (x y: word n), wordToN (wand x y) = N.land (wordToN x) (wordToN y). Proof. - intros. + intros n x y. apply N.bits_inj_iff; unfold N.eqf; intro k. rewrite N.land_spec. repeat rewrite wordToN_testbit. revert x y. generalize (N.to_nat k) as k'. - induction n; intros; shatter x; shatter y; simpl; [reflexivity|]. + induction n as [|n IHn]; intros; shatter x; shatter y; simpl; [reflexivity|]. induction k'; [reflexivity|]. fold wand. rewrite IHn. @@ -730,13 +731,13 @@ Section WordBounds. Lemma wordize_or: forall {n} (x y: word n), wordToN (wor x y) = N.lor (wordToN x) (wordToN y). Proof. - intros. + intros n x y. apply N.bits_inj_iff; unfold N.eqf; intro k. rewrite N.lor_spec. repeat rewrite wordToN_testbit. revert x y. generalize (N.to_nat k) as k'; clear k. - induction n; intros; shatter x; shatter y; simpl; [reflexivity|]. + induction n as [|n IHn]; intros; shatter x; shatter y; simpl; [reflexivity|]. induction k'; [reflexivity|]. rewrite IHn. reflexivity. @@ -756,7 +757,7 @@ Qed. Lemma weqb_false_iff : forall sz (x y : word sz), weqb x y = false <-> x <> y. Proof. - split; intros. + intros sz x y; split; intros. + intro eq_xy; apply weqb_true_iff in eq_xy; congruence. + case_eq (weqb x y); intros weqb_xy; auto. apply weqb_true_iff in weqb_xy. @@ -786,7 +787,7 @@ Fixpoint correct_wordsize_eq (x y : nat) : wordsize_eq x y -> x = y Lemma correct_wordsize_eq_refl n pf : correct_wordsize_eq n n pf = eq_refl. Proof. - induction n; [ reflexivity | simpl ]. + induction n as [|n IHn]; [ reflexivity | simpl ]. rewrite IHn; reflexivity. Qed. @@ -827,13 +828,13 @@ Definition clearbit {b} n {H:n < b} (w:word b) : word b := Lemma wordToNat_wzero {n} : wordToNat (wzero n) = 0. Proof. - unfold wzero; induction n; simpl; try rewrite_hyp!*; omega. + unfold wzero; induction n as [|n IHn]; simpl; try rewrite_hyp!*; omega. Qed. Lemma wordToNat_combine : forall {a} (wa:word a) {b} (wb:word b), wordToNat (wa ++ wb) = wordToNat wa + 2^a * wordToNat wb. Proof. - induction wa; intros; simpl; rewrite ?IHwa; break_match; nia. + induction wa as [|??? IHwa]; intros; simpl; rewrite ?IHwa; break_match; nia. Qed. Lemma wordToNat_zext_ge {n m pf} (w:word m) : wordToNat (@zext_ge n m pf w) = wordToNat w. @@ -853,7 +854,7 @@ Proof. | _ => I end. reflexivity. } - { intros; rewrite IHx; clear IHx; revert x. + { intros x' y y'; rewrite IHx; clear IHx; revert x. refine match x' in word Sn return match Sn return word Sn -> _ with | 0 => fun _ => True | S _ => fun x' => forall x, WS (f b' (whd x')) (bitwp f (x ++ y) (wtl x' ++ y')) = WS (f b' (whd (x' ++ y'))) (bitwp f (x ++ y) (wtl (x' ++ y'))) @@ -897,7 +898,7 @@ Proof. rewrite pow2_id in *. { assert (b - c = 0) by omega. assert (2^b <= 2^c) by auto using pow_le_mono_r with arith. - generalize dependent (b - c); intros; destruct x0; try omega; []. + generalize dependent (b - c); intros n x0 H0 H2; destruct x0; try omega; []. simpl; rewrite mul_0_r, add_0_r. rewrite mod_small by omega. omega. } @@ -929,7 +930,7 @@ Proof. rewrite pow2_id in *. { assert (b - c = 0) by omega. assert (2^b <= 2^c) by auto using pow_le_mono_r with arith. - generalize dependent (b - c); intros; destruct x0; try omega. + generalize dependent (b - c); intros n x0 H0 H2; destruct x0; try omega. simpl; rewrite mul_0_r, add_0_r. rewrite mod_small by omega. omega. } @@ -939,9 +940,9 @@ Qed. Lemma wordToNat_split1 : forall a b w, wordToNat (split1 a b w) = (wordToNat w) mod (2^a). Proof. - intro a; induction a. + intro a; induction a as [|a IHa]. { reflexivity. } - { simpl; intros; rewrite IHa; clear IHa. + { simpl; intros b w; rewrite IHa; clear IHa. rewrite (shatter_word w); simpl. change (2^a + (2^a + 0)) with (2 * 2^a). rewrite (mul_comm 2 (2^a)). @@ -983,7 +984,7 @@ Section Bounds. Lemma wordToN_wplus : bounds_2statement (@wplus _) Z.add. Proof. - intros. + intros sz x y H H0. rewrite <- wordize_plus; [rewrite N2Z.inj_add; reflexivity|]. destruct (N.eq_dec (wordToN x + wordToN y) 0%N) as [e|e]; [rewrite e; apply Npow2_gt0|]. @@ -1014,7 +1015,7 @@ Section Bounds. Lemma wordToN_wmult : bounds_2statement (@wmult _) Z.mul. Proof. - intros. + intros sz x y H H0. rewrite <- wordize_mult; [rewrite N2Z.inj_mul; reflexivity|]. destruct (N.eq_dec (wordToN x * wordToN y) 0%N) as [e|e]; [rewrite e; apply Npow2_gt0|]. @@ -1277,7 +1278,7 @@ Arguments wlast {_} _. Lemma combine_winit_wlast : forall {sz} a b (c:word (sz+1)), @combine sz a 1 b = c <-> a = winit c /\ b = (WS (wlast c) WO). Proof. - intros; split; unfold winit, wlast; intro H. + intros sz a b c; split; unfold winit, wlast; intro H. - rewrite <- H. rewrite split1_combine, split2_combine. @@ -1289,7 +1290,7 @@ Proof. - destruct H as [H0 H1]; rewrite H0. replace b with (split2 sz 1 c); [apply combine_split|]. rewrite H1. - generalize (split2 sz 1 c) as b'; intro. + generalize (split2 sz 1 c) as b'; intro b'. shatter b'. generalize (wtl b') as b''; intro; shatter b''; reflexivity. @@ -1309,7 +1310,7 @@ Qed. Lemma WordNZ_split1 : forall {n m} w, Z.of_N (Word.wordToN (Word.split1 n m w)) = Z.pow2_mod (Z.of_N (Word.wordToN w)) (Z.of_nat n). Proof. - intros; unfold Z.pow2_mod. + intros n m w; unfold Z.pow2_mod. rewrite wordToN_split1. apply Z.bits_inj_iff'; intros k Hpos. rewrite Z.land_spec. @@ -1324,28 +1325,28 @@ Proof. apply Z2N.inj_le; [apply Nat2Z.is_nonneg|assumption|]. etransitivity; [|apply N.ge_le; eassumption]. apply N.eq_le_incl. - induction n; simpl; reflexivity. + induction n as [|n IHn]; simpl; reflexivity. - rewrite Z.ones_spec_low, N.ones_spec_low; [reflexivity|assumption|split; [omega|]]. apply Z2N.inj_lt; [assumption|apply Nat2Z.is_nonneg|]. eapply N.lt_le_trans; [eassumption|]. apply N.eq_le_incl. - induction n; simpl; reflexivity. + induction n as [|n IHn]; simpl; reflexivity. Qed. (* TODO : automate *) Lemma WordNZ_split2 : forall {n m} w, Z.of_N (Word.wordToN (Word.split2 n m w)) = Z.shiftr (Z.of_N (Word.wordToN w)) (Z.of_nat n). Proof. - intros; unfold Z.pow2_mod. + intros n m w; unfold Z.pow2_mod. rewrite wordToN_split2. apply Z.bits_inj_iff'; intros k Hpos. rewrite Z2N.inj_testbit; [|assumption]. rewrite Z.shiftr_spec, N.shiftr_spec; [|apply N2Z.inj_le; rewrite Z2N.id|]; try assumption. rewrite Z2N.inj_testbit; [f_equal|omega]. rewrite Z2N.inj_add; [f_equal|assumption|apply Nat2Z.is_nonneg]. - induction n; simpl; reflexivity. + induction n as [|n IHn]; simpl; reflexivity. Qed. Lemma WordNZ_range : forall {n} B w, diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 936b4ce76..01e125e00 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -53,7 +53,7 @@ Module Z. Lemma pos_pow_nat_pos : forall x n, Z.pos x ^ Z.of_nat n > 0. Proof. - do 2 (intros; induction n; subst; simpl in *; auto with zarith). + do 2 (try intros x n; induction n as [|n]; subst; simpl in *; auto with zarith). rewrite <- Pos.add_1_r, Zpower_pos_is_exp. apply Zmult_gt_0_compat; auto; reflexivity. Qed. @@ -64,7 +64,7 @@ Module Z. Lemma pow_Z2N_Zpow : forall a n, 0 <= a -> ((Z.to_nat a) ^ n = Z.to_nat (a ^ Z.of_nat n)%Z)%nat. Proof. - intros; induction n; try reflexivity. + intros a n H; induction n as [|n IHn]; try reflexivity. rewrite Nat2Z.inj_succ. rewrite pow_succ_r by apply le_0_n. rewrite Z.pow_succ_r by apply Zle_0_nat. @@ -94,14 +94,14 @@ Module Z. Lemma divide2_even_iff : forall n, (2 | n) <-> Z.even n = true. Proof. - intro; split. { + intros n; split. { intro divide2_n. Z.divide_exists_mul; [ | pose proof (Z.mod_pos_bound n 2); omega]. rewrite divide2_n. apply Z.even_mul. } { intro n_even. - pose proof (Zmod_even n). + pose proof (Zmod_even n) as H. rewrite n_even in H. apply Zmod_divide; omega || auto. } @@ -109,7 +109,7 @@ Module Z. Lemma prime_odd_or_2 : forall p (prime_p : prime p), p = 2 \/ Z.odd p = true. Proof. - intros. + intros p prime_p. apply Decidable.imp_not_l; try apply Z.eq_decidable. intros p_neq2. pose proof (Zmod_odd p) as mod_odd. @@ -127,7 +127,7 @@ Module Z. Lemma shiftr_add_shiftl_high : forall n m a b, 0 <= n <= m -> 0 <= a < 2 ^ n -> Z.shiftr (a + (Z.shiftl b n)) m = Z.shiftr b (m - n). Proof. - intros. + intros n m a b H H0. rewrite !Z.shiftr_div_pow2, Z.shiftl_mul_pow2 by omega. replace (2 ^ m) with (2 ^ n * 2 ^ (m - n)) by (rewrite <-Z.pow_add_r by omega; f_equal; ring). @@ -141,7 +141,7 @@ Module Z. Lemma shiftr_add_shiftl_low : forall n m a b, 0 <= m <= n -> 0 <= a < 2 ^ n -> Z.shiftr (a + (Z.shiftl b n)) m = Z.shiftr a m + Z.shiftr b (m - n). Proof. - intros. + intros n m a b H H0. rewrite !Z.shiftr_div_pow2, Z.shiftl_mul_pow2, Z.shiftr_mul_pow2 by omega. replace (2 ^ n) with (2 ^ (n - m) * 2 ^ m) by (rewrite <-Z.pow_add_r by omega; f_equal; ring). @@ -155,8 +155,8 @@ Module Z. 0 <= a < 2 ^ n -> Z.testbit (a + Z.shiftl b n) i = Z.testbit b (i - n). Proof. - intros ? ?. - apply natlike_ind with (x := i); intros; try assumption; + intros i ?. + apply natlike_ind with (x := i); [ intros a b n | intros x H0 H1 a b n | ]; intros; try assumption; (destruct (Z_eq_dec 0 n); [ subst; rewrite Z.pow_0_r in *; replace a with 0 by omega; f_equal; ring | ]); try omega. rewrite <-Z.add_1_r at 1. rewrite <-Z.shiftr_spec by assumption. @@ -195,7 +195,7 @@ Module Z. Lemma land_add_land : forall n m a b, (m <= n)%nat -> Z.land ((Z.land a (Z.ones (Z.of_nat n))) + (Z.shiftl b (Z.of_nat n))) (Z.ones (Z.of_nat m)) = Z.land a (Z.ones (Z.of_nat m)). Proof. - intros. + intros n m a b H. rewrite !Z.land_ones by apply Nat2Z.is_nonneg. rewrite Z.shiftl_mul_pow2 by apply Nat2Z.is_nonneg. replace (b * 2 ^ Z.of_nat n) with @@ -232,7 +232,7 @@ Module Z. Lemma pow2_lt_or_divides : forall a b, 0 <= b -> 2 ^ a < 2 ^ b \/ (2 ^ a) mod 2 ^ b = 0. Proof. - intros. + intros a b H. destruct (Z_lt_dec a b); [left|right]. { apply Z.pow_lt_mono_r; auto; omega. } { replace a with (a - b + b) by ring. @@ -243,7 +243,7 @@ Module Z. Lemma odd_mod : forall a b, (b <> 0)%Z -> Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a. Proof. - intros. + intros a b H. rewrite Zmod_eq_full by assumption. rewrite <-Z.add_opp_r, Z.odd_add, Z.odd_opp, Z.odd_mul. case_eq (Z.odd b); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto using Bool.xorb_false_r. @@ -251,7 +251,7 @@ Module Z. Lemma mod_same_pow : forall a b c, 0 <= c <= b -> a ^ b mod a ^ c = 0. Proof. - intros. + intros a b c H. replace b with (b - c + c) by ring. rewrite Z.pow_add_r by omega. apply Z_mod_mult. @@ -287,14 +287,14 @@ Module Z. Lemma shiftr_le : forall a b i : Z, 0 <= i -> a <= b -> a >> i <= b >> i. Proof. - intros until 1. revert a b. apply natlike_ind with (x := i); intros; auto. + intros a b i ?; revert a b. apply natlike_ind with (x := i); intros; auto. rewrite !shiftr_succ, shiftr_1_r_le; eauto. reflexivity. Qed. Hint Resolve shiftr_le : zarith. Lemma ones_pred : forall i, 0 < i -> Z.ones (Z.pred i) = Z.shiftr (Z.ones i) 1. Proof. - induction i; [ | | pose proof (Pos2Z.neg_is_neg p) ]; try omega. + induction i as [|p|p]; [ | | pose proof (Pos2Z.neg_is_neg p) ]; try omega. intros. unfold Z.ones. rewrite !Z.shiftl_1_l, Z.shiftr_div_pow2, <-!Z.sub_1_r, Z.pow_1_r, <-!Z.add_opp_r by omega. @@ -310,12 +310,12 @@ Module Z. Lemma shiftr_ones' : forall a n, 0 <= a < 2 ^ n -> forall i, (0 <= i) -> Z.shiftr a i <= Z.ones (n - i) \/ n <= i. Proof. - intros until 1. + intros a n H. apply natlike_ind. + unfold Z.ones. rewrite Z.shiftr_0_r, Z.shiftl_1_l, Z.sub_0_r. omega. - + intros. + + intros x H0 H1. destruct (Z_lt_le_dec x n); try omega. intuition auto with zarith lia. left. @@ -360,7 +360,7 @@ Module Z. Lemma lor_shiftl : forall a b n, 0 <= n -> 0 <= a < 2 ^ n -> Z.lor a (Z.shiftl b n) = a + (Z.shiftl b n). Proof. - intros. + intros a b n H H0. apply Z.bits_inj'; intros t ?. rewrite Z.lor_spec, Z.shiftl_spec by assumption. destruct (Z_lt_dec t n). @@ -449,7 +449,7 @@ Module Z. Lemma pow2_mod_id_iff : forall a n, 0 <= n -> (Z.pow2_mod a n = a <-> 0 <= a < 2 ^ n). Proof. - intros. + intros a n H. rewrite Z.pow2_mod_spec by assumption. assert (0 < 2 ^ n) by Z.zero_bounds. rewrite Z.mod_small_iff by omega. @@ -460,8 +460,8 @@ Module Z. (forall n, ~ (n < x) -> Z.testbit a n = false) -> a < 2 ^ x. Proof. - intros. - assert (a = Z.pow2_mod a x). { + intros a x H H0. + assert (H1 : a = Z.pow2_mod a x). { apply Z.bits_inj'; intros. rewrite Z.testbit_pow2_mod by omega; break_match; auto. } @@ -472,7 +472,7 @@ Module Z. Lemma lor_range : forall x y n, 0 <= x < 2 ^ n -> 0 <= y < 2 ^ n -> 0 <= Z.lor x y < 2 ^ n. Proof. - intros; assert (0 <= n) by auto with zarith omega. + intros x y n H H0; assert (0 <= n) by auto with zarith omega. repeat match goal with | |- _ => progress intros | |- _ => rewrite Z.lor_spec @@ -493,7 +493,7 @@ Module Z. (0 <= y < 2 ^ n)%Z -> (0 <= Z.lor y (Z.shiftl x n) < 2 ^ (n + m))%Z. Proof. - intros. + intros x y n m H H0 H1 H2. apply Z.lor_range. { split; try omega. apply Z.lt_le_trans with (m := (2 ^ n)%Z); try omega. @@ -512,8 +512,8 @@ Module Z. Lemma Pos_land_upper_bound_l : forall a b, (Pos.land a b <= N.pos a)%N. Proof. - induction a; destruct b; intros; try solve [cbv; congruence]; - simpl; specialize (IHa b); case_eq (Pos.land a b); intro; simpl; + induction a as [a IHa|a IHa|]; destruct b as [b|b|]; try solve [cbv; congruence]; + simpl; specialize (IHa b); case_eq (Pos.land a b); intro p; simpl; try (apply N_le_1_l || apply N.le_0_l); intro land_eq; rewrite land_eq in *; unfold N.le, N.compare in *; rewrite ?Pos.compare_xI_xI, ?Pos.compare_xO_xI, ?Pos.compare_xO_xO; @@ -524,7 +524,7 @@ Module Z. Lemma land_upper_bound_l : forall a b, (0 <= a) -> (0 <= b) -> Z.land a b <= a. Proof. - intros. + intros a b H H0. destruct a, b; try solve [exfalso; auto]; try solve [cbv; congruence]. cbv [Z.land]. rewrite <-N2Z.inj_pos, <-N2Z.inj_le. @@ -542,7 +542,7 @@ Module Z. Lemma le_fold_right_max : forall low l x, (forall y, In y l -> low <= y) -> In x l -> x <= fold_right Z.max low l. Proof. - induction l; intros ? lower_bound In_list; [cbv [In] in *; intuition | ]. + induction l as [|a l IHl]; intros ? lower_bound In_list; [cbv [In] in *; intuition | ]. simpl. destruct (in_inv In_list); subst. + apply Z.le_max_l. @@ -553,13 +553,13 @@ Module Z. Lemma le_fold_right_max_initial : forall low l, low <= fold_right Z.max low l. Proof. - induction l; intros; try reflexivity. + induction l as [|a l IHl]; intros; try reflexivity. etransitivity; [ apply IHl | apply Z.le_max_r ]. Qed. Lemma add_compare_mono_r: forall n m p, (n + p ?= m + p) = (n ?= m). Proof. - intros. + intros n m p. rewrite <-!(Z.add_comm p). apply Z.add_compare_mono_l. Qed. @@ -997,7 +997,7 @@ Module Z. Lemma lt_mul_2_mod_sub : forall a b, b <> 0 -> b <= a < 2 * b -> a mod b = a - b. Proof. - intros. + intros a b H H0. replace (a mod b) with ((1 * b + (a - b)) mod b) by (f_equal; ring). rewrite Z.mod_add_l by auto. apply Z.mod_small. @@ -1093,7 +1093,7 @@ Module Z. Lemma lt_pow_2_shiftr : forall a n, 0 <= a < 2 ^ n -> a >> n = 0. Proof. - intros. + intros a n H. destruct (Z_le_dec 0 n). + rewrite Z.shiftr_div_pow2 by assumption. auto using Z.div_small. @@ -1118,7 +1118,7 @@ Module Z. Lemma lt_mul_2_pow_2_shiftr : forall a n, 0 <= a < 2 * 2 ^ n -> a >> n = if Z_lt_dec a (2 ^ n) then 0 else 1. Proof. - intros; break_match; [ apply lt_pow_2_shiftr; omega | ]. + intros a n H; break_match; [ apply lt_pow_2_shiftr; omega | ]. destruct (Z_le_dec 0 n). + replace (2 * 2 ^ n) with (2 ^ (n + 1)) in * by (rewrite Z.pow_add_r; try omega; ring). @@ -1217,7 +1217,7 @@ Module Z. Section ZInequalities. Lemma land_le : forall x y, (0 <= x)%Z -> (Z.land x y <= x)%Z. Proof. - intros; apply Z.ldiff_le; [assumption|]. + intros x y H; apply Z.ldiff_le; [assumption|]. rewrite Z.ldiff_land, Z.land_comm, Z.land_assoc. rewrite <- Z.land_0_l with (a := y); f_equal. rewrite Z.land_comm, Z.land_lnot_diag. @@ -1226,7 +1226,7 @@ Module Z. Lemma lor_lower : forall x y, (0 <= x)%Z -> (0 <= y)%Z -> (x <= Z.lor x y)%Z. Proof. - intros; apply Z.ldiff_le; [apply Z.lor_nonneg; auto|]. + intros x y H H0; apply Z.ldiff_le; [apply Z.lor_nonneg; auto|]. rewrite Z.ldiff_land. apply Z.bits_inj_iff'; intros k Hpos; apply Z.le_ge in Hpos. rewrite Z.testbit_0_l, Z.land_spec, Z.lnot_spec, Z.lor_spec; @@ -1240,7 +1240,7 @@ Module Z. -> (y <= z)%Z -> (Z.lor x y <= (2 ^ Z.log2_up (z+1)) - 1)%Z. Proof. - intros; apply Z.ldiff_le. + intros x y z H H0 H1; apply Z.ldiff_le. - apply Z.le_add_le_sub_r. replace 1%Z with (2 ^ 0)%Z by (cbv; reflexivity). @@ -1538,7 +1538,7 @@ Module N2Z. Lemma inj_shiftl: forall x y, Z.of_N (N.shiftl x y) = Z.shiftl (Z.of_N x) (Z.of_N y). Proof. - intros. + intros x y. apply Z.bits_inj_iff'; intros k Hpos. rewrite Z2N.inj_testbit; [|assumption]. rewrite Z.shiftl_spec; [|assumption]. diff --git a/src/Util/ZUtil/Land.v b/src/Util/ZUtil/Land.v index b3d3f3727..f46d541e9 100644 --- a/src/Util/ZUtil/Land.v +++ b/src/Util/ZUtil/Land.v @@ -5,7 +5,7 @@ Local Open Scope Z_scope. Module Z. Lemma land_same_r : forall a b, (a &' b) &' b = a &' b. Proof. - intros; apply Z.bits_inj'; intros. + intros a b; apply Z.bits_inj'; intros n H. rewrite !Z.land_spec. case_eq (Z.testbit b n); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; reflexivity. diff --git a/src/Util/ZUtil/Modulo.v b/src/Util/ZUtil/Modulo.v index 511898b48..4e14907e8 100644 --- a/src/Util/ZUtil/Modulo.v +++ b/src/Util/ZUtil/Modulo.v @@ -14,38 +14,38 @@ Module Z. Hint Resolve elim_mod : zarith. Lemma mod_add_full : forall a b c, (a + b * c) mod c = a mod c. - Proof. intros; destruct (Z_zerop c); try subst; autorewrite with zsimplify; reflexivity. Qed. + Proof. intros a b c; destruct (Z_zerop c); try subst; autorewrite with zsimplify; reflexivity. Qed. Hint Rewrite mod_add_full : zsimplify. Lemma mod_add_l_full : forall a b c, (a * b + c) mod b = c mod b. - Proof. intros; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed. + Proof. intros a b c; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed. Hint Rewrite mod_add_l_full : zsimplify. Lemma mod_add'_full : forall a b c, (a + b * c) mod b = a mod b. - Proof. intros; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed. + Proof. intros a b c; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed. Lemma mod_add_l'_full : forall a b c, (a * b + c) mod a = c mod a. - Proof. intros; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed. + Proof. intros a b c; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed. Hint Rewrite mod_add'_full mod_add_l'_full : zsimplify. Lemma mod_add_l : forall a b c, b <> 0 -> (a * b + c) mod b = c mod b. - Proof. intros; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed. + Proof. intros a b c H; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed. Lemma mod_add' : forall a b c, b <> 0 -> (a + b * c) mod b = a mod b. - Proof. intros; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed. + Proof. intros a b c H; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed. Lemma mod_add_l' : forall a b c, a <> 0 -> (a * b + c) mod a = c mod a. - Proof. intros; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed. + Proof. intros a b c H; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed. Lemma add_pow_mod_l : forall a b c, a <> 0 -> 0 < b -> ((a ^ b) + c) mod a = c mod a. Proof. - intros; replace b with (b - 1 + 1) by ring; + intros a b c H H0; replace b with (b - 1 + 1) by ring; rewrite Z.pow_add_r, Z.pow_1_r by omega; auto using Z.mod_add_l. Qed. Lemma mod_exp_0 : forall a x m, x > 0 -> m > 1 -> a mod m = 0 -> a ^ x mod m = 0. Proof. - intros. + intros a x m H H0 H1. replace x with (Z.of_nat (Z.to_nat x)) in * by (apply Z2Nat.id; omega). induction (Z.to_nat x). { simpl in *; omega. @@ -70,8 +70,8 @@ Module Z. Lemma mod_pow : forall (a m b : Z), (0 <= b) -> (m <> 0) -> a ^ b mod m = (a mod m) ^ b mod m. Proof. - intros; rewrite <- (Z2Nat.id b) by auto. - induction (Z.to_nat b); auto. + intros a m b H H0; rewrite <- (Z2Nat.id b) by auto. + induction (Z.to_nat b) as [|n IHn]; auto. rewrite Nat2Z.inj_succ. do 2 rewrite Z.pow_succ_r by apply Nat2Z.is_nonneg. rewrite Z.mul_mod by auto. @@ -90,7 +90,7 @@ Module Z. Lemma mul_div_eq_full : forall a m, m <> 0 -> m * (a / m) = (a - a mod m). Proof. - intros. rewrite (Z_div_mod_eq_full a m) at 2 by auto. ring. + intros a m H. rewrite (Z_div_mod_eq_full a m) at 2 by auto. ring. Qed. Hint Rewrite mul_div_eq_full using zutil_arith : zdiv_to_mod. @@ -126,14 +126,14 @@ Module Z. Lemma mul_div_eq : forall a m, m > 0 -> m * (a / m) = (a - a mod m). Proof. - intros. + intros a m H. rewrite (Z_div_mod_eq a m) at 2 by auto. ring. Qed. Lemma mul_div_eq' : (forall a m, m > 0 -> (a / m) * m = (a - a mod m))%Z. Proof. - intros. + intros a m H. rewrite (Z_div_mod_eq a m) at 2 by auto. ring. Qed. diff --git a/src/Util/ZUtil/Testbit.v b/src/Util/ZUtil/Testbit.v index a315f7e4b..175d07b02 100644 --- a/src/Util/ZUtil/Testbit.v +++ b/src/Util/ZUtil/Testbit.v @@ -22,7 +22,7 @@ Module Z. then true else if Z_lt_dec m n then true else false. Proof. - intros. + intros n m. repeat (break_match || autorewrite with Ztestbit); try reflexivity; try omega. unfold Z.ones. rewrite <- Z.shiftr_opp_r, Z.shiftr_eq_0 by (simpl; omega); simpl. @@ -34,7 +34,7 @@ Module Z. Lemma testbit_pow2_mod : forall a n i, 0 <= n -> Z.testbit (Z.pow2_mod a n) i = if Z_lt_dec i n then Z.testbit a i else false. Proof. - cbv [Z.pow2_mod]; intros; destruct (Z_le_dec 0 i); + cbv [Z.pow2_mod]; intros a n i H; destruct (Z_le_dec 0 i); repeat match goal with | |- _ => rewrite Z.testbit_neg_r by omega | |- _ => break_innermost_match_step @@ -50,7 +50,7 @@ Module Z. then if Z_lt_dec i 0 then false else Z.testbit a i else if Z_lt_dec i n then Z.testbit a i else false. Proof. - intros; destruct (Z_lt_dec n 0); [ | apply testbit_pow2_mod; omega ]. + intros a n i; destruct (Z_lt_dec n 0); [ | apply testbit_pow2_mod; omega ]. unfold Z.pow2_mod. autorewrite with Ztestbit_full; repeat break_match; @@ -80,7 +80,7 @@ Module Z. Lemma testbit_add_shiftl_low : forall i, (0 <= i) -> forall a b n, (i < n) -> Z.testbit (a + Z.shiftl b n) i = Z.testbit a i. Proof. - intros. + intros i H a b n H0. erewrite Z.testbit_low; eauto. rewrite Z.land_ones, Z.shiftl_mul_pow2 by omega. rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 n); omega). -- cgit v1.2.3