diff options
-rw-r--r-- | src/Util/ListUtil.v | 13 | ||||
-rw-r--r-- | src/Util/NatUtil.v | 51 | ||||
-rw-r--r-- | src/Util/Tactics.v | 27 |
3 files changed, 85 insertions, 6 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 8260058f1..8823a177e 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -633,11 +633,6 @@ Lemma length_cons : forall {T} (x:T) xs, length (x::xs) = S (length xs). reflexivity. Qed. -Lemma S_pred_nonzero : forall a, (a > 0 -> S (pred a) = a)%nat. -Proof. - destruct a; omega. -Qed. - Lemma cons_length : forall A (xs : list A) a, length (a :: xs) = S (length xs). Proof. auto. @@ -976,6 +971,14 @@ Qed. Hint Rewrite @sum_firstn_succ_default : simpl_sum_firstn. +Lemma sum_firstn_0 : forall xs, + sum_firstn xs 0 = 0%Z. +Proof. + destruct xs; reflexivity. +Qed. + +Hint Rewrite @sum_firstn_0 : simpl_sum_firstn. + Lemma sum_firstn_succ : forall l i x, nth_error l i = Some x -> sum_firstn l (S i) = (x + sum_firstn l i)%Z. diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index c8a6e8247..02122719e 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -1,10 +1,14 @@ +Require Coq.Logic.Eqdep_dec. Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega. Require Import Coq.micromega.Psatz. Import Nat. Create HintDb natsimplify discriminated. -Hint Rewrite @Nat.mod_small using omega : natsimplify. +Hint Resolve mod_bound_pos : arith. +Hint Resolve (fun x y p q => proj1 (@Nat.mod_bound_pos x y p q)) (fun x y p q => proj2 (@Nat.mod_bound_pos x y p q)) : arith. + +Hint Rewrite @mod_small @mod_mod @mod_1_l @mod_1_r succ_pred using omega : natsimplify. Local Open Scope nat_scope. @@ -134,7 +138,52 @@ Qed. Hint Resolve pow_nonzero : arith. +Lemma S_pred_nonzero : forall a, (a > 0 -> S (pred a) = a)%nat. +Proof. + destruct a; omega. +Qed. + +Hint Rewrite S_pred_nonzero using omega : natsimplify. + Lemma mod_same_eq a b : a <> 0 -> a = b -> b mod a = 0. Proof. intros; subst; apply mod_same; assumption. Qed. Hint Rewrite @mod_same_eq using omega : natsimplify. +Hint Resolve mod_same_eq : arith. + +Lemma mod_mod_eq a b c : a <> 0 -> b = c mod a -> b mod a = b. +Proof. intros; subst; autorewrite with natsimplify; reflexivity. Qed. + +Hint Rewrite @mod_mod_eq using (reflexivity || omega) : natsimplify. + +Local Arguments minus !_ !_. + +Lemma S_mod_full a b : a <> 0 -> (S b) mod a = if eq_nat_dec (S (b mod a)) a + then 0 + else S (b mod a). +Proof. + change (S b) with (1+b); intros. + pose proof (mod_bound_pos b a). + rewrite add_mod by assumption. + destruct (eq_nat_dec (S (b mod a)) a) as [H'|H']; + destruct a as [|[|a]]; autorewrite with natsimplify in *; + try congruence; try reflexivity. +Qed. + +Hint Rewrite S_mod_full using omega : natsimplify. + +Lemma S_mod a b : a <> 0 -> S (b mod a) <> a -> (S b) mod a = S (b mod a). +Proof. + intros; rewrite S_mod_full by assumption. + edestruct eq_nat_dec; omega. +Qed. + +Hint Rewrite S_mod using (omega || autorewrite with natsimplify; omega) : natsimplify. + +Lemma eq_nat_dec_refl x : eq_nat_dec x x = left (Logic.eq_refl x). +Proof. + edestruct eq_nat_dec; try congruence. + apply f_equal, Eqdep_dec.UIP_dec, eq_nat_dec. +Qed. + +Hint Rewrite eq_nat_dec_refl : natsimplify. diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 304ae3c20..4630e4ab7 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -260,3 +260,30 @@ Ltac side_conditions_before_to_side_conditions_after tac_in H := here, after evars are instantiated, and not above. *) move H after H'; clear H' | .. ]. + +(** Do something with every hypothesis. *) +Ltac do_with_hyp' tac := + match goal with + | [ H : _ |- _ ] => tac H + end. + +(** Rewrite with any applicable hypothesis. *) +Tactic Notation "rewrite_hyp" "*" := do_with_hyp' ltac:(fun H => rewrite H). +Tactic Notation "rewrite_hyp" "->" "*" := do_with_hyp' ltac:(fun H => rewrite -> H). +Tactic Notation "rewrite_hyp" "<-" "*" := do_with_hyp' ltac:(fun H => rewrite <- H). +Tactic Notation "rewrite_hyp" "?*" := repeat do_with_hyp' ltac:(fun H => rewrite !H). +Tactic Notation "rewrite_hyp" "->" "?*" := repeat do_with_hyp' ltac:(fun H => rewrite -> !H). +Tactic Notation "rewrite_hyp" "<-" "?*" := repeat do_with_hyp' ltac:(fun H => rewrite <- !H). +Tactic Notation "rewrite_hyp" "!*" := progress rewrite_hyp ?*. +Tactic Notation "rewrite_hyp" "->" "!*" := progress rewrite_hyp -> ?*. +Tactic Notation "rewrite_hyp" "<-" "!*" := progress rewrite_hyp <- ?*. + +Tactic Notation "rewrite_hyp" "*" "in" "*" := do_with_hyp' ltac:(fun H => rewrite H in * ). +Tactic Notation "rewrite_hyp" "->" "*" "in" "*" := do_with_hyp' ltac:(fun H => rewrite -> H in * ). +Tactic Notation "rewrite_hyp" "<-" "*" "in" "*" := do_with_hyp' ltac:(fun H => rewrite <- H in * ). +Tactic Notation "rewrite_hyp" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => rewrite !H in * ). +Tactic Notation "rewrite_hyp" "->" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => rewrite -> !H in * ). +Tactic Notation "rewrite_hyp" "<-" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => rewrite <- !H in * ). +Tactic Notation "rewrite_hyp" "!*" "in" "*" := progress rewrite_hyp ?* in *. +Tactic Notation "rewrite_hyp" "->" "!*" "in" "*" := progress rewrite_hyp -> ?* in *. +Tactic Notation "rewrite_hyp" "<-" "!*" "in" "*" := progress rewrite_hyp <- ?* in *. |