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/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 +- 21 files changed, 276 insertions(+), 252 deletions(-) (limited to 'src/Util') 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