From f1b4633e833a08295e368851eed461a3759d22f0 Mon Sep 17 00:00:00 2001
From: jadep <jade.philipoom@gmail.com>
Date: Wed, 29 Mar 2017 15:15:54 -0400
Subject: added tuple [repeat]

---
 src/Util/Tuple.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'src/Util/Tuple.v')

diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index d175954d2..cdae79191 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -827,5 +827,20 @@ Proof.
     apply mapi_with'_invariant; auto.
 Qed.
 
+Fixpoint repeat {A} (a:A) n : tuple A n :=
+  match n with
+  | O => tt
+  | S n' => append a (repeat a n')
+  end.
+
+Lemma map_repeat {A B} (f:A->B) (a: A) n :
+  map f (repeat a n) = repeat (f a) n.
+Proof.
+  induction n; simpl repeat; [reflexivity|rewrite map_append; congruence].
+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.
+
 Require Import Crypto.Util.ListUtil. (* To initialize [distr_length] database *)
 Hint Rewrite length_to_list' @length_to_list : distr_length.
-- 
cgit v1.2.3