diff options
| author |  jadep <jade.philipoom@gmail.com> | 2017-03-29 15:15:54 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2017-03-30 16:43:30 -0400 |
| commit | f1b4633e833a08295e368851eed461a3759d22f0 (patch) | |
| tree | f4f5a9a1e0aec7bd5c8e24827777d704d619bcf4 /src/Util/Tuple.v | |
| parent | 16d3eb50638fc280b790aff9cdaa6d28cbb42c8a (diff) | |
added tuple [repeat]
Diffstat (limited to 'src/Util/Tuple.v')
| -rw-r--r-- | src/Util/Tuple.v | 15 |
1 files changed, 15 insertions, 0 deletions
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. |