Add ZUtil, list lemmas

2 files changed, 60 insertions, 0 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 00f446811..0a0b0c5da 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -6,6 +6,7 @@ Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.Pointed.
 Require Import Crypto.Util.Prod.
+Require Import Crypto.Util.Decidable.
 Require Export Crypto.Util.FixCoqMistakes.
 Require Export Crypto.Util.Tactics.BreakMatch.
 Require Export Crypto.Util.Tactics.DestructHead.
@@ -2019,3 +2020,31 @@ Proof. revert v; induction xs; cbn; intros; congruence. Qed.
 Lemma fold_right_flat_map A B C (f : A -> list B) xs (F : _ -> _ -> C) v
   : fold_right F v (flat_map f xs) = fold_right (fun x y => fold_right F y (f x)) v xs.
 Proof. revert v; induction xs; cbn; intros; rewrite ?fold_right_app; congruence. Qed.
+
+Lemma fold_right_id_ext A B f v xs : (forall x y, f x y = y) -> @fold_right A B f v xs = v.
+Proof. induction xs; cbn; intro H; rewrite ?H; auto. Qed.
+Lemma nth_default_repeat A (v:A) n (d:A) i : nth_default d (repeat v n) i = if dec (i < n)%nat then v else d.
+Proof.
+  revert i; induction n as [|n IHn], i; cbn; try reflexivity.
+  rewrite nth_default_cons_S, IHn; do 2 edestruct dec; try reflexivity; omega.
+Qed.
+Lemma fold_right_if_dec_eq_seq A start len i f (x v : A)
+  : ((start <= i < start + len)%nat -> f i v = x)
+    -> (forall j v, (i <> j)%nat -> f j v = v)
+    -> fold_right f v (seq start len) = if dec (start <= i < start + len)%nat then x else v.
+Proof.
+  revert start v; induction len as [|len IHlen]; intros start v H H'; [ | rewrite seq_snoc, fold_right_app; cbn [fold_right] ].
+  { edestruct dec; try reflexivity; omega. }
+  { destruct (dec (i = (start + len)%nat)); subst; [ | rewrite H' by omega ];
+      rewrite IHlen; eauto; intros; clear IHlen;
+        repeat match goal with
+               | _ => reflexivity
+               | _ => omega
+               | _ => progress subst
+               | _ => progress specialize_by omega
+               | [ H : context[dec ?P] |- _ ] => destruct (dec P)
+               | [ |- context[dec ?P] ] => destruct (dec P)
+               | [ H : f _ _ = _ |- _ ] => rewrite H
+               | [ H : forall j, f j ?v = _ |- context[f _ ?v] ] => rewrite H
+               end. }
+Qed.
diff --git a/src/Util/ZUtil/Modulo.v b/src/Util/ZUtil/Modulo.v
index e0a80544d..953b3b2f3 100644
--- a/src/Util/ZUtil/Modulo.v
+++ b/src/Util/ZUtil/Modulo.v
@@ -278,4 +278,35 @@ Module Z.
                                    => assert (q0 = q1) by nia; subst q0
                                  end ] ].
   Qed.
+
+  Lemma mod_mod_0_0_eq x y : x mod y = 0 -> y mod x = 0 -> x = y \/ x = - y \/ x = 0 \/ y = 0.
+  Proof.
+    destruct (Z_zerop x), (Z_zerop y); eauto.
+    Z.div_mod_to_quot_rem; subst.
+    rewrite ?Z.add_0_r in *.
+    match goal with
+    | [ H : ?x = ?x * ?q * ?q' |- _ ]
+      => assert (q * q' = 1) by nia;
+          destruct_head'_or;
+          first [ assert (q < 0) by nia
+                | assert (0 < q) by nia ];
+          first [ assert (q' < 0) by nia
+                | assert (0 < q') by nia ]
+    end;
+      nia.
+  Qed.
+  Lemma mod_mod_0_0_eq_pos x y : 0 < x -> 0 < y -> x mod y = 0 -> y mod x = 0 -> x = y.
+  Proof. intros ?? H0 H1; pose proof (mod_mod_0_0_eq x y H0 H1); omega. Qed.
+  Lemma mod_mod_trans x y z : y <> 0 -> x mod y = 0 -> y mod z = 0 -> x mod z = 0.
+  Proof.
+    destruct (Z_zerop x), (Z_zerop z); subst; autorewrite with zsimplify_const; auto; intro.
+    Z.generalize_div_eucl x y.
+    Z.generalize_div_eucl y z.
+    intros; subst.
+    rewrite ?Z.add_0_r in *.
+    rewrite <- Z.mul_assoc.
+    rewrite <- Zmult_mod_idemp_l, Z_mod_same_full.
+    autorewrite with zsimplify_const.
+    reflexivity.
+  Qed.
 End Z.