Add eta_tuple functions

These are for getting nicely reduced forms of, e.g., Tuple.map, without
knowing exactly what the tuple is

1 files changed, 37 insertions, 0 deletions

diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index b8a5c2738..bf0288ae4 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -633,6 +633,43 @@ Proof.
       apply IHn; auto.
 Qed.
 
+Fixpoint eta_tuple'_dep {T n} : forall (P : tuple' T n -> Type),
+    (forall ts : tuple' T n, P ts) -> forall ts : tuple' T n, P ts
+  := match n with
+     | 0 => fun P f => f
+     | S n' => fun P f (ts : tuple' T n' * T)
+               => let '(ts', x) := ts in
+                  @eta_tuple'_dep T n' (fun ts' => P (ts', x)) (fun ts'' => f (ts'', x)) ts'
+     end.
+Definition eta_tuple' {T n B} : (tuple' T n -> B) -> (tuple' T n -> B)
+  := @eta_tuple'_dep T n (fun _ => B).
+Definition eta_tuple_dep {T n} : forall (P : tuple T n -> Type),
+    (forall ts : tuple T n, P ts) -> forall ts : tuple T n, P ts
+  := match n with
+     | 0 => fun P f => f
+     | S n' => @eta_tuple'_dep T n'
+     end.
+Definition eta_tuple {T n B} : (tuple T n -> B) -> (tuple T n -> B)
+  := @eta_tuple_dep T n (fun _ => B).
+
+Fixpoint eta_rtuple'_dep {T n} : forall (P : rtuple' T n -> Type),
+    (forall ts : rtuple' T n, P ts) -> forall ts : rtuple' T n, P ts
+  := match n with
+     | 0 => fun P f => f
+     | S n' => fun P f (ts : T * rtuple' T n')
+               => let '(x, ts') := ts in
+                  @eta_rtuple'_dep T n' (fun ts' => P (x, ts')) (fun ts'' => f (x, ts'')) ts'
+     end.
+Definition eta_rtuple' {T n B} : (rtuple' T n -> B) -> (rtuple' T n -> B)
+  := @eta_rtuple'_dep T n (fun _ => B).
+Definition eta_rtuple_dep {T n} : forall (P : rtuple T n -> Type),
+    (forall ts : rtuple T n, P ts) -> forall ts : rtuple T n, P ts
+  := match n with
+     | 0 => fun P f => f
+     | S n' => @eta_rtuple'_dep T n'
+     end.
+Definition eta_rtuple {T n B} : (rtuple T n -> B) -> (rtuple T n -> B)
+  := @eta_rtuple_dep T n (fun _ => B).
 
 Require Import Crypto.Util.ListUtil. (* To initialize [distr_length] database *)
 Hint Rewrite length_to_list' @length_to_list : distr_length.