Added lemmas to ZUtil and NatUtil (for Testbit)

2 files changed, 54 insertions, 0 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 169564c23..9225ee065 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -173,6 +173,19 @@ Proof.
   omega.
 Qed.
 
+(* Note: this is a duplicate of a lemma that exists in 8.5, included for
+   8.4 support *)
+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;
+    match goal with H : In _ _ |- _ => simpl in H; destruct H end.
+  + subst. exists 0. simpl; split; auto || omega.
+  + destruct IHxs as [i [ ]]; auto.
+    exists (S i).
+    split; auto; simpl; try omega.
+Qed.
+
 Hint Rewrite @map_nth_default using omega : push_nth_default.
 
 Ltac nth_tac :=
@@ -343,6 +356,16 @@ Proof. auto. Qed.
 Lemma firstn0 : forall {T} (xs:list T), firstn 0 xs = nil.
 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.
+  right.
+  exists xs; split.
+  + f_equal; auto using in_eq.
+  + intros; auto using in_cons.
+Qed.
+
 Lemma splice_nth_equiv_update_nth : forall {T} n f d (xs:list T),
   splice_nth n (f (nth_default d xs n)) xs =
   if lt_dec n (length xs)
@@ -961,6 +984,17 @@ Proof.
   congruence.
 Qed.
 
+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.
+  destruct (lt_dec n (length l)).
+  + rewrite nth_default_eq; auto using nth_In.
+  + rewrite nth_default_out_of_bounds by omega.
+    auto.
+Qed.
+
 Lemma nth_error_first : forall {T} (a b : T) l,
   nth_error (a :: l) 0 = Some b -> a = b.
 Proof.
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index 83375f99a..6d4efd9f4 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -64,6 +64,26 @@ Proof.
   reflexivity.
 Qed.
 
+Lemma div_add_l' : forall a b c, a <> 0 -> (a * b + c) / a = b + c / a.
+Proof.
+  intros; rewrite Nat.mul_comm; auto using div_add_l.
+Qed.
+
+Lemma mod_add_l : forall a b c, b <> 0 -> (a * b + c) mod b = c mod b.
+Proof.
+  intros; rewrite Nat.add_comm; auto using mod_add.
+Qed.
+
+Lemma mod_add_l' : forall a b c, b <> 0 -> (b * a + c) mod b = c mod b.
+Proof.
+  intros; rewrite Nat.mul_comm; auto using mod_add_l.
+Qed.
+
+Lemma mod_div_eq0 : forall a b, b <> 0 -> a mod b / b = 0.
+Proof.
+  intros; apply Nat.div_small, mod_bound_pos; omega.
+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.