diff options
Diffstat (limited to 'src/Arithmetic')
| -rw-r--r-- | src/Arithmetic/Core.v | 14 | ||||
| -rw-r--r-- | src/Arithmetic/ModularArithmeticPre.v | 6 | ||||
| -rw-r--r-- | src/Arithmetic/ModularArithmeticTheorems.v | 23 | ||||
| -rw-r--r-- | src/Arithmetic/PrimeFieldTheorems.v | 8 | ||||
| -rw-r--r-- | src/Arithmetic/Saturated.v | 8 |
5 files changed, 29 insertions, 30 deletions
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. |